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