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 (2015-)
7% cf. Belov, Stuckey, Tack, Wallace. Improved Linearization of Constraint Programming Models. CP 2016.
8*/
9
10%----------------------------- BOOL2INT --------------------------------%
11function var bool: reverse_map(var int: x) = (x==1);
12function bool: reverse_map(int: x) = (x==1);
13
14predicate mzn_reverse_map_var(var bool: b) = let {
15 var int: x = bool2int(b)
16} in true;
17
18function var int: bool2int(var bool: x) :: promise_total =
19 let { var 0..1: b2i;
20 constraint (x = reverse_map(b2i)) ::is_reverse_map ;
21 } in
22 b2i;
23
24predicate bool_eq(var bool: x, var bool: y) =
25%% trace(" bool_eq: \(x), \(y) \n") /\
26 bool2int(x)==bool2int(y);
27
28%---------------------------- BASIC (HALF)REIFS -----------------------------%
29
30include "options.mzn";
31include "redefs_bool_reifs.mzn";
32include "redefs_bool_imp.mzn";
33
34include "domain_encodings.mzn";
35include "redefs_lin_reifs.mzn";
36include "redefs_lin_imp.mzn";
37include "redefs_lin_halfreifs.mzn";
38
39include "nosets.mzn"; %% For set_le, set_lt ... Usind std/nosets
40 %% as long as the linearization is good.
41
42%-----------------------------------------------------------------------------%
43% Strict inequality
44
45% Uncomment the following redefinition for FlatZinc MIP solver interfaces that
46% do not support strict inequality. Note that it does not preserve equivalence
47% (some solutions of the original problem may become invalid).
48
49predicate float_lt(var float: x, var float: y) =
50% (x - y) <= (-float_lt_EPS_coef__)*max(abs(ub(x - y)), abs(ub(y-x)));
51 x <= y - float_lt_EPS;
52
53predicate float_lin_lt(array[int] of float: c, array[int] of var float: x,
54 float: d) =
55 float_lt(sum(i in index_set(x))( c[i]*x[i] ), d);
56
57%-----------------------------------------------------------------------------%
58% Minimum, maximum, absolute value
59% Use unary as well? TODO
60
61predicate int_abs(var int: x, var int: z) =
62%% The simplifications seem worse on league.mzn model90-18-20.dzn:
63%% but the .lp seem to differ just by order...?? TODO
64 if lb(x)>=0 then z==x
65 elseif ub(x)<=0 then z==-x
66 else
67 let { var bool: p }
68 in
69 z >= x /\
70 z >= -x /\
71 z >= 0 /\ % This is just for preprocessor
72 z <= max([ub(x), -lb(x)]) /\ % And this
73 % z <= x \/ z <= -x %% simple
74 aux_int_le_if_1(z, x, p) /\ %% even simpler
75 aux_int_le_if_0(z, -x, p) /\
76 int_le_reif(0, x, p) % with reifs
77 %int_eq_reif(z, x, p) /\
78 %int_eq_reif(z, -x, not p)
79 endif
80 ;
81
82predicate int_min(var int: x, var int: y, var int: z) =
83 array_int_minimum(z, [x, y]);
84
85predicate int_max(var int: x, var int: y, var int: z) =
86 array_int_maximum(z, [x, y]);
87
88predicate float_abs(var float: x, var float: z) =
89 if lb(x)>=0.0 then z==x
90 elseif ub(x)<=0.0 then z==-x
91 else
92 let { var bool: p }
93 in
94 z >= x /\
95 z >= -x /\
96 z >= 0.0 /\ % This is just for preprocessor
97 z <= max([ub(x), -lb(x)]) /\ % And this
98 % z <= x \/ z <= -x
99 aux_float_le_if_1(z, x, (p)) /\
100 aux_float_le_if_0(z, -x, (p))
101 % /\
102 % float_le_reif(0.0, x, p) % with reifs - no point for floats? TODO
103 % float_eq_reif(z, x, p) /\
104 % float_eq_reif(z, -x, not p)
105 endif;
106
107predicate float_min(var float: x, var float: y, var float: z) =
108 array_float_minimum(z, [x, y]);
109
110predicate float_max(var float: x, var float: y, var float: z) =
111 array_float_maximum(z, [x, y]);
112
113predicate array_float_minimum_I(var float: m, array[int] of var float: x) =
114 let { int: n = length(x),
115 constraint assert(1 == min(index_set(x)), " array_float_minimum_I: argument indexed not from 1??"),
116 int: iMinUB = arg_min([ub(x[i]) | i in 1..n]),
117 float: MinUB = ub(x[iMinUB]),
118 set of int: sLBLess = { i | i in 1..n where lb(x[i])<MinUB },
119 set of int: sUBEqual = { i | i in 1..n where ub(x[i])==MinUB },
120 set of int: sActive = if card(sLBLess intersect sUBEqual)>0 then sLBLess
121 else sLBLess union { iMinUB } endif,
122 } in
123 if 1==card(sActive) then
124 m == x[min(sActive)]
125 else
126 let {
127 array[1..n] of var int: p = [
128 if i in sActive then let { var 0..1: pi } in pi else 0 endif | i in 1..n ],
129 constraint 1==sum(p),
130 constraint m >= lb_array(x),
131 constraint m <= MinUB,
132 } in
133 forall (i in index_set(x))
134 (
135 if i in sActive %% for at least 1 element
136 then
137 m<=x[i] /\ aux_float_ge_if_1(m, x[i], p[i])
138 else true endif )
139 %% -- exclude too big x[i]
140 /\
141 if card(sActive)>1 /\ fMinimumCutsXZ then
142 let {
143 array[int] of float: AL = [ lb(x[i]) | i in 1..n],
144 array[int] of int: srt = sort_by([i | i in 1..n], AL),
145 %indices of lb in sorted order
146 array[int] of float: AL_srt = [AL[srt[i]] | i in 1..n],
147 array[int] of float: AU_srt = [ub(x[srt[i]]) | i in 1..n],
148 array[int] of float: AM_srt = AL_srt ++ [MinUB]
149 %% -- these are z-levels of extreme points
150 } in
151 forall (i in 2..n+1 where
152 AM_srt[i]<=MinUB /\ %% this is a new "start level"
153 AM_srt[i]!=AM_srt[i-1] )( %% and would produce a new cut
154 m >= AM_srt[i]
155 - sum(j in 1..i-1 where AL_srt[j]<AM_srt[i] /\ AL_srt[j]<AU_srt[j])
156 ( (AU_srt[j]-x[srt[j]]) * (AM_srt[i]-AL_srt[j]) / (AU_srt[j]-AL_srt[j]) ) :: MIP_cut
157 )
158 else true endif
159 /\
160 if card(sActive)>1 /\ fMinimumCutsXZB then
161 array_var_float_element__XBZ_lb([ -x[i] | i in sActive ], [ p[i] | i in sActive ], -m) :: MIP_cut
162 else true endif
163 endif
164 ;
165
166%-----------------------------------------------------------------------------%
167% Multiplication and division
168
169predicate int_div(var int: x, var int: y, var int: q) =
170 q == aux_int_division_modulo_fn(x,y)[1];
171
172
173predicate int_mod(var int: x, var int: y, var int: r) =
174 r == aux_int_division_modulo_fn(x,y)[2];
175
176
177function array[int] of var int: aux_int_division_modulo_fn(var int: x, var int: y) =
178 let {
179 %% Domain of q
180 set of int: dom_q =
181 if lb(y)*ub(y)>0 then
182 let {
183 set of int: EP = { ub(x) div ub(y), ub(x) div lb(y), lb(x) div ub(y), lb(x) div lb(y) },
184 } in min(EP)..max(EP)
185 else
186 let {
187 int: mm = max( abs(lb(x)), abs(ub(x)) ),
188 } in -mm..mm %% TODO case when -1 or 1 not in dom(x)
189 endif,
190 var dom_q: q;
191 int: by = max(abs(lb(y)), abs(ub(y)));
192 var -by+1..by-1: r;
193 constraint x = y * q + r,
194 constraint 0 <= x -> 0 <= r, %% which is 0 > x \/ 0 <= r
195 constraint x < 0 -> r <= 0, %% which is x >= 0 \/ r <= 0
196 % abs(r) < abs(y)
197 var 1.. max(abs(lb(y)), abs(ub(y))): w = abs(y),
198 constraint w > r /\ w > -r,
199 } in
200 [ q, r ];
201
202%% Can also have int_times(var float, var int) ......... TODO
203
204predicate int_times(var int: x, var int: y, var int: z) =
205if is_fixed(x) then
206 z==fix(x)*y %%%%% Need to use fix() otherwise added to map & nothing happens
207elseif is_fixed(y) then
208 z==x*fix(y)
209 else
210 if 0..1==dom(x) /\ 0..1==dom(y) then bool_and__INT(x,y,z)
211 elseif card(dom(x))==2 /\ card(dom(y))==2 /\ 0 in dom(x) /\ 0 in dom(y)
212 then let {
213 var 0..1: xn;
214 var 0..1: yn;
215 var 0..1: zn;
216 constraint x=xn*max(dom(x) diff {0});
217 constraint y=yn*max(dom(y) diff {0});
218 constraint z=zn*max(dom(x) diff {0})*max(dom(y) diff {0});
219 } in
220 bool_and__INT(xn,yn,zn)
221 elseif card(dom(x)) * card(dom(y)) > nMZN__UnarySizeMax_intTimes
222 \/ ( fIntTimesBool /\ (
223 %% Peter's idea for *bool. More optimal but worse values on carpet cutting.
224 (card(dom(x))==2 /\ 0 in dom(x))
225 \/ (card(dom(y))==2 /\ 0 in dom(y))
226 ) )
227 then %% PARAM
228 %% ALSO NO POINT IF <=4. TODO
229 if card(dom(x)) > card(dom(y)) \/
230 ( card(dom(x))==card(dom(y)) /\ 0 in dom(y) /\ not (0 in dom(x)) )
231 then int_times(y,x,z)
232 else
233 let {
234 set of int: s = lb(x)..ub(x),
235 set of int: r = {lb(x)*lb(y), lb(x)*ub(y), ub(x)*lb(y), ub(x)*ub(y)},
236 array[s] of var min(r)..max(r): ady = array1d(s, [ d*y | d in s ]) }
237 in
238 ady[x] = z %% use element()
239 endif
240 else
241 int_times_unary(x, { }, y, z)
242 endif
243endif;
244
245%% domx__ can be used to narrow domain... NOT IMPL.
246predicate int_times_unary(var int: x, set of int: domx__, var int: y, var int: z) =
247 let {
248 set of int: r = {lb(x)*lb(y), lb(x)*ub(y), ub(x)*lb(y), ub(x)*ub(y)},
249 %% set of int: domx = if card(domx__)>0 then domx__ else dom(x) endif,
250 array[int, int] of var int: pp=eq_encode(x, y)
251 } in
252 z>=min(r) /\ z<=max(r) /\
253 z==sum(i in index_set_1of2(pp), j in index_set_2of2(pp))
254 (i * j * pp[i, j]) /\
255 forall(i in index_set_1of2(pp), j in index_set_2of2(pp)
256 where not ((i*j) in dom(z))
257 )(pp[i, j]==0)
258 ;
259
260
261predicate int_times_unary__NOFN(var int: x, set of int: domx__, var int: y, var int: z) =
262 let {
263 set of int: r = {lb(x)*lb(y), lb(x)*ub(y), ub(x)*lb(y), ub(x)*ub(y)},
264 %% set of int: domx = if card(domx__)>0 then domx__ else dom(x) endif,
265 array[int] of var int: pX = eq_encode(x),
266 array[int] of var int: pY = eq_encode(y),
267 array[int] of int: valX = [ v | v in index_set(pX) ], %% NOT domx.
268 array[int] of int: valY = [ v | v in index_set(pY) ], %% -- according to eq_encode!
269 array[index_set(valX), index_set(valY)] of var 0..1: pp %% both dim 1..
270 } in
271 if is_fixed(x) \/ is_fixed(y) then
272 z==x*y
273 else
274 z>=min(r) /\ z<=max(r) /\
275 sum(pp)==1 /\
276 z==sum(i in index_set(valX), j in index_set(valY))
277 (valX[i] * valY[j] * pp[i, j]) /\
278 forall(i in index_set(valX))
279 ( pX[valX[i]] == sum(j in index_set(valY))( pp[i, j] ) ) /\
280 forall(j in index_set(valY))
281 ( pY[valY[j]] == sum(i in index_set(valX))( pp[i, j] ) )
282 endif;
283
284predicate float_times(var float: a, var float: b, var float: c) =
285 abort("Unable to create linear formulation for the `float_times` constraint. This model instance cannot be solved using a linear solver.");
286
287%%%Define int_pow
288predicate int_pow( var int: x, var int: y, var int: r ) =
289 let {
290 array[ int, int ] of int: x2y = array2d( lb(x)..ub(x), lb(y)..ub(y),
291 [ pow( X, Y ) | X in lb(x)..ub(x), Y in lb(y)..ub(y) ] )
292 } in
293 r == x2y[ x, y ];
294
295%%% Adding a version returning float for efficiency
296/** @group builtins.arithmetic Return \(\a x ^ {\a y}\) */
297function var float: pow_float(var int: x, var int: y) =
298 let {
299 int: yy = if is_fixed(y) then fix(y) else -1 endif;
300 } in
301 if yy = 0 then 1
302 elseif yy = 1 then x else
303 let { var float: r ::is_defined_var;
304 constraint int_pow_float(x,y,r) ::defines_var(r);
305 } in r
306 endif;
307%%%Define int_pow_float
308predicate int_pow_float( var int: x, var int: y, var float: r ) =
309 let {
310 array[ int, int ] of float: x2y = array2d( lb(x)..ub(x), lb(y)..ub(y),
311 [ pow( X, Y ) | X in lb(x)..ub(x), Y in lb(y)..ub(y) ] )
312 } in
313 r == x2y[ x, y ];
314
315
316
317%-----------------------------------------------------------------------------%
318% Array 'element' constraints
319
320predicate array_bool_element(var int: x, array[int] of bool: a, var bool: z) =
321 array_int_element(x, arrayXd(a, [bool2int(a[i]) | i in index_set(a)]), bool2int(z));
322
323predicate array_var_bool_element(var int: x, array[int] of var bool: a,
324 var bool: z) =
325 array_var_int_element(x, arrayXd(a, [bool2int(a[i]) | i in index_set(a)]), bool2int(z));
326
327predicate array_int_element(var int: x, array[int] of int: a, var int: z) =
328 let {
329 constraint x in { i | i in index_set(a) where a[i] in dom(z) },
330 } in
331 array_float_element(x, arrayXd(a, [int2float(a[i]) | i in index_set(a)]), int2float(z));
332
333predicate array_var_int_element(var int: x, array[int] of var int: a,
334 var int: z) =
335 let {
336 constraint x in { i | i in index_set(a) where 0 < card(dom(a[i]) intersect dom(z)) },
337 } in
338 %%%% Relate to the float version:
339 array_var_float_element(x, arrayXd(a, [int2float(a[i]) | i in index_set(a)]), int2float(z));
340 %%%% Simplistic version:
341 %%%% Complete binarization: MEMORY FULL. Need exact domains & sparse encoding
342
343
344predicate array_float_element(var int: i00, array[int] of float: a,
345 var float: z) =
346 let { set of int: ix = index_set(a),
347 constraint i00 in { i | i in ix where a[i]>=lb(z) /\ a[i]<=ub(z) },
348 } in %%% Finish domain before dMin/dMax
349 let {
350 float: dMin = min(i in dom(i00))(a[i]),
351 float: dMax = max(i in dom(i00))(a[i]),
352 } in
353 if dMin==dMax then
354 z==dMin
355 else
356 z >= dMin /\
357 z <= dMax /\
358 let {
359 int: nUBi00 = max(dom(i00)),
360 int: nLBi00 = min(dom(i00)),
361 float: nMinDist = min(i in nLBi00 .. nUBi00-1)(a[i+1]-a[i]),
362 float: nMaxDist = max(i in nLBi00 .. nUBi00-1)(a[i+1]-a[i]),
363 } in
364 if nMinDist == nMaxDist then %% The linear case
365 z == a[nLBi00] + nMinDist*(i00-nLBi00)
366 else
367 let {
368 array[int] of var int: p = eq_encode(i00) %% this needs i00 in ix
369 }
370 in
371 assert(dom(i00) subset index_set(p), "", true) /\
372 sum(i in dom(i00))( a[i] * int2float(p[i]) ) == z %% add more hull?
373 endif
374 endif;
375
376predicate array_var_float_element(var int: i00, array[int] of var float: a,
377 var float: z) =
378 let { set of int: ix = index_set(a),
379 constraint i00 in { i | i in ix where
380 lb(a[i])<=ub(z) /\ ub(a[i])>=lb(z)
381 },
382 } in %% finish domain first
383 let {
384 float: minLB=min(i in dom(i00))(lb(a[i])),
385 float: maxUB=max(i in dom(i00))(ub(a[i]))
386 } in
387 if minLB==maxUB then
388 z==minLB
389 else
390 z >= minLB /\
391 z <= maxUB /\
392 if {0,1}==dom(i00) /*ub(i00)-lb(i00)==1*/ /*2==card( dom( i00 ) )*/ then
393 aux_float_eq_if_1(z, a[lb(i00)], (ub(i00)-i00)) /\
394 aux_float_eq_if_1(z, a[ub(i00)], (i00-lb(i00)))
395 else
396 let {
397 array[int] of var int: p = eq_encode(i00),
398 } in
399 assert(dom(i00) subset index_set(p), "", true) /\
400 %%% The convexified bounds seem slow for ^2 and ^3 equations:
401 % sum(i in dom(i01))( lb(a[i]) * int2float(p[i]) ) <= z /\ %% convexify lower bounds
402 % sum(i in dom(i01))( ub(a[i]) * int2float(p[i]) ) >= z /\ %% convexify upper bounds
403 forall (i in dom(i00))(
404 aux_float_eq_if_1(z, a[i], p[i])
405 )
406 %% Cuts:
407 /\
408 if fElementCutsXZ then
409 array_var_float_element__ROOF([ a[i] | i in dom(i00) ], z) :: MIP_cut %% these 2 better as user cuts - too slow
410 /\ array_var_float_element__ROOF([ -a[i] | i in dom(i00) ], -z) :: MIP_cut %% or even skip them
411 else true endif
412 /\
413 if fElementCutsXZB then
414 array_var_float_element__XBZ_lb([ a[i] | i in dom(i00) ], [ p[i] | i in dom(i00) ], z) :: MIP_cut
415 /\ array_var_float_element__XBZ_lb([ -a[i] | i in dom(i00) ], [ p[i] | i in dom(i00) ], -z) :: MIP_cut
416 else true endif
417 endif
418 endif;
419
420%%% Facets on the upper surface of the z-a polytope
421%%% Possible parameter: maximal number of first cuts taken only
422predicate array_var_float_element__ROOF(array[int] of var float: a,
423 var float: z) =
424 let { set of int: ix = index_set(a),
425 int: n = length(a),
426 array[int] of float: AU = [ ub(a[i]) | i in 1..n],
427 array[int] of int: srt_ub = sort_by([i | i in 1..n], AU),
428 %indices of ub sorted up
429 array[int] of float: AU_srt_ub = [ub(a[srt_ub[i]]) | i in 1..n],
430 array[int] of float: AL_srt_ub = [lb(a[srt_ub[i]]) | i in 1..n],
431 array[int] of float: MaxLBFrom =
432 [ max(j in index_set(AL_srt_ub) where j>=i)(AL_srt_ub[j])
433 | i in 1..n ], %% direct, O(n^2)
434 array[int] of float: ULB = [
435 if 1==i then MaxLBFrom[1]
436 else max([AU_srt_ub[i-1], MaxLBFrom[i]])
437 endif | i in 1..n ]
438 } in
439 %%% "ROOF"
440 forall (i in 1..n where
441 if i==n then true else ULB[i]!=ULB[i+1] endif %% not the same base bound
442 )(
443 z <= ULB[i]
444 + sum( j in i..n where AU_srt_ub[i] != AL_srt_ub[i] ) %% not a const
445 ( (AU_srt_ub[j]-ULB[i]) * (a[srt_ub[j]]-AL_srt_ub[j]) / (AU_srt_ub[j]-AL_srt_ub[j]) ) )
446 ;
447
448predicate array_var_float_element__XBZ_lb(array[int] of var float: x, array[int] of var int: b, var float: z) =
449 if fUseXBZCutGen then
450 array_var_float_element__XBZ_lb__cutgen(x, b, z) :: MIP_cut
451 else
452 %% Adding some cuts a priori, also to make solver extract the variables
453 let {
454 int: i1 = min(index_set(x))
455 } in
456 (z <= sum(i in index_set(x))(ub(x[i]) * b[i])) %:: MIP_cut -- does not work to put them here TODO
457 /\
458 forall(i in index_set(x) intersect i1..(i1+19)) %% otherwise too many on amaze2
459 ( assert(lb(x[i]) == -ub(-x[i]) /\ ub(x[i]) == -lb(-x[i]), " negated var's bounds should swap " ) /\
460 z <= x[i] + sum(j in index_set(x) where i!=j)((ub(x[j])-lb(x[i]))*b[j])) %:: MIP_cut %% (ub_j-lb_i) * b_j
461 /\
462 forall(i in index_set(x) intersect i1..(i1+19))
463 ( z <= ub(x[i])*b[i] + sum(j in index_set(x) where i!=j)(x[j]+lb(x[j])*(b[j]-1)) ) %:: MIP_cut
464 /\
465 (z <= sum(i in index_set(x))(x[i] + lb(x[i]) * (b[i]-1))) %:: MIP_cut
466 endif;
467
468%-----------------------------------------------------------------------------%
469% Set constraints
470%% ----------------------------------------------- (NO) SETS ----------------------------------------------
471% XXX only for a fixed set here, general see below.
472% Normally not called because all plugged into the domain.
473% Might be called instead of set_in(x, var set of int s) if s gets fixed?
474predicate set_in(var int: x, set of int: s__) =
475 let {
476 set of int: s = if has_bounds(x) then s__ intersect dom(x) else s__ endif,
477 constraint min(s) <= x,
478 constraint x <= max(s),
479 } in
480 if s = min(s)..max(s) then true
481 elseif fPostprocessDomains then
482 set_in__POST(x, s)
483 else %% Update eq_encode
484 let {
485 array[int] of var int: p = eq_encode(x);
486 } in
487 forall(i in index_set(p) diff s)(p[i]==0)
488% let {
489% array[int] of int: sL = [ e | e in s where not (e - 1 in s) ];
490% array[int] of int: sR = [ e | e in s where not (e + 1 in s) ];
491% array [index_set(sR)] of var 0..1: B;
492% constraint assert(length(sR)==length(sL), "N of lb and ub of sub-intervals of a set should be equal");
493% } in
494% sum(B) = 1 %% use indicators
495% /\
496% x >= sum(i in index_set(sL))(B[i]*sL[i])
497% /\
498% x <= sum(i in index_set(sR))(B[i]*sR[i])
499 endif;
500
501%%% for a fixed set
502predicate set_in_reif(var int: x, set of int: s__, var bool: b) =
503 if is_fixed(b) then
504 if fix(b) then x in s__ else x in dom(x) diff s__ endif
505 elseif has_bounds(x) /\ not (s__ subset dom(x)) then
506 b <-> x in s__ intersect dom(x) %% Use CSE
507 else
508 let {
509 set of int: s = if has_bounds(x) then s__ intersect dom(x) else s__ endif,
510 } in
511 (
512 if dom(x) subset s then b==true
513 elseif card(dom(x) intersect s)==0 then b==false
514 elseif fPostprocessDomains then
515 set_in_reif__POST(x, s, b)
516 %% Bad. Very much so for CBC. 27.06.2019: elseif s == min(s)..max(s) then
517 %% b <-> (min(s) <= x /\ x <= max(s))
518 else
519 if card(dom(x))<=nMZN__UnaryLenMax_setInReif then %% PARAM TODO
520 let {
521 array[int] of var int: p = eq_encode(x);
522 } in
523 sum(i in s intersect dom(x))(p[i]) == bool2int(b)
524 else
525 bool2int(b) == fVarInBigSetOfInt(x, s)
526 endif
527 endif
528 )
529 endif;
530
531 % Alternative
532predicate alt_set_in_reif(var int: x, set of int: s, var bool: b) =
533 b <->
534 exists(i in 1..length([ 0 | e in s where not (e - 1 in s) ]))(
535 let { int: l = [ e | e in s where not (e - 1 in s) ][i],
536 int: r = [ e | e in s where not (e + 1 in s) ][i] }
537 in
538 l <= x /\ x <= r
539 );
540
541%%% for a fixed set
542predicate set_in_imp(var int: x, set of int: s__, var bool: b) =
543 if is_fixed(b) then
544 if fix(b) then x in s__ else true endif
545 elseif has_bounds(x) /\ not (s__ subset dom(x)) then
546 b -> x in s__ intersect dom(x) %% Use CSE
547 else
548 let {
549 set of int: s = if has_bounds(x) then s__ intersect dom(x) else s__ endif,
550 } in
551 (
552 if dom(x) subset s then true
553 elseif card(dom(x) intersect s)==0 then b==false
554 elseif s == min(s)..max(s) then
555 (b -> min(s) <= x) /\ (b -> x <= max(s))
556 else
557 if card(dom(x))<=nMZN__UnaryLenMax_setInReif then %% PARAM TODO
558 let {
559 array[int] of var int: p = eq_encode(x);
560 } in
561 sum(i in s intersect dom(x))(p[i]) >= bool2int(b)
562 else
563 bool2int(b) <= fVarInBigSetOfInt(x, s)
564 endif
565 endif
566 )
567 endif;
568
569function var 0..1: fVarInBigSetOfInt(var int: x, set of int: s)
570 = let {
571 array[int] of int: sL = [ e | e in s where not (e - 1 in s) ];
572 array[int] of int: sR = [ e | e in s where not (e + 1 in s) ];
573 constraint assert(length(sR)==length(sL), "N of lb and ub of sub-intervals of a set should be equal");
574 } in
575 sum(i in index_set(sL)) (bool2int(x>=sL[i] /\ x<=sR[i])); %% use indicators
576
577%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% OTHER SET STUFF COMING FROM nosets.mzn %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
578%-----------------------------------------------------------------------------%
579%-----------------------------------------------------------------------------%
580
581annotation bool_search(array[$X] of var bool: x, ann:a1, ann:a2, ann:a3) =
582 let { array[int] of var bool: xx = array1d(x) } in
583 int_search([bool2int(xx[i]) | i in index_set(xx)],a1,a2,a3);
584
585annotation warm_start( array[int] of var bool: x, array[int] of bool: v ) =
586 warm_start( [ bool2int(x[i]) | i in index_set(x) ], [ bool2int(v[i]) | i in index_set(v) ] );
587
588
589%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% DOMAIN POSTPROCESSING BUILT-INS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
590 % Single variable: x = d <-> x_eq_d[d]
591predicate equality_encoding__POST(var int: x, array[int] of var int: x_eq_d);
592
593%%%%%%% var int: b: bool2int is a reverse_map, not passed to .fzn
594predicate set_in__POST(var int: x, set of int: s__);
595predicate set_in_reif__POST(var int: x, set of int: s__, var int: b);
596
597
598
599
600%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LOGICAL CONSTRAINTS TO THE SOLVER %%%%%%%%%%%%%%%%%%%%%%%%%%
601%%%%%%% var int: b: bool2int is a reverse_map, not passed to .fzn => REPEAT TESTS. TODO
602predicate int_lin_eq_reif__IND(array[int] of int: c, array[int] of var int: x, int: d, var int: b);
603predicate int_lin_le_reif__IND(array[int] of int: c, array[int] of var int: x, int: d, var int: b);
604predicate int_lin_ne__IND(array[int] of int: c, array[int] of var int: x, int: d);
605predicate aux_int_le_zero_if_0__IND(var int: x, var int: b);
606predicate float_lin_le_reif__IND(array[int] of float: c, array[int] of var float: x, float: d, var int: b);
607predicate aux_float_eq_if_1__IND(var float: x, var float: y, var int: b);
608predicate aux_float_le_zero_if_0__IND(var float: x, var int: b);
609
610predicate array_int_minimum__IND(var int: m, array[int] of var int: x);
611predicate array_int_maximum__IND(var int: m, array[int] of var int: x);
612predicate array_float_minimum__IND(var float: m, array[int] of var float: x);
613predicate array_float_maximum__IND(var float: m, array[int] of var float: x);
614
615%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% XBZ cut generator, currently CPLEX only %%%%%%%%%%%%%%%%%%%%%%%%%%
616predicate array_var_float_element__XBZ_lb__cutgen(array[int] of var float: x, array[int] of var int: b, var float: z);
617