From 6ed9a9983255d0ee44d180b21888c373c818b753 Mon Sep 17 00:00:00 2001
From: Markus Triska <triska@metalevel.at>
Date: Thu, 12 Oct 2023 21:04:22 +0200
Subject: [PATCH] ENHANCED: Omit unnecessary residual constraints in
 disentailed reified (//)/2

Example:

    ?- #\ 0#=(Y// -1)/0.
    %@    clpz:(Y in inf..sup).

This addresses #2104.
---
 src/lib/clpz.pl | 40 +++++++++++++++++++++++-----------------
 1 file changed, 23 insertions(+), 17 deletions(-)

diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl
index faad7c0f..26373bb0 100644
--- a/src/lib/clpz.pl
+++ b/src/lib/clpz.pl
@@ -2647,18 +2647,22 @@ parse_goal(p(Prop0)) -->
 morphing(pplus).
 morphing(ptimes).
 morphing(pexp).
+morphing(ptzdiv).
 
 morphing_propagator(P0, P, Target) :-
         P0 =.. [F|Args0],
         (   morphing(F) ->
-            append(Args0, [Target], Args)
-        ;   Args = Args0
+            append(Args0, [Last], Args),
+            Target = p(Last)
+        ;   Args = Args0,
+            Target = none
         ),
         P =.. [F|Args].
 
-morph_into_propagator(MState, Vs, Propagator, Morph) -->
+morph_into_propagator(MState, Vs, P0, Morph) -->
         kill(MState),
-        { make_propagator(Propagator, Morph) },
+        { morphing_propagator(P0, P, _),
+          make_propagator(P, Morph) },
         init_propagator_(Vs, Morph),
         trigger_prop(Morph).
 
@@ -3651,19 +3655,17 @@ reified_goal(p(Vs, Prop), _) -->
         [( { propagator_state(P, S), S == dead } -> [] ; [p(P)])].
 reified_goal(p(Prop0), Ds) -->
         { term_variables(Prop0, Vs),
-          morphing_propagator(Prop0, Prop, Target),
-          (   functor(Prop0, F, _), morphing(F) ->
-              Ts = [p(Target)]
-          ;   Ts = []
-          ) },
-        [Ts],
+          morphing_propagator(Prop0, Prop, Target) },
+        target_propagator(Target),
         reified_goal(p(Vs,Prop), Ds).
 reified_goal(function(D,Op,A,B,R), Ds) -->
         reified_goals([d(D),p(pfunction(Op,A,B,R)),a(A,B,R)], Ds).
 reified_goal(function(D,Op,A,R), Ds) -->
         reified_goals([d(D),p(pfunction(Op,A,R)),a(A,R)], Ds).
 reified_goal(skeleton(A,B,D,R,F), Ds) -->
-        { Prop =.. [F,X,Y,Z] },
+        { Prop0 =.. [F,X,Y,Z],
+          morphing_propagator(Prop0, Prop, Target) },
+        target_propagator(Target),
         reified_goals([d(D1),l(p(P)),g(make_propagator(Prop, P)),
                        p([A,B,D2,R], pskeleton(A,B,D2,[X,Y,Z]-P,R,F)),
                        p(reified_and(D1,[],D2,[],D)),a(D2),a(A,B,R)], Ds).
@@ -3671,7 +3673,10 @@ reified_goal(a(V), _)     --> [a(V)].
 reified_goal(a(X,V), _)   --> [a(X,V)].
 reified_goal(a(X,Y,V), _) --> [a(X,Y,V)].
 reified_goal(l(L), _)     --> [[L]].
-reified_goal(ls(Ls), _)   --> [seq(Ls)].
+reified_goal(ls(Ls), _)   --> [Ls].
+
+target_propagator(p(Prop)) --> [[p(Prop)]].
+target_propagator(none)    --> [].
 
 parse_init_dcg([], _)     --> [].
 parse_init_dcg([V|Vs], P) --> [{init_propagator(V, P)}], parse_init_dcg(Vs, P).
@@ -4835,7 +4840,7 @@ run_propagator(pplus(X,Y,Z,Morph), MState) -->
                 )
             )
         ;   (   X == Y ->
-                morph_into_propagator(MState, [X,Z], ptimes(2,X,Z,_), Morph)
+                morph_into_propagator(MState, [X,Z], ptimes(2,X,Z), Morph)
             ;   X == Z -> kill(MState), Y = 0
             ;   Y == Z -> kill(MState), X = 0
             ;   { fd_get(X, XD, XL, XU, XPs),
@@ -4908,7 +4913,7 @@ run_propagator(ptimes(X,Y,Z,Morph), MState) -->
                 )
             )
         ;   (   X == Y ->
-                morph_into_propagator(MState, [X,Z], pexp(X,2,Z,_), Morph)
+                morph_into_propagator(MState, [X,Z], pexp(X,2,Z), Morph)
             ;   { fd_get(X, XD, XL, XU, XPs),
                   fd_get(Y, _, YL, YU, _),
                   fd_get(Z, ZD, ZL, ZU, _) },
@@ -4940,7 +4945,7 @@ run_propagator(ptimes(X,Y,Z,Morph), MState) -->
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % X // Y = Z (round towards zero)
-run_propagator(ptzdiv(X,Y,Z), MState) -->
+run_propagator(ptzdiv(X,Y,Z,Morph), MState) -->
         (   nonvar(X) ->
             (   nonvar(Y) -> kill(MState), Y =\= 0, Z is X // Y
             ;   { fd_get(Y, YD, YL, YU, YPs) },
@@ -4984,7 +4989,8 @@ run_propagator(ptzdiv(X,Y,Z), MState) -->
         ;   nonvar(Y) ->
             Y =\= 0,
             (   Y =:= 1 -> kill(MState), X = Z
-            ;   Y =:= -1 -> kill(MState), { Z #= -X }
+            ;   Y =:= -1 ->
+                morph_into_propagator(MState, [X,Z], pplus(X,Z,0), Morph)
             ;   { fd_get(X, XD, XL, XU, XPs) },
                 (   nonvar(Z) ->
                     kill(MState),
@@ -7805,7 +7811,7 @@ attribute_goal_(absdiff_neq(X,Y,C))    --> [abs(#X - #Y) #\= C].
 attribute_goal_(x_eq_abs_plus_v(X,V))  --> [#X #= abs(#X) + #V].
 attribute_goal_(x_neq_y_plus_z(X,Y,Z)) --> [#X #\= #Y + #Z].
 attribute_goal_(x_leq_y_plus_c(X,Y,C)) --> [#X #=< #Y + C].
-attribute_goal_(ptzdiv(X,Y,Z))         --> [#X // #Y #= #Z].
+attribute_goal_(ptzdiv(X,Y,Z,_))       --> [#X // #Y #= #Z].
 attribute_goal_(pexp(X,Y,Z,_))         --> [#X ^ #Y #= #Z].
 attribute_goal_(psign(X,Y))            --> [#Y #= sign(#X)].
 attribute_goal_(pabs(X,Y))             --> [#Y #= abs(#X)].
-- 
2.54.0