More improvement on mod from CLP(Z)

diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl
index 08933a7d8ad58dac270c813cb84cbf165aea0284..2844f69f54c40b7c7bb11ef6a8530ea4a89c31af 100644 (file)
--- 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 (file)
index 0000000..6c5629c
--- /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 (file)
index 0000000..6d3c184
--- /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 (file)
index 0000000..7d91f91
--- /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.