From: Markus Triska <triska@metalevel.at>
Date: Thu, 3 Jun 2021 18:23:03 +0000 (+0200)
Subject: ENHANCED: Goal expansion for reified constraints.
X-Git-Tag: v0.9.0~57^2
X-Git-Url: https://git.sagredo.dev/?a=commitdiff_plain;h=fc8d33a98af24d6c8853a1f558e8fc82faa6ad0d;p=scryer-prolog.git

ENHANCED: Goal expansion for reified constraints.

Used in package precautionary by @dcnorris.
---

diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl
index 90a4045f..ee4174b3 100644
--- a/src/lib/clpz.pl
+++ b/src/lib/clpz.pl
@@ -2963,6 +2963,7 @@ clpz_expandable(_ #=< _).
 clpz_expandable(_ #> _).
 clpz_expandable(_ #< _).
 clpz_expandable(_ #\= _).
+clpz_expandable(_ #<==> _).
 
 clpz_expansion(Var in Dom, In) :-
         (   ground(Dom), Dom = L..U, integer(L), integer(U) ->
@@ -2973,6 +2974,22 @@ clpz_expansion(Var in Dom, In) :-
                 ), In)
         ;   In = clpz:clpz_in(Var, Dom)
         ).
+clpz_expansion(A #<==> B, Reif) :-
+        nonvar(A),
+        A =.. [F0,X0,Y0],
+        clpz_builtin(F0, F),
+        phrase(expr_conds(X0, X), Cs0, Cs),
+        phrase(expr_conds(Y0, Y), Cs),
+        list_goal(Cs0, Cond),
+        Expr =.. [F,X,Y],
+        expansion_simpler(( Cond, ( var(B) ; integer(B) ) ->
+                            (   Expr ->
+                                B = 1
+                            ;   B = 0
+                            )
+                          ; clpz:reify(A, RA),
+                            clpz:reify(B, RA)
+                          ), Reif).
 clpz_expansion(X0 #= Y0, Equal) :-
         phrase(expr_conds(X0, X), CsX),
         phrase(expr_conds(Y0, Y), CsY),
@@ -3021,6 +3038,13 @@ clpz_expansion(X0 #\= Y0, Neq) :-
               ), Neq).
 
 
+clpz_builtin(#=, =:=).
+clpz_builtin(#\=, =\=).
+clpz_builtin(#>, >).
+clpz_builtin(#<, <).
+clpz_builtin(#>=, >=).
+clpz_builtin(#=<, =<).
+
 expansion_simpler((True->Then0;_), Then) :-
         is_true(True), !,
         expansion_simpler(Then0, Then).