Bug in unifying dictionaries that contain CLP(Q) constraints

General
1

Hi there, just got what seems like a bug:

:- use_module(library(clpq)).

test :-
        X = #{a:0,b:1},
        Y = #{a:_,b:_,c:_},
        {Y.a + Y.b = Y.c},
        {Y.c > 0},
        X >:< Y.

The above test fails unexpectedly. However, if we remove {Y.c > 0}, it succeeds.

Not sure if this is a problem with CLP(Q) or the > : < unification predicate.

Any thoughts? Many thanks :slight_smile:

2

I suspect that dictionary-specific references are not meant to be used within clp :slightly_smiling_face:

This works as expected:

:- use_module(library(clpq)).

test(YC) :-
        {YA = 0, YB = 1},
        {YA + YB = YC},
        {YC > 0}.

Result:

?- test(YC).
YC = 1.
3

It has nothing to do with '>:<'/2. The code is the same as:

t2(YC) :-
        {YA + YB = YC},
        {YC > 0},
        u(0,1) = u(YA,YB).

And

101 ?- t2(YC).
false.

So, it is clp(Q) that is to blame. The library is poorly maintained :frowning:

4

Just found a workaround by replacing X >:< Y with X.a = Y.a, X.b = Y.b, that is:

test :-
        X = #{a:0,b:1},
        Y = #{a:_,b:_,c:_},
        {Y.a + Y.b = Y.c},
        {Y.c > 0},
        % X >:< Y,  % not working
        % (X.a, X.b) = (Y.a, Y.b),  % doesn't work either
        X.a = Y.a, X.b = Y.b.  % works fine

Note that instead of unifying them one by one as shown, (X.a, X.b) = (Y.a, Y.b) doesn’t work.

Hmm… Does this tell us something?

5

Yes. clp(Q) is apparently broken when a single unification binds multiple variables :frowning: