Constraint Handling Rules in SWI Prolog: The `neq` constraint doesn't work

Question

I am learning Constraint Handling Rules (CHR) in swi-prolog.

I started with the tutorial from Tom Schrijvers' Constraint Handling Rules A Tutorial for (Prolog) Programmers.

In p.286, the author gave an example to implement Inequality constraint.

:- use_module(library(chr)).

:- chr_constraint neq/2.

neq(X,X) <=> fail.
neq(X,Y) <=> X \= Y | true.

But it does not work as expected in swi-prolog.

For example, in swi-prolog

?- neq(A,B).
true.

?- neq(A,B), A = B.
A = $VAR(B).

but it should be

?- neq(A,B).
neq(A,B).

?- neq(A,B), A = B.
false.

How can I get the same result as in the slide?

My swi-prolog version (threaded, 64 bits, version 8.2.4) on windows.

Thanks.

Answer 1

You may use ?=/2 for your second clause:

:- use_module(library(chr)).
:- chr_constraint neq/2.

neq(X,X) <=> fail.
neq(X,Y) <=> ?=(X,Y) | true.

Sample runs:

?- neq(a,a).
false.

?- neq(a,b).
true.

?- neq(A,B).
neq(A, B).

?- neq(A,B), A = f(C), B = f(D).
A = f(C),
B = f(D),
neq(f(C), f(D)).

?- neq(A,B), A = [1,X], B=[].
A = [1, X],
B = [].

Answer 2

Here is a temporary workaround for neq:

:- use_module(library(chr)).

:- chr_constraint neq/2.

neq(X,X) <=> fail.
neq(X,Y) <=> ground(X), ground(Y) | true.

It can pass all the tests in the slide:

?- neq(a,a).
false.

?- neq(a,b).
true.

?- neq(A,B).
neq($VAR(A),$VAR(B)).

?- neq(A,B), A = B.
false.

?- neq(A,B), A = a, B = a.
false.

?- neq(A,B), A = a, B = b.
A = a,
B = b.

?- neq(A,B), A = f(C), B = f(D).
A = f($VAR(C)),
B = f($VAR(D)),
neq(f($VAR(C)),f($VAR(D))).

%% And some other tests which not in the slide.

?- neq([1,2,3], [1,2,X]).
neq([1,2,3],[1,2,$VAR(X)]).

?- neq([1,2,3], [1,2,X]), X=3.
false.

?- neq([1,2,3], [1,2,X]), X=4.
X = 4.

?- neq([1,2,3], X).
neq([1,2,3],$VAR(X)).

?- neq([1,2,3], X), X=[1,2,3].
false.

?- neq([1,2,3], X), X=[1,2,Y].
X = [1,2,$VAR(Y)],
neq([1,2,3],[1,2,$VAR(Y)]).

It seems that the current CHR implementation inhibits binding variables that appear at the head in guards (see Check guard bindings yourself), even if these bindings could roll back via \+. Note that X \= Y equivalents to \+ X = Y. Also, the unification predicate = in guards seems only comparing with variables' identifier instead of unifying them.

The drawback of this workaround is that, for example,

?- neq(A,B), A = [1,X], B=[].

A = [1,$VAR(X)],
B = [],
neq([1,$VAR(X)],[]).

Since A is not ground, the second rule doesn't fire, but we know that A and B cannot be equal, i.e. neq([1,$VAR(X)],[]) should have been removed.

Anyway, it's just a temporary workaround. If someone has a better solution or explanation, I could delete this answer.