clpb missing a solution

[infradig]

The only example from the clpb.pl doc that is out-right wrong (so far)...

~/trealla (devel) $ tpl
Trealla Prolog (c) Infradig 2020-2023, v2.27.20-1-gc049-dirty
?- use_module(library(clpb)).
   true.
?- sat(X*Y + X*Z), labeling([X,Y,Z]).
   X = 1, Y = X, Z = 0
;  X = 1, Y = X, Z = X
;  false.
?- 

The first solution is missing, as per below...

~/trealla (devel) $ scryer-prolog
?- use_module(library(clpb)).
   true.
?- sat(X*Y + X*Z), labeling([X,Y,Z]).
   X = 1, Y = 0, Z = 1
;  X = 1, Y = 1, Z = 0
;  X = 1, Y = 1, Z = 1.
?- 

[triska]

The choicepoint is also unexpected!

[infradig]

Gone from missing a solution to having one extra...

~/trealla (devel) $ tpl
Trealla Prolog (c) Infradig 2020-2023, v2.27.54-2-g9792
?- use_module(library(clpb)).
   true.
?-  sat(X*Y + X*Z), labeling([X,Y,Z]).
   X = 1, Y = 0, Z = Y
;  X = 1, Y = 0, Z = X
;  X = 1, Y = X, Z = 0
;  X = 1, Y = X, Z = X.
?- 

[triska]

I highly recommend first getting clpb right, and only then start looking at the clpz issue!

[infradig]

This clpz query is about as simple as it gets:

  ?- A#=B+C.
  false.

no hook involved, so it seems a good place to work on. Also, all remaining clpz errors seem to end up at the same place so i'm optimistic it's possibly the last stumbling block.

[triska]

I highly recommend you focus on library(clpb) first.

For the present issue, we can see a problem already without labeling/1:

