| # | Query | Answer | dif_si/2 | IV | SICStus | ECLiPSe | IF | YAP | B | SWI | Scryer | Trealla |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| # | Query, quads | answer description | dif_si/2 | IV | SICStus | ECLiPSe | IF | YAP | B | SWI | Scryer | Trealla |
| introduced | Œdipe | 0.6 | Sepia <2.10 | V5.0 | <6.4 | 5.5.3 | ||||||
| date | 1972-05 | 1987 | <1989-04 | <1996-05 | <2000 | <2003 | 2004-03 | 2019-02 | 2021-04 | |||
| conforming extension | via 5.5.9 and 5.5.11 | yes | yes | yes | yes | yes | yes | yes | yes | yes | yes | |
| strictly conforming extension | 5.1 e | built-in | built-in | library prolog_extras | library const_delay | neither | built-in | default dif | library dif | library dif new | ||
| e1 | ?- asserta(dif(1,1)), dif(1,2).% in 5.1 e | false. | p._e.(m.,st.,_). | p._e.(m.,st.,_). | OK | OK | true. | p._e.(m.,st.,_). | OK | OK | OK | |
| e2 | ?- dif(1,2).% in 5.1 e | ex._e.(p.,dif/2). | true. | true. | OK | OK | true. | true. | true. | OK | OK new | |
| consistency | n/a | full | full | full | weak | full | full | full | full | full | ||
| term-termination | n/a | yes | yes | yes | yes | yes | yes | partial | yes | yes | ||
| tree-termination | n/a | yes | yes | no | no | yes | no | partial | yes | partial? | ||
| display of constraints | i._e. | no 2 | yes | yes | no 3 | yes | no 1 | yes | yes | partially | ||
| call_residue_vars/2 | no | yes | call_residue/2 | no | yes | no | yes | yes | yes | |||
| redundant constraints | ? | no | yes | ? | no | ?no | no | no new | no new | |||
| 1 | ?- dif(1,2). | true. | OK | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 2 | ?- dif(1,Y), Y=1. | false. | OKR | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 3 | ?- dif(1,Y), Y=2. | Y=2. | OKR | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 4 | ?- dif(X,-Y), X= -Y. | false. | OKR | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 5 | ?- dif(X,Y), X=Y. | false. | OKR | OK | OK | OK | true. | OK | OK | OK | OK | OK |
| 6 | ?- dif(X,Y), X=Y, X=1. | false. | OKR | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 7 | ?- dif(-X,-Y), X=Y. | false. | OKR | OK | OK | OK | true. | OK | OK | OK | OK | OK |
| 8 | ?- dif(-X,-Y), X=Y, X=1. | false. | OKR | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 9 | ?- dif(-X,X). | trueo2 | maybet7. | sto | OK2 | OK | OK | true. | OK | true. | OK | OK | OK |
| 10 | ?- dif(-X,Y), X=Y. | trueo2 | maybet7. | stoR | OK2 | OK | OK | true. | OK | true. | OK | OK | OK |
| 11 | ?- X=Y, dif(X-Y,1-2). | X=Y. | OK | OK | OK | OK | OK | X=X | OK | OK | OK | OK |
| 12 | ?- dif(X-Y,1-2), X=Y. | X=Y. | OKR | OK | OK | ,X-X~=1-2. | 3 | X=X | OK | OK | OK new | OK new |
| 13 | ?- X=Y, Y=1, dif(X-Y,1-2). | X=1, Y=1. | OK | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 14 | ?- dif(X-Y,1-2), X=Y, Y=1. | X=1, Y=1. | OKR | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 15 | ?- dif(X-Y,1-2), X=Y, X=2. | X=2, Y=2. | OKR | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 16 | ?- dif(A-C,B-D), C-D=z-z, A-B=1-2. | A=1, C=z, B=2, D=z. | OKR | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 17 | ?- A-B=1-2, C-D=z-z, dif(A-C,B-D). | A=1, B=2, C=z, D=z. | OK | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 18 | ?- dif(A,[C|B]), A=[[]|_], A=[B]. | A=[[]], B=[], dif([[]],[C]). | i._e. | ..., dif(C,[]).2 | OK | OK | A=[[]], B=[]. | OK | A=[[]], B=[]. | OK | OK | OK |
| 19 | ?- dif([E],[/]), E=1. | E=1. | OKR | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 20 | ?- dif([a],B), B=[_|_], B=[b]. | B=[b]. | OKR | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| 21 | ?- dif([],A), A = [_]. | A = [_A]. | OKR | OK | OK | OK | OK | OK | OK | OK | OK new | OK new |
| 22 | ?- A = [_], dif([],A). | A = [_A]. | OK | OK | OK | OK | OK | OK | OK | OK | OK | OK |
| Rational tree unification | ||||||||||||
| t1 | ?- \+ \+ -X=X. | sto, true. | OK | OK | OK | OK | OK | OK | OK | OK | OK | |
| t2 | ?- -X=X, -Y=Y, X\=Y. | sto, false. | OK | OK | loops. | OK | OK | loops. | OK | OK | OK | |
| t3 | ?- -X=X, dif(X,1). | sto, X = -X. | OK | OK | OK | OK | OK | OK | OK | OK | ||
| t4 | ?- -X=X, -Y=Y, dif(X,Y). | sto, false. | OK | OK | OK | OK | OK | OK | OK | OK | ||
| t5 | ?- dif(X,Y), -X=X, -Y=Y. | sto, false. | OKR | OK | OK | loops. | OK | OK | OK | OK | ||
| t6 | ?- A=[[]|A],dif(A,B),B=[[]|A]. | sto, false. | OKR | OK | OK | loops. | OK | OK | OK | OK | ||
| t7 | ?- dif(-X,X),-Y=Y,X=Y. | sto, false. | OKR | OK | OK | OK | OK | OK | OK | OK | ||
| Occurs-check unification | ||||||||||||
| o1 | ?- -X=X. | sto, false. | OK | OK | OK | |||||||
| o2 | ?- dif(-X,X). | true. | OK | OK | OK | OK | ||||||
| o3 | ?- dif(-X,Y), X=Y. | Y = X. | OKR | OK | OK new | OK new | ||||||
–
The following reference implementation is
used. Either directly (OK) or after reordering goals (OKR). An
instantiation error is an indication for pending constraints.
dif_si(X, Y) :- X \== Y, ( X \= Y -> true ; throw(error(instantiation_error,_Imp_def)) ). |
| 1 B Prolog worked in 7.1b5.1, no display in 7.3 up to 8.1 |
2 Prolog IV has an internal
mechanism to obtain the constraints attached to specific variables,
but no way to obtain such variables.
?- dif(X-Y,1-2),X=Y,symbolic_cstrbis([X,Y], V1,V2,V3,V4,V5,V6).
A ex
V6 = true, V5 = true, V4 = true, V3 = true, V2 = true, V1 = [A,A], X = Y, Y ~ tree, A ~ tree.
?- dif(X-Y,1-2), symbolic_cstrbis([X,Y], V1,V2,V3,V4,V5,V6).
A ex B ex
V6 = true, V5 = true, V4 = true, V3 = true,
V2 = difrat([B,A],[1,2]),
V1 = [B,A], Y ~ tree, X ~ tree, A ~ tree, B ~ tree.
?- symbolic_cstrbis([X,Y], V1,V2,V3,V4,V5,V6).
V6 = true, V5 = true, V4 = true, V3 = true, V2 = true, V1 ~ [tree,tree], Y ~ tree, X ~ tree.
|
3 IF/Prolog
has is_constraint/1 to test for the presence of
constraints.
|
Excluded: means to enable dif/2 similar
to Prolog prologue.
Open: Interaction with subsumes_term/2