correct overeager CLP(ℤ) goal expansion

For instance, consider:

    t(X) :- X #= 1.

We *cannot* expand this to:

    ?- listing(t/1).
    t(A) :-
       (  integer(A) ->
          A=:=A
       ;  (  var(A) ->
             true
          ;  true,
             clpz:clpz_equal(A,A)
          )
       ).

Also, a new binding *must not* be dragged outside of disjunctions,
since the code may look for example like this:

        i(X) :-
            (   X #= 3
            ;   X #= 4
            ).

This commit fixes such issues, and still rewrites CLP(ℤ) expressions
as far as possible already at compilation time.

For example:

    n(X) :- X #= 1+3.

This is now compiled to (note that 1+3 is evaluated to 4):

    ?- listing(n/1).
    n(A) :-
       (  integer(A) ->
          A=:=4
       ;  (  var(A) ->
             A=4
          ;  B=4,
             clpz:clpz_equal(A,B)
          )
       ).

Ideally, it should be compiled to:

    n(4).
This commit is contained in:
Markus Triska
2020-05-01 18:29:00 +02:00
parent 1b7c226779
commit ca5a5b4392

View File

@@ -3038,13 +3038,13 @@ expansion_simpler((A0,B0), (A,B)) :- !,
expansion_simpler(Var is Expr0, Goal) :- expansion_simpler(Var is Expr0, Goal) :-
ground(Expr0), !, ground(Expr0), !,
phrase(expr_conds(Expr0, Expr), Gs), phrase(expr_conds(Expr0, Expr), Gs),
( maplist(call, Gs) -> Var is Expr, Goal = true ( maplist(call, Gs) -> Value is Expr, Goal = (Var = Value)
; Goal = false ; Goal = false
). ).
expansion_simpler(Var =:= Expr0, Goal) :- expansion_simpler(Var =:= Expr0, Goal) :-
ground(Expr0), !, ground(Expr0), !,
phrase(expr_conds(Expr0, Expr), Gs), phrase(expr_conds(Expr0, Expr), Gs),
( maplist(call, Gs) -> Goal = (Var =:= Expr) ( maplist(call, Gs) -> Value is Expr, Goal = (Var =:= Value)
; Goal = false ; Goal = false
). ).
expansion_simpler(between(L,U,V), Goal) :- maplist(integer, [L,U,V]), !, expansion_simpler(between(L,U,V), Goal) :- maplist(integer, [L,U,V]), !,