These predicates create a list of all the solutions of a goal.
findall/3findall(Template, Goal, Instances) is true iff Instances unifies with the list of values to which a variable X not occurring in Template or Goal would be instantiated by successive re-executions of call(Goal), X=Template. after systematic replacement of all variables in X by new variables.
Templates and modes for the predicate are as follows:
findall(?term, +callable_term, ?list)
Let's start with some simple tests verifying success of failure of single goals.
| Goal | Theory | success(String goal,String theory) |
|---|---|---|
| findall(X, (X=1;Y=2), S). | null | true |
| findall(X+Y, (X=1), S). | null | true |
| findall(X, fail, L). | null | true |
| findall(X, (X=1;X=1), S). | null | true |
| findall(X, (X=1;X=2), [X,Y]). | null | true |
| Goal | Theory | success(String goal,String theory) |
|---|---|---|
| findall(X, (X=2; X=1), [1, 2]). | null | false |
Tests With Results
| Goal | Theory | Variable | success(String goal,String theory,String variable) |
|---|---|---|---|
| findall(X, (X=1;Y=2), S). | null | S | [1,_] |
| findall(X+Y, (X=1), S). | null | S | ['+'(1,_)] |
| findall(X, fail, L). | null | L | [] |
| findall(X, (X=1;X=1), S). | null | S | [1,1] |
| findall(X, (X=1;X=2), [X,Y]). | null | X | 1 |
| findall(X, (X=1;X=2), [X,Y]). | null | Y | 2 |
| findall(X, (X=1;X=2), S). | null | S | [1,2] |
Test With Exception
| Goal | Theory | success(String goal) | Type Of Error |
|---|---|---|---|
| findall(X,Goal,S). | null | true | |
| findall(X,4,S). | null | true |
bagof/3bagof/3 assembles as a list the solutions of a goal for each different instantiation of the free variables in that goal. The elements of each list are in order of solution, but the order in which each list is found is undefined.
Note that bagof/3 is re-executable.
Templates and modes for the predicate are as follows:
bagof(?term, +callable_term, ?list)
Let's start with some simple tests verifying success of failure of single goals.
| Goal | Theory | success(String goal,String theory) |
|---|---|---|
| bagof(X,(X=1;X=2), S). | null | true |
| bagof(X,(X=1;X=2), X). | null | true |
| bagof(X,(X=Y;X=Z), S1). | null | true |
| bagof(1,(Y=1;Y=2), L). | null | true |
| bagof(f(X,Y), (X=a;Y=b), L1). | null | true |
| bagof(X, Y^((X=1,Y=1);(X=2;Y=2)), L2). | null | true |
| bagof(X, Y^((X=1;Y=1);(X=2;Y=2)), L3). | null | true |
| bagof(X, Y^((X=1;Y=2);X=3), Si1). | null | true |
| bagof(X, (X=Y;X=Z;Y=1), S3). | null | true |
| Goal | Theory | success(String goal,String theory) |
|---|---|---|
| bagof(X,fail,S2). | null | false |
Tests With Results
| Goal | Theory | Variable | success(String goal,String theory,String variable) |
|---|---|---|---|
| bagof(X,(X=1;X=2), S). | null | S | [1,2] |
| bagof(X,(X=1;X=2), X). | null | X | [1,2] |
| bagof(X,(X=Y;X=Z), S1). | null | S1 | [Y,Z] |
| bagof(1,(Y=1;Y=2), L). | null | L | [1] |
| bagof(f(X,Y), (X=a;Y=b), L1). | null | L1 | [f(a,_),f(_,b)] |
| bagof(X, Y^((X=1,Y=1);(X=2;Y=2)), L2). | null | L2 | [1,2,_] |
| bagof(X, Y^((X=1;Y=1);(X=2;Y=2)), L3). | null | L3 | [1,_,2,_] |
| bagof(X, Y^((X=1;Y=2);X=3), Si1). | null | Si1 | [1,_,3] |
| bagof(X, (X=Y;X=Z;Y=1), S3). | null | S3 | [Y,Z] |
Tests With Exception
| Goal | Theory | success(String goal) | Type Of Error |
|---|---|---|---|
| bagof(X,Y^Z,L). | null | true | |
| bagof(X,1,L). | null | true | |
| bagof(X,4,S). | null | true |
setof/3setof/3 assembles as a list the solutions of a goal for each different instantiation of the free variables in that goal. Each list is a sorted list, but the order in which each list is found is undefined.
Note that bagof/3 is re-executable.
Templates and modes for the predicate are as follows:
setof(?term, +callable_term, ?list)
Let's start with some simple tests verifying success of failure of single goals.
| Goal | Theory | success(String goal,String theory) |
|---|---|---|
| setof(X,(X=1;X=2),S). | null | true |
| setof(X,(X=1;X=2),X). | null | true |
| setof(X,(X=2;X=1),S). | null | true |
| setof(X,(X=2;X=2),S). | null | true |
| setof(X,(X=Y;X=Z),S). | null | true |
| setof(1,(Y=2;Y=1),L). | null | true |
| setof(f(X,Y),(X=a;Y=b),L). | null | true |
| setof(X,Y^((X=1,Y=1);(X=2,Y=2)),S). | null | true |
| setof(X,Y^((X=1;Y=1);(X=2,Y=2)),S). | null | true |
| setof(X,Y^((X=1,Y=1);X=3),S). | null | true |
| setof(X,(X=Y;X=Z;Y=1),S). | null | true |
| setof(X,a(X,Y),L). | a(1,f(_)). a(2,f(_)). | true |
| setof(X,member(X,[f(U,b),f(V,c)]),L). | null | true |
| setof(X,member(X,[f(b,U),f(c,V)]),[f(b,a),f(c,a)]). | null | true |
| setof(X,member(X,[V,U,f(U),f(V)]),L). | null | true |
| setof(X,member(X,[V,U,f(U),f(V)]),[a,b,f(a),f(b)]). | null | true |
| Goal | Theory | success(String goal,String theory) |
|---|---|---|
| setof(X,fail,S). | null | false |
| setof(X,member(X,[V,U,f(U),f(V)]),[a,b,f(b),f(a)]). | null | false |
Test With Results
| Goal | Theory | Variable | success(String goal,String theory,String variable) |
|---|---|---|---|
| setof(X,(X=1;X=2),S). | null | S | [1,2] |
| setof(X,(X=1;X=2),X). | null | X | [1,2] |
| setof(X,(X=2;X=1),S). | null | S | [1,2] |
| setof(X,(X=2;X=2),S). | null | S | [2] |
| setof(X,(X=Y;X=Z),S). | null | S | [Y,Z] |
| setof(1,(Y=2;Y=1),L). | null | L | [1] |
| setof(f(X,Y),(X=a;Y=b),L). | null | L | [f(_,b),f(a,_)] |
| setof(X,Y^((X=1,Y=1);(X=2,Y=2)),S). | null | S | [1,2] |
| setof(X,Y^((X=1;Y=1);(X=2,Y=2)),S). | null | S | [_,1,2] |
| setof(X,Y^((X=1,Y=1);X=3),S). | null | S | [1,3] |
| setof(X,(X=Y;X=Z;Y=1),S). | null | S | [Y,Z] |
| setof(X,a(X,Y),L). | a(1,f(_)). a(2,f(_)). | L | [1,2] |
| setof(X,member(X,[f(U,b),f(V,c)]),L). | null | L | [f(U,b),f(V,c)] |
| setof(X,member(X,[V,U,f(U),f(V)]),L). | null | L | [V,U,f(V),f(U)] |
| setof(X,member(X,[V,U,f(U),f(V)]),[a,b,f(a),f(b)]). | null | V | a |