?- sat(X*Y + X*Z).
   clpb:sat(X=\=X*Z#Z), unexpected.

For comparison, Scryer Prolog yields the expected answer:

?- sat(X*Y + X*Z).
   X = 1, clpb:sat(Y=\=Y*Z#Z).

And a simpler goal, with Trealla:

?- clpb:parse_sat(X*Y + X*Z, Sat).
   Sat = X+Z, clpb:sat(X=:=X),clpb:sat(Z=:=Z), unexpected.

Whereas with Scryer, we get the expected answer:

?- clpb:parse_sat(X*Y + X*Z, Sat).
   Sat = X*Y+X*Z, clpb:sat(X=:=X), clpb:sat(Y=:=Y), clpb:sat(Z=:=Z).

[triska]

Systematically reducing it further, we have:

?- clpb:sat_rewrite(X*Y + X*Z, Sat). 
   Sat = X+Z, unexpected.

The expected answer is:

?- clpb:sat_rewrite(X*Y + X*Z, Sat).
   Sat = X*Y+X*Z.

[triska]

Here is a small sample program that shows the problem:

sat_rewrite(V, V)       :- var(V), !.
sat_rewrite(P0*Q0, P*Q) :- sat_rewrite(P0, P), sat_rewrite(Q0, Q).
sat_rewrite(P0+Q0, P+Q) :- sat_rewrite(P0, P), sat_rewrite(Q0, Q).

We get:

?- sat_rewrite(X*Y + X*Z, Sat).
   Sat = X+Z, unexpected.

Whereas the expected result is:

?- sat_rewrite(X*Y + X*Z, Sat).
   Sat = X*Y+X*Z.

So, something really elementary is currently broken.

[triska]

The issue persists:

?- sat_rewrite(X*Y + X*Z, Sat).
   Sat = X+Z, unexpected.

[triska]

The issue still persists:

?- sat_rewrite(X*Y + X*Z, Sat).
   Sat = X+Z.

[infradig]

I'm getting this... ~/trealla (devel) $ tpl Trealla Prolog (c) Infradig 2020-2023, v2.29.2 ?- use_module(library(clpb)). true. ?- clpb:parse_sat(X*Y + X*Z, Sat). Sat = X*Y+X*Z, clpb:sat(X=:=X),clpb:sat(Y=:=Y),clpb:sat(Z=:=Z). ?- ~/trealla (devel) $ Also, try adding -O0 to the command line as it seems to be a problem with TCO's and attributes.

…

On Mon, Oct 9, 2023 at 1:18 AM Markus Triska ***@***.***> wrote: The issue still persists: *?- sat_rewrite(X*Y + X*Z, Sat).* Sat = X+Z. — Reply to this email directly, view it on GitHub <#338 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFNKSEUJEJSCJDTTSOLW3K3X6K75LAVCNFSM6AAAAAA43KOP42VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONJSGA2TENRXHA> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[triska]

Here is the full interaction, using the code I posted in #338 (comment):

$ ./tpl 
Trealla Prolog (c) Infradig 2020-2023, v2.29.2
?- [user].
sat_rewrite(V, V)       :- var(V), !.
sat_rewrite(P0*Q0, P*Q) :- sat_rewrite(P0, P), sat_rewrite(Q0, Q).
sat_rewrite(P0+Q0, P+Q) :- sat_rewrite(P0, P), sat_rewrite(Q0, Q).
% Ctrl+d
   true.
?- sat_rewrite(X*Y + X*Z, Sat).
   Sat = X+Z.

No attributes occur in this example! This is really basic code, it would be ridiculous to try to tackle library(clpz) as long as such elementary errors are present in the engine.

I can confirm that the problem is not present when I invoke Trealla with -O0.

[infradig]

Well there's something that interacts badly with TCO because -O0 just disables that.

…

On Mon, 9 Oct 2023, 07:25 Markus Triska, ***@***.***> wrote: Here is the full interaction, using the code I posted in #338 (comment) <#338 (comment)> : *$ ./tpl Trealla Prolog (c) Infradig 2020-2023, v2.29.2 ?- [user].* sat_rewrite(V, V) :- var(V), !. sat_rewrite(P0*Q0, P*Q) :- sat_rewrite(P0, P), sat_rewrite(Q0, Q). sat_rewrite(P0+Q0, P+Q) :- sat_rewrite(P0, P), sat_rewrite(Q0, Q).*% Ctrl+d* true.*?- sat_rewrite(X*Y + X*Z, Sat).* Sat = X+Z. *No attributes occur in this example!* This is really basic code, it would be ridiculous to try to tackle library(clpz) as long as such elementary errors are present in the engine. I can confirm that the problem is not present when I invoke Trealla with -O0. — Reply to this email directly, view it on GitHub <#338 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFNKSEVVSNXZB2IQT5IIKVLX6MK5VAVCNFSM6AAAAAA43KOP42VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONJSGE3DMMBRGQ> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[infradig]

Fixed the TCO problem. It was overwriting the bb_b_put/2 backtracking info in the environment.

…

On Mon, Oct 9, 2023 at 1:18 AM Markus Triska ***@***.***> wrote: The issue still persists: *?- sat_rewrite(X*Y + X*Z, Sat).* Sat = X+Z. — Reply to this email directly, view it on GitHub <#338 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFNKSEUJEJSCJDTTSOLW3K3X6K75LAVCNFSM6AAAAAA43KOP42VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONJSGA2TENRXHA> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[triska]

As far as I can tell, the issue persists:

$ ./tpl
Trealla Prolog (c) Infradig 2020-2023, v2.29.5
?- [user].
sat_rewrite(V, V)       :- var(V), !.
sat_rewrite(P0*Q0, P*Q) :- sat_rewrite(P0, P), sat_rewrite(Q0, Q).
sat_rewrite(P0+Q0, P+Q) :- sat_rewrite(P0, P), sat_rewrite(Q0, Q).

   true.
?- sat_rewrite(X*Y + X*Z, Sat).
   Sat = X+Z.

[infradig]

Correct I merely disabled TCO with clpb.pl while looking at other things. That issue still needs addressing.

…

On Tue, Oct 10, 2023 at 2:49 AM Markus Triska ***@***.***> wrote: As far as I can tell, the issue persists: *$ ./tpl* Trealla Prolog (c) Infradig 2020-2023, v2.29.5*?- [user].* sat_rewrite(V, V) :- var(V), !. sat_rewrite(P0*Q0, P*Q) :- sat_rewrite(P0, P), sat_rewrite(Q0, Q). sat_rewrite(P0+Q0, P+Q) :- sat_rewrite(P0, P), sat_rewrite(Q0, Q). true.*?- sat_rewrite(X*Y + X*Z, Sat).* Sat = X+Z. — Reply to this email directly, view it on GitHub <#338 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFNKSEWZPBLL3ESCSETK6SLX6QTKLAVCNFSM6AAAAAA43KOP42VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONJTGM2DKOJUG4> . You are receiving this because you authored the thread.Message ID: ***@***.***>

[infradig]

Ok, I think all the issues above are resolved excpet the original problem, which is back to missing one solution...

~/trealla (devel) $ tpl
Trealla Prolog (c) Infradig 2020-2023, v2.29.7
?- use_module(library(clpb)).
true.
?- sat(XY + XZ), labeling([X,Y,Z]).
X = 1, Y = X, Z = 0
; X = 1, Y = X, Z = X.
?-

[infradig]

Can you please recheck this one as well?

[triska]

I get:

?- sat(X*Y + X*Z), labeling([X,Y,Z]).
   X = 1, Y = 1, Z = 0
;  X = 1, Y = 1, Z = 1
;  false.

You can easily see that this is not correct, from the comparison with Scryer Prolog:

?- sat(X*Y + X*Z), labeling([X,Y,Z]).
   X = 1, Y = 0, Z = 1
;  X = 1, Y = 1, Z = 0
;  X = 1, Y = 1, Z = 1.

You can also use Trealla itself to see that either the first or the following is wrong, because adding constraints succeeds where a generalization fails:

?- X = 1, Y = 0, Z = 1, sat(X*Y + X*Z), labeling([X,Y,Z]).
   X = 1, Y = 0, Z = 1.

In short, we have:

?- sat(X*Y + X*Z), labeling([X,Y,Z]), Y = 0.
   false.

Whereas:

?- Y = 0, sat(X*Y + X*Z), labeling([X,Y,Z]).
   Y = 0, X = 1, Z = 1
;  false.