From 51c00fce5762a28ac3bc3dc07b18611890fd4fd1 Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sun, 8 Oct 2023 09:26:22 +0200 Subject: [PATCH 1/6] adapt query to Scryer Prolog --- src/lib/clpz.pl | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl index b29847be..18475721 100644 --- a/src/lib/clpz.pl +++ b/src/lib/clpz.pl @@ -3647,8 +3647,12 @@ reified_goal(l(L), _) --> [[L]]. parse_init_dcg([], _) --> []. parse_init_dcg([V|Vs], P) --> [{init_propagator(V, P)}], parse_init_dcg(Vs, P). -%?- set_prolog_flag(answer_write_options, [portray(true)]), -% clpz:parse_reified_clauses(Cs), maplist(portray_clause, Cs). +/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - +?- use_module(library(lists)), + use_module(library(format)), + clpz:parse_reified_clauses(Cs), + maplist(portray_clause, Cs). +- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */ reify(E, B) :- reify(E, B, _). From 4d910f6bfe346ac4e0af20644a6ab6d0bb99f6fd Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sun, 8 Oct 2023 09:43:10 +0200 Subject: [PATCH 2/6] FIXED: variables in reified propagators must share the same queue Otherwise, propagation steps may be inadvertently omitted, if propagators are scheduled in a different queue. This addresses #2084. --- src/lib/clpz.pl | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl index 18475721..7bace705 100644 --- a/src/lib/clpz.pl +++ b/src/lib/clpz.pl @@ -3625,7 +3625,8 @@ reified_goal(g(Goal), _) --> [{Goal}]. reified_goal(p(Vs, Prop), _) --> [{make_propagator(Prop, P)}], parse_init_dcg(Vs, P), - [{trigger_once(P)}], + [{variables_same_queue(Vs), + trigger_once(P)}], [( { propagator_state(P, S), S == dead } -> [] ; [p(P)])]. reified_goal(p(Prop), Ds) --> { term_variables(Prop, Vs) }, From 8121dce2a46889ed0a74fe3dba068781e26b51ac Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sun, 8 Oct 2023 09:43:59 +0200 Subject: [PATCH 3/6] instead of prdiv, use ptimes directly --- src/lib/clpz.pl | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl index 7bace705..023f3747 100644 --- a/src/lib/clpz.pl +++ b/src/lib/clpz.pl @@ -2572,7 +2572,7 @@ parse_clpz(E, R, m(A mod B) => [g(B #\= 0), p(pmod(A, B, R))], m(A rem B) => [g(B #\= 0), p(prem(A, B, R))], m(abs(A)) => [g(#R #>= 0), p(pabs(A, R))], - m(A/B) => [g(B #\= 0), p(prdiv(A, B, R))], + m(A/B) => [g(B #\= 0), p(ptimes(R, B, A))], m(A//B) => [g(B #\= 0), p(ptzdiv(A, B, R))], m(A div B) => [g(#R #= (A - (A mod B)) // B)], m(A^B) => [p(pexp(A, B, R))], @@ -4918,11 +4918,6 @@ run_propagator(ptimes(X,Y,Z), MState) --> run_propagator(pdiv(X,Y,Z), MState) --> { kill(MState), Z #= (X-(X mod Y)) // Y }. -% X rdiv Y = Z -run_propagator(prdiv(X,Y,Z), MState) --> - { kill(MState), Z*Y #= X }. - - % X // Y = Z (round towards zero) run_propagator(ptzdiv(X,Y,Z), MState) --> ( nonvar(X) -> @@ -7786,7 +7781,6 @@ attribute_goal_(x_neq_y_plus_z(X,Y,Z)) --> [#X #\= #Y + #Z]. attribute_goal_(x_leq_y_plus_c(X,Y,C)) --> [#X #=< #Y + C]. attribute_goal_(ptzdiv(X,Y,Z)) --> [#X // #Y #= #Z]. attribute_goal_(pdiv(X,Y,Z)) --> [#X div #Y #= #Z]. -attribute_goal_(prdiv(X,Y,Z)) --> [#X / #Y #= #Z]. attribute_goal_(pexp(X,Y,Z)) --> [#X ^ #Y #= #Z]. attribute_goal_(psign(X,Y)) --> [#Y #= sign(#X)]. attribute_goal_(pabs(X,Y)) --> [#Y #= abs(#X)]. From ff63eacf2cfcc53db81e96d7917a552748270bc4 Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sun, 8 Oct 2023 11:28:52 +0200 Subject: [PATCH 4/6] replace list//1 by seq//1 from library(dcgs) --- src/lib/clpz.pl | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl index 023f3747..a2d37014 100644 --- a/src/lib/clpz.pl +++ b/src/lib/clpz.pl @@ -1030,8 +1030,8 @@ term_expansion(Term0, Term) :- once(duodcg_body(Body0, Body, As0, As, Bs0, Bs)). duodcg_body([], (As0=As,Bs0=Bs), As0, As, Bs0, Bs). -duodcg_body(Xs+Ys, (phrase(list(Xs), As0, As), - phrase(list(Ys), Bs0, Bs)), As0, As, Bs0, Bs). +duodcg_body(Xs+Ys, (phrase(seq(Xs), As0, As), + phrase(seq(Ys), Bs0, Bs)), As0, As, Bs0, Bs). duodcg_body({Goal}, call(Goal), As, As, Bs, Bs). duodcg_body((A0,B0), (A,B), As0, As, Bs0, Bs) :- duodcg_body(A0, A, As0, As1, Bs0, Bs1), @@ -3698,7 +3698,7 @@ reify_(tuples_in(Tuples, Relation), B) --> #B #<==> And }, propagator_init_trigger([B], tuples_not_in(Tuples, Relation, B)), kill_reified_tuples(Bs, Ps, Bs), - list(Ps), + seq(Ps), as([B|Bs]). reify_(finite_domain(V), B) --> propagator_init_trigger(reified_fd(V,B)), @@ -3730,20 +3730,17 @@ arithmetic(L, R, B, Functor) --> { phrase((parse_reified_clpz(L, LR, LD), parse_reified_clpz(R, RR, RD)), Ps), Prop =.. [Functor,LD,LR,RD,RR,Ps,B] }, - list(Ps), + seq(Ps), propagator_init_trigger([LD,LR,RD,RR,B], Prop), a(B). boolean(L, R, B, Functor) --> { reify(L, LR, Ps1), reify(R, RR, Ps2), Prop =.. [Functor,LR,Ps1,RR,Ps2,B] }, - list(Ps1), list(Ps2), + seq(Ps1), seq(Ps2), propagator_init_trigger([LR,RR,B], Prop), a(LR, RR, B). -list([]) --> []. -list([L|Ls]) --> [L], list(Ls). - a(X,Y,B) --> ( nonvar(X) -> a(Y, B) ; nonvar(Y) -> a(X, B) @@ -6056,7 +6053,7 @@ domain_to_list(Domain, List) :- phrase(domain_to_list(Domain), List). domain_to_list(split(_, Left, Right)) --> domain_to_list(Left), domain_to_list(Right). domain_to_list(empty) --> []. -domain_to_list(from_to(n(F),n(T))) --> { numlist(F, T, Ns) }, list(Ns). +domain_to_list(from_to(n(F),n(T))) --> { numlist(F, T, Ns) }, seq(Ns). difference_arcs([], []) --> []. difference_arcs([V|Vs], FL0) --> @@ -7754,7 +7751,7 @@ attributes_goals([propagator(P, State)|As]) --> ; maplist(unwrap_with(=), Gs, Gs1) ), maplist(with_clpz, Gs1, Gs2) }, - list(Gs2) + seq(Gs2) ; [P] % possibly user-defined constraint ), attributes_goals(As). From 5cce8ddd7da6414a3e0c29b9085c637c98c0ad3f Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sun, 8 Oct 2023 11:53:06 +0200 Subject: [PATCH 5/6] ENHANCED: avoid pending residual constraints in disentailed reified (div)/2 This addresses #2083: ?- #\0#=0//0 div 2. true. --- src/lib/clpz.pl | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl index a2d37014..bdc747f9 100644 --- a/src/lib/clpz.pl +++ b/src/lib/clpz.pl @@ -3521,7 +3521,8 @@ L #\ R :- (L #\/ R) #/\ #\ (L #/\ R). means that V is an auxiliary variable that was introduced while parsing a compound expression. a(X,V) means V is auxiliary unless it is ==/2 X, and a(X,Y,V) means V is auxiliary unless it is ==/2 X - or Y. l(L) means the literal L occurs in the described list. + or Y. l(L) means the literal L occurs in the described list, + and ls(Ls) means the literals Ls occur in the described list. When a constraint becomes entailed or subexpressions become undefined, created auxiliary constraints are killed, and the @@ -3552,8 +3553,11 @@ parse_reified(E, R, D, m(A^B) => [d(D), p(pexp(A,B,R)), a(A,B,R)], m(A/B) => [d(D1), p(preified_slash(A,B,D2,R)), p(reified_and(D1,[],D2,[],D)),a(D2),a(A,B,R)], + m(A div B) => [d(D1), + g(phrase(parse_reified_clpz(((A-(A mod B)) // B), R, D2), Ps)), + ls(Ps), + p(reified_and(D1,[],D2,[],D)),a(D2),a(A,B,R)], m(A//B) => [skeleton(A,B,D,R,ptzdiv)], - m(A div B) => [skeleton(A,B,D,R,pdiv)], m(A mod B) => [skeleton(A,B,D,R,pmod)], m(A rem B) => [skeleton(A,B,D,R,prem)], % bitwise operations @@ -3644,6 +3648,7 @@ reified_goal(a(V), _) --> [a(V)]. reified_goal(a(X,V), _) --> [a(X,V)]. reified_goal(a(X,Y,V), _) --> [a(X,Y,V)]. reified_goal(l(L), _) --> [[L]]. +reified_goal(ls(Ls), _) --> [seq(Ls)]. parse_init_dcg([], _) --> []. parse_init_dcg([V|Vs], P) --> [{init_propagator(V, P)}], parse_init_dcg(Vs, P). @@ -4911,10 +4916,6 @@ run_propagator(ptimes(X,Y,Z), MState) --> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% X div Y = Z -run_propagator(pdiv(X,Y,Z), MState) --> - { kill(MState), Z #= (X-(X mod Y)) // Y }. - % X // Y = Z (round towards zero) run_propagator(ptzdiv(X,Y,Z), MState) --> ( nonvar(X) -> From f34703a279b3fe2609ba7f101cbf609cc119b8da Mon Sep 17 00:00:00 2001 From: Markus Triska Date: Sun, 8 Oct 2023 12:07:17 +0200 Subject: [PATCH 6/6] remove no longer needed goal projection for pdiv --- src/lib/clpz.pl | 1 - 1 file changed, 1 deletion(-) diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl index bdc747f9..274275b2 100644 --- a/src/lib/clpz.pl +++ b/src/lib/clpz.pl @@ -7778,7 +7778,6 @@ attribute_goal_(x_eq_abs_plus_v(X,V)) --> [#X #= abs(#X) + #V]. attribute_goal_(x_neq_y_plus_z(X,Y,Z)) --> [#X #\= #Y + #Z]. attribute_goal_(x_leq_y_plus_c(X,Y,C)) --> [#X #=< #Y + C]. attribute_goal_(ptzdiv(X,Y,Z)) --> [#X // #Y #= #Z]. -attribute_goal_(pdiv(X,Y,Z)) --> [#X div #Y #= #Z]. attribute_goal_(pexp(X,Y,Z)) --> [#X ^ #Y #= #Z]. attribute_goal_(psign(X,Y)) --> [#Y #= sign(#X)]. attribute_goal_(pabs(X,Y)) --> [#Y #= abs(#X)].