From 37ac5bb3c1bcb4e7d973c9074cebf3536c2bb6de Mon Sep 17 00:00:00 2001
From: notoria <notoria@users.noreply.github.com>
Date: Sun, 25 May 2025 13:37:28 +0200
Subject: [PATCH 1/3] Strengthened `(mod)/2` in CLP(Z)

?- Z = 8, X = 9, #Z #= #X mod #Y.
   Z = 8, X = 9, clpz:(Y in 9..sup), clpz:(9 mod#Y#=8). % unexpected
Expected: false
---
 src/lib/clpz.pl | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl
index b14546bc..9daad75c 100644
--- a/src/lib/clpz.pl
+++ b/src/lib/clpz.pl
@@ -5088,11 +5088,21 @@ run_propagator(pmod(X,Y,Z), MState) -->
         ;   nonvar(Z), nonvar(X) ->
             (   Z > 0 ->
                 (   X < 0 -> true
-                ;   X >= Z
+                ;   X >= Z,
+                    % due to X = Z+Y*_ and Y > Z
+                    (   X-Z > 0 ->
+                        X-Z > Z
+                    ;   true
+                    )
                 )
             ;   Z < 0 ->
                 (   X > 0 -> true
-                ;   X =< Z
+                ;   X =< Z,
+                    % due to X = Z+Y*_ and Y < Z
+                    (   X-Z < 0 ->
+                        X-Z < Z
+                    ;   true
+                    )
                 )
             ;   Z =:= 0 % Multiple solutions so do nothing special.
             ),

From 4a6f86591cc8c5108910e4117b47395b2a817799 Mon Sep 17 00:00:00 2001
From: notoria <notoria@users.noreply.github.com>
Date: Sun, 25 May 2025 13:38:56 +0200
Subject: [PATCH 2/3] Strengthened `(mod)/2` in CLP(Z)

?- 0 #= 2 mod #Y.
   clpz:(Y in inf.. -1\/1..sup), clpz:(2 mod#Y#=0). % unexpected
Expected: clpz:(Y in-2.. -1\/1..2), clpz:(2 mod Y#=0)
---
 src/lib/clpz.pl | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl
index 9daad75c..0f383094 100644
--- a/src/lib/clpz.pl
+++ b/src/lib/clpz.pl
@@ -5122,7 +5122,16 @@ run_propagator(pmod(X,Y,Z), MState) -->
                       domain_remove_greater_than(YD, YMax, YD1) },
                     fd_put(Y, YD1, YPs)
                     % queue_goal(Y #< Z)
-                ;   true
+                ;   Z =:= 0,
+                    (   X =:= 0 ->
+                        kill(MState) % trivial
+                    ;   % only 4 solutions {-abs(X),-1,1,abs(X)}
+                        { YL is -abs(X), YU is abs(X),
+                          fd_get(Y, YD0, YPs),
+                          domain_remove_smaller_than(YD0, YL, YD1),
+                          domain_remove_greater_than(YD1, YU, YD) },
+                        fd_put(Y, YD, YPs)
+                    )
                 )
             )
         ;   run_propagator(pmodz(X,Y,Z), MState),

From 4b480a7eab68b4e1dc8d07c36ae7b1645ee073bb Mon Sep 17 00:00:00 2001
From: notoria <notoria@users.noreply.github.com>
Date: Sun, 25 May 2025 13:39:31 +0200
Subject: [PATCH 3/3] Strengthened `(mod)/2` in CLP(Z)

?- 8 #= -1 mod #Y.
   clpz:(Y in 9..sup), clpz:(-1 mod#Y#=8). % unexpected
Expected: Y = 9
?- 8 #= -12 mod #Y.
   clpz:(Y in 9..sup), clpz:(-12 mod#Y#=8). % unexpected
Expected `Y` with finite domain
---
 src/lib/clpz.pl | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl
index 0f383094..89019b4f 100644
--- a/src/lib/clpz.pl
+++ b/src/lib/clpz.pl
@@ -5110,7 +5110,23 @@ run_propagator(pmod(X,Y,Z), MState) -->
                   YU < X, X =< 0 } -> kill(MState), Z =:= X
             ;   { fd_get(Y, _, n(YL), _, _),
                   YL > X, X >= 0 } -> kill(MState), Z =:= X
-            ;   (   Z > 0 ->
+            ;   (   Z > 0, X < 0 ->
+                    { fd_get(Y, YD, YPs),
+                      YMin is Z+1,
+                      YMax is Z-X,
+                      domain_remove_smaller_than(YD, YMin, YD1),
+                      domain_remove_greater_than(YD1, YMax, YD2) },
+                    fd_put(Y, YD2, YPs)
+                    % queue_goal((Y #> Z, Y #=< Z-X))
+                ;   Z < 0, X > 0 ->
+                    { fd_get(Y, YD, YPs),
+                      YMax is Z-1,
+                      YMin is Z-X,
+                      domain_remove_greater_than(YD, YMax, YD1),
+                      domain_remove_smaller_than(YD1, YMin, YD2) },
+                    fd_put(Y, YD2, YPs)
+                    % queue_goal((Y #< Z, Y #>= Z-X))
+                ;   Z > 0 ->
                     { fd_get(Y, YD, YPs),
                       YMin is Z + 1,
                       domain_remove_smaller_than(YD, YMin, YD1) },