%----------------------------------------------------------
% Reified unification constraint
% considering variable quantification
% in CHR
% Version 2: considers domain restrictions
% Marco Gavanelli
% 14 October 2003
%----------------------------------------------------------
:-module(reified_unif,[reif_unify/3, make_choice/0, inst/1,if_unary_substitute/4,unify_constr/2]).
:- use_module(library(chr)).
:- use_module(quantif).
%:- use_module(library(clpb)).
%:- use_module(library(clpfd)).
:- use_module(library(terms)).
:- use_module(library(lists)).
%:- ensure_loaded(solver). or ensure_loaded(load_solver).
:- use_module(solver).
%handler reified_unification.
:- ensure_loaded(my_chr_extensions).
%:- chr_option(debug,off).
%:- chr_option(optimize,full).
:- chr_constraint reif_unify/3, unify_constr/2, not_unify_constr/2, inst/1, make_choice/0.
% Reified Unification
% reif_unify(?Term1,?Term2,?Boolean)
% If Boolean=1, then Term1 and Term2 should unify
% If Boolean=0, then Term1 and Term2 should not unify
%yes @ reif_unify(T1,T2,B) <=> T1 == T2 | B=1.
yes @ reif_unify(T,T,B) <=> B=1.
% The following rule improves very much the efficiency, but MUST be after rule 'yes'
not_unif_syntactical @ reif_unify(T1,T2,B) <=> ?=(T1,T2), \+fd_or_num(T1), \+fd_or_num(T1) | B=0.
reif_comb @ reif_unify(T1,T2,B) <=> nonvar(T1), nonvar(T2),
functor(T1,F1,N1), functor(T2,F2,N2) |
(F1=F2, N1=N2
-> reif_unify_args(N1,T1,T2,B)
; B=0).
unify_c @ reif_unify(T1,T2,1) <=> unify_constr(T1,T2).
not_unify_c @ reif_unify(T1,T2,0) <=> not_unify_constr(T1,T2).
% fd_or_num should be after the '&' (I don't know why, but otherwise it does not work).
% Remember that checking cstr_var is enough to infer that is existential only for the clpfd solver
reif_unif_fd1 @ reif_unify(X,Y,B) <=> var(X), nonvar(Y), get_quant(X,existsf), cstr_var(X), fd_or_num(Y) | reified_equality_solver(X,Y,B).
reif_unif_fd2 @ reif_unify(X,Y,B) <=> var(Y), nonvar(X), get_quant(Y,existsf), fd_or_num(X), cstr_var(Y) | reified_equality_solver(X,Y,B).
reif_unif_fd3 @ reif_unify(X,Y,B) <=> var(Y), var(X), get_quant(Y,existsf), get_quant(X,existsf), cstr_var(X), cstr_var(Y) | reified_equality_solver(X,Y,B).
reif_unif_nonflag_exists @ reif_unify(X,Y,B) <=> var(X), get_quant(X,exists), not_unifies_exists(Y) | B=0.
reif_unif_nonflag_exists @ reif_unify(Y,X,B) <=> var(X), get_quant(X,exists), not_unifies_exists(Y) | B=0.
not_unifies_exists(Y):- nonvar(Y),!.
not_unifies_exists(Y):- get_quant(Y,Q), Q\=forallf, Q\=forall.
% Mettere una regola che da successo se una variabile forall viene unificata con qualcosa!
reif_unify_forall_norestr @ reif_unify(X,Y,B) <=>
is_universal(X), get_restrictions(X,[]) |
Y=X, =(B,1).
/*
reif_unify_forall_1 @
reif_unify(X,Y,B)
<=>
is_universal(X)
|
(X=Y -> B=1;B=0).
reif_unify_forall_2 @
reif_unify(X,Y,B)
<=>
is_universal(Y)
|
(X=Y -> B=1;B=0).
*/
reif_unify_forall_norestr @ reif_unify(Y,X,B) <=>
is_universal(X), get_restrictions(X,[]) |
Y=X, =(B,1).
% MarcoG 28 sep 2006:
% if a universal variable (with quant restrictions)
% is unified with a ground term, try the unification.
% MarcoG: Modified 1 dec 06
% This is complete if the quantifier restrictions are unary
% (do not involve other variables). If they involve exist.
% variables, subsequent propagations might insert choice
% points, so the cut will drop some success branches
reif_unify_forall_restr_ground @ reif_unify(Y,X,B) <=>
is_universal(X), ground(Y), get_restrictions(X,R),
term_variables(R,[Var]), Var == X
|
(Y=X -> =(B,1) ; =(B,0)).
reif_unify_forall_restr_ground @ reif_unify(X,Y,B) <=>
is_universal(X), ground(Y), get_restrictions(X,R),
term_variables(R,[Var]), Var == X
|
(Y=X -> =(B,1) ; =(B,0)).
reif_unify(_,_,B) ==> binary_domain(B).
:- chr_constraint and_reif_unify(?natural,?natural,?natural).
% This is a normal and(A,B,C), meaning that C = A /\ B,
% but we assume that the booleans A and B occur in the boolean of reif_unify.
% If we have an AND, and one of the arguments is 0, the output is 0 and we
% don't care about the other argument, so we can remove the constraints
% associated with it (in particular, reif_unify).
and_reif_unify(0,B,C), reif_unify(_,_,B) <=> C=0.
and_reif_unify(A,0,C), reif_unify(_,_,A) <=> C=0.
and_reif_unify(0,_,C) <=> C=0.
and_reif_unify(_,0,C) <=> C=0.
and_reif_unify(A,B,1) <=> A=1, B=1.
and_reif_unify(1,B,C) <=> B=C.
and_reif_unify(A,1,C) <=> A=C.
reif_unify_args(0,_,_,1):- !.
reif_unify_args(N,X,Y,B):-
is_identical(B,0),
!, not_unify_args(N,X,Y).
reif_unify_args(N,X,Y,B) :-
arg(N,X,Xn),
arg(N,Y,Yn),
reif_unify(Xn,Yn,Bn), %write(Bn), nl,
(Bn == 0
-> B = 0 %, write(N), write(' ')
; and_reif_unify(Bn,Bn1,B),
%B #<=> (Bn #/\ Bn1),
N1 is N-1,
reif_unify_args(N1,X,Y,Bn1)
).
yes @ unify_constr(T1,T2) <=> T1 == T2 | true.
% The following rule improves very much the efficiency, but MUST be after rule 'yes'
not_unif_syntactical @ unify_constr(T1,T2) <=> ?=(T1,T2), \+fd_or_num(T1), \+fd_or_num(T2) | false.
unify_constr(X,Y) <=>
nonvar(X), nonvar(Y)|
functor(X,F,N), functor(Y,F,N),
unify_args(N,X,Y).
unif_symm @ unify_constr(X,Y) <=> nonvar(X), var(Y) | unify_constr(Y,X).
% Regola strana per risolvere il problema degli NE nel body...
% Probabilmente questa regola dovrebbe essere inserita anche nell'unificazione
% a basso livello (nella quantif.pl).
nonflagged_exists1 @ unify_constr(X,Y) <=> var(X), var(Y), % inutile: fallisce gia` get_quant se sono nonvar
get_quant(X,QX), get_quant(Y,exists), QX \= forallf | false.
nonflagged_exists2 @ unify_constr(Y,X) <=> var(X), var(Y),
get_quant(X,QX), get_quant(Y,exists), QX \= forallf | false.
nonflagged_exists3 @ unify_constr(X,Y) <=> var(X),
nonvar(Y), get_quant(X,exists) | false.
unify_var_nonvar @ unify_constr(X,Y) <=> var(X), get_quant(X,Q), Q \==exists, nonvar(Y) | term_equality(X,Y).
%% Aggiunto da Marco A:
univ_exist_1 @ unify_constr(X,Y) <=>
is_universal(X),
get_restrictions(X,[]),is_existential(Y) | term_equality(X,Y).
univ_exist_2 @ unify_constr(Y,X) <=> is_universal(X),
get_restrictions(X,[]),is_existential(Y) | term_equality(X,Y).
existsf_unif_existsf @ unify_constr(X,Y) <=>
is_existential(X),is_existential(Y) | term_equality(X,Y).
%cannot happen (see rule unif_symm).
%unify_constr(Y,X) <=> var(X), nonvar(Y), get_quant(X,exists) | false.
%unify_constr(X,Y) <=> X=Y.
% Added MarcoG 9 may 2005
% from D8, page 165:
% a universaly quantified variabe can unify with an existentially quant. var.
% The result is that the quantifier restrictions become constraints.
% This is already achieved when the two variables are unified, so we only
% have to unify the variabls.
univ_exist_3 @ unify_constr(X,Y) <=>
is_universal(X),
get_quant(Y,existsf)
| term_equality(X,Y).
univ_exist_3 @ unify_constr(Y,X) <=>
is_universal(X),
get_quant(Y,existsf)
| term_equality(X,Y).
unify_args(0,_,_):-!.
unify_args(N,X,Y):-
arg(N,X,Xn),
arg(N,Y,Yn),
unify_constr(Xn,Yn),
N1 is N-1,
unify_args(N1,X,Y).
no @ not_unify_constr(T1,T2) <=> T1 == T2 | false.
% The following rule improves very much the efficiency, but MUST be after rule 'no'
not_unif_syntactical @ not_unify_constr(T1,T2) <=> ?=(T1,T2) | true.
nu1 @ not_unify_constr(X,Y) <=> nonvar(X), nonvar(Y),
functor(X,F,N), functor(Y,F,N) |
not_unify_args(N,X,Y).
nu2 @ not_unify_constr(X,Y) <=> nonvar(X), nonvar(Y) | X \= Y.
%nu3 @ not_unify_constr(X,Y) <=> X==Y | false. Mi sembra identica alla "no"
% nu4 is occur check: we skip it (for now)
nu5a @ not_unify_constr(X,Y) <=> var(Y), nonvar(X) | not_unify_constr(Y,X).
% Qui dovrei anche considerare se X e` free
nu5b @ not_unify_constr(X,Y) <=> var(Y), get_quant(Y,forall),
var(X), get_quant(X,QX), QX \= forall, QX \=forallf | not_unify_constr(Y,X).
% Stessa cosa per le flagged
nu5bf @ not_unify_constr(X,Y) <=> var(Y), get_quant(Y,forallf),
var(X), get_quant(X,QX), QX \= forall, QX \=forallf | not_unify_constr(Y,X).
%nu6a @ not_unify_constr(X,_) <=> var(X), get_quant(X,forall), get_restrictions(X,[]) | false.
%nu6af @ not_unify_constr(X,_) <=> var(X), get_quant(X,forallf), get_restrictions(X,[]) | false.
%not_unify_constr(_,X) <=> var(X), get_quant(X,forall) | false.
nu6b @ not_unify_constr(X,Y) <=> var(X),
is_universal(X), existsf_or_ground(Y) |
get_restrictions(X,Rx),
impose_neg_constraints(X,Rx,Y).
% Checks that unification of the existentially quantified vars
% is unfeasible.
% Notice that if the solver is not complete, then the \+ may
% fail even if the unification is impossible!
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Modified by Federico Chesani - 20060314 1530
% New Version:
nu6c @ not_unify_constr(X,Y) <=> var(X), var(Y),
is_universal(X), is_universal(Y),
get_restrictions(X,_Rx), get_restrictions(Y,_Ry) |
\+( (existsf(E), E=X, E=Y) ).
% End New Version
% Old Version
/*
nu6c @ not_unify_constr(X,Y) <=> var(X), var(Y),
is_universal(X), is_universal(Y),
get_restrictions(X,Rx), get_restrictions(Y,Ry) |
\+( (silly, existsf(E), E=X, E=Y) ).
*/
% End Old Version
% End Modification
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nu_clpfd1 @ not_unify_constr(X,Y) <=> cstr_var(X), get_quant(X,existsf), cstr_var(Y), get_quant(Y,existsf) | neq(X,Y).
nu_clpfd1 @ not_unify_constr(X,Y) <=> cstr_var(X), get_quant(X,existsf), is_number(Y) | neq(X,Y).
%nu_clpfd2 @ not_unify_constr(X,Y) <=> cstr_var(X), number(Y) | X #\=Y.
nu_clpfd3 @ not_unify_constr(X,Y) <=> cstr_var(X), nonvar(Y), \+number(Y) |true.
%not_unify_args(0,_,_). Must fail
%not_unify_args(N,X,Y):-
% arg(N,X,Xn),
% arg(N,Y,Yn),
% (not_unify_constr(Xn,Yn) ;
% N1 is N-1,
% not_unify_args(N1,X,Y)).
%not_unify_args(N,X,Y):-
% reif_unify_args(N,X,Y,0).
not_unify_args(_,X,Y):-
get_disunif_variables(X,Y,Lx,Ly),
disunif_list(Lx,Ly).
% Creates in Lx and Ly the pairs of terms that should disunify (at least one
% pair should disunify). Each pair contains at least one variable.
get_disunif_variables(X,Y,Lx,Ly):-
(var(X);var(Y)),!, Lx=[X], Ly=[Y].
get_disunif_variables(X,Y,Lx,Ly):-
(ground(X),ground(Y)
; ?=(X,Y)
),
!,
X \= Y,
Lx=[],Ly=[].
get_disunif_variables(X,Y,Lx,Ly):-
X =.. [F|ArgX],
Y =.. [F|ArgY],
get_disunif_variables_args(ArgX,ArgY,Lx,Ly).
get_disunif_variables_args([],_,[],[]):-!. % Dovrebbero avere lo stesso numero di argomenti
get_disunif_variables_args([X|ArgX],[Y|ArgY],Lx,Ly):-
(get_disunif_variables(X,Y,Lx1,Ly1) ; Lx1=[], Ly1=[]),!,
get_disunif_variables_args(ArgX,ArgY,Lx2,Ly2),
append(Lx1,Lx2,Lx),
append(Ly1,Ly2,Ly).
disunif_list([X],[Y]):- !,not_unify_constr(X,Y).
disunif_list([X1,X2|Tx],[Y1,Y2|Ty]):-
reif_unify(X1,Y1,B1),
(B1 == 0 -> !
; (B1 == 1 -> fail % undo the unification X1=Y1 and take next clause
; !,disunif_list_constr(B1,[X2|Tx],[Y2|Ty])
)
).
% X1 and Y1 necessarily unify: continue with the other arguments
disunif_list([_X1,X2|Tx],[_Y1,Y2|Ty]):-
disunif_list([X2|Tx],[Y2|Ty]).
:- chr_constraint disunif_list_constr(?natural,?any,?any).
disunif_list_constr(0,_,_) <=> true.
disunif_list_constr(1,Lx,Ly) <=> disunif_list(Lx,Ly).
existsf_or_ground(Y):- ground(Y),!.
existsf_or_ground(Y):-
get_quant(Y,existsf).
% if_unary_substitute(X,R,Y,T)
% If R is not a unary constraint with only variable X fails.
% Otherwise, it substitutes all the occurrences of X in R
% with Y, and returns the constraint in T
% MarcoG, 9 may 2005
% I extend it in order to deal with abductive EC.
% If all the other variables are existentially quantified,
% then it is still sensible to impose the opposite constraint.
if_unary_substitute(X,R,Y,T):- X == R,!, Y=T.
%if_unary_substitute(_,R,_,_):- var(R),!, fail.
if_unary_substitute(_,R,_,T):- var(R),get_quant(R,existsf), !, T=R.
if_unary_substitute(_,R,_,_):- var(R),get_quant(R,Q),
(Q=forall; Q=forallf ; Q= exists), !,
write('*** Unimplemented feature: disunification of '),
write(Q), write(' with constrained forallf ***'), nl,
fail.
if_unary_substitute(_,R,_,T):- ground(R),!, T=R.
% MG: if it is a st/1, remove it, otherwise the subsequente #<=> will raise an error
if_unary_substitute(X,st(R),Y,T):- !, if_unary_substitute(X,R,Y,T).
if_unary_substitute(X,R,Y,T):-
functor(R,F,N), functor(T,F,N),
if_unary_substitute_arg(N,X,R,Y,T).
if_unary_substitute_arg(0,_,_,_,_).
if_unary_substitute_arg(N,X,R,Y,T):-
N>0,
arg(N,R,Rn),
arg(N,T,Tn),
N1 is N-1,
if_unary_substitute(X,Rn,Y,Tn),
if_unary_substitute_arg(N1,X,R,Y,T).
inst(X) <=> ground(X) | true.
grounding_inst @
make_choice \ inst(B) <=>
var(B) |
(B=1 ; B=0).
grounding_reif_unify @
make_choice, reif_unify(_,_,B) ==>
var(B) |
(B=1 ; B=0).
/*make_choice :-
findall_constraints(inst(_),L),
get_bool_inst(L,LT1,Tail),
findall_constraints(reif_unify(_,_,_),L2),
get_bool_reif(L2,Tail,[]),
label_bools(LT1).*/
get_bool_inst([],X,X).
get_bool_inst([inst(T)|R],[T|RT],X):-
get_bool_inst(R,RT,X).
get_bool_reif([],X,X).
get_bool_reif([reif_unify(_,_,T)|R],[T|RT],X):-
get_bool_reif(R,RT,X).
label_bools([]).
label_bools([1|L]):-
label_bools(L).
label_bools([0|L]):-
label_bools(L).