Prolog understanding setof/3 with ^ markings

Could someone explain to me what this is doing?

(\+ setof((P1,C),P^R^Bag,PS) -> ...
otherwise ->...

I have read the documentation of setof; my understanding is that the thrid argument gets unified with the facts.

However, I can't make sense of the code snippet above.

The full snippet is:


solve_task_bt(go(Target),Agenda,ClosedSet,F,G,NewPos,RR,BackPath) :-
  Agenda = [Current|Rest],
  Current = [c(F,G,P)|RPath],
  NewAgenda = Rest,
  Bag = search(P,P1,R,C),
  (\+ setof((P1,C),P^R^Bag,PS) -> solve_task_bt(go(Target),Rest,[Current|ClosedSet],F,G,NewPos,RR,BackPath);
    otherwise -> 
    setof((P1,C),P^R^Bag,PS),
    addChildren(PS,RPath,Current,NewAgenda,Target,Result),
    NewClosedSet = [Current|ClosedSet],
    NewestAgenda = Result,
    solve_task_bt(go(Target),NewestAgenda,NewClosedSet,F1,G1,Pos,P|RPath,BackPath)
    ).  % backtrack search

Solution

Update a bit later: The below is not quite correct, better go to the parent reference: What is the Prolog operator ^?

So, just focusing on the setof/3

setof((P1,C),P^R^Bag,PS)

Let's replace Bag by its syntactic equivalent set a line earlier:

setof((P1,C),P^R^search(P,P1,R,C),PS)

The description of setof/3 says that it

Calls argument 2 as a goal;
Collects the solutions according to argument 1, the template;
Puts the result of the templating into argument 3, the bag, leaving out duplicates.

So in this case, setof/3 will call (give the expression to the Prolog processor to prove) search(P,P1,R,C), and when this succeeds, collect the resulting values P1,C as a conjunction (P1,C) (which is really special, why not use a 2-element list?) and put everything into PS

Let's just try a runnable example similar to the above, using a list instead of the conjunction and using different names:

search(1,a,n,g).
search(2,a,m,g).

search(2,a,m,j).
search(1,a,m,j).
search(3,a,w,j).
search(3,a,v,j).

search(2,b,v,g).
search(3,b,m,g).
search(5,b,m,g).

search(1,b,m,j).
search(1,b,v,j).

search(2,b,w,h).

get_closed(Bag)   :- setof([X,Y],P^R^search(P,X,R,Y),Bag). 
get_open(Bag,P,R) :- setof([X,Y],    search(P,X,R,Y),Bag).

Notice that you can write

get_closed(Bag) :- setof([X,Y],P^R^search(P,X,R,Y),Bag).

without the compiler warning about "singleton variables", whereas

get_open(Bag) :- setof([X,Y],search(P,X,R,Y),Bag).

will give you a complaint:

Singleton variables: [P,R]

and there is a reason for that: P and R are visible at "clause level". Here we add P and R to the head, which gives us good printout later.

Closed solution

The we can do:

?- get_closed(Bag).
Bag = [[a, g], [a, j], [b, g], [b, h], [b, j]].

Bag now contains all possible solutions [X,Y] for:

search(P,X,P,Y)

where we don't care about the values of the (P,R) tuple outside of the inner goal. Values of P and R are invisible outside the goal called by setof/3, backtracking stays "internal".

Alternative solution for [X,Y] due to differing (P,R) are collapsed by setof/3. If one was using bagof/3 instead:

?- bagof([X,Y],P^R^search(P,X,R,Y),Bag).
Bag = [[a, g], [a, g], [a, j], [a, j], [a, j], [a, j], [b, g], ....

In effect, the query to the Prolog Processor is:

Construct Bag, which is a list of [X,Y] such that:

∀ [X,Y]: ∃P,∃R: search(P,X,R,Y) is true.

Open solution

?- get_open(Bag,P,R).
Bag = [[a, j], [b, j]],
P = 1,
R = m ;
Bag = [[a, g]],
P = 1,
R = n ;
Bag = [[b, j]],
P = 1,
R = v ;
Bag = [[a, g], [a, j]],
P = 2,
R = m ;
Bag = [[b, g]],
P = 2,
R = v ;
Bag = [[b, h]],
P = 2,
R = w ;
Bag = [[b, g]],
P = 3,
R = m ;
Bag = [[a, j]],
P = 3,
R = v ;
Bag = [[a, j]],
P = 3,
R = w ;
Bag = [[b, g]],
P = 5,
R = m.

In this case, Bag contains all solutions for a fixed (P,R) tuple, and Prolog allows you to backtrack over the possible (P,R) at the level of the setof/3 predicate. Variables P and R are "visible outside" of setof/3.

In effect, the query to the Prolog Processor is:

Construct P,R such that:

you can construct Bag, which is a list of [X,Y] such that

∀ [X,Y]: search(P,X,R,Y) is true.

A problem of notation

This would be clearer if Prolog had had a Lambda operator to indicate where the cross-level attach points (i.e. between metapredicate and predicate) are. Assuming what is in setof/3 stays in setof/3 (the opposite attitude of Prolog), one would be able to write:

get_closed(Bag) :- setof([X,Y],λX.λY.search(P,X,R,Y),Bag).

get_closed(Bag) :- setof([X,Y],search(P,X,R,Y),Bag).

and

get_open(Bag)   :- λP.λR.setof([X,Y],search(P,X,R,Y),Bag).

Or one could simply write

get_closed(Bag) :- setof([X,Y],search_closed(X,Y),Bag). 

search_closed(X,Y) :- search(_,X,_,Y).

which would also make clear what is going as variables are not exported outside of the clause they appear in.