this repo has no description
dekker.one
1/*
2% FlatZinc built-in redefinitions for linear solvers.
3%
4% AUTHORS
5% Sebastian Brand
6% Gleb Belov
7*/
8
9%-----------------------------------------------------------------------------%
10%
11% Linear equations and inequations
12% TODO Use indicators for (half)reifs.
13% Otherwise and more using unary encoding for reasonable domains
14%
15%-----------------------------------------------------------------------------%
16
17% Domains: reduce all to aux_ stuff?
18%% never use Concert's reif feature
19
20%% var, var
21predicate int_le_reif(var int: x, var int: y, var bool: b) =
22%% trace(" int_le_reif VV: \(x), \(y), \(b) \n") /\
23 if is_fixed(b) then
24 if true==fix(b) then x<=y else x>y endif
25 elseif ub(x)<=lb(y) then b==true
26 elseif lb(x)>ub(y) then b==false
27 elseif fPostprocessDomains /\ fPostproDom_DIFF then
28 int_le_reif__POST(x-y, 0, b)
29 else
30 int_le_reif__NOPOST(x, y, b)
31 endif
32;
33
34%% const, var
35predicate int_le_reif(int: x, var int: y, var bool: b) =
36%% trace(" int_le_reif CV: \(x), \(y), \(b) \n") /\
37 if is_fixed(b) then
38 if true==fix(b) then x<=y else x>y endif
39 elseif ub(x)<=lb(y) then b==true
40 elseif lb(x)>ub(y) then b==false
41 elseif not (x in dom(y)) then %% dom(y) has holes
42 let {
43 set of int: sDom2 = dom(y) intersect x+1..infinity,
44 constraint assert( card( sDom2 ) > 0,
45 "Variable: dom(\(y)) = \(dom(y)), but dom() intersect \(x)..inf: \(sDom2)\n" ),
46 } in
47 b <-> min( sDom2 ) <= y
48 elseif fPostprocessDomains then
49 int_ge_reif__POST(y, x, b)
50 else
51 int_le_reif(-y, -x, b)
52 endif
53;
54
55%% var, const
56predicate int_le_reif(var int: x, int: y, var bool: b) =
57%% trace(" int_le_reif VC: \(x), \(y), \(b) \n") /\
58 if is_fixed(b) then
59 if true==fix(b) then x<=y else x>y endif
60 elseif ub(x)<=lb(y) then b==true
61 elseif lb(x)>ub(y) then b==false
62 elseif not (y in dom(x)) then %% dom(x) has holes
63 let {
64 set of int: sDom2 = dom(x) intersect -infinity..y-1,
65 constraint assert( card( sDom2 ) > 0,
66 "Variable: dom(\(x)) = \(dom(x)), but dom() intersect -inf..\(y): \(sDom2)\n" ),
67 } in
68 b <-> x <= max( sDom2 )
69 else
70 if fPostprocessDomains then
71 int_le_reif__POST(x, y, b)
72 else
73 int_le_reif__NOPOST(x, y, b)
74 endif
75 endif
76;
77
78%% var int, var int
79predicate int_le_reif__NOPOST(var int: x, var int: y, var bool: b) =
80 aux_int_le_if_1(x, y, b) /\ %% This can call POSTs... TODO
81 aux_int_gt_if_0(x, y, b)
82 ;
83
84%% var, var
85predicate int_lt_reif(var int: x, var int: y, var bool: b) =
86 %% int_le_reif(x-y, -1, b); %% This would produce a new variable x-y and possibly POST it
87 %% but it looks like differences should not be
88 if is_fixed( x ) then
89 int_le_reif(x+1, y, b)
90 else
91 int_le_reif(x, y-1, b)
92 endif;
93
94%% var, var
95predicate int_ne(var int: x, var int: y) =
96 if fPostproDom_DIFF then
97 int_ne(x-y, 0)
98 else
99 int_ne__SIMPLE(x-y, 0)
100 endif;
101
102%% var, const
103predicate int_ne(var int: x, int: y) =
104 if y in dom(x) then
105 if y==ub(x) then
106 x <= y-1
107 elseif y==lb(x) then
108 x >= y+1
109 elseif fPostprocessDomains then
110 int_ne__POST(x, y)
111 elseif card(dom(x))<nMZN__UnaryLenMax_neq then
112 let {
113 array[int] of var int: p = eq_encode(x);
114 } in
115 p[y]==false
116 else int_ne__SIMPLE(x, y)
117 endif
118 else
119 true
120 endif;
121
122%% var, const. No postprocessing
123predicate int_ne__SIMPLE(var int: x, int: y) =
124 if true then
125 let { var 0..1: p }
126 in
127 aux_int_lt_if_1(x, y, p) /\
128 aux_int_gt_if_0(x, y, p)
129 else %TODO: Why is this not half-reified?
130 1 == (x<y) + (x>y)
131 endif;
132
133%% var, var
134predicate int_eq_reif(var int: x, var int: y, var bool: b) =
135%% trace(" int_eq_reif VV: \(x), \(y), \(b) \n") /\
136 if is_fixed(b) then
137 if fix(b) then x==y else x!=y endif
138 elseif card(dom(x) intersect dom(y))>0 then
139 if is_fixed(x) then
140 if is_fixed(y) then
141 b <-> fix(x)==fix(y)
142 else
143 int_eq_reif(y, fix(x), b)
144 endif
145 elseif is_fixed(y) then
146 int_eq_reif(x, fix(y), b)
147 elseif fPostprocessDomains /\ fPostproDom_DIFF then
148 int_eq_reif(x-y, 0, b)
149 else
150 aux_int_eq_iff_1(x, y, b)
151 endif
152 else
153 not b
154 endif;
155
156%% var, const
157predicate int_eq_reif(var int: x, int: y, var bool: b) =
158%% trace(" int_eq_reif VC: \(x), \(y), \(b) \n") /\
159 if is_fixed(b) then
160 if fix(b) then x==y else x!=y endif
161 elseif y in dom(x) then
162 if is_fixed(x) then
163 b <-> y==fix(x)
164 elseif card(dom(x))==2 then
165 x == max(dom(x) diff {y}) + b*(y - max(dom(x) diff {y})) %% This should directly connect b to var 0..1: x
166 elseif fPostprocessDomains then
167 int_eq_reif__POST(x, y, b)
168%%% THIS seems pretty complex, especially for binaries, and does not connect to eq_encoding (/ MIPD?)
169%% elseif y==lb(x) then
170%% int_lt_reif(y, x, not b)
171%% elseif y==ub(x) then
172%% int_lt_reif(x, y, not b)
173 elseif card(dom(x))<nMZN__UnaryLenMax_eq then
174 let {
175 array[int] of var int: p = eq_encode(x);
176 } in
177 p[y]==b
178 else
179 aux_int_eq_iff_1(x, y, bool2int(b))
180 endif
181 else
182 b==false
183 endif;
184
185
186predicate int_ne_reif(var int: x, var int: y, var bool: b) =
187 int_eq_reif(x, y, not b);
188
189predicate int_ne_reif(var int: x, int: y, var bool: b) =
190 int_eq_reif(x, y, not b);
191
192%-----------------------------------------------------------------------------%
193
194%% To avoid creating a new int var = sum...
195function var float: sum2float( array[int] of int: c, array[int] of var int: x ) =
196 let {
197 array[int] of float: cF = c;
198 array[int] of var float: xF = x;
199 } in
200 sum(i in index_set(xF))( cF[i]*xF[i] );
201
202%% lin_expr, const
203predicate int_lin_le_reif(array[int] of int: c, array[int] of var int: x,
204 int: d, var bool: b) =
205 if fPostprocessDomains /\ fPostproDom_DIFF then
206 int_le_reif(sum(i in index_set(x))( c[i] * x[i] ), d, b)
207 elseif fAvoidNI then
208 aux_float_le_if_1(sum2float( c, x ), d, b) /\
209 aux_float_ge_if_0(sum2float( c, x ), d+1, b)
210 else
211 int_le_reif__NOPOST(sum(i in index_set(x))( c[i] * x[i] ), d, b)
212 endif;
213
214
215predicate int_lin_lt_reif(array[int] of int: c, array[int] of var int: x,
216 int: d, var bool: b) =
217 if true then
218 abort("int_lin_lt_reif not supposed to be called")
219 else
220 int_lin_le_reif(c, x, d - 1, b)
221 endif;
222
223%% lin_expr, const
224predicate int_lin_eq_reif(array[int] of int: c, array[int] of var int: x,
225 int: d, var bool: b) =
226 if fPostprocessDomains /\ fPostproDom_DIFF then
227 int_eq_reif(sum(i in index_set(x))( c[i]*x[i] ), d, b)
228 elseif fAvoidNI /\ fAuxIntEqOLD00 then
229 aux_int_eq_iff_1__float(sum2float( c, x ), d, b)
230 else
231 aux_int_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, b)
232 endif;
233
234%% lin_expr, const
235predicate int_lin_ne(array[int] of int: c, array[int] of var int: x, int: d) =
236 if fPostprocessDomains /\ fPostproDom_DIFF then
237 int_ne(sum(i in index_set(x))( c[i]*x[i] ),d)
238 elseif fAvoidNI then
239 int_lin_eq_reif(c, x, d, false)
240 else
241 int_ne__SIMPLE(sum(i in index_set(x))( c[i]*x[i] ),d)
242 endif;
243
244%% lin_expr, const
245predicate int_lin_ne_reif(array[int] of int: c, array[int] of var int: x,
246 int: d, var bool: b) =
247 if fPostprocessDomains /\ fPostproDom_DIFF then
248 int_ne_reif(sum(i in index_set(x))( c[i]*x[i] ), d, b)
249 else
250 int_lin_eq_reif(c, x, d, not (b))
251 endif;
252
253
254%-----------------------------------------------------------------------------%
255
256%% var float, const
257predicate float_le_reif(var float: x, float: y, var bool: b) =
258%% trace( "float_le_reif(\(x), \(y), \(b))\n" ) /\
259 if is_fixed(b) then
260 if true==fix(b) then x<=y else x>y endif
261 elseif false then
262 float_lin_le_reif__IND( [1.0, -1.0], [x, y], 0.0, b)
263 elseif ub(x) <= y then
264 b == true
265 elseif lb(x) > y then
266 b == false
267 elseif fPostprocessDomains then
268 float_le_reif__POST(x, y, b, float_lt_EPS)
269 else
270 float_le_reif__NOPOST(x, y, b)
271 endif;
272
273%% const, var float
274predicate float_le_reif(float: x, var float: y, var bool: b) =
275 if is_fixed(b) then
276 if true==fix(b) then x<=y else x>y endif
277 elseif false then
278 float_lin_le_reif__IND( [1.0, -1.0], [x, y], 0.0, b)
279 elseif ub(x) <= lb(y) then
280 b == true
281 elseif lb(x) > ub(y) then
282 b == false
283 elseif fPostprocessDomains then
284 float_ge_reif__POST(y, x, b, float_lt_EPS)
285 else
286 float_le_reif(-y, -x, b)
287 endif;
288
289%% var float, var float
290predicate float_le_reif(var float: x, var float: y, var bool: b) =
291 if is_fixed(b) then
292 if true==fix(b) then x<=y else x>y endif
293 elseif ub(x)<=lb(y) then b==true
294 elseif lb(x)>ub(y) then b==false
295 elseif fPostprocessDomains /\ fPostproDom_DIFF then
296 float_le_reif(x-y, 0.0, b)
297 else
298 float_le_reif__NOPOST(x-y, 0, b)
299 endif
300;
301
302%% var float, var float
303predicate float_le_reif__NOPOST(var float: x, var float: y, var bool: b) =
304 aux_float_le_if_1(x, y, (b)) /\ %% Can call __POSTs TODO
305 aux_float_gt_if_0(x, y, (b))
306 ;
307
308%% TODO
309predicate float_lt_reif(var float: x, var float: y, var bool: b) =
310 %% Actually = float_le_reif(x, y-eps, b).
311 if is_fixed(b) then
312 if true==fix(b) then x<y else x>=y endif
313 elseif fPostprocessDomains /\ fPostproDom_DIFF then
314 aux_float_lt_zero_iff_1__POST(x - y, b, float_lt_EPS)
315 else
316 aux_float_lt_if_1(x, y, (b)) /\
317 aux_float_ge_if_0(x, y, (b))
318 endif;
319
320%% var, const
321predicate float_ne(var float: x, float: y) =
322 if fPostprocessDomains then
323 float_ne__POST(x, y, float_lt_EPS)
324 else
325 float_ne__SIMPLE(x, y)
326 endif;
327
328predicate float_ne__SIMPLE(var float: x, var float: y) =
329 if true then
330 let { var 0..1: p }
331 in
332 aux_float_lt_if_1(x, y, (p)) /\
333 aux_float_gt_if_0(x, y, (p))
334 else %TODO: Why is this not half-reified?
335 1 == (x>y) + (x<y)
336 endif;
337
338%% var, var
339predicate float_ne(var float: x, var float: y) =
340 if fPostprocessDomains /\ fPostproDom_DIFF then
341 float_ne(x-y, 0.0)
342 else
343 float_ne__SIMPLE(x-y, 0.0)
344 endif;
345
346%% TODO Why is disequality with EPS but equality not??
347
348%% var, var? TODO
349predicate float_eq_reif(var float: x, var float: y, var bool: b) =
350 if is_fixed(b) then
351 if true==fix(b) then x==y else x!=y endif
352 elseif ub(x)<lb(y) \/ lb(x)>ub(y) then
353 b == false
354 elseif is_fixed(x) /\ is_fixed(y) then
355 b == (fix(x) == fix(y))
356 elseif fPostprocessDomains /\ fPostproDom_DIFF then
357 float_eq_reif__POST(x-y, 0, b, float_lt_EPS)
358 else
359 aux_float_eq_iff_1(x, y, (bool2int(b)))
360 endif;
361
362predicate float_ne_reif(var float: x, var float: y, var bool: b) =
363 float_eq_reif(x, y, not (b));
364
365%-----------------------------------------------------------------------------%
366
367predicate float_lin_eq_reif(array[int] of float: c, array[int] of var float: x,
368 float: d, var bool: b) =
369 if fPostprocessDomains /\ fPostproDom_DIFF then
370 float_eq_reif(sum(i in index_set(x))( c[i]*x[i] ), d, b)
371 else
372 aux_float_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, b)
373 endif;
374
375predicate float_lin_ne_reif(array[int] of float: c, array[int] of var float: x,
376 float: d, var bool: b) =
377 if fPostprocessDomains /\ fPostproDom_DIFF then
378 float_ne_reif(sum(i in index_set(x))( c[i]*x[i] ), d, not b)
379 else
380 aux_float_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, not b)
381 endif;
382
383predicate float_lin_le_reif(array[int] of float: c, array[int] of var float: x,
384 float: d, var bool: b) =
385 if fPostprocessDomains /\ fPostproDom_DIFF then
386 float_le_reif(sum(i in index_set(x))( c[i]*x[i] ), d, b)
387 else
388 float_le_reif__NOPOST(sum(i in index_set(x))( c[i]*x[i] ), d, b)
389 endif;
390
391predicate float_lin_lt_reif(array[int] of float: c, array[int] of var float: x,
392 float: d, var bool: b) =
393 float_lt_reif(sum(i in index_set(x))( c[i]*x[i] ), d, b);
394
395
396%-----------------------------------------------------------------------------%
397% Auxiliary: equality reified onto a 0/1 variable
398
399predicate aux_int_eq_iff_1(var int: x, var int: y, var int: p) =
400 if is_fixed(p) then
401 if 1==fix(p) then x==y else x!=y endif
402 elseif fPostprocessDomains /\ fPostproDom_DIFF then
403 abort(" aux_int_eq_iff_1 should not be used with full domain postprocessing")
404 elseif false then
405 true
406 elseif fAuxIntEqOLD00 then
407 let { array[1..2] of var 0..1: q }
408 in
409 aux_int_le_if_1(x, y, p) /\
410 aux_int_ge_if_1(x, y, p) /\
411 aux_int_lt_if_0(x, y, q[1]) /\
412 aux_int_gt_if_0(x, y, q[2]) /\
413 sum(q) == p + 1
414 else
415 %% redundant p == (x<=y /\ y<=x) /\
416 1+p == (x<=y) + (y<=x)
417 endif;
418
419predicate aux_int_eq_iff_1__float(var float: x, float: y, var int: p) =
420 if fAuxIntEqOLD00 then
421 assert( false, "Don't use aux_int_eq_iff_1__float" )
422/* let { array[1..2] of var 0..1: q }
423 in
424 aux_int_le_if_1(x, y, p) /\
425 aux_int_ge_if_1(x, y, p) /\
426 aux_int_lt_if_0(x, y, q[1]) /\
427 aux_int_gt_if_0(x, y, q[2]) /\
428 sum(q) == p + 1 */
429 else
430 assert( false, "Don't use aux_int_eq_iff_1__float with fAuxIntEqOLD00" )
431 endif;
432
433 % Alternative 2
434predicate aux_int_eq_iff_1__WEAK1(var int: x, var int: y, var int: p) =
435 let { array[1..2] of var 0..1: q_458 }
436 in
437 aux_int_lt_if_0(x - p, y, q_458[1]) /\
438 aux_int_gt_if_0(x + p, y, q_458[2]) /\
439 sum(q_458) <= 2 - 2*p /\
440 sum(q_458) <= 1 + p;
441
442 % Alternative 1
443predicate alt_1_aux_int_eq_iff_1(var int: x, var int: y, var int: p) =
444 let { array[1..2] of var 0..1: q }
445 in
446 aux_int_lt_if_0(x - p, y, q[1]) /\
447 aux_int_gt_if_0(x + p, y, q[2]) /\
448 q[1] <= 1 - p /\
449 q[2] <= 1 - p /\
450 sum(q) <= 1 + p;
451
452predicate aux_float_eq_iff_1(var float: x, var float: y, var int: p) =
453 if is_fixed(p) then
454 if 1==fix(p) then x==y else x!=y endif
455 elseif fPostprocessDomains /\ fPostproDom_DIFF then
456 abort(" aux_float_eq_iff_1 should not be used with full domain postprocessing")
457 elseif fAuxFloatEqOLD00 then
458 let { array[1..2] of var 0..1: q }
459 in
460 aux_float_le_if_1(x, y, p) /\
461 aux_float_ge_if_1(x, y, p) /\
462 aux_float_lt_if_0(x, y, (q[1])) /\
463 aux_float_gt_if_0(x, y, (q[2])) /\
464 sum(i in 1..2)((q[i])) == 1 + p
465 else
466 %% redundant p == (x<=y /\ y<=x) /\
467 1+p == (x<=y) + (y<=x)
468 endif;
469
470
471
472% ----------------------------- Domains postpro ---------------------------
473
474%%%%%%%%%%%%%%%%%% predicate int_le_reif__POST(var int: x, var int: y, var int: b);
475%%%%%%%%%%%%%%%%%% predicate int_le_reif__POST(int: x, var int: y, var int: b);
476%%%%%%% var int: b: bool2int is a reverse_map, not passed to .fzn
477%% var, const
478predicate int_le_reif__POST(var int: x, int: y, var int: b);
479%% var, const
480predicate int_ge_reif__POST(var int: x, int: y, var int: b);
481
482%% var, const
483predicate int_eq_reif__POST(var int: x, int: y, var int: b);
484%% var, const
485predicate int_ne__POST(var int: x, int: y);
486
487%%%%%%%%%%%%%%%%%% predicate float_le_reif__POST(var float: x, var float: y, var int: b);
488%%%%%%%%%%%%%%%%%% predicate float_le_reif__POST(float: x, var float: y, var int: b);
489%% var, const
490predicate float_le_reif__POST(var float: x, float: y, var int: b, float: epsRel);
491%% var, const
492predicate float_ge_reif__POST(var float: x, float: y, var int: b, float: epsRel);
493
494%% var, var
495predicate aux_float_lt_zero_iff_1__POST(var float: x, var int: b, float: epsRel);
496
497%% var, const
498predicate float_eq_reif__POST(var float: x, float: y, var int: b, float: epsRel);
499%% var, const
500predicate float_ne__POST(var float: x, float: y, float: epsRel);
501
502