Sets
When there are many solutions to a problem, and when all those solutions are
required to be collected together, this can be achieved by repeatedly
backtracking and gradually building up a list of the solutions.
The following evaluable predicates are provided to automate this process.
- setof(X, P, S)
- setof/3 (L)
Read this as S is the set of all instances of X such that P
is provable''.
If P is not provable, setof(X,P,S) succeeds with S
instantiated to the empty list [].
The term P specifies a goal or goals as in call(P).
S is a set of terms represented as a list of those terms,
without duplicates, in the standard order for terms
(see Section
![[*]](crossref.png)
).
If there are uninstantiated variables in P
which do not also appear in X,
then a call to this evaluable predicate may backtrack,
generating alternative values for S corresponding to different
instantiations of the free variables of P.
Variables occurring in P will not be treated as free if they are
explicitly bound within P by an existential quantifier.
An existential quantification is written:
meaning there exists a Y such that Q is true,
where Y is some Prolog term
(usually, a variable, or tuple or list of variables).
- bagof(X, P, Bag)
- bagof/3 (L)
This is the same as setof except that the list
(or alternative lists) returned will not be ordered,
and may contain duplicates.
If P is unsatisfiable, bagof succeeds binding Bag
to the empty list.
The effect of this relaxation is to save considerable
time and space in execution.
- findall(X, P, L)
- findall/3 (L)
Similar to bagof/3,
except that variables in P that do not occur in X are treated as local,
and alternative lists are not returned for different bindings
of such variables.
The list L is, in general, unordered, and may contain duplicates.
If P is unsatisfiable,
findall succeeds binding S to the empty list.
- X∧P
- ∧/2 (L)
The system recognises this as meaning there exists an X such
that P is true, and treats it as equivalent to call(P).
The use of this explicit existential quantifier outside the setof
and bagof constructs is superfluous.