Not precisely sure how this is happening, but it looks like the _
s are being identified somehow.
?- dif((p(1) :- q),(_B:-_C)).
dif(f(_B, _C), f(p(1), q)).
?- dif((p(1) :- q),(_:-_)).
true.
Not precisely sure how this is happening, but it looks like the _
s are being identified somehow.
?- dif((p(1) :- q),(_B:-_C)).
dif(f(_B, _C), f(p(1), q)).
?- dif((p(1) :- q),(_:-_)).
true.
This explains it:
109 ?- call_residue_vars(dif(a(p, q), a(_,_)), L).
L = [_49086, _49092, _49098],
dif(f(_49086, _49092), f(p, q)).
In other words, the problem is that anonymous variables are not reported and that is also the case if they have constraints on them. If you do this in a real application you get the same problem: the program succeeds with some internal variables that have constraints that have never been bound.
call_residue_vars/2 does two things: it ensures such variables are not garbage collected and it reports them. Once upon a time it was implemented by scanning the entire term stack. Eventually I found a way to implement this that is both efficient and correct. AFAIK this predicate comes from SICStus and is mostly supposed to debug constraint issues.
Note that logically this is correct: there are bindings for the two anonymous variables for which this dif/2 holds edit but, be aware that constraint solvers may not always have propagated all consequences. Thus, there are cases where a constraint succeeds while there is no possible labeling. In that case the answer is logically wrong!
?- call_residue_vars(dif((p(1):-q), (B:-C)), Vars).
Vars = [B, C, _1736],
dif(f(B, C), f(p(1), q)).
(The output looks a bit weird to me … but basically it shows that B
and C
have attributes … I have no idea where f/2
comes from.)