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