All solutions

These predicates create a list of all the solutions of a goal.

1. findall/3

findall(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)

1.1 Example tests

Let's start with some simple tests verifying success of failure of single goals.

jTrolog.engine.SimpleGoalFixture
goalsuccess()exception()
findall(X, (X=2; X=1), [1, 2]). false no exception
findall(X, Goal, S). false instantiation_error
findall(X, 4, S). false type_error(callable, 4)

Now let's run some tests verifying the unification for some of the variables in goals.

First of all, let's start an appropriate fixture containing an engine.

fit.ActionFixture
start jTrolog.engine.EngineFixture

Then, ask the engine to solve a query, and check variable bindings.

fit.ActionFixture
enter query findall(X, (X=1; X=2), S).
check hasSolution true
enter variable S
check binding [1, 2]
enter query findall(X+Y, (X=1), S).
check hasSolution true
enter variable S
check binding [1 + _]
enter query findall(X, fail, L).
check hasSolution true
enter variable L
check binding []
enter query findall(X, (X=1; X=1), S).
check hasSolution true
enter variable S
check binding [1, 1]
enter query findall(X, (X=1; X=2), [X, Y]).
check hasSolution true
enter variable X
check binding 1
enter variable Y
check binding 2

2. bagof/3

bagof/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)

2.1 Example tests

Let's start with some simple tests verifying success of failure of single goals.

jTrolog.engine.SimpleGoalFixture
goalsuccess()exception()
bagof(X, fail, S). false no exception
bagof(X, Y^Z, L). false instantiation_error
bagof(X, 1, L). false type_error(callable, 1)

Let's run some tests verifying the unification for some of the variables in goals.

First of all, let's start an appropriate fixture containing an engine.

fit.ActionFixture
start jTrolog.engine.EngineFixture

Then, ask the engine to solve a query, and check variable bindings.

fit.ActionFixture
enter query bagof(X, (X=1; X=2), S). Free variable set: {}
check hasSolution true
enter variable S
check binding [1, 2]
enter query bagof(X, (X=1; X=2), X). Free variable set: {}
check hasSolution true
enter variable X
check binding [1, 2]
enter query bagof(X, (X=Y; X=Z), S). Free variable set: {Y, Z}
check hasSolution true
enter variable S
check binding [Y, Z]
enter query bagof(1, (Y=1; Y=2), L). Free variable set: {Y}
check hasSolution true
enter variable L
check binding [1]
enter variable Y
check binding 1
check hasAnotherSolution true
enter variable L
check binding [1]
enter variable Y
check binding 2
enter query bagof(f(X, Y), (X=a; Y=b), L). Free variable set: {}
check hasSolution true
enter variable L
check binding [f(a, _), f(_, b)]
enter query bagof(X, Y^((X=1, Y=1) ; (X=2, Y=2)), S). Free variable set: {}
check hasSolution true
enter variable S
check binding [1, 2]
enter query bagof(X, Y^((X=1; Y=1) ; (X=2, Y=2)), S). Free variable set: {}
check hasSolution true
enter variable S
check binding [1, _, 2]
enter query bagof(X, (Y^(X=1; Y=2) ; X=3), S). Free variable set: {Y}
check hasSolution true
enter variable S
check binding [3]
enter variable Y
check binding _
enter query bagof(X, (X=Y; X=Z; Y=1), S). Free variable set: {Y, Z}
check hasSolution true
enter variable S
check binding [Y, Z]
check hasAnotherSolution true
enter variable S
check binding [_]
enter variable Y
check binding 1

Let's now use a real theory to exercise the predicate on.

fit.ActionFixture
enter theory a(1, f(_)).
a(2, f(_)).
enter query bagof(X, a(X, Y), L). Free variable set: {Y}
check hasSolution true
enter variable L
check binding [1, 2]
enter variable Y
check binding f(_)
enter theory b(1, 1).
b(1, 1).
b(1, 2).
b(2, 1).
b(2, 2).
b(2, 2).
enter query bagof(X, b(X, Y), L). Free variable set: {Y}
check hasSolution true
enter variable L
check binding [1, 1, 2]
enter variable Y
check binding 1
check hasAnotherSolution true
enter variable L
check binding [1, 2, 2]
enter variable Y
check binding 2

3. setof/3

setof/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)

3.1 Example tests

Let's start with some simple tests verifying success of failure of single goals.

jTrolog.engine.SimpleGoalFixture
goalsuccess()exception()
setof(X, fail, S). false no exception

Let's run some tests verifying the unification for some of the variables in goals.

First of all, let's start an appropriate fixture containing an engine.

fit.ActionFixture
start jTrolog.engine.EngineFixture

Then, ask the engine to solve a query, and check variable bindings.

