potassco / clingo

🤔 A grounder and solver for logic programs.
https://potassco.org/clingo
MIT License
601 stars 79 forks source link

New X < Y < Z feature fails #396

Closed MaxOstrowski closed 1 year ago

MaxOstrowski commented 1 year ago

Given the program:

event(1,1,r1).
event(2,2,r2).
event(3,3,r3).

between1(Z, X, Y) :- event(LX, UX, X), event(LY, UY, Y), X != Y, LX <= UY, event(LZ, UZ, Z), LX <= LZ, LZ <= UY, Z != X, Z != Y.
between2(Z, X, Y) :- event(LX, UX, X), event(LY, UY, Y), X != Y, LX <= UY, event(LZ, UZ, Z), LX <= LZ <= UY, Z != X, Z != Y.

the only difference between between1 and between2 is the new short form LX <= LZ <= UY instead of LX <= LZ, LZ <= UY.

clingo --version
clingo version 5.6.1
Address model: 64-bit

libclingo version 5.6.1
Configuration: with Python 3.9.13, without Lua

libclasp version 3.3.9 (libpotassco version 1.1.0)
Configuration: WITH_THREADS=1

clingo bug.lp --text
event(1,1,r1).
event(2,2,r2).
event(3,3,r3).
between2(r2,r1,r3).
between1(r2,r1,r3).

behaves correctly, but

clingo-dl --version
clingo-dl version 1.4.1
Address model: 64-bit

libclingo version 5.6.1
Configuration: without Python, without Lua

libclasp version 3.3.9 (libpotassco version 1.1.0)
Configuration: WITH_THREADS=1

clingo-dl bug.lp --text
event(1,1,r1).
event(2,2,r2).
event(3,3,r3).
between2(r1,r2,r3).
between2(r2,r1,r3).
between2(r3,r1,r2).
between1(r2,r1,r3).

messes up the comparison although they use the same clingo-lib version.

rkaminsk commented 1 year ago

Looks like a bug in the AST processing:

clingo-dl test.lp 0 --verbose
clingo-dl version 1.4.0
Reading from test.lp
Reading      : ************** parsed program **************
#theory dl{
  term{+ :1,binary,left,- :1,binary,left,* :2,binary,left,/ :2,binary,left,- :3,unary};
  &__diff_h/0:term,{<=,>=,<,>,=,!=},term,head;
  &__diff_b/0:term,{<=,>=,<,>,=,!=},term,body
}.
event(1,1,r1).
event(2,2,r2).
event(3,3,r3).
between1(Z,X,Y):-event(LX,UX,X);event(LY,UY,Y);X!=Y;LX<=UY;event(LZ,UZ,Z);LX<=LZ;LZ<=UY;Z!=X;Z!=Y.
between2(Z,X,Y):-event(LX,UX,X);event(LY,UY,Y);X!=Y;LX<=UY;event(LZ,UZ,Z);LX<=UY;Z!=X;Z!=Y.

Looks like the LZ in the comparison is somehow lost.