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 length(c) == 1 /\ (d mod c[1] = 0) then % TODO: modulus not required when floating point calculations are possible
206 if c[1] > 0 then
207 int_le_reif(x[1], d div c[1], b)
208 else
209 int_le_reif(d div c[1], x[1], b)
210 endif
211 elseif fPostprocessDomains /\ fPostproDom_DIFF then
212 int_le_reif(sum(i in index_set(x))( c[i] * x[i] ), d, b)
213 elseif fAvoidNI then
214 aux_float_le_if_1(sum2float( c, x ), d, b) /\
215 aux_float_ge_if_0(sum2float( c, x ), d+1, b)
216 else
217 int_le_reif__NOPOST(sum(i in index_set(x))( c[i] * x[i] ), d, b)
218 endif;
219
220
221predicate int_lin_lt_reif(array[int] of int: c, array[int] of var int: x,
222 int: d, var bool: b) =
223 if true then
224 abort("int_lin_lt_reif not supposed to be called")
225 else
226 int_lin_le_reif(c, x, d - 1, b)
227 endif;
228
229%% lin_expr, const
230predicate int_lin_eq_reif(array[int] of int: c, array[int] of var int: x,
231 int: d, var bool: b) =
232 if length(c) == 1 then
233 if d mod c[1] != 0 then
234 not b
235 else
236 int_eq_reif(x[1], d div c[1], b)
237 endif
238 elseif fPostprocessDomains /\ fPostproDom_DIFF then
239 int_eq_reif(sum(i in index_set(x))( c[i]*x[i] ), d, b)
240 elseif fAvoidNI /\ fAuxIntEqOLD00 then
241 aux_int_eq_iff_1__float(sum2float( c, x ), d, b)
242 else
243 aux_int_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, b)
244 endif;
245
246%% lin_expr, const
247predicate int_lin_ne(array[int] of int: c, array[int] of var int: x, int: d) =
248 if length(c) == 1 then
249 (d mod c[1] = 0) -> int_ne(x[1], d div c[1])
250 elseif fPostprocessDomains /\ fPostproDom_DIFF then
251 int_ne(sum(i in index_set(x))( c[i]*x[i] ),d)
252 elseif fAvoidNI then
253 int_lin_eq_reif(c, x, d, false)
254 else
255 int_ne__SIMPLE(sum(i in index_set(x))( c[i]*x[i] ),d)
256 endif;
257
258%% lin_expr, const
259predicate int_lin_ne_reif(array[int] of int: c, array[int] of var int: x,
260 int: d, var bool: b) =
261 if length(c) == 1 then
262 if d mod c[1] != 0 then
263 b
264 else
265 int_ne_reif(x[1], d div c[1], b)
266 endif
267 elseif fPostprocessDomains /\ fPostproDom_DIFF then
268 int_ne_reif(sum(i in index_set(x))( c[i]*x[i] ), d, b)
269 else
270 int_lin_eq_reif(c, x, d, not (b))
271 endif;
272
273
274%-----------------------------------------------------------------------------%
275
276%% var float, const
277predicate float_le_reif(var float: x, float: y, var bool: b) =
278%% trace( "float_le_reif(\(x), \(y), \(b))\n" ) /\
279 if is_fixed(b) then
280 if true==fix(b) then x<=y else x>y endif
281 elseif false then
282 float_lin_le_reif__IND( [1.0, -1.0], [x, y], 0.0, b)
283 elseif ub(x) <= y then
284 b == true
285 elseif lb(x) > y then
286 b == false
287 elseif fPostprocessDomains then
288 float_le_reif__POST(x, y, b, float_lt_EPS)
289 else
290 float_le_reif__NOPOST(x, y, b)
291 endif;
292
293%% const, var float
294predicate float_le_reif(float: x, var float: y, var bool: b) =
295 if is_fixed(b) then
296 if true==fix(b) then x<=y else x>y endif
297 elseif false then
298 float_lin_le_reif__IND( [1.0, -1.0], [x, y], 0.0, b)
299 elseif ub(x) <= lb(y) then
300 b == true
301 elseif lb(x) > ub(y) then
302 b == false
303 elseif fPostprocessDomains then
304 float_ge_reif__POST(y, x, b, float_lt_EPS)
305 else
306 float_le_reif(-y, -x, b)
307 endif;
308
309%% var float, var float
310predicate float_le_reif(var float: x, var float: y, var bool: b) =
311 if is_fixed(b) then
312 if true==fix(b) then x<=y else x>y endif
313 elseif ub(x)<=lb(y) then b==true
314 elseif lb(x)>ub(y) then b==false
315 elseif fPostprocessDomains /\ fPostproDom_DIFF then
316 float_le_reif(x-y, 0.0, b)
317 else
318 float_le_reif__NOPOST(x-y, 0, b)
319 endif
320;
321
322%% var float, var float
323predicate float_le_reif__NOPOST(var float: x, var float: y, var bool: b) =
324 aux_float_le_if_1(x, y, (b)) /\ %% Can call __POSTs TODO
325 aux_float_gt_if_0(x, y, (b))
326 ;
327
328%% TODO
329predicate float_lt_reif(var float: x, var float: y, var bool: b) =
330 %% Actually = float_le_reif(x, y-eps, b).
331 if is_fixed(b) then
332 if true==fix(b) then x<y else x>=y endif
333 elseif fPostprocessDomains /\ fPostproDom_DIFF then
334 aux_float_lt_zero_iff_1__POST(x - y, b, float_lt_EPS)
335 else
336 aux_float_lt_if_1(x, y, (b)) /\
337 aux_float_ge_if_0(x, y, (b))
338 endif;
339
340%% var, const
341predicate float_ne(var float: x, float: y) =
342 if fPostprocessDomains then
343 float_ne__POST(x, y, float_lt_EPS)
344 else
345 float_ne__SIMPLE(x, y)
346 endif;
347
348predicate float_ne__SIMPLE(var float: x, var float: y) =
349 if true then
350 let { var 0..1: p }
351 in
352 aux_float_lt_if_1(x, y, (p)) /\
353 aux_float_gt_if_0(x, y, (p))
354 else %TODO: Why is this not half-reified?
355 1 == (x>y) + (x<y)
356 endif;
357
358%% var, var
359predicate float_ne(var float: x, var float: y) =
360 if fPostprocessDomains /\ fPostproDom_DIFF then
361 float_ne(x-y, 0.0)
362 else
363 float_ne__SIMPLE(x-y, 0.0)
364 endif;
365
366%% TODO Why is disequality with EPS but equality not??
367
368%% var, var? TODO
369predicate float_eq_reif(var float: x, var float: y, var bool: b) =
370 if is_fixed(b) then
371 if true==fix(b) then x==y else x!=y endif
372 elseif ub(x)<lb(y) \/ lb(x)>ub(y) then
373 b == false
374 elseif is_fixed(x) /\ is_fixed(y) then
375 b == (fix(x) == fix(y))
376 elseif fPostprocessDomains /\ fPostproDom_DIFF then
377 float_eq_reif__POST(x-y, 0, b, float_lt_EPS)
378 else
379 aux_float_eq_iff_1(x, y, (bool2int(b)))
380 endif;
381
382predicate float_ne_reif(var float: x, var float: y, var bool: b) =
383 float_eq_reif(x, y, not (b));
384
385%-----------------------------------------------------------------------------%
386
387predicate float_lin_eq_reif(array[int] of float: c, array[int] of var float: x,
388 float: d, var bool: b) =
389 if fPostprocessDomains /\ fPostproDom_DIFF then
390 float_eq_reif(sum(i in index_set(x))( c[i]*x[i] ), d, b)
391 else
392 aux_float_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, b)
393 endif;
394
395predicate float_lin_ne_reif(array[int] of float: c, array[int] of var float: x,
396 float: d, var bool: b) =
397 if fPostprocessDomains /\ fPostproDom_DIFF then
398 float_ne_reif(sum(i in index_set(x))( c[i]*x[i] ), d, not b)
399 else
400 aux_float_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, not b)
401 endif;
402
403predicate float_lin_le_reif(array[int] of float: c, array[int] of var float: x,
404 float: d, var bool: b) =
405 if fPostprocessDomains /\ fPostproDom_DIFF then
406 float_le_reif(sum(i in index_set(x))( c[i]*x[i] ), d, b)
407 else
408 float_le_reif__NOPOST(sum(i in index_set(x))( c[i]*x[i] ), d, b)
409 endif;
410
411predicate float_lin_lt_reif(array[int] of float: c, array[int] of var float: x,
412 float: d, var bool: b) =
413 float_lt_reif(sum(i in index_set(x))( c[i]*x[i] ), d, b);
414
415
416%-----------------------------------------------------------------------------%
417% Auxiliary: equality reified onto a 0/1 variable
418
419predicate aux_int_eq_iff_1(var int: x, var int: y, var int: p) =
420 if is_fixed(p) then
421 if 1==fix(p) then x==y else x!=y endif
422 elseif fPostprocessDomains /\ fPostproDom_DIFF then
423 abort(" aux_int_eq_iff_1 should not be used with full domain postprocessing")
424 elseif false then
425 true
426 elseif fAuxIntEqOLD00 then
427 let { array[1..2] of var 0..1: q }
428 in
429 aux_int_le_if_1(x, y, p) /\
430 aux_int_ge_if_1(x, y, p) /\
431 aux_int_lt_if_0(x, y, q[1]) /\
432 aux_int_gt_if_0(x, y, q[2]) /\
433 sum(q) == p + 1
434 else
435 %% redundant p == (x<=y /\ y<=x) /\
436 1+p == (x<=y) + (y<=x)
437 endif;
438
439predicate aux_int_eq_iff_1__float(var float: x, float: y, var int: p) =
440 if fAuxIntEqOLD00 then
441 assert( false, "Don't use aux_int_eq_iff_1__float" )
442/* let { array[1..2] of var 0..1: q }
443 in
444 aux_int_le_if_1(x, y, p) /\
445 aux_int_ge_if_1(x, y, p) /\
446 aux_int_lt_if_0(x, y, q[1]) /\
447 aux_int_gt_if_0(x, y, q[2]) /\
448 sum(q) == p + 1 */
449 else
450 assert( false, "Don't use aux_int_eq_iff_1__float with fAuxIntEqOLD00" )
451 endif;
452
453 % Alternative 2
454predicate aux_int_eq_iff_1__WEAK1(var int: x, var int: y, var int: p) =
455 let { array[1..2] of var 0..1: q_458 }
456 in
457 aux_int_lt_if_0(x - p, y, q_458[1]) /\
458 aux_int_gt_if_0(x + p, y, q_458[2]) /\
459 sum(q_458) <= 2 - 2*p /\
460 sum(q_458) <= 1 + p;
461
462 % Alternative 1
463predicate alt_1_aux_int_eq_iff_1(var int: x, var int: y, var int: p) =
464 let { array[1..2] of var 0..1: q }
465 in
466 aux_int_lt_if_0(x - p, y, q[1]) /\
467 aux_int_gt_if_0(x + p, y, q[2]) /\
468 q[1] <= 1 - p /\
469 q[2] <= 1 - p /\
470 sum(q) <= 1 + p;
471
472predicate aux_float_eq_iff_1(var float: x, var float: y, var int: p) =
473 if is_fixed(p) then
474 if 1==fix(p) then x==y else x!=y endif
475 elseif fPostprocessDomains /\ fPostproDom_DIFF then
476 abort(" aux_float_eq_iff_1 should not be used with full domain postprocessing")
477 elseif fAuxFloatEqOLD00 then
478 let { array[1..2] of var 0..1: q }
479 in
480 aux_float_le_if_1(x, y, p) /\
481 aux_float_ge_if_1(x, y, p) /\
482 aux_float_lt_if_0(x, y, (q[1])) /\
483 aux_float_gt_if_0(x, y, (q[2])) /\
484 sum(i in 1..2)((q[i])) == 1 + p
485 else
486 %% redundant p == (x<=y /\ y<=x) /\
487 1+p == (x<=y) + (y<=x)
488 endif;
489
490
491
492% ----------------------------- Domains postpro ---------------------------
493
494%%%%%%%%%%%%%%%%%% predicate int_le_reif__POST(var int: x, var int: y, var int: b);
495%%%%%%%%%%%%%%%%%% predicate int_le_reif__POST(int: x, var int: y, var int: b);
496%%%%%%% var int: b: bool2int is a reverse_map, not passed to .fzn
497%% var, const
498predicate int_le_reif__POST(var int: x, int: y, var int: b);
499%% var, const
500predicate int_ge_reif__POST(var int: x, int: y, var int: b);
501
502%% var, const
503predicate int_eq_reif__POST(var int: x, int: y, var int: b);
504%% var, const
505predicate int_ne__POST(var int: x, int: y);
506
507%%%%%%%%%%%%%%%%%% predicate float_le_reif__POST(var float: x, var float: y, var int: b);
508%%%%%%%%%%%%%%%%%% predicate float_le_reif__POST(float: x, var float: y, var int: b);
509%% var, const
510predicate float_le_reif__POST(var float: x, float: y, var int: b, float: epsRel);
511%% var, const
512predicate float_ge_reif__POST(var float: x, float: y, var int: b, float: epsRel);
513
514%% var, var
515predicate aux_float_lt_zero_iff_1__POST(var float: x, var int: b, float: epsRel);
516
517%% var, const
518predicate float_eq_reif__POST(var float: x, float: y, var int: b, float: epsRel);
519%% var, const
520predicate float_ne__POST(var float: x, float: y, float: epsRel);
521
522