From 314baabf1d1d54345e8c8596ef369ee4b2c4d693 Mon Sep 17 00:00:00 2001 From: notoria Date: Thu, 13 Aug 2020 10:38:57 +0200 Subject: [PATCH] More improvement on mod from CLP(Z) --- src/lib/clpz.pl | 259 ++++++++++++++++++---------------- src/tests/clpz/combination.pl | 17 +++ src/tests/clpz/permutation.pl | 27 ++++ src/tests/clpz/test_clpz.pl | 129 +++++++++++++++++ 4 files changed, 310 insertions(+), 122 deletions(-) create mode 100644 src/tests/clpz/combination.pl create mode 100644 src/tests/clpz/permutation.pl create mode 100644 src/tests/clpz/test_clpz.pl diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl index 08933a7d..2844f69f 100644 --- a/src/lib/clpz.pl +++ b/src/lib/clpz.pl @@ -4924,98 +4924,6 @@ run_propagator(ptzdiv(X,Y,Z), MState) --> %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % Z = X mod Y -run_propagator(pmod_(X,Y,Z), MState) --> - ( nonvar(X) -> - ( nonvar(Y) -> kill(MState), Y =\= 0, Z is X mod Y - ; true - ) - ; nonvar(Y) -> - Y =\= 0, - ( abs(Y) =:= 1 -> kill(MState), Z = 0 - ; var(Z) -> - YP is abs(Y) - 1, - ( Y > 0, { fd_get(X, _, n(XL), n(XU), _) } -> - ( XL >= 0, XU < Y -> - kill(MState), Z = X, ZL = XL, ZU = XU - ; ZL = 0, ZU = YP - ) - ; Y > 0 -> ZL = 0, ZU = YP - ; YN is -YP, ZL = YN, ZU = 0 - ), - ( { fd_get(Z, ZD, ZPs) } -> - { domains_intersection(ZD, from_to(n(ZL), n(ZU)), ZD1), - domain_infimum(ZD1, n(ZMin)), - domain_supremum(ZD1, n(ZMax)) }, - fd_put(Z, ZD1, ZPs) - ; ZMin = Z, ZMax = Z - ), - ( { fd_get(X, XD, XPs), domain_infimum(XD, n(XMin)) } -> - Z1 is XMin mod Y, - ( { between(ZMin, ZMax, Z1) } -> true - ; Y > 0 -> - Next is ((XMin - ZMin + Y - 1) div Y)*Y + ZMin, - { domain_remove_smaller_than(XD, Next, XD1) }, - fd_put(X, XD1, XPs) - ; neq_num(X, XMin) - ) - ; true - ), - ( { fd_get(X, XD2, XPs2), domain_supremum(XD2, n(XMax)) } -> - Z2 is XMax mod Y, - ( { between(ZMin, ZMax, Z2) } -> true - ; Y > 0 -> - Prev is ((XMax - ZMin) div Y)*Y + ZMax, - { domain_remove_greater_than(XD2, Prev, XD3) }, - fd_put(X, XD3, XPs2) - ; neq_num(X, XMax) - ) - ; true - ) - ; { fd_get(X, XD, XPs) }, - % if possible, propagate at the boundaries - ( { domain_infimum(XD, n(Min)) } -> - ( Min mod Y =:= Z -> true - ; Y > 0 -> - Next is ((Min - Z + Y - 1) div Y)*Y + Z, - { domain_remove_smaller_than(XD, Next, XD1) }, - fd_put(X, XD1, XPs) - ; neq_num(X, Min) - ) - ; true - ), - ( { fd_get(X, XD2, XPs2) } -> - ( { domain_supremum(XD2, n(Max)) } -> - ( Max mod Y =:= Z -> true - ; Y > 0 -> - Prev is ((Max - Z) div Y)*Y + Z, - { domain_remove_greater_than(XD2, Prev, XD3) }, - fd_put(X, XD3, XPs2) - ; neq_num(X, Max) - ) - ; true - ) - ; true - ) - ) - ; X == Y -> kill(MState), Z = 0 - ; { fd_get(X, XD, XPs), - fd_get(Y, YD, _), - fd_get(Z, ZD, ZPs) }, - ( { domain_infimum(XD, n(XMin)), XMin >= 0, - domain_infimum(YD, n(YMin)), YMin > 0 } -> - { domain_remove_smaller_than(ZD, 0, ZD1) } - ; ZD1 = ZD - ), - ( { domain_supremum(YD, n(YMax)), YMax > 0 } -> - { Max is YMax - 1, Min is -Max, - domain_remove_smaller_than(ZD1, Min, ZD2), - domain_remove_greater_than(ZD2, Max, ZD3) } - ; ZD3 = ZD1 - ), - fd_put(Z, ZD3, ZPs) - % TODO: propagate more - ). - run_propagator(pmod(X,Y,Z), MState) --> ( Y == 0 -> { false } ; Y == Z -> { false } @@ -5029,6 +4937,25 @@ run_propagator(pmod(X,Y,Z), MState) --> ; nonvar(Y), nonvar(Z) -> ( Y > 0 -> Z >= 0, Z < Y ; Y < 0 -> Z =< 0, Z > Y + ), + ( { fd_get(X, _, n(XL), _, _) } -> + ( (XL - Z) mod Y =\= 0 -> + { XMin is Z + Y * ((XL - Z) div Y + 1) } + ; { XMin is Z + Y * ((XL - Z) div Y) } + ), + { fd_get(X, XD0, XPs), + domain_remove_smaller_than(XD0, XMin, XD2), + fd_put(X, XD2, XPs) } + % queue_goal(X #>= XMin) + ; true + ), + ( { fd_get(X, _, _, n(XU), _) } -> + { XMax is Z + Y * ((XU - Z) div Y) }, + { fd_get(X, XD1, XPs), + domain_remove_greater_than(XD1, XMax, XD3), + fd_put(X, XD3, XPs) } + % queue_goal(X #=< XMax) + ; true ) % kill(MState), % queue_goal(X #= Z + Y * _) % Add a variable to be efficient. @@ -5043,13 +4970,22 @@ run_propagator(pmod(X,Y,Z), MState) --> ) ; Z =:= 0 % Multiple solutions so do nothing special. ), - ( Z > 0 -> queue_goal(Y #> 0) - ; Z < 0 -> queue_goal(Y #< 0) + ( Z > 0 -> + { fd_get(Y, YD, YPs), + YMin is Z + 1, + domain_remove_smaller_than(YD, YMin, YD1), + fd_put(Y, YD1, YPs) } + % queue_goal(Y #> Z) + ; Z < 0 -> + { fd_get(Y, YD, YPs), + YMax is Z - 1, + domain_remove_greater_than(YD, YMax, YD1), + fd_put(Y, YD1, YPs) } + % queue_goal(Y #< Z) ; true ) ; run_propagator(pmodz(X,Y,Z), MState), run_propagator(pmody(X,Y,Z), MState), - run_propagator(pmodx(X,Y,Z), MState), true ). @@ -5057,44 +4993,118 @@ run_propagator(pmodz(X,Y,Z), MState) --> ( nonvar(Z) -> true % Nothing to do. ; nonvar(X) -> ( X =:= 0 -> kill(MState), Z = X - ; X > 0 -> queue_goal(Z #=< X) - ; X < 0 -> queue_goal(Z #>= X) + ; X > 0 -> + ( { fd_get(Y, _, n(YL), _, _), YL > X } -> + kill(MState), + Z = X + ; { fd_get(Z, ZD0, ZPs), + domain_remove_greater_than(ZD0, X, ZD2), + fd_put(Z, ZD2, ZPs) } + % queue_goal(Z #=< X) + ) + ; X < 0 -> + ( { fd_get(Y, _, _, n(YU), _), YU < X } -> + kill(MState), + Z = X + ; { fd_get(Z, ZD0, ZPs), + domain_remove_smaller_than(ZD0, X, ZD2), + fd_put(Z, ZD2, ZPs) } + % queue_goal(Z #>= X) + ) ), ( { fd_get(Y, _, n(YL), n(YU), _), YL > 0 } -> { ZMax is YU - 1 }, - queue_goal(Z in 0..ZMax) + { fd_get(Z, ZD1, ZPs), + domain_remove_smaller_than(ZD1, 0, ZD3), + domain_remove_greater_than(ZD3, ZMax, ZD5), + fd_put(Z, ZD5, ZPs) } + % queue_goal(Z in 0..ZMax) ; { fd_get(Y, _, n(YL), n(YU), _), YU < 0 } -> { ZMin is YL + 1 }, - queue_goal(Z in ZMin..0) + { fd_get(Z, ZD1, ZPs), + domain_remove_greater_than(ZD1, 0, ZD3), + domain_remove_smaller_than(ZD3, ZMin, ZD5), + fd_put(Z, ZD5, ZPs) } + % queue_goal(Z in ZMin..0) ; true ) ; nonvar(Y) -> ( abs(Y) =:= 1 -> kill(MState), Z = 0 ; Y < 0 -> { ZMin is Y + 1 }, - queue_goal(Z in ZMin..0) + { fd_get(Z, ZD1, ZPs), + domain_remove_greater_than(ZD1, 0, ZD3), + domain_remove_smaller_than(ZD3, ZMin, ZD5), + fd_put(Z, ZD5, ZPs) } + % queue_goal(Z in ZMin..0) ; Y > 0 -> { ZMax is Y - 1 }, - queue_goal(Z in 0..ZMax) + { fd_get(Z, ZD1, ZPs), + domain_remove_smaller_than(ZD1, 0, ZD3), + domain_remove_greater_than(ZD3, ZMax, ZD5), + fd_put(Z, ZD5, ZPs) } + % queue_goal(Z in 0..ZMax) ), ( { fd_get(X, _, n(XL), n(XU), _), XL >= 0 } -> - queue_goal(Z #=< XU) + { fd_get(Z, ZD0, ZPs), + domain_remove_greater_than(ZD0, XU, ZD2), + fd_put(Z, ZD2, ZPs) } + % queue_goal(Z #=< XU) ; { fd_get(X, _, n(XL), n(XU), _), XU =< 0 } -> - queue_goal(Z #>= XL) + { fd_get(Z, ZD0, ZPs), + domain_remove_smaller_than(ZD0, XL, ZD2), + fd_put(Z, ZD2, ZPs) } + % queue_goal(Z #>= XL) ; true ) ; ( { fd_get(X, _, n(XL), n(XU), _), XL >= 0 } -> - queue_goal(Z #=< XU) + { fd_get(Z, ZD0, ZPs), + domain_remove_greater_than(ZD0, XU, ZD2), + fd_put(Z, ZD2, ZPs) } + % queue_goal(Z #=< XU) ; { fd_get(X, _, n(XL), n(XU), _), XU =< 0 } -> - queue_goal(Z #>= XL) + { fd_get(Z, ZD0, ZPs), + domain_remove_smaller_than(ZD0, XL, ZD2), + fd_put(Z, ZD2, ZPs) } + % queue_goal(Z #>= XL) ; true ), ( { fd_get(Y, _, n(YL), n(YU), _), YL > 0 } -> { ZMax is YU - 1 }, - queue_goal(Z in 0..ZMax) + { fd_get(Z, ZD1, ZPs), + domain_remove_smaller_than(ZD1, 0, ZD3), + domain_remove_greater_than(ZD3, ZMax, ZD5), + fd_put(Z, ZD5, ZPs) } + % queue_goal(Z in 0..ZMax) ; { fd_get(Y, _, n(YL), n(YU), _), YU < 0 } -> { ZMin is YL + 1 }, - queue_goal(Z in ZMin..0) + { fd_get(Z, ZD1, ZPs), + domain_remove_greater_than(ZD1, 0, ZD3), + domain_remove_smaller_than(ZD3, ZMin, ZD5), + fd_put(Z, ZD5, ZPs) } + % queue_goal(Z in ZMin..0) + ; { fd_get(Y, _, n(YL), n(YU), _) } -> + { ZMin is YL + 1, + ZMax is YU - 1 }, + { fd_get(Z, ZD1, ZPs), + domain_remove_greater_than(ZD1, ZMax, ZD3), + domain_remove_smaller_than(ZD3, ZMin, ZD5), + fd_put(Z, ZD5, ZPs) } + % queue_goal(Z in ZMin..ZMax) + %/* This doesn't work very well. + ; { fd_get(Y, _, _, n(YU), _), YU > 0 } -> + { fd_get(Z, ZD1, ZPs), + ZMax is YU - 1, + domain_remove_greater_than(ZD1, ZMax, ZD3), + fd_put(Z, ZD3, ZPs) } + % queue_goal(Z #< YU) + ; { fd_get(Y, _, n(YL), _, _), YL < 0 } -> + { fd_get(Z, ZD1, ZPs), + ZMin is YL + 1, + domain_remove_smaller_than(ZD1, ZMin, ZD3), + fd_put(Z, ZD3, ZPs) } + % queue_goal(Z #> YL) + % */ ; true ) ). @@ -5103,29 +5113,34 @@ run_propagator(pmody(X,Y,Z), MState) --> ( nonvar(Y) -> true % Nothing to do. % ; nonvar(X) -> true ; nonvar(Z) -> - ( Z > 0 -> queue_goal(Y #> Z) - ; Z < 0 -> queue_goal(Y #< Z) + ( Z > 0 -> % queue_goal(Y #> Z) + { fd_get(Y, YD, YPs), + YMin is Z + 1, + domain_remove_smaller_than(YD, YMin, YD1), + fd_put(Y, YD1, YPs) } + ; Z < 0 -> % queue_goal(Y #< Z) + { fd_get(Y, YD, YPs), + YMax is Z - 1, + domain_remove_greater_than(YD, YMax, YD1), + fd_put(Y, YD1, YPs) } ; Z =:= 0 -> kill(MState), queue_goal(X / Y #= _) ) ; ( { fd_get(Z, _, n(ZL), _, _), ZL > 0 } -> - queue_goal(Y #> ZL) + { fd_get(Y, YD, YPs), + YMin is ZL + 1, + domain_remove_smaller_than(YD, YMin, YD1), + fd_put(Y, YD1, YPs) } + % queue_goal(Y #> ZL) ; { fd_get(Z, _, _, n(ZU), _), ZU < 0 } -> - queue_goal(Y #< ZU) + { fd_get(Y, YD, YPs), + YMax is ZU - 1, + domain_remove_greater_than(YD, YMax, YD1), + fd_put(Y, YD1, YPs) } + % queue_goal(Y #< ZU) ; true ) ). -run_propagator(pmodx(X,Y,Z), MState) --> - ( nonvar(X) -> true % Nothing to do. - % ; nonvar(Y) -> true - /* - ; nonvar(Z) -> - ( Z =:= 0 -> kill(MState), queue_goal(X / Y #= _) - ; true - ) - % */ - ; true - ). %% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %% % Z = X rem Y diff --git a/src/tests/clpz/combination.pl b/src/tests/clpz/combination.pl new file mode 100644 index 00000000..6c5629cb --- /dev/null +++ b/src/tests/clpz/combination.pl @@ -0,0 +1,17 @@ +:- module(combination, [combination/2, combinationr/2]). + +combination([], []). +combination([L|Ls], [L|Ms]) :- + combination(Ls, Ms). +combination([_|Ls], Ms) :- + combination(Ls, Ms). + +combinationr([], []). +combinationr([L|Ls], Ms) :- + combinationr_(Ms, [L|Ls]). + +combinationr_([], _). +combinationr_([M|Ms], [M|Ls]) :- + combinationr_(Ms, [M|Ls]). +combinationr_([M|Ms], [_|Ls]) :- + combinationr_([M|Ms], Ls). diff --git a/src/tests/clpz/permutation.pl b/src/tests/clpz/permutation.pl new file mode 100644 index 00000000..6d3c1842 --- /dev/null +++ b/src/tests/clpz/permutation.pl @@ -0,0 +1,27 @@ +:- module(permutation, [arrangement/2, arrangementr/2, permutation/2]). +:- use_module(library(lists), [member/2, same_length/2, select/3]). + +permutation(As, Bs) :- + same_length(As, Bs), + permutation_(Bs, As). + +permutation_([B|Bs], As) :- select(B, As, Cs), permutation_(Bs, Cs). +permutation_([], []). + +arrangement([], []). +arrangement([A|As], [B|Bs]) :- + arrangement_([B|Bs], [A|As]). + +arrangement_([], _). +arrangement_([B|Bs], As) :- + select(B, As, Cs), + arrangement_(Bs, Cs). + +arrangementr([], []). +arrangementr([A|As], Bs) :- + arrangementr_(Bs, [A|As]). + +arrangementr_([], _). +arrangementr_([B|Bs], As) :- + member(B, As), + arrangementr_(Bs, As). diff --git a/src/tests/clpz/test_clpz.pl b/src/tests/clpz/test_clpz.pl new file mode 100644 index 00000000..7d91f918 --- /dev/null +++ b/src/tests/clpz/test_clpz.pl @@ -0,0 +1,129 @@ +:- use_module(library(debug)). +:- use_module(library(format)). +:- use_module(library(lists)). +:- use_module(library(tabling)). +:- use_module('../../lib/clpz'). +:- use_module(combination). +:- use_module(permutation). + +nat(N) :- + nat_(0, N). + +nat_(N, N). +nat_(N0, N) :- + N1 #= N0 + 1, + nat_(N1, N). + +n_factorial(0, 1). +n_factorial(N, F) :- + F #= N * F1, + N1 #= N - 1, + n_factorial(N1, F1). + +pmod(G, X, Y, Z) :- G = (X mod Y #= Z). +pplus(G, X, Y, Z) :- G = (X + Y #= Z). +rel(G, X, Y) :- G = (X #=< Y). + +operation(2, Op, [X, Y], G) :- + call(Op, G, X, Y). + +operation(3, Op, [X, Y, Z], G) :- + call(Op, G, X, Y, Z). + +/* +operation(Op, Vs, G) :- + Goal =.. [Op, G|Vs], + call(Goal). +% */ + +conjonction(G1, G2, G) :- + G = (G2, G1). + +run :- + $nat(N), + NegN #= -N, + Settings = [Nv, Niv, Nr, Nm], + + Settings ins 0..N, + Nm #> 0, % Testing Powers. + + label([Nv]), + length(Vs, Nv), + Vs ins inf..sup, % No labeling. + ( Nv > 1 -> + bagof(Pr, (length(Pr, 2), arrangement(Vs, Pr)), V2s) % No repetitions. + ; % Allow repetitions. + bagof(Pr, (length(Pr, 2), arrangementr(Vs, Pr)), V2s) + ), + bagof(Pr, (length(Pr, 3), arrangementr(Vs, Pr)), V3s), + + ( Nv > 1 -> + Nr #=< Nv + ; Nr #= 0 + ), + label([Nm, Nr]), + length(Gs1, Nm), + ( Nv > 1 -> + length(Gs3, Nr) + ; length(Gs3, 0) + ), + append(Gs3, Gs1, Gs4), + + length(MVs, Nm), + combinationr(V3s, MVs), + maplist(operation(3, pmod), MVs, Gs1), + + ( Nv > 1 -> + length(RVs, Nr), + combination(V2s, RVs), + maplist(operation(2, rel), RVs, Gs3) + ; true + ), + + label([Niv]), + length(Vs1, Niv), + length(Vs2, Niv), + combination(Vs, Vs1), + Vs2 ins NegN..N, + label(Vs2), + Vs1 = Vs2, + + % portray_clause([N, Settings, Vs, Gs4]), nl, + catch( + findall( + Ds, + ( permutation(Gs4, Gs), + foldl(conjonction, Gs, true, G), + call(G), + maplist(fd_dom, Vs, Ds) + ), + Dss + ), + E, + ( write('caugth: '), write(E), nl, + portray_clause([N, Settings, Vs, Gs4, Dss]), nl, + false + ) + ), + length(Dss, Dn), + length(Gs4, Gs4n), + ( Dn == 0 -> true % All false. + ; ( n_factorial(Gs4n, Dn) -> true + ; write('Not a factorial: '), write([Gs4n, Dn]), nl, + portray_clause([N, Settings, Vs, Gs4, Dss]), nl, + *halt(1) + ) + ), + ( \+ maplist(=(_), Dss) -> + write('Bound issue:'), nl, + write(Dss), nl, + transpose(Dss, Dss1), + maplist(sort, Dss1, Dss2), + portray_clause(Dss2), + portray_clause([N, Settings, Vs, Gs4]), nl, + % Not easy to solve due to the fact that multiple variables + % can not have the right bound. + *halt(1) + ; true + ), + false. -- 2.54.0