From 2fe1d2ef533322531bd12f00cbcb59a688781caf Mon Sep 17 00:00:00 2001
From: Markus Triska <triska@metalevel.at>
Date: Tue, 10 Jan 2023 17:10:45 +0100
Subject: [PATCH] FIXED: correctly reify (/)/2.

Example:

    ?- 0 #==> X #= 1/2.
    %@    clpz:(X in inf..sup)
    %@ ;  false.

This addresses #1501.
---
 src/lib/clpz.pl | 28 ++++++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl
index 2734a683..94b3d11c 100644
--- a/src/lib/clpz.pl
+++ b/src/lib/clpz.pl
@@ -3509,9 +3509,12 @@ L #\ R :- (L #\/ R) #/\ #\ (L #/\ R).
    undefined, created auxiliary constraints are killed, and the
    "clpz" attribute is removed from auxiliary variables.
 
-   For (/)/2, mod/2 and rem/2, we create a skeleton propagator and
+   For mod/2, div/2, rem/2 etc. we create a skeleton propagator and
    remember it as an auxiliary constraint. The pskeleton propagator
    can use the skeleton when the constraint is defined.
+
+   We cannot use a skeleton propagator for (/)/2, since (/)/2 can
+   fail in cases such as 0 #==> X #= 1/2, where we expect success.
 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */
 
 parse_reified(E, R, D,
@@ -3528,7 +3531,7 @@ parse_reified(E, R, D,
                m(max(A,B))   => [d(D), p(pgeq(R, A)), p(pgeq(R, B)), p(pmax(A,B,R)), a(A,B,R)],
                m(min(A,B))   => [d(D), p(pgeq(A, R)), p(pgeq(B, R)), p(pmin(A,B,R)), a(A,B,R)],
                m(abs(A))     => [g(?(R)#>=0), d(D), p(pabs(A, R)), a(A,R)],
-               m(A/B)        => [skeleton(A,B,D,R,prdiv)],
+               m(A/B)        => [p(preified_slash(A,B,D,R)), 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)],
@@ -5832,6 +5835,26 @@ run_propagator(pimpl(X, Y, Ps), MState) -->
         ;   []
         ).
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+run_propagator(preified_slash(X, Y, D, R), MState) -->
+        (   Y == 0 ->
+            kill(MState),
+            D = 0
+        ;   nonvar(X),
+            nonvar(Y) ->
+            kill(MState),
+            (   X mod Y =:= 0 ->
+                D = 1,
+                R is X // Y
+            ;   D = 0
+            )
+        ;   D == 1 ->
+            kill(MState),
+            queue_goal(X/Y #= R)
+        ;   []
+        ).
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -7756,6 +7779,7 @@ attribute_goal_(reified_geq(DX,X,DY,Y,_,B)) -->
 attribute_goal_(reified_and(X,_,Y,_,B))    --> [?(X) #/\ ?(Y) #<==> ?(B)].
 attribute_goal_(reified_or(X, _, Y, _, B)) --> [?(X) #\/ ?(Y) #<==> ?(B)].
 attribute_goal_(reified_not(X, Y))         --> [#\ ?(X) #<==> ?(Y)].
+attribute_goal_(preified_slash(X, Y, _, R)) --> [?(X)/ ?(Y) #= R].
 attribute_goal_(pimpl(X, Y, _))            --> [?(X) #==> ?(Y)].
 attribute_goal_(pfunction(Op, A, B, R)) -->
         { Expr =.. [Op,?(A),?(B)] },
-- 
2.54.0