9
10:-module(reified_unif,[reif_unify/3, make_choice/0, inst/1,if_unary_substitute/4,unify_constr/2]). 11
12
13:- use_module(library(chr)). 14:- use_module(quantif). 17:- use_module(library(terms)). 18:- use_module(library(lists)). 20:- use_module(solver). 22:- ensure_loaded(my_chr_extensions). 23%:- chr_option(debug,off).
24%:- chr_option(optimize,full).
25
26:- chr_constraint reif_unify/3, unify_constr/2, not_unify_constr/2, inst/1, make_choice/0.
27
28% Reified Unification
29% reif_unify(?Term1,?Term2,?Boolean)
30% If Boolean=1, then Term1 and Term2 should unify
31% If Boolean=0, then Term1 and Term2 should not unify
32
33
34
35%yes @ reif_unify(T1,T2,B) <=> T1 == T2 | B=1.
36yes @ reif_unify(T,T,B) <=> B=1.
37% The following rule improves very much the efficiency, but MUST be after rule 'yes'
38not_unif_syntactical @ reif_unify(T1,T2,B) <=> ?=(T1,T2), \+fd_or_num(T1), \+fd_or_num(T1) | B=0.
39reif_comb @ reif_unify(T1,T2,B) <=> nonvar(T1), nonvar(T2),
40 functor(T1,F1,N1), functor(T2,F2,N2) |
41 (F1=F2, N1=N2
42 -> reif_unify_args(N1,T1,T2,B)
43 ; B=0).
44
45unify_c @ reif_unify(T1,T2,1) <=> unify_constr(T1,T2).
46not_unify_c @ reif_unify(T1,T2,0) <=> not_unify_constr(T1,T2).
47% fd_or_num should be after the '&' (I don't know why, but otherwise it does not work).
48% Remember that checking cstr_var is enough to infer that is existential only for the clpfd solver
49reif_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).
50reif_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).
51reif_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).
52reif_unif_nonflag_exists @ reif_unify(X,Y,B) <=> var(X), get_quant(X,exists), not_unifies_exists(Y) | B=0.
53reif_unif_nonflag_exists @ reif_unify(Y,X,B) <=> var(X), get_quant(X,exists), not_unifies_exists(Y) | B=0.
54
55not_unifies_exists(Y):- nonvar(Y),!.
56not_unifies_exists(Y):- get_quant(Y,Q), Q\=forallf, Q\=forall.
57
58% Mettere una regola che da successo se una variabile forall viene unificata con qualcosa!
59
60reif_unify_forall_norestr @ reif_unify(X,Y,B) <=>
61 is_universal(X), get_restrictions(X,[]) |
62 Y=X, =(B,1).
63
64/*
65reif_unify_forall_1 @
66 reif_unify(X,Y,B)
67 <=>
68 is_universal(X)
69 |
70 (X=Y -> B=1;B=0).
71
72
73reif_unify_forall_2 @
74 reif_unify(X,Y,B)
75 <=>
76 is_universal(Y)
77 |
78 (X=Y -> B=1;B=0).
79*/
80
81reif_unify_forall_norestr @ reif_unify(Y,X,B) <=>
82 is_universal(X), get_restrictions(X,[]) |
83 Y=X, =(B,1).
84
85
86% MarcoG 28 sep 2006:
87% if a universal variable (with quant restrictions)
88% is unified with a ground term, try the unification.
89% MarcoG: Modified 1 dec 06
90% This is complete if the quantifier restrictions are unary
91% (do not involve other variables). If they involve exist.
92% variables, subsequent propagations might insert choice
93% points, so the cut will drop some success branches
94reif_unify_forall_restr_ground @ reif_unify(Y,X,B) <=>
95 is_universal(X), ground(Y), get_restrictions(X,R),
96 term_variables(R,[Var]), Var == X
97 |
98 (Y=X -> =(B,1) ; =(B,0)).
99
100reif_unify_forall_restr_ground @ reif_unify(X,Y,B) <=>
101 is_universal(X), ground(Y), get_restrictions(X,R),
102 term_variables(R,[Var]), Var == X
103 |
104 (Y=X -> =(B,1) ; =(B,0)).
105
106reif_unify(_,_,B) ==> binary_domain(B).
107
108:- chr_constraint and_reif_unify(?natural,?natural,?natural).
109% This is a normal and(A,B,C), meaning that C = A /\ B,
110% but we assume that the booleans A and B occur in the boolean of reif_unify.
111% If we have an AND, and one of the arguments is 0, the output is 0 and we
112% don't care about the other argument, so we can remove the constraints
113% associated with it (in particular, reif_unify).
114and_reif_unify(0,B,C), reif_unify(_,_,B) <=> C=0.
115and_reif_unify(A,0,C), reif_unify(_,_,A) <=> C=0.
116and_reif_unify(0,_,C) <=> C=0.
117and_reif_unify(_,0,C) <=> C=0.
118and_reif_unify(A,B,1) <=> A=1, B=1.
119and_reif_unify(1,B,C) <=> B=C.
120and_reif_unify(A,1,C) <=> A=C.
121
122reif_unify_args(0,_,_,1):- !.
123reif_unify_args(N,X,Y,B):-
124 is_identical(B,0),
125 !, not_unify_args(N,X,Y).
126reif_unify_args(N,X,Y,B) :-
127 arg(N,X,Xn),
128 arg(N,Y,Yn),
129 reif_unify(Xn,Yn,Bn), 130 (Bn == 0
131 -> B = 0 132 ; and_reif_unify(Bn,Bn1,B),
133 134 N1 is N-1,
135 reif_unify_args(N1,X,Y,Bn1)
136 ).
137
138yes @ unify_constr(T1,T2) <=> T1 == T2 | true.
139% The following rule improves very much the efficiency, but MUST be after rule 'yes'
140not_unif_syntactical @ unify_constr(T1,T2) <=> ?=(T1,T2), \+fd_or_num(T1), \+fd_or_num(T2) | false.
141unify_constr(X,Y) <=>
142 nonvar(X), nonvar(Y)|
143 functor(X,F,N), functor(Y,F,N),
144 unify_args(N,X,Y).
145
146unif_symm @ unify_constr(X,Y) <=> nonvar(X), var(Y) | unify_constr(Y,X).
147
148
149
150% Regola strana per risolvere il problema degli NE nel body...
151% Probabilmente questa regola dovrebbe essere inserita anche nell'unificazione
152% a basso livello (nella quantif.pl).
153nonflagged_exists1 @ unify_constr(X,Y) <=> var(X), var(Y), % inutile: fallisce gia` get_quant se sono nonvar
154 get_quant(X,QX), get_quant(Y,exists), QX \= forallf | false.
155nonflagged_exists2 @ unify_constr(Y,X) <=> var(X), var(Y),
156 get_quant(X,QX), get_quant(Y,exists), QX \= forallf | false.
157nonflagged_exists3 @ unify_constr(X,Y) <=> var(X),
158 nonvar(Y), get_quant(X,exists) | false.
159
160unify_var_nonvar @ unify_constr(X,Y) <=> var(X), get_quant(X,Q), Q \==exists, nonvar(Y) | term_equality(X,Y).
161
162%% Aggiunto da Marco A:
163
164univ_exist_1 @ unify_constr(X,Y) <=>
165 is_universal(X),
166 get_restrictions(X,[]),is_existential(Y) | term_equality(X,Y).
167univ_exist_2 @ unify_constr(Y,X) <=> is_universal(X),
168 get_restrictions(X,[]),is_existential(Y) | term_equality(X,Y).
169
170existsf_unif_existsf @ unify_constr(X,Y) <=>
171is_existential(X),is_existential(Y) | term_equality(X,Y).
172
173 %cannot happen (see rule unif_symm).
174%unify_constr(Y,X) <=> var(X), nonvar(Y), get_quant(X,exists) | false.
175
176%unify_constr(X,Y) <=> X=Y.
177
178% Added MarcoG 9 may 2005
179% from D8, page 165:
180% a universaly quantified variabe can unify with an existentially quant. var.
181% The result is that the quantifier restrictions become constraints.
182% This is already achieved when the two variables are unified, so we only
183% have to unify the variabls.
184univ_exist_3 @ unify_constr(X,Y) <=>
185 is_universal(X),
186 get_quant(Y,existsf)
187 | term_equality(X,Y).
188univ_exist_3 @ unify_constr(Y,X) <=>
189 is_universal(X),
190 get_quant(Y,existsf)
191 | term_equality(X,Y).
192
193unify_args(0,_,_):-!.
194unify_args(N,X,Y):-
195 arg(N,X,Xn),
196 arg(N,Y,Yn),
197 unify_constr(Xn,Yn),
198 N1 is N-1,
199 unify_args(N1,X,Y).
200
201no @ not_unify_constr(T1,T2) <=> T1 == T2 | false.
202% The following rule improves very much the efficiency, but MUST be after rule 'no'
203not_unif_syntactical @ not_unify_constr(T1,T2) <=> ?=(T1,T2) | true.
204nu1 @ not_unify_constr(X,Y) <=> nonvar(X), nonvar(Y),
205 functor(X,F,N), functor(Y,F,N) |
206 not_unify_args(N,X,Y).
207nu2 @ not_unify_constr(X,Y) <=> nonvar(X), nonvar(Y) | X \= Y.
208%nu3 @ not_unify_constr(X,Y) <=> X==Y | false. Mi sembra identica alla "no"
209% nu4 is occur check: we skip it (for now)
210nu5a @ not_unify_constr(X,Y) <=> var(Y), nonvar(X) | not_unify_constr(Y,X).
211% Qui dovrei anche considerare se X e` free
212nu5b @ not_unify_constr(X,Y) <=> var(Y), get_quant(Y,forall),
213 var(X), get_quant(X,QX), QX \= forall, QX \=forallf | not_unify_constr(Y,X).
214% Stessa cosa per le flagged
215nu5bf @ not_unify_constr(X,Y) <=> var(Y), get_quant(Y,forallf),
216 var(X), get_quant(X,QX), QX \= forall, QX \=forallf | not_unify_constr(Y,X).
217%nu6a @ not_unify_constr(X,_) <=> var(X), get_quant(X,forall), get_restrictions(X,[]) | false.
218%nu6af @ not_unify_constr(X,_) <=> var(X), get_quant(X,forallf), get_restrictions(X,[]) | false.
219%not_unify_constr(_,X) <=> var(X), get_quant(X,forall) | false.
220
221nu6b @ not_unify_constr(X,Y) <=> var(X),
222 is_universal(X), existsf_or_ground(Y) |
223 get_restrictions(X,Rx),
224 impose_neg_constraints(X,Rx,Y).
225
226
227
228
229% Checks that unification of the existentially quantified vars
230% is unfeasible.
231% Notice that if the solver is not complete, then the \+ may
232% fail even if the unification is impossible!
233
234%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
235% Modified by Federico Chesani - 20060314 1530
236% New Version:
237nu6c @ not_unify_constr(X,Y) <=> var(X), var(Y),
238 is_universal(X), is_universal(Y),
239 get_restrictions(X,_Rx), get_restrictions(Y,_Ry) |
240 \+( (existsf(E), E=X, E=Y) ).
241% End New Version
242% Old Version
243/*
244nu6c @ not_unify_constr(X,Y) <=> var(X), var(Y),
245 is_universal(X), is_universal(Y),
246 get_restrictions(X,Rx), get_restrictions(Y,Ry) |
247 \+( (silly, existsf(E), E=X, E=Y) ).
248*/
249% End Old Version
250% End Modification
251%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
252
253nu_clpfd1 @ not_unify_constr(X,Y) <=> cstr_var(X), get_quant(X,existsf), cstr_var(Y), get_quant(Y,existsf) | neq(X,Y).
254nu_clpfd1 @ not_unify_constr(X,Y) <=> cstr_var(X), get_quant(X,existsf), is_number(Y) | neq(X,Y).
255%nu_clpfd2 @ not_unify_constr(X,Y) <=> cstr_var(X), number(Y) | X #\=Y.
256nu_clpfd3 @ not_unify_constr(X,Y) <=> cstr_var(X), nonvar(Y), \+number(Y) |true.
257
265
268
269not_unify_args(_,X,Y):-
270 get_disunif_variables(X,Y,Lx,Ly),
271 disunif_list(Lx,Ly).
272
275get_disunif_variables(X,Y,Lx,Ly):-
276 (var(X);var(Y)),!, Lx=[X], Ly=[Y].
277get_disunif_variables(X,Y,Lx,Ly):-
278 (ground(X),ground(Y)
279 ; ?=(X,Y)
280 ),
281 !,
282 X \= Y,
283 Lx=[],Ly=[].
284get_disunif_variables(X,Y,Lx,Ly):-
285 X =.. [F|ArgX],
286 Y =.. [F|ArgY],
287 get_disunif_variables_args(ArgX,ArgY,Lx,Ly).
288get_disunif_variables_args([],_,[],[]):-!. 289get_disunif_variables_args([X|ArgX],[Y|ArgY],Lx,Ly):-
290 (get_disunif_variables(X,Y,Lx1,Ly1) ; Lx1=[], Ly1=[]),!,
291 get_disunif_variables_args(ArgX,ArgY,Lx2,Ly2),
292 append(Lx1,Lx2,Lx),
293 append(Ly1,Ly2,Ly).
294
295disunif_list([X],[Y]):- !,not_unify_constr(X,Y).
296disunif_list([X1,X2|Tx],[Y1,Y2|Ty]):-
297 reif_unify(X1,Y1,B1),
298 (B1 == 0 -> !
299 ; (B1 == 1 -> fail 300 ; !,disunif_list_constr(B1,[X2|Tx],[Y2|Ty])
301 )
302 ).
304disunif_list([_X1,X2|Tx],[_Y1,Y2|Ty]):-
305 disunif_list([X2|Tx],[Y2|Ty]).
306
307:- chr_constraint disunif_list_constr(?natural,?any,?any).
308disunif_list_constr(0,_,_) <=> true.
309disunif_list_constr(1,Lx,Ly) <=> disunif_list(Lx,Ly).
310
311
312
313existsf_or_ground(Y):- ground(Y),!.
314existsf_or_ground(Y):-
315 get_quant(Y,existsf).
316
317
318
323
328if_unary_substitute(X,R,Y,T):- X == R,!, Y=T.
330if_unary_substitute(_,R,_,T):- var(R),get_quant(R,existsf), !, T=R.
331if_unary_substitute(_,R,_,_):- var(R),get_quant(R,Q),
332 (Q=forall; Q=forallf ; Q= exists), !,
333 write('*** Unimplemented feature: disunification of '),
334 write(Q), write(' with constrained forallf ***'), nl,
335 fail.
336if_unary_substitute(_,R,_,T):- ground(R),!, T=R.
338if_unary_substitute(X,st(R),Y,T):- !, if_unary_substitute(X,R,Y,T).
339if_unary_substitute(X,R,Y,T):-
340 functor(R,F,N), functor(T,F,N),
341 if_unary_substitute_arg(N,X,R,Y,T).
342
343if_unary_substitute_arg(0,_,_,_,_).
344if_unary_substitute_arg(N,X,R,Y,T):-
345 N>0,
346 arg(N,R,Rn),
347 arg(N,T,Tn),
348 N1 is N-1,
349 if_unary_substitute(X,Rn,Y,Tn),
350 if_unary_substitute_arg(N1,X,R,Y,T).
351
352
353inst(X) <=> ground(X) | true.
354
355
356grounding_inst @
357make_choice \ inst(B) <=>
358 var(B) |
359 (B=1 ; B=0).
360grounding_reif_unify @
361make_choice, reif_unify(_,_,B) ==>
362 var(B) |
363 (B=1 ; B=0).
364
371
372get_bool_inst([],X,X).
373get_bool_inst([inst(T)|R],[T|RT],X):-
374 get_bool_inst(R,RT,X).
375
376get_bool_reif([],X,X).
377get_bool_reif([reif_unify(_,_,T)|R],[T|RT],X):-
378 get_bool_reif(R,RT,X).
379
380label_bools([]).
381label_bools([1|L]):-
382 label_bools(L).
383label_bools([0|L]):-
384 label_bools(L)