fit.ActionFixture
enter query setof(X, (X=1; X=2), S). Free variable set: {}
check hasSolution true
enter variable S
check binding [1, 2]
enter query bagof(X, (X=1; X=2), X). Free variable set: {}
check hasSolution true
enter variable X
check binding [1, 2]
enter query setof(X, (X=2; X=1), S). Free variable set: {}
check hasSolution true
enter variable S
check binding [1, 2]
enter query setof(X, (X=2; X=2), S). Free variable set: {}
check hasSolution true
enter variable S
check binding [2]
enter query setof(X, (X=Y; X=Z), S). Free variable set: {Y, Z}
check hasSolution true
enter variable S
check binding [Y, Z] Depending on the implementation, the binding could also be [Z, Y]
enter query setof(1, (Y=2; Y=1), L). Free variable set: {Y}
check hasSolution true The order of solutions is undefined
enter variable L
check binding [1]
enter variable Y
check binding 1
check hasAnotherSolution true The order of solutions is undefined
enter variable L
check binding [1]
enter variable Y
check binding 2
enter query setof(f(X, Y), (X=a; Y=b), L). Free variable set: {}
check hasSolution true
enter variable L
check binding [f(_, b), f(a, _)]
enter query setof(X, Y^((X=1, Y=1) ; (X=2, Y=2)), S). Free variable set: {}
check hasSolution true
enter variable S
check binding [1, 2]
enter query setof(X, Y^((X=1; Y=1) ; (X=2, Y=2)), S). Free variable set: {}
check hasSolution true
enter variable S
check binding [_, 1, 2]
enter query setof(X, (Y^(X=1; Y=2) ; X=3), S). Free variable set: {Y}
check hasSolution true
enter variable S
check binding [3]
enter variable Y
check binding _
enter query setof(X, (X=Y; X=Z; Y=1), S). Free variable set: {Y, Z}
check hasSolution true
enter variable S
check binding [Y, Z] Depending on the implementation, the binding could also be [Z, Y]
check hasAnotherSolution true
enter variable S
check binding [_]
enter variable Y
check binding 1

The following examples assume that member/2 is defined with the following clauses:

member(X, [X | _]).
member(X, [_ | L]) :- member(X, L).

Let's start with some simple tests verifying success of failure of single goals.

jTrolog.engine.SimpleGoalFixture
goalsuccess()exception()
setof(X, (exists(U,V)^member(X, [V, U, f(U), f(V)])), [a, b, f(b), f(a)]). false no exception

Let's run some tests verifying the unification for some of the variables in goals.

First of all, let's start an appropriate fixture containing an engine.

fit.ActionFixture
start jTrolog.engine.EngineFixture

Then, ask the engine to solve a query, and check variable bindings.

fit.ActionFixture
enter query setof(X, member(X, [f(U,b), f(V,c)]), L). Free variable set: {U, V}
check hasSolution true
enter variable L
check binding [f(U,b), f(V,c)] Depending on the implementation, the binding could also be [f(V,c), f(U,b)]
enter query setof(X, member(X, [f(U,b), f(V,c)]), [f(a,c), f(a,b)]). Free variable set: {U, V}
check hasSolution false Depending on the implementation, the query could also succeed unifying both U and V with a
enter query setof(X, member(X, [f(b,U), f(c,V)]), [f(b,a), f(c,a)]). Free variable set: {U, V}
check hasSolution true
enter variable U
check binding a
enter variable V
check binding a
enter query setof(X, member(X, [V, U, f(U), f(V)]), [a, b, f(a), f(b)]). Free variable set: {U, V}
check hasSolution true
enter variable U
check binding b Depending on the implementation, the binding could also be a
enter variable V
check binding a Depending on the implementation, the binding could also be b

Let's now use a real theory to exercise the predicate on.

fit.ActionFixture
enter theory a(1, f(_)).
a(2, f(_)).
enter query setof(X, a(X, Y), L). Free variable set: {Y}
check hasSolution true
enter variable L
check binding [1, 2]
enter variable Y
check binding f(_)
enter theory b(1, 1).
b(1, 1).
b(1, 2).
b(2, 1).
b(2, 2).
b(2, 2).
enter query setof(X, b(X, Y), L). Free variable set: {Y}
check hasSolution true
enter variable L
check binding [1, 2]
enter variable Y
check binding 1
check hasAnotherSolution true
enter variable L
check binding [1, 2]
enter variable Y
check binding 2
enter query setof(X-Xs, Y^setof(Y, b(X, Y), Xs), L). Free variable set: {}
check hasSolution true
enter variable L
check binding [1-[1, 2], 2-[1,2]]
enter query setof(X-Xs, setof(Y, b(X, Y), Xs), L). Free variable set: {Y}
check hasSolution true
enter variable L
check binding [1-[1, 2], 2-[1, 2]]
enter variable Y
check binding _
enter theory d(1, 1).
d(1, 2).
d(1, 1).
d(2, 2).
d(2, 1).
d(2, 2).
enter query setof(X-Xs, bagof(Y, d(X, Y), Xs), L). Free variable set: {Y}
check hasSolution true
enter variable L
check binding [1-[1, 2, 1], 2-[2, 1, 2]]
enter variable Y
check binding _

Note that there are no tests covering the cases when an error or exception is thrown by the engine while solving a query, despite setof/3 being known for throwing three different types of exceptions.

The results of the tests for All solutions are as follows:

fit.Summary