All Solutions and Aggregate Predicates

Often there are many solutions to a problem and it is necessary somehow to compare these solutions with one another. The most general way of doing this is to collect all the solutions into a list, which may then be processed in any way desired. So XSB provides several builtin all-solutions predicates which collect solutions into lists. Sometimes however, one wants simply to perform some aggregate operation over the set of solutions, for example to find the maximum or minimum of the set of solutions. XSB uses tabling and HiLog to provide a general and powerful aggregation facility through the use of two new builtins.

setof(?X, +Goal, ?Set)

This predicate may be read as `` Set is the set of all instances of X such that Goal is provable''. If  Goal is not provable, setof/3 fails. The term Goal specifies a goal or goals as in call(Goal). Set is a set of terms represented as a list of those terms, without duplicates, in the standard order for terms (see Section 6.7). If there are uninstantiated variables in Goal which do not also appear in X, then a call to this evaluable predicate may backtrack, generating alternative values for  Set corresponding to different instantiations of the free variables of  Goal. Variables occurring in Goal will not be treated as free if they are explicitly bound within  Goal by an existential quantifier. An existential quantification can be specified as:

Y ^ G

meaning there exists a Y such that G is true, where Y is some Prolog term (usually, a variable).

Exceptions: Same as predicate call/1 (see Section 6.8).

bagof(?X, +Goal, ?Bag)

This predicate has the same semantics as setof/3 except that the third argument returns an unordered list that may contain duplicates.

Exceptions: Same as predicate call/1 (see Section 6.8).

findall(?X, +Goal, ?List)

Similar to predicate bagof/3, except that variables in Goal that do not occur in X are treated as existential, and alternative lists are not returned for different bindings of such variables. This makes findall/3 deterministic (non-backtrackable). Unlike setof/3 and bagof/3, if Goal is unsatisfiable, findall/3 succeeds binding List to the empty list.

Exceptions: Same as predicate call/1 (see Section 6.8).

tfindall(?X, +Goal, ?List)

Tabling
Like findall/3, tfindall/3 treats all variables in Goal that do not occur in X as existential. However, in tfindall/3, the Goal must be a call to a single tabled predicate.

tfindall/3 allows the user to build programs that use stratified aggregation. If the table to Goal is incomplete, tfindall/3 suspends until the table has been completed, and only then computes List. See Chapter 5 for further discussion of tfindall/3. Like findall/3, if Goal is unsatisfiable, tfindall/3 succeeds binding List to the empty list.

Some of the differences between predicates findall/3 and tfindall/3 can be seen from the following example:

            | ?- [user].
            [Compiling user]
            :- table p/1.
            p(a).
            p(b).
            [user compiled, cpu time used: 0.639 seconds]
            [user loaded]

            yes
            | ?- p(X), findall(Y, p(Y), L).

            X = a
            Y = _922928
            L = [a];

            X = b
            Y = _922820
            L = [a,b];

            no
            | ?- abolish_all_tables.

            yes
            | ?- p(X), tfindall(Y, p(Y), L).

            X = b
            Y = _922820
            L = [b,a];

            X = a
            Y = _922820
            L = [b,a];

            no

Exceptions: Same as predicate findall/3 (see above). Also:

table_error

Upon execution Goal is not a subgoal of a tabled predicate.

tbagof(?X, +Goal, ?List) / tsetof(?X, +Goal, ?List)

Tabling

The standard predicates tbagof/3 and tsetof/3 provide tabled versions of bagof/3 and setof/3 in a similar manner to the way in which tfindall/3 provides a tabled version of findall/3.

X ^ Goal

The system recognises this as meaning there exists an X such that Goal is true, and treats it as equivalent to call(Goal). The use of this explicit existential quantifier outside predicates setof/3 and bagof/3 constructs is superfluous.