From f6d4821a688d173afa0cab4fdcdaaf5943f195ce Mon Sep 17 00:00:00 2001 From: notoria Date: Sun, 7 Mar 2021 18:38:04 +0100 Subject: [PATCH 1/2] Small improvement for mod in CLP(Z) --- src/lib/clpz.pl | 31 ++++++++++++++++++------------- tests/scryer.rs | 1 + 2 files changed, 19 insertions(+), 13 deletions(-) diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl index 0c561b92..367059b7 100644 --- a/src/lib/clpz.pl +++ b/src/lib/clpz.pl @@ -4972,19 +4972,24 @@ run_propagator(pmod(X,Y,Z), MState) --> ) ; Z =:= 0 % Multiple solutions so do nothing special. ), - ( 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 + ( { fd_get(Y, _, _, n(YU), _), + YU < X, X =< 0 } -> kill(MState), Z =:= X + ; { fd_get(Y, _, n(YL), _, _), + YL > X, X >= 0 } -> kill(MState), Z =:= X + ; ( 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), diff --git a/tests/scryer.rs b/tests/scryer.rs index 55d67a73..03c14c3e 100644 --- a/tests/scryer.rs +++ b/tests/scryer.rs @@ -60,6 +60,7 @@ fn setup_call_cleanup() { } #[test] +#[ignore] // ignored as this does not terminate fn clpz() { test_file("src/tests/clpz/test_clpz.pl", Some(b"")); } From bd222ed2bf7d3911b2e9b569fbac1be38a6016f8 Mon Sep 17 00:00:00 2001 From: notoria Date: Wed, 10 Mar 2021 21:19:47 +0100 Subject: [PATCH 2/2] Added a test for mod in CLP(Z) --- src/tests/clpz/test_clpz.pl | 2 +- src/tests/clpz/test_clpz2.pl | 80 ++++++++++++++++++++++++++++++++++++ 2 files changed, 81 insertions(+), 1 deletion(-) create mode 100644 src/tests/clpz/test_clpz2.pl diff --git a/src/tests/clpz/test_clpz.pl b/src/tests/clpz/test_clpz.pl index 7d91f918..98fd827b 100644 --- a/src/tests/clpz/test_clpz.pl +++ b/src/tests/clpz/test_clpz.pl @@ -100,7 +100,7 @@ run :- Dss ), E, - ( write('caugth: '), write(E), nl, + ( write('caught: '), write(E), nl, portray_clause([N, Settings, Vs, Gs4, Dss]), nl, false ) diff --git a/src/tests/clpz/test_clpz2.pl b/src/tests/clpz/test_clpz2.pl new file mode 100644 index 00000000..7ee94094 --- /dev/null +++ b/src/tests/clpz/test_clpz2.pl @@ -0,0 +1,80 @@ +:- use_module(library(debug)). +:- use_module(library(clpz)). +% :- use_module('../../lib/clpz'). +:- use_module(library(format)). +:- use_module(library(lists)). +:- use_module(library(time)). +:- use_module(combination). +:- use_module(permutation). + +nat(N) :- + nat(0, N). + +nat(N, N). +nat(N0, N) :- + N1 is N0 + 1, + nat(N1, N). + +bound(X, L, U) :- L #=< X, X #=< U. + +/* + * This test stops only if there is an mistake in the propagator. + * This test is general enough to quickly test other operators. + * This test does not test if permutating the clause changes the final result. + */ +run(N) :- + Vs = [X0, X1, X2, L0, L1, L2, U0, U1, U2], + + Xs = [X0, X1, X2], + Ls = [L0, L1, L2], + Us = [U0, U1, U2], + + Bs = [L0, L1, L2, U0, U1, U2], + + % maplist(#=<, Ls, Us), + maplist(#\=(0), [X1, L1, U1]), + maplist(bound, Xs, Ls, Us), + + % nat(N), + format("~d\n", [N]), + NegN is -N - 1, + Domain = NegN..N, + + I in 0..6, + indomain(I), + length(Is, I), + combination(Bs, Is), + Is ins Domain, + labeling([], Is), + + ( % Every solution is generated and only solution. + X2 #= X0 mod X1, + Xs ins Domain, + labeling([], Xs), + ( catch(X2 is X0 mod X1, _, false) -> + true + ; format("~q\n", [error0([N, Vs, Ys])]) % Found a non-solution. + ) + ; % Every solution is found and only solution. + copy_term(Xs, Ys), + Ys = [Y0, Y1, Y2], + Ys ins Domain, + labeling([], Ys), + ( catch(Y2 is Y0 mod Y1, _, false) -> + ( X2 #= X0 mod X1 -> + ( maplist(=, Ys, Xs) -> + % Find a specific solution. + true + ; format("~q\n", [error1([N, Vs, Ys])]) + ) + ; format("~q\n", [error2([N, Vs, Ys])]) + ) + ; X2 #= X0 mod X1, + ( maplist(=, Ys, Xs) -> + % Found a non-solution. + format("~q\n", [error3([N, Vs, Ys])]) + ; true + ) + ) + ), + false.