trealla
trealla copied to clipboard
trealla-prolog
clpb missing a solution
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.
?-
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.
?-
I highly recommend first getting clpb right, and only then start looking at the clpz issue!
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.
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).
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.
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.
I'm getting this...
~/trealla (devel) $ tpl Trealla Prolog (c) Infradig 2020-2023, v2.29.2 ?- use_module(library(clpb)). true. ?- clpb:parse_sat(XY + XZ, Sat). Sat = XY+XZ, 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(XY + XZ, Sat). Sat = X+Z.
— Reply to this email directly, view it on GitHub https://github.com/trealla-prolog/trealla/issues/338#issuecomment-1752052678, or unsubscribe https://github.com/notifications/unsubscribe-auth/AFNKSEUJEJSCJDTTSOLW3K3X6K75LAVCNFSM6AAAAAA43KOP42VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONJSGA2TENRXHA . You are receiving this because you authored the thread.Message ID: @.***>
Here is the full interaction, using the code I posted in https://github.com/trealla-prolog/trealla/issues/338#issuecomment-1747544829:
$ ./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.
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) https://github.com/trealla-prolog/trealla/issues/338#issuecomment-1747544829 :
$ ./tpl Trealla Prolog (c) Infradig 2020-2023, v2.29.2 ?- [user]. sat_rewrite(V, V) :- var(V), !. sat_rewrite(P0Q0, PQ) :- 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(XY + XZ, 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 https://github.com/trealla-prolog/trealla/issues/338#issuecomment-1752166014, or unsubscribe https://github.com/notifications/unsubscribe-auth/AFNKSEVVSNXZB2IQT5IIKVLX6MK5VAVCNFSM6AAAAAA43KOP42VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONJSGE3DMMBRGQ . You are receiving this because you authored the thread.Message ID: @.***>
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(XY + XZ, Sat). Sat = X+Z.
— Reply to this email directly, view it on GitHub https://github.com/trealla-prolog/trealla/issues/338#issuecomment-1752052678, or unsubscribe https://github.com/notifications/unsubscribe-auth/AFNKSEUJEJSCJDTTSOLW3K3X6K75LAVCNFSM6AAAAAA43KOP42VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONJSGA2TENRXHA . You are receiving this because you authored the thread.Message ID: @.***>
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.
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(P0Q0, PQ) :- 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(XY + XZ, Sat). Sat = X+Z.
— Reply to this email directly, view it on GitHub https://github.com/trealla-prolog/trealla/issues/338#issuecomment-1753345947, or unsubscribe https://github.com/notifications/unsubscribe-auth/AFNKSEWZPBLL3ESCSETK6SLX6QTKLAVCNFSM6AAAAAA43KOP42VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONJTGM2DKOJUG4 . You are receiving this because you authored the thread.Message ID: @.***>
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. ?-
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.