1 % (c) 2009-2015 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(chr_integer_inequality,[chr_leq/2, chr_lt/2, chr_eq/2, chr_eq/3, chr_neq/2, chr_in_interval/4,
6 enable_complex_rules/0, attach_chr_integer_inequality_to_wf_store/1]).
7
8 :- use_module(library(clpfd)).
9
10 :- use_module(library(chr)).
11 :- chr_option(check_guard_bindings,off).
12 :- chr_option(optimize,full).
13 :- chr_option(debug,off).
14 %:- chr_option(generate_debug_info,true). % does not work
15
16 % restore operators overwritten by chr library
17 % otherwise, unary operators might not be parseable
18 :- op(200, fy, [+,-]).
19 % :- op(500, yfx, \).
20 :- op(0,yfx,'#').
21
22
23 :- use_module(probsrc(self_check), [assert_must_succeed/1, assert_must_fail/1]).
24 :- use_module(probsrc(kernel_waitflags), [get_enumeration_starting_wait_flag/3]).
25 :- use_module(probsrc(preferences), [get_preference/2]).
26 :- use_module(probsrc(debug), [debug_println/2]).
27
28 :- assert_must_succeed(( chr_leq(X,Y), chr_leq(Y,Z), Z=X, Y==X, Y==Z, X=5)).
29 :- assert_must_succeed(( chr_leq(X,Y), chr_leq(Y,Z), chr_leq(Z,X), Y==X, Y==Z, X=5)).
30 :- assert_must_fail(( chr_leq(X,Y), chr_lt(Y,X))).
31 :- assert_must_succeed(( chr_leq(X,Y), X=5, Y=7)).
32 :- assert_must_succeed(( chr_leq(X,Y), chr_leq(Y,X), X==Y, X=5)).
33 :- assert_must_fail(( chr_lt(X,Y), chr_eq(X,Y) )).
34 :- assert_must_fail(( chr_leq(X,Y), chr_neq(X,Y), chr_leq(Y,X) )).
35 :- assert_must_succeed(( chr_leq(X*X,4), chr_leq(4,X*X), 0 #< X, X==2)).
36 % does not work on sicstus 4.3 as #= is handled by a propagator rather than unification
37 % :- assert_must_succeed(( chr_eq(X,Y), chr_leq(4,Y*Y), chr_leq(X*X,4), %X #= Y, 0 #< X, X==2)).
38 % :- assert_must_succeed(( chr_eq(X,Y), chr_leq(4,2*Y), chr_leq(X*X,4),
39 % X #= Y, 0 #< X, X==2)).
40 :- assert_must_succeed((X*X #=< Y*Y, chr_leq(X*X,Y*Y),
41 4 #=< X*X, chr_leq(4,X*X),
42 Y=2, 0 #< X, X==2)).
43 % This is hard to infer by an easy rule
44 %:- assert_must_succeed((post_constraint2( X*X #=< Y*Y, _ ), chr_leq(X*X,Y*Y),
45 % post_constraint2( Y*Y #=< X*X, _), chr_leq(X*X,Y*Y),
46 % X==Y)).
47 :- assert_must_fail(( chr_lt(X*X,Y*Y), chr_lt(Y*Y,X*X) )).
48
49
50
51 % assumes we use CLP(FD) to complement it
52
53 chr_leq(X,Y) :-
54 simplify_expr(X,SX), simplify_expr(Y,SY), %print(chr_leq(X,Y,SX,SY)),nl,
55 leq(SX,SY).
56 chr_lt(X,Y) :-
57 simplify_expr(X,SX), simplify_expr(Y,SY), %print(chr_lt(X,Y,SX,SY)),nl,
58 lt(SX,SY).
59
60 :- use_module(probsrc(clpfd_interface),[computable_arith_expression/1]).
61 simplify_expr(E,R) :-
62 % TO DO: avoid redoing the same check in clpfd_interface after doing CHR propagation
63 % pass simplification result back to caller ??!
64 (computable_arith_expression(E) -> R is E ; R=E).
65
66 chr_eq(X,Y) :- is_idl(X,Y,A,B,C),!,idl(A,B,C). %TODO: should we set up chr_eq/3 in addition to idl/3?
67 chr_eq(X,Y) :- is_idl(Y,X,A,B,C),!,idl(A,B,C). % Alternative: introduce on demand out of chr_eq/3?
68 chr_eq(X,Y) :-
69 chr_eq(X,Y,pred_true).
70
71
72 is_idl(X,Y, A,B,C) :- % A = B+C
73 simple(X),
74 %var(X), % should we also allow numbers ? 100 = x+y ?
75 nonvar(Y),
76 (Y = -(A,B) -> simple(A),simple(B),C=X % , print(idl(X,Y)),nl.
77 ; Y = +(B,C) -> simple(B),simple(C), A=X). %,print(is_idl(X,Y)),print_idl(A,B,C).
78
79
80 chr_eq(X,Y,R) :- simplify_expr(X,SX), simplify_expr(Y,SY), % print(chr_eq(SX,SY,R)),nl,
81 eq(SX,SY,R),
82 eq(SY,SX,R). % commutativity, add constraint the other way around
83 chr_neq(X,Y) :- chr_eq(X,Y,pred_false), chr_eq(Y,X,pred_false).
84
85 :- public setup_eq/2.
86 setup_eq(X,Y) :- % print(setup_eq(X,Y)),nl,
87 (var(X), ground(Y) -> X is Y ;
88 var(Y), ground(X) -> Y is X ;
89 var(X), var(Y) -> X = Y ;
90 fd_var(X), fd_var(Y) -> chr_eq(X,Y), call(X #= Y) ;
91 ground(X), ground(Y) -> true ; % X =:= Y check is done by clpfd
92 otherwise -> chr_eq(X,Y),
93 call(X #= Y)). % the call is necessary; otherwise we get an error for complex arguments such as: "expected an integer, but found _109*_109"
94
95 :- public setup_lt/2.
96 setup_lt(X,Y) :- number(X),number(Y),!, X<Y.
97 setup_lt(X,Y) :- %print(lt(X,Y)),nl,
98 lt(X,Y),
99 call_dif_when_necesssary(X,Y), % ensure that frozen_dif detects these variables to be different
100 call(X #< Y). % Do we need those ?? Isn't CLPFD doing this automatically ? TO DO : check
101 %post_constraint2(X #< Y, _Posted).
102
103
104 % set up a dif co-routine only if necessary; assumption: E1,E2 are either number or variable
105 call_dif_when_necesssary(E1,E2) :- (number(E1) ; number(E2)),!. % nothing to be gained by posting dif
106 call_dif_when_necesssary(E1,E2) :-
107 dif(E1,E2). % ensure that frozen_dif detects these variables to be different
108
109 :- public setup_leq/2.
110 setup_leq(X,Y) :- number(X),number(Y),!, X=<Y.
111 setup_leq(X,Y) :- %print(leq(X,Y)),nl,
112 leq(X,Y),
113 call(X #=< Y).
114 %post_constraint2(X #=< Y, _Posted).
115
116 % this constraints can be added to the store to enable complex
117 % propagation rules if nessasary
118 % (i.e. before enumerating infinite domains)
119 :- chr_constraint enable_idl_rules/0, disable_idl_rules/0.
120 enable_complex_rules :- % print('ENABLE IDL RULES'),nl,nl,
121 enable_idl_rules.
122 %enable_complex_rules :- print('BACKTRACK ENABLE IDL'),nl,fail.
123
124 disable_complex_rules :- disable_idl_rules.
125
126 %enable1 @ enable_idl_rules ==> format('~nEnabling CHR-IDL~n~n',[]).
127 disable1 @ disable_idl_rules \ enable_idl_rules <=> true. % ,format('~nDisabling CHR-IDL~n~n',[]).
128 rm_disable @ disable_idl_rules <=> true, debug_println(4,disabled_chr_complex_rules).
129
130 attach_chr_integer_inequality_to_wf_store(WF) :-
131 get_preference(use_chr_solver,true), !,
132 disable_complex_rules,
133 get_enumeration_starting_wait_flag(chr_integer_inequality,WF,LWF),
134 enable_complex_rules_block(WF,LWF).
135 attach_chr_integer_inequality_to_wf_store(_).
136
137 :- block enable_complex_rules_block(?,-).
138 enable_complex_rules_block(_WF,_) :- % kernel_waitflags:portray_waitflags(_WF),
139 enable_complex_rules.
140
141 :- chr_constraint leq/2, lt/2.
142 :- chr_constraint eq/3.
143
144 :- public '@'/2.
145 reflexivity @ leq(X,X) <=> true.
146 antisymmetry @ leq(X,Y), leq(Y,X) <=> setup_eq(X,Y).
147 idempotence @ leq(X,Y) \ leq(X,Y) <=> true.
148 transitivity @ leq(X,Y), leq(Y,Z) ==> setup_leq(X,Z).
149
150 % checking is done by CLP(FD)
151 % checking @ leq(X,Y) <=> ground(X),ground(Y) | X =< Y.
152
153 % Only handled by CLP(FD) if value is known!
154 antireflexivity @ lt(X,X) <=> %print(inconsistent(X,X)),nl,
155 fail.
156 idempotence @ lt(X,Y) \ lt(X,Y) <=> true.
157 transitivity @ lt(X,Y), leq(Y,Z) ==> setup_lt(X,Z).
158 transitivity @ leq(X,Y), lt(Y,Z) ==> setup_lt(X,Z).
159 transitivity @ lt(X,Y), lt(Y,Z) ==> setup_lt(X,Z).
160 plus1rule1 @ leq(A+B,Y) ==> pos_add1(A,B,X) | %print(plus1_leq(X,Y)),nl,
161 setup_lt(X,Y). % no need to setup CLPFD; is actually <=> ; Discuss with Sebastian; but we need to set up dif
162 plus1rule2 @ lt(X,A+B) ==> pos_add1(A,B,Y) | %print(plus1_2_lt(X,Y)),nl,
163 leq(X,Y). % ditto
164 plus1weak1 @ lt(A+B,Y) ==> pos_add(A,B,X) | %print(plus1_weak_lt(X,Y)),nl,
165 setup_lt(X,Y).
166 % TO DO: add rules for minus; maybe rewrite using idl constraints
167
168 % --------------------
169
170 :- chr_constraint in_interval/4.
171 % assert X..Y <: V..W either Y<X or V<=X & Y <= W
172 chr_in_interval(X,Y,V,W) :-
173 simplify_expr(X,SX), simplify_expr(Y,SY), simplify_expr(V,SV), simplify_expr(W,SW),
174 %print(post(in(SX,SY,SV,SW))),nl,
175 in_interval(SX,SY,SV,SW).
176
177 pos_in_interval1 @ leq(X,Y) \ in_interval(X,Y,V,W) <=> setup_leq(V,X), setup_leq(Y,W). % | print(in(X,Y,V,W)),nl.
178 pos_in_interval2 @ lt(X,Y) \ in_interval(X,Y,V,W) <=> setup_leq(V,X), setup_leq(Y,W). % | print(inlt(X,Y,V,W)),nl.
179 eq_in_interval @ in_interval(X,X,V,W) <=> setup_leq(V,X), setup_leq(X,W). % | print(inlt(X,X,V,W)),nl.
180 neg_in_interval @ lt(Y,X) \ in_interval(X,Y,_V,_W) <=> true. % | print(in_empty(X,Y,V,W)),nl.
181
182 % --------------------
183
184 /*
185 leads to loop for test 1403
186 lt_idl_rule1 @ lt(X,Y), idl(X,Y,Z) ==> not_negative(Z) | setup_lt(0,Z).
187 lt_idl_rule2 @ lt(X,Y), idl(X,Z,Y) ==> not_negative(Z) | setup_lt(0,Z).
188 lt_idl_rule3 @ lt(Y,X), idl(X,Y,Z) ==> not_positive(Z) | setup_lt(Z,0).
189 lt_idl_rule4 @ lt(Y,X), idl(X,Z,Y) ==> not_positive(Z) | setup_lt(Z,0).
190
191 leq_idl_rule1 @ leq(X,Y), idl(X,Y,Z) ==> not_definitely_geq(Z,0) | setup_leq(0,Z).
192 leq_idl_rule2 @ leq(X,Y), idl(X,Z,Y) ==> not_definitely_geq(Z,0) | setup_leq(0,Z).
193 leq_idl_rule3 @ leq(Y,X), idl(X,Y,Z) ==> not_definitely_leq(Z,0) | setup_leq(Z,0).
194 leq_idl_rule4 @ leq(Y,X), idl(X,Z,Y) ==> not_definitely_leq(Z,0) | setup_leq(Z,0).
195
196
197 not_positive(V) :- \+ positive(V).
198 positive(Var) :- clpfd_interface:clpfd_domain(Var,Low,_), number(Low), Low>0.
199 not_definitely_geq(V,N) :- \+ definitely_geq(V,N).
200 definitely_geq(Var,Bound) :- clpfd_interface:clpfd_domain(Var,Low,_), number(Low), Low>=Bound.
201 not_negative(V) :- \+ negative(V).
202 negative(Var) :- clpfd_interface:clpfd_domain(Var,_,Up), number(Up), Up<0.
203 not_definitely_leq(V,N) :- \+ definitely_geq(V,N).
204 definitely_leq(Var,Bound) :- clpfd_interface:clpfd_domain(Var,_,Up), number(Up), Up=<Bound.
205 */
206
207
208 % checking is done by CLP(FD)
209 % checking @ lt(X,Y) <=> ground(X),ground(Y) | X < Y.
210
211 % idempotence of equality seems to be costly. remove this rule?
212 % idempotence @ eq(X,Y,R) \ eq(X,Y,R) <=> true.
213 became_equal @ eq(X,X,R) <=> R=pred_true.
214 % same @ eq(X,Y,R1) \ eq(X,Y,R2) <=> print(eq_same(X,Y,R1,R2)),nl,R1=R2. % not really required as R1/2 = pred_false or pred_true, if pred_true will force X=Y
215
216 strengthen @ eq(X,Y,pred_false) \ leq(X,Y) <=> setup_lt(X,Y).
217 % strengthen @ eq(Y,X,pred_false) \ leq(X,Y) <=> setup_lt(X,Y). % not required anymore, we add eq both ways
218
219 % this reifies to disequality if lt constraint was generated above
220 eq_lt_contradiction @ eq(X,Y,R), lt(X,Y) ==> R = pred_false.
221 %eq_lt_contradiction @ eq(X,Y,R), lt(Y,X) ==> R = pred_false. % not required anymore, we add eq both ways
222
223 :- public pos_add/3, pos_add1/3. % Spider does not seem to detect usage above
224 pos_add(A,B,X) :- positive_constant_addition(A,B,X,_).
225 pos_add1(A,B,X) :- (B==1 -> X=A ; A==1, X=B).
226 positive_constant_addition(X,Y,Var,Cst) :-
227 (var(X) -> pos_aux(X,Y,Var,Cst)
228 ; var(Y) -> pos_aux(Y,X,Var,Cst)).
229 :- use_module(probsrc(clpfd_interface),[clpfd_check_geq_nr/2]).
230 pos_aux(X,Y,Var,Cst) :-
231 clpfd_check_geq_nr(Y,1), Var=X, Cst=Y.
232
233 % if an expression is ground, we can calculate it (might not be needed?)
234 % calculate @ leq(X,Y) ==> compound(X), ground(X) | V is X, leq(V,Y).
235 % calculate @ leq(X,Y) ==> compound(Y), ground(Y) | V is Y, leq(X,V).
236
237 :- chr_constraint idl/3.
238 :- chr_constraint idl_sym/3.
239
240 % now that the idl constraints are only evaluated later on
241 % some of them might be inferred already.
242 % remove those!
243 % if two arguments are ground, clp(fd) inferred the third!
244 remove_idl_done @ idl(A,B,C) <=> (ground(A) -> (ground(B); ground(C)) ; ground(B),ground(C)) | true. %, print(removed_idl(A,B,C)),nl.
245
246 % proof rules for IDL like expressions
247 %introduce_idl @ eq(V,X-Y,pred_true) <=> idl(V,X,Y).
248
249 idempotence1 @ enable_idl_rules, idl(X1,Y,R) \ idl(X2,Y,R) <=> %print(idem1(X1,X2,Y+R)),nl,
250 X1=X2.
251 idempotence2 @ enable_idl_rules, idl(X1,Y,R) \ idl(X2,R,Y) <=> %print(idem2(X1,X2,Y+R)),nl,
252 X1=X2.
253
254 neq_idl1 @ enable_idl_rules, idl(X,V,Y), eq(X,Y,pred_false) ==> clpfd_interface:clpfd_neq_expr(V,0). %eq(V,0,pred_false). %, print(idl1(V,X,Y,EQXY)),nl.
255 neq_idl2 @ enable_idl_rules, idl(X,Y,V), eq(X,Y,pred_false) ==> clpfd_interface:clpfd_neq_expr(V,0).
256
257 %idl_eq_zero1 @ enable_idl_rules \ idl(X,V,X) <=> print(eq_zero1(V,X)),nl, clpfd_eq_expr(V,0).
258 %idl_eq_zero2 @ enable_idl_rules \ idl(X,X,V) <=> print(eq_zero2(V,X)),nl, clpfd_eq_expr(V,0).
259 idl_eq_zero1 @ enable_idl_rules, idl(X,V,X) ==> %print(eq_zero1(V,X)),nl,
260 clpfd_eq_expr(V,0).
261 idl_eq_zero2 @ enable_idl_rules, idl(X,X,V) ==> %print(eq_zero2(V,X)),nl,
262 clpfd_eq_expr(V,0).
263 % the following rules infer lt from idl, e.g., lt(x,y) in x:1..3 & y=2+x & v={x,y} & card(v)=r
264 idl_lt1 @ enable_idl_rules, idl(X,N,Y) ==> number(N), N>0 %, print(idl_lt(X,N,Y)),nl
265 | lt(Y,X).
266 idl_lt2 @ enable_idl_rules, idl(X,N,Y) ==> number(N), N<0 %, print(idl_lt(X,N,Y)),nl
267 | lt(X,Y).
268 % add rule
269
270 %idl_eq_zero @ eq(V,X-Y,pred_true) \ eq(X,Y,pred_true) <=> true | print(idl_eq_zero(V,X,Y)),nl, clpfd_eq_expr(V,0).
271
272 :- use_module(probsrc(clpfd_interface),[clpfd_eq_expr/2, clpfd_eq_expr_optimized/2]).
273 %finite_idl1 @ idl(X0,V2,X1) \ enable_idl_rules <=> finite(V2) | idl_finite(X0,V2,X1), print(finite1(X0,V2,X1)),nl.
274 %finite_idl2 @ idl(X0,X1,V2) \ enable_idl_rules <=> finite(V2) | idl_finite(X0,V2,X1), print(finite2(X0,V2,X1)),nl.
275
276 % generate an idl target goal for deriving new constraints about infinite variables
277 gen_idl_sym_target1 @ enable_idl_rules, idl(A,B,C) ==> %print('Check: '),print_idl(A,B,C),
278 infinite(B)
279 | %print(target1(B,(A,B,C))),nl,
280 idl_sym(A,B,C).
281 gen_idl_sym_target2 @ enable_idl_rules, idl(A,C,B) ==>
282 infinite(B) | %print(target2(B,(A,B,C))),nl,
283 idl_sym(A,B,C).
284
285 remove_idl_sym @ idl_sym(_,V,_) <=> finite(V) | true.
286 % try and infer new constraints for infinite variables
287 transitivity_idl1 @ enable_idl_rules, idl_sym(X0,V2,X1), idl(X0,V0,X2), idl(X1,V1,X2) ==>
288 infinite(V2) | %print(idl3(V2,V0-V1)),nl,
289 setup_eq(V2,V0-V1).
290 transitivity_idl2 @ enable_idl_rules, idl_sym(X0,V2,X1), idl(X0,V0,X2), idl(X1,X2,V1) ==>
291 infinite(V2) | %print(idl4(V2,V0-V1)),nl,
292 setup_eq(V2,V0-V1).
293 transitivity_idl3 @ enable_idl_rules, idl_sym(X0,V2,X1), idl(X0,X2,V0), idl(X1,X2,V1) ==>
294 infinite(V2) | %print(idl5(V2,V0-V1)),nl,
295 setup_eq(V2,V0-V1).
296 transitivity_idl4 @ enable_idl_rules, idl_sym(X0,V2,X1), idl(X0,X2,V0), idl(X1,V1,X2) ==>
297 infinite(V2) | %print(idl6(V2,V0-V1)),nl,
298 setup_eq(V2,V0-V1).
299
300 % next rule relevant for solving x+y=100 & y<x or x=100-y & y<x
301 transitivity_idl5 @ enable_idl_rules, idl_sym(A,X,Y), lt(X,Y) ==>
302 (number(A);infinite(X);infinite(Y)) | %print(idl7(A,X,Y)),nl,
303 setup_lt(A,Y+Y),setup_lt(X+X,A).
304
305 /*
306
307 transitivity_idl3 @ enable_idl_rules, idl(X0,X2,V0), idl(X1,X2,V1) \ idl_sym(X0,V2,X1) <=>
308 chck_infinite(V2) | print(idl5(V2,V0-V1)),nl,
309 setup_eq(V2,V0-V1).
310
311
312 old version with idl_pair
313 transitivity_idl1 @ enable_idl_rules, idl(X0,V2,X1), idl_finite(X0,V0,X2), idl_finite(X1,V1,X2) ==>
314 infinite(V2) | print(idl3(V2,V1,V0)),nl, setup_eq(V2,V0-V1).
315 transitivity_idl2 @ enable_idl_rules, idl(X0,V2,X1), idl_finite(X0,V0,X2), idl_finite(X1,X2,V1) ==>
316 infinite(V2) | print(idl4(V2,V1,V0)),nl, setup_eq(V2,V0-V1).
317 :- chr_constraint idl_pair/4.
318 % idempotence @ idl_pair(V,W,Y,R) \ idl_pair(V,W,Y,R) <=> true. % not beneficial ?
319 transitivity_pair1 @ enable_idl_rules, idl(V,X,YY), idl(W,YY,Z)
320 ==> print(pair1(V,W,X,Z)),nl,
321 idl_pair(V,W,X,Z). % V+W = X-Z
322 transitivity_pair2 @ enable_idl_rules, idl(YY,X,V), idl(W,YY,Z)
323 ==> print(pair2(V,W,X,Z)),nl,
324 idl_pair(V,W,X,Z). % V+W = X-Z
325 transitivity_idl @ enable_idl_rules, idl_pair(V,W,X,Z), idl(U,X,Z)
326 ==> idl_worth_it(U,V,W) | print(idl5(U,V+W)),nl,
327 %% idl(V,U,W).
328 %clpfd_eq_expr(U,V+W).
329 setup_eq(U,V+W).
330 %kernel_objects:int_plus(int(V),int(W),int(U)).
331 % heuristic: only set up new constraint when we have an infinite domain
332 %idl_worth_it(U,V,W) :-print_fd(U),print_fd(V),print_fd(W),nl,fail.
333 idl_worth_it(U,_V,_W) :- clpfd_interface:clpfd_size(U,sup),!.
334 idl_worth_it(_U,V,_W) :- clpfd_interface:clpfd_size(V,sup),!.
335 idl_worth_it(_U,_V,W) :- clpfd_interface:clpfd_size(W,sup),!.
336 */
337
338 :- public finite/1.
339 infinite(Var) :- clpfd_interface:clpfd_size(Var,sup).
340 finite(Var) :- \+ infinite(Var).
341
342 :- public print_idl/3.
343 print_idl(A,B,C) :- print(' IDL: '), print_fd(A), print(' = '), print_fd(B), print(' + '), print_fd(C),nl.
344 print_fd(N) :- number(N),!,print(N).
345 print_fd(V) :- clpfd_interface:clpfd_domain(V,VA,VB), %clpfd_interface:clpfd_size(V,Sz),
346 format('~w:(~w..~w)',[V,VA,VB]). %print(fd(V,size(Sz),VA:VB)).
347
348 % much slower:
349 %%transitivity_pair @ idl(V,X,Y), idl(W,Y,Z) ==> clpfd_eq_expr(V+W,VW), idl(VW,X,Z).