CHR x CLP behaviour

Hi there, I’ve got confused by the behaviour of CHR combined with CLP. The following can recreate the issue:

:- use_module(library(clpfd)).
:- use_module(library(chr)).
:- chr_constraint chr/1.

test :-
    chr(A), chr(B), A #\= B,
    findall(V, find_chr_constraint(chr(V)), [X, X]).

The expected outcome should be false, but this gives true. The CLP constraint A #\= B somehow gets lost after find_chr_constraint/1.

Is this something reasonable or a bug?

Any comments appreciated!

Using findall/3 and friends to collect solutions can be tricky. I won’t go into a detailed explanation but you need to watch out for variables copied to the collected solutions.

Start with:

130 ?- chr(X), findall(C,find_chr_constraint(chr(C)),L).
L = [_],
chr(X).

Note that the variable in L is a “fresh” variable, not the original X. Adding a Y and a #\= constraint:

131 ?- chr(X), chr(Y), X #\= Y, findall(C,find_chr_constraint(chr(C)),L).
L = [_A, _B],
chr(Y),
chr(X),
X#\=Y,
_B#\=_,
_#\=_A.

Again the collected variables (_A and _B) are not connected to the original variables (X and Y). The original constraint on X and Y isn’t lost. And it’s copied to each of the collected solutions.

This is explainable behaviour and not a bug. And it doesn’t have anything to do with CHR or CLPFD:

132 ?- Xs=[X1,X2,X3], findall(X,member(X,Xs),L).
Xs = [X1, X2, X3],
L = [_, _, _].

Thank you! It makes sense.
But the way findall/3 acts doesn’t seem helpful in most situations, I guess?
Cheers!

It makes a lot of sense when the collected terms are ground or the variables are just “don’t cares”. I think that’s quite useful in many situations.