1%-----------------------------------------------------------------------------%
2% FlatZinc built-in redefinitions for linear solvers.
3%
4% Sebastian Brand
5% Gleb Belov     Corrected array_var_float_element and float_lin_lt_reif
6%-----------------------------------------------------------------------------%
7
8function var bool: reverse_map(var int: x) = (x==1);
9function bool: reverse_map(int: x) = (x==1);
10
11function var int: bool2int(var bool: x) :: promise_total =
12 let { var 0..1: b2i;
13       constraint (x = reverse_map(b2i)) ::is_reverse_map ;
14      } in b2i;
15
16predicate bool_eq(var bool: x, var bool: y) =
17  bool2int(x)==bool2int(y);
18
19%-----------------------------------------------------------------------------%
20% Strict inequality
21%
22% Uncomment the following redefinition for FlatZinc MIP solver interfaces that
23% do not support strict inequality.  Note that it does not preserve equivalence
24% (some solutions of the original problem may become invalid).
25
26% predicate float_lt(var float: x, var float: y) = x + 1e-06 <= y;
27
28%-----------------------------------------------------------------------------%
29%
30% Logic operations
31%
32%-----------------------------------------------------------------------------%
33
34predicate bool_not(var bool: p, var bool: q) =
35    let { var 0..1: x = bool2int(p),
36          var 0..1: y = bool2int(q) }
37    in
38    x + y = 1;
39
40
41predicate bool_and(var bool: p, var bool: q, var bool: r) =
42    let { var 0..1: x = bool2int(p),
43          var 0..1: y = bool2int(q),
44          var 0..1: z = bool2int(r) }
45    in
46    x + y <= z + 1 /\
47    x + y >= z * 2;
48    % x >= z /\ y >= z;     % alternative
49
50
51predicate bool_or(var bool: p, var bool: q, var bool: r) =
52    let { var 0..1: x = bool2int(p),
53          var 0..1: y = bool2int(q),
54          var 0..1: z = bool2int(r) }
55    in
56    x + y >= z /\
57    x + y <= z * 2;
58    % x <= z /\ y <= z;     % alternative
59
60
61predicate bool_xor(var bool: p, var bool: q, var bool: r) =
62    let { var 0..1: x = bool2int(p),
63          var 0..1: y = bool2int(q),
64          var 0..1: z = bool2int(r) }
65    in
66    x <= y + z /\
67    y <= x + z /\
68    z <= x + y /\
69    x + y + z <= 2;
70
71
72predicate bool_eq_reif(var bool: p, var bool: q, var bool: r) =
73    if is_fixed(q) then   % frequent case
74        if fix(q) = true then p = r else bool_not(p,r) endif
75    else
76    let { var 0..1: x = bool2int(p),
77          var 0..1: y = bool2int(q),
78          var 0..1: z = bool2int(r) }
79    in
80    x + y <= z + 1 /\
81    x + z <= y + 1 /\
82    y + z <= x + 1 /\
83    x + y + z >= 1
84    endif;
85
86
87predicate bool_ne_reif(var bool: p, var bool: q, var bool: r) =
88    bool_xor(p, q, r);
89
90
91predicate bool_le(var bool: p, var bool: q) =
92    let { var 0..1: x = bool2int(p),
93          var 0..1: y = bool2int(q) }
94    in
95    x <= y;
96
97
98predicate bool_le_reif(var bool: p, var bool: q, var bool: r) =
99    let { var 0..1: x = bool2int(p),
100          var 0..1: y = bool2int(q),
101          var 0..1: z = bool2int(r) }
102    in
103    1 - x + y >= z /\
104    1 - x + y <= z * 2;
105    % 1 - x <= z /\ y <= z; % alternative
106
107
108predicate bool_lt(var bool: p, var bool: q) =
109    not p /\ q;
110
111
112predicate bool_lt_reif(var bool: p, var bool: q, var bool: r) =
113    (not p /\ q) <-> r;
114
115%-----------------------------------------------------------------------------%
116
117predicate array_bool_or(array[int] of var bool: a, var bool: b) =
118    if is_fixed(b) then   % frequent case
119        if fix(b) = true then
120            sum(i in index_set(a))( bool2int(a[i]) ) >= 1
121        else
122            forall(i in index_set(a))( not a[i] )
123        endif
124    else
125    let { var 0..1: x = bool2int(b),
126          array[1..length(a)] of var 0..1: c =
127              [ bool2int(a[i]) | i in index_set(a) ] }
128    in
129    sum(c) >= x /\
130    sum(c) <= x * length(a)
131    endif;
132
133predicate array_bool_and(array[int] of var bool: a, var bool: b) =
134    let { var 0..1: x = bool2int(b),
135          array[1..length(a)] of var 0..1: c =
136              [ bool2int(a[i]) | i in index_set(a) ] }
137    in
138    length(a) - sum(c) >=  1 - x /\
139    length(a) - sum(c) <= (1 - x) * length(a);
140
141predicate array_bool_xor(array[int] of var bool: a) =
142     let { var 0..length(a): m }
143     in
144     sum(i in 1..length(a))( bool2int(a[i]) ) = 1 + 2 * m;
145
146predicate bool_clause(array[int] of var bool: p, array[int] of var bool: n) =
147      sum(i in index_set(p))( bool2int(p[i]) )
148    - sum(i in index_set(n))( bool2int(n[i]) )
149    + length(n)
150    >= 1;
151
152% predicate array_bool_xor(array[int] of var bool: a) = .. sum(a) is odd ..
153
154%-----------------------------------------------------------------------------%
155%
156% Linear equations and inequations
157%
158%-----------------------------------------------------------------------------%
159
160predicate int_le_reif(var int: x, var int: y, var bool: b) =
161    let { var 0..1: p = bool2int(b) }
162    in
163    aux_int_le_if_1(x, y, p) /\
164    aux_int_gt_if_0(x, y, p);
165
166
167predicate int_lt_reif(var int: x, var int: y, var bool: b) =
168    int_le_reif(x, y - 1, b);
169
170
171predicate int_ne(var int: x, var int: y) =
172    let { var 0..1: p }
173    in
174    aux_int_lt_if_1(x, y, p) /\
175    aux_int_gt_if_0(x, y, p);
176
177predicate int_lin_ne(array[int] of int: c, array[int] of var int: x, int: d) =
178    int_ne(sum(i in index_set(x))( c[i]*x[i] ),d);
179
180predicate int_eq_reif(var int: x, var int: y, var bool: b) =
181    aux_int_eq_iff_1(x, y, bool2int(b));
182
183
184predicate int_ne_reif(var int: x, var int: y, var bool: b) =
185    aux_int_eq_iff_1(x, y, 1 - bool2int(b));
186
187%-----------------------------------------------------------------------------%
188
189predicate int_lin_eq_reif(array[int] of int: c, array[int] of var int: x,
190                          int: d, var bool: b) =
191    aux_int_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, bool2int(b));
192
193
194predicate int_lin_ne_reif(array[int] of int: c, array[int] of var int: x,
195                          int: d, var bool: b) =
196    aux_int_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, 1 - bool2int(b));
197
198
199predicate int_lin_le_reif(array[int] of int: c, array[int] of var int: x,
200                          int: d, var bool: b) =
201    let { var 0..1: p = bool2int(b) }
202    in
203    aux_int_le_if_1(sum(i in index_set(x))( c[i] * x[i] ), d, p) /\
204    aux_int_gt_if_0(sum(i in index_set(x))( c[i] * x[i] ), d, p);
205
206
207predicate int_lin_lt_reif(array[int] of int: c, array[int] of var int: x,
208                          int: d, var bool: b) =
209    int_lin_le_reif(c, x, d - 1, b);
210
211%-----------------------------------------------------------------------------%
212
213predicate float_le_reif(var float: x, var float: y, var bool: b) =
214    let { var 0..1: p = bool2int(b) }
215    in
216    aux_float_le_if_1(x, y, int2float(p)) /\
217    aux_float_gt_if_0(x, y, int2float(p));
218
219
220predicate float_lt_reif(var float: x, var float: y, var bool: b) =
221    let { var 0..1: p = bool2int(b) }
222    in
223    aux_float_lt_if_1(x, y, int2float(p)) /\
224    aux_float_ge_if_0(x, y, int2float(p));
225
226
227predicate float_ne(var float: x, var float: y) =
228    let { var 0..1: p }
229    in
230    aux_float_lt_if_1(x, y, int2float(p)) /\
231    aux_float_gt_if_0(x, y, int2float(p));
232
233
234predicate float_eq_reif(var float: x, var float: y, var bool: b) =
235    aux_float_eq_iff_1(x, y, int2float(bool2int(b)));
236
237
238predicate float_ne_reif(var float: x, var float: y, var bool: b) =
239    aux_float_eq_iff_1(x, y, 1.0 - int2float(bool2int(b)));
240
241%-----------------------------------------------------------------------------%
242
243predicate float_lin_eq_reif(array[int] of float: c, array[int] of var float: x,
244                            float: d, var bool: b) =
245    aux_float_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d,
246        int2float(bool2int(b)));
247
248
249predicate float_lin_ne_reif(array[int] of float: c, array[int] of var float: x,
250                            float: d, var bool: b) =
251    aux_float_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d,
252        1.0 - int2float(bool2int(b)));
253
254
255predicate float_lin_le_reif(array[int] of float: c, array[int] of var float: x,
256                            float: d, var bool: b) =
257    let { var 0.0..1.0: p = int2float(bool2int(b)) }
258    in
259    aux_float_le_if_1(sum(i in index_set(x))( c[i] * x[i] ), d, p) /\
260    aux_float_gt_if_0(sum(i in index_set(x))( c[i] * x[i] ), d, p);
261
262
263predicate float_lin_lt_reif(array[int] of float: c, array[int] of var float: x,
264                            float: d, var bool: b) =
265    let { var 0.0..1.0: p = int2float(bool2int(b)) }
266    in
267    aux_float_lt_if_1(sum(i in index_set(x))( c[i] * x[i] ), d, p) /\
268    aux_float_ge_if_0(sum(i in index_set(x))( c[i] * x[i] ), d, p);
269
270%-----------------------------------------------------------------------------%
271% Minimum, maximum, absolute value
272
273predicate int_abs(var int: x, var int: z) =
274    let { var 0..1: p }
275    in
276    % z <= x \/ z <= -x
277    aux_int_le_if_1(z,  x, p) /\
278    aux_int_le_if_0(z, -x, p) /\
279    z >=  x /\
280    z >= -x /\
281    z >= 0;
282
283
284predicate int_min(var int: x, var int: y, var int: z) =
285    let { var 0..1: p }
286    in
287    % z >= x \/ z >= y
288    aux_int_ge_if_1(z, x, p) /\
289    aux_int_ge_if_0(z, y, p) /\
290    z <= x /\
291    z <= y;
292
293
294predicate int_max(var int: x, var int: y, var int: z) =
295    let { var 0..1: p }
296    in
297    % z <= x \/ z <= y
298    aux_int_le_if_1(z, x, p) /\
299    aux_int_le_if_0(z, y, p) /\
300    z >= x /\
301    z >= y;
302
303
304predicate float_abs(var float: x, var float: z) =
305    let { var 0..1: p }
306    in
307    % z <= x \/ z <= -x
308    aux_float_le_if_1(z,  x, int2float(p)) /\
309    aux_float_le_if_0(z, -x, int2float(p)) /\
310    z >=  x /\
311    z >= -x /\
312    z >= 0.0;
313
314
315predicate float_min(var float: x, var float: y, var float: z) =
316    let { var 0..1: p }
317    in
318    % z >= x \/ z >= y
319    aux_float_ge_if_1(z, x, int2float(p)) /\
320    aux_float_ge_if_0(z, y, int2float(p)) /\
321    z <= x /\
322    z <= y;
323
324
325predicate float_max(var float: x, var float: y, var float: z) =
326    let { var 0..1: p }
327    in
328    % z <= x \/ z <= y
329    aux_float_le_if_1(z, x, int2float(p)) /\
330    aux_float_le_if_0(z, y, int2float(p)) /\
331    z >= x /\
332    z >= y;
333
334%-----------------------------------------------------------------------------%
335% Multiplication and division
336
337predicate int_div(var int: x, var int: y, var int: q) =
338    let { var 0..max(abs(lb(y)), abs(ub(y))) - 1: r }
339    in
340    aux_int_division_modulo(x,y,q,r);
341
342
343predicate int_mod(var int: x, var int: y, var int: r) =
344    let {
345      int: bx = max(abs(lb(x)), abs(ub(x)));
346      var -bx..bx: q;
347      int: by = max(abs(lb(y)), abs(ub(y)));
348      constraint r in -by..by;
349    }
350    in
351    aux_int_division_modulo(x,y,q,r);
352
353
354predicate aux_int_division_modulo(var int: x, var int: y, var int: q,
355        var int: r) =
356    x = y * q + r /\
357    let { array[1..2] of var 0..1: p }
358    in
359    % 0 < x -> 0 <= r    which is    0 >= x \/ 0 <= r
360    aux_int_le_if_1(x, 0, p[1]) /\
361    aux_int_ge_if_0(r, 0, p[1]) /\
362    % x < 0 -> r <= 0    which is    x >= 0 \/ r <= 0
363    aux_int_ge_if_1(x, 0, p[2]) /\
364    aux_int_le_if_0(r, 0, p[2]) /\
365    % abs(r) < abs(y)
366    let { var 1.. max(abs(lb(y)), abs(ub(y))): w = abs(y) }
367    in
368    w >  r /\
369    w > -r;
370
371
372predicate int_times(var int: x, var int: y, var int: z) =
373    if card(dom(x)) > card(dom(y)) then int_times(y,x,z)
374    else
375    let { set of int: s = lb(x)..ub(x),
376          set of int: r = {lb(x)*lb(y), lb(x)*ub(y), ub(x)*lb(y), ub(x)*ub(y)},
377          array[s] of var min(r)..max(r): ady = array1d(s, [ d*y | d in s ]) }
378    in
379    ady[x] = z
380    endif;
381
382%-----------------------------------------------------------------------------%
383% Array 'element' constraints
384
385predicate array_bool_element(var int: x, array[int] of bool: a, var bool: z) =
386    x in index_set(a) /\
387    forall(d in index_set(a))( x = d -> a[d] = z );
388
389
390predicate array_var_bool_element(var int: x, array[int] of var bool: a,
391                                 var bool: z) =
392    x in index_set(a) /\
393    forall(d in index_set(a))( x = d -> a[d] = z );
394
395
396predicate array_int_element(var int: x, array[int] of int: a, var int: z) =
397    x in index_set(a) /\
398    forall(d in index_set(a))( x = d -> a[d] = z );
399
400predicate array_var_int_element(var int: x, array[int] of var int: a,
401                                var int: z) =
402    x in index_set(a) /\
403    forall(d in index_set(a))( x = d -> a[d] = z );
404
405
406predicate array_float_element(var int: x, array[int] of float: a,
407                              var float: z) =
408    let { set of int: ix = index_set(a),
409          array[ix] of var 0..1: x_eq_d }
410    in
411    sum(i in ix)(     x_eq_d[i] ) = 1
412    /\
413    sum(i in ix)( i * x_eq_d[i] ) = x
414    /\
415    sum(i in ix)( a[i] * int2float(x_eq_d[i]) ) = z;
416
417
418predicate array_var_float_element(var int: x, array[int] of var float: a,
419                                  var float: z) =
420    let { set of int: ix = index_set(a),
421          array[ix] of var 0..1: x_eq_d }
422    in
423    sum(i in ix)(     x_eq_d[i] ) = 1
424    /\
425    sum(i in ix)( i * x_eq_d[i] ) = x
426    /\
427    forall(i in ix)(
428        % x_eq_d[i] -> a[i] = a2[i]
429        a[i] - z >= (lb(a[i])-ub(z))*int2float(1-x_eq_d[i])
430        /\
431        z - a[i] >= (lb(z)-ub(a[i]))*int2float(1-x_eq_d[i])
432    );
433
434%-----------------------------------------------------------------------------%
435% Domain constraints
436
437% XXX  only for a fixed set
438
439predicate set_in(var int: x, set of int: s) =
440    if s = min(s)..max(s) then
441        min(s) <= x /\ x <= max(s)
442    else
443        exists(e in s)( x = e )
444    endif;
445
446% XXX  only for a fixed set
447predicate set_in_reif(var int: x, set of int: s, var bool: b) =
448    b <->
449        exists(i in 1..length([ 0 | e in s where not (e - 1 in s) ]))(
450            let { int: l = [ e | e in s where not (e - 1 in s) ][i],
451                  int: r = [ e | e in s where not (e + 1 in s) ][i] }
452            in
453            l <= x /\ x <= r
454        );
455
456    % Alternative
457predicate alt_set_in_reif(var int: x, set of int: s, var bool: b) =
458    b <->
459        if s = min(s)..max(s) then
460            min(s) <= x /\ x <= max(s)
461        else
462            exists(e in s)( x = e )
463        endif;
464
465%-----------------------------------------------------------------------------%
466% Auxiliary: equality reified onto a 0/1 variable
467
468predicate aux_int_eq_iff_1(var int: x, var int: y, var int: p) =
469    let { array[1..2] of var 0..1: q_458 }
470    in
471    aux_int_lt_if_0(x - p, y, q_458[1]) /\
472    aux_int_gt_if_0(x + p, y, q_458[2]) /\
473    sum(q_458) <= 2 - 2*p /\
474    sum(q_458) <= 1 + p;
475
476    % Alternative 1
477predicate alt_1_aux_int_eq_iff_1(var int: x, var int: y, var int: p) =
478    let { array[1..2] of var 0..1: q }
479    in
480    aux_int_lt_if_0(x - p, y, q[1]) /\
481    aux_int_gt_if_0(x + p, y, q[2]) /\
482    q[1] <= 1 - p /\
483    q[2] <= 1 - p /\
484    sum(q) <= 1 + p;
485
486    % Alternative 2
487predicate alt_2_aux_int_eq_iff_1(var int: x, var int: y, var int: p) =
488    let { array[1..2] of var 0..1: q }
489    in
490    aux_int_le_if_1(x, y, p) /\
491    aux_int_ge_if_1(x, y, p) /\
492    aux_int_lt_if_0(x, y, q[1]) /\
493    aux_int_gt_if_0(x, y, q[2]) /\
494    sum(q) <= p + 1;
495
496
497predicate aux_float_eq_iff_1(var float: x, var float: y, var float: p) =
498    let { array[1..2] of var 0..1: q }
499    in
500    aux_float_le_if_1(x, y, p) /\
501    aux_float_ge_if_1(x, y, p) /\
502    aux_float_lt_if_0(x, y, int2float(q[1])) /\
503    aux_float_gt_if_0(x, y, int2float(q[2])) /\
504    int2float(sum(q)) <= 1.0 + p;
505
506%-----------------------------------------------------------------------------%
507% Auxiliary: indicator constraints
508%   p -> x # 0  where p is a 0/1 variable and # is a comparison
509
510% Base cases
511
512predicate aux_int_le_zero_if_0(var int: x, var int: p) =
513    x <= ub(x) * p;
514
515predicate aux_float_le_zero_if_0(var float: x, var float: p) =
516    x <= ub(x) * p;
517
518predicate aux_float_lt_zero_if_0(var float: x, var float: p) =
519    let { float: rho = 1e-02 * abs(ub(x)) }  % same order of magnitude as ub(x)
520    in
521    x < (ub(x) + rho) * p;
522
523
524% Derived cases
525
526predicate aux_int_le_if_0(var int: x, var int: y, var int: p) =
527    aux_int_le_zero_if_0(x - y, p);
528
529predicate aux_int_ge_if_0(var int: x, var int: y, var int: p) =
530    aux_int_le_zero_if_0(y - x, p);
531
532predicate aux_int_le_if_1(var int: x, var int: y, var int: p) =
533    aux_int_le_zero_if_0(x - y, 1 - p);
534
535predicate aux_int_ge_if_1(var int: x, var int: y, var int: p) =
536    aux_int_le_zero_if_0(y - x, 1 - p);
537
538predicate aux_int_lt_if_0(var int: x, var int: y, var int: p) =
539    aux_int_le_zero_if_0(x - y + 1, p);
540
541predicate aux_int_gt_if_0(var int: x, var int: y, var int: p) =
542    aux_int_le_zero_if_0(y - x + 1, p);
543
544predicate aux_int_lt_if_1(var int: x, var int: y, var int: p) =
545    aux_int_le_zero_if_0(x - y + 1, 1 - p);
546
547
548predicate aux_float_le_if_0(var float: x, var float: y, var float: p) =
549    aux_float_le_zero_if_0(x - y, p);
550
551predicate aux_float_ge_if_0(var float: x, var float: y, var float: p) =
552    aux_float_le_zero_if_0(y - x, p);
553
554predicate aux_float_le_if_1(var float: x, var float: y, var float: p) =
555    aux_float_le_zero_if_0(x - y, 1.0 - p);
556
557predicate aux_float_ge_if_1(var float: x, var float: y, var float: p) =
558    aux_float_le_zero_if_0(y - x, 1.0 - p);
559
560predicate aux_float_lt_if_0(var float: x, var float: y, var float: p) =
561    aux_float_lt_zero_if_0(x - y, p);
562
563predicate aux_float_gt_if_0(var float: x, var float: y, var float: p) =
564    aux_float_lt_zero_if_0(y - x, p);
565
566predicate aux_float_lt_if_1(var float: x, var float: y, var float: p) =
567    aux_float_lt_zero_if_0(x - y, 1.0 - p);
568
569%-----------------------------------------------------------------------------%
570%-----------------------------------------------------------------------------%
571
572annotation bool_search(array[int] of var bool: x, ann:a1, ann:a2, ann:a3) =
573  int_search([bool2int(x[i]) | i in index_set(x)],a1,a2,a3);
574
575predicate array_int_maximum(var int: m, array[int] of var int: x) =
576    let { int: l = min(index_set(x)),
577          int: u = max(index_set(x)),
578          int: ly = lb_array(x),
579          int: uy = ub_array(x),
580          array[l..u] of var ly..uy: y } in
581    y[l] = x[l] /\
582    m = y[u] /\
583    forall (i in l+1 .. u) ( y[i] == max(x[i],y[i-1]) );
584
585predicate array_float_maximum(var float: m, array[int] of var float: x) =
586    let { int: l = min(index_set(x)),
587          int: u = max(index_set(x)),
588          float: ly = lb_array(x),
589          float: uy = ub_array(x),
590          array[l..u] of var ly..uy: y } in
591    y[l] = x[l] /\
592    m = y[u] /\
593    forall (i in l+1 .. u) ( y[i] == max(x[i],y[i-1]) );
594
595predicate array_int_minimum(var int: m, array[int] of var int: x) =
596    let { int: l = min(index_set(x)),
597          int: u = max(index_set(x)),
598          int: ly = lb_array(x),
599          int: uy = ub_array(x),
600          array[l..u] of var ly..uy: y } in
601    y[l] = x[l] /\
602    m = y[u] /\
603    forall (i in l+1 .. u) ( y[i] == min(x[i],y[i-1]) );
604
605predicate array_float_minimum(var float: m, array[int] of var float: x) =
606    let { int: l = min(index_set(x)),
607          int: u = max(index_set(x)),
608          float: ly = lb_array(x),
609          float: uy = ub_array(x),
610          array[l..u] of var ly..uy: y } in
611    y[l] = x[l] /\
612    m = y[u] /\
613    forall (i in l+1 .. u) ( y[i] == min(x[i],y[i-1]) );
614
615mzn_opt_only_range_domains = true;
616