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