ENHANCED: Goal expansion for reified constraints.

Used in package precautionary by @dcnorris.
This commit is contained in:
Markus Triska
2021-06-03 20:23:03 +02:00
parent 87ef3519d9
commit fc8d33a98a

View File

@@ -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).