this repo has no description
dekker.one
1%-----------------------------------------------------------------------------%
2% MiniZinc standard library.
3%-----------------------------------------------------------------------------%
4% This file contains declarations of all functions, predicates and annotations
5% available in the base MiniZinc language.
6
7/***
8 @groupdef MAIN The MiniZinc library
9*/
10
11/***
12 @groupdef annotations Annotations
13
14 These annotations control evaluation and solving behaviour.
15*/
16
17
18/***
19 @groupdef annotations.general General annotations
20*/
21
22/** @group annotations.general Declare function as total, i.e. it does not put
23 any constraints on its arguments. */
24annotation promise_total;
25
26/** @group annotations.export Always export function to intermediate representation to ensure
27 availability for later use. */
28annotation export;
29
30/** @group annotations.general Declare that expression may have undefined result (to avoid warnings) */
31annotation maybe_partial;
32
33/** @group annotations.general Declare that the annotated variable should be added to the output
34of the model. This annotation only has an effect when the model does not have an output item. */
35annotation add_to_output;
36
37/** @group annotations.general Declare that the annotated variable should be only used for output.
38 This annotation can be used to define variables that are required for solution checkers, or
39 that are necessary for the output item. The annotated variable must be par.
40 */
41annotation output_only;
42
43/** @group annotations.general Declare that the annotated variable is required for checking solutions. */
44annotation mzn_check_var;
45
46/** @group annotations.general Declare that the annotated variable is required for checking solutions and has an enum type. */
47annotation mzn_check_enum_var(set of int);
48
49/** @group annotations.general Declare a name for the annotated expression. */
50annotation mzn_expression_name(string);
51
52/** @group annotations.general Declare a name for the annotated constraint. */
53annotation mzn_constraint_name(string);
54
55
56/** @group annotations.general Declare the annotated variable as being functionally defined.
57 This annotation is introduced into FlatZinc code by the compiler. */
58annotation is_defined_var;
59/** @group annotations.general Declare a variable as being introduced by the compiler. */
60annotation var_is_introduced;
61/** @group annotations.general Declare variable: \a c as being functionally defined
62 by the annotated constraint. This annotation is introduced into FlatZinc code by the compiler. */
63annotation defines_var(var $t: c);
64/** @group annotations.general Declare that the annotated array should be printed by
65 the solver with the given index sets \a a. This annotation is introduced into FlatZinc code by
66 the compiler. */
67annotation output_array(array[$u] of set of int:a);
68/** @group annotations.general Declare that the annotated variable should be printed by
69 the solver. This annotation is introduced into FlatZinc code by
70 the compiler. */
71annotation output_var;
72/** @group annotations.general Declare that the annotated expression is used to map
73 an expression back from FlatZinc to MiniZinc. */
74annotation is_reverse_map;
75/** @group annotations.general Document the function or variable declaration item with
76 the string \a s. */
77annotation doc_comment(string: s);
78/** @group annotations.general Representation of the call-stack when the annotated item
79 was introduced, as a string \a s. Can be used to uniquely identify variables and constraints across different
80 compilations of a model that may have different names. This annotations is introduced into
81 FlatZinc code by the compiler and is retained if --keep-paths argument is used. */
82annotation mzn_path(string: s);
83/** @group annotations.general With debug build of mzn2fzn, call MiniZinc::mzn_break_here when
84 flattening this expression to make debugging easier. This annotation is ignored by the
85 release build.*/
86annotation mzn_break_here;
87/** @group annotations.general Used to attach a name \a s to an expression, this should also propagate to
88 any sub-expressions or decomposition of the annotated expression. String annotations on expressions
89 are re-written as expression_name annotations */
90annotation expression_name(string: s);
91/** @group annotations.general Used to attach a name \a s to a constraint and its decomposition. String
92 annotations on constraint keywords are re-written as constraint_name annotations */
93annotation constraint_name(string: s);
94
95/** @group annotations.general Used internally by the compiler */
96annotation mzn_rhs_from_assignment;
97
98/** @group annotations.general Marks a constraint as a recorded domain changing constraint (when mzn2fzn
99 called with -g flag */
100annotation domain_change_constraint;
101
102/***
103 @groupdef annotations.prop Propagation strength annotations
104*/
105
106/** @group annotations.prop Annotate a constraint to use domain propagation */
107annotation domain;
108/** @group annotations.prop Annotate a constraint to use bounds propagation */
109annotation bounds;
110
111
112/***
113 @groupdef annotations.search Search annotations
114*/
115
116/** @group annotations.search Sequentially perform the searches specified in array \a s */
117annotation seq_search(array[int] of ann: s);
118
119/** @group annotations.search Specify search on variables \a x, with variable selection
120 strategy \a select, value choice strategy \a choice, and exploration strategy
121 \a explore. If \a x is a multi-dimensional array, it is coerced to one-dimensional
122 in row-major order (as with the array1d function).
123*/
124annotation int_search(
125 array[$X] of var int: x,
126 ann: select,
127 ann: choice,
128 ann: explore,
129);
130
131/** @group annotations.search Specify search on variables \a x, with variable selection
132 strategy \a select, and value choice strategy \a choice.
133 If \a x is a multi-dimensional array, it is coerced to one-dimensional
134 in row-major order (as with the array1d function).
135*/
136annotation int_search(
137 array[$X] of var int: x,
138 ann: select,
139 ann: choice
140) = int_search(x,select,choice,complete);
141
142/** @group annotations.search Specify search on variables \a x, with variable selection
143 strategy \a select, value choice strategy \a choice, and exploration strategy
144 \a explore.
145 If \a x is a multi-dimensional array, it is coerced to one-dimensional
146 in row-major order (as with the array1d function).
147*/
148annotation bool_search(
149 array[$X] of var bool: x,
150 ann: select,
151 ann: choice,
152 ann: explore
153);
154
155/** @group annotations.search Specify search on variables \a x, with variable selection
156 strategy \a select, and value choice strategy \a choice.
157 If \a x is a multi-dimensional array, it is coerced to one-dimensional
158 in row-major order (as with the array1d function).
159*/
160annotation bool_search(
161 array[$X] of var bool: x,
162 ann: select,
163 ann: choice
164) = bool_search(x,select,choice,complete);
165
166/** @group annotations.search Specify search on variables \a x,
167 with precision \a prec, variable selection
168 strategy \a select, value choice strategy \a choice, and exploration strategy
169 \a explore.
170 If \a x is a multi-dimensional array, it is coerced to one-dimensional
171 in row-major order (as with the array1d function).
172*/
173annotation float_search(
174 array[$X] of var float: x,
175 float: prec,
176 ann: select,
177 ann: choice,
178 ann: explore
179);
180
181/** @group annotations.search Specify search on variables \a x,
182 with precision \a prec, variable selection
183 strategy \a select, and value choice strategy \a choice.
184 If \a x is a multi-dimensional array, it is coerced to one-dimensional
185 in row-major order (as with the array1d function).
186*/
187annotation float_search(
188 array[$X] of var float: x,
189 float: prec,
190 ann: select,
191 ann: choice
192) = float_search(x,prec,select,choice,complete);
193
194/** @group annotations.search Specify search on variables \a x, with variable selection
195 strategy \a select, value choice strategy \a choice, and exploration strategy
196 \a explore.
197 If \a x is a multi-dimensional array, it is coerced to one-dimensional
198 in row-major order (as with the array1d function).
199*/
200annotation set_search(
201 array[$X] of var set of int: x,
202 ann: select,
203 ann: choice,
204 ann: explore
205);
206
207/** @group annotations.search Specify search on variables \a x, with variable selection
208 strategy \a select, and value choice strategy \a choice.
209 If \a x is a multi-dimensional array, it is coerced to one-dimensional
210 in row-major order (as with the array1d function).
211*/
212annotation set_search(
213 array[$X] of var set of int: x,
214 ann: select,
215 ann: choice
216) = set_search(x,select,choice,complete);
217
218/***
219 @groupdef annotations.search.varsel Variable selection annotations
220*/
221
222/** @group annotations.search.varsel Search variables in the given order */
223annotation input_order;
224/** @group annotations.search.varsel Choose the variable with the smallest domain */
225annotation first_fail;
226/** @group annotations.search.varsel Choose the variable with the largest domain */
227annotation anti_first_fail;
228/** @group annotations.search.varsel Choose the variable with the smallest value in its domain */
229annotation smallest;
230/** @group annotations.search.varsel Choose the variable with the largest value in its domain */
231annotation largest;
232/** @group annotations.search.varsel Choose the variable with the largest number of attached constraints */
233annotation occurrence;
234/** @group annotations.search.varsel Choose the variable with the smallest domain,
235 breaking ties using the number of attached constraints */
236annotation most_constrained;
237/** @group annotations.search.varsel Choose the variable with largest difference
238 between the two smallest values in its domain */
239annotation max_regret;
240/** @group annotations.search.varsel Choose the variable with largest domain, divided
241 by the number of attached constraints weighted by how often they have caused failure */
242annotation dom_w_deg;
243/** @group annotations.search.varsel Choose the variable with the highest impact so
244 far during the search */
245annotation impact;
246
247/***
248 @groupdef annotations.search.choice Value choice annotations
249*/
250
251/** @group annotations.search.choice Assign values in ascending order */
252annotation indomain;
253/** @group annotations.search.choice Assign the smallest value in the domain */
254annotation indomain_min;
255/** @group annotations.search.choice Assign the largest value in the domain */
256annotation indomain_max;
257/** @group annotations.search.choice Assign the value in the domain closest to
258 the mean of its current bounds */
259annotation indomain_middle;
260/** @group annotations.search.choice Assign the middle value in the domain */
261annotation indomain_median;
262/** @group annotations.search.choice Assign a random value from the domain */
263annotation indomain_random;
264/** @group annotations.search.choice Bisect the domain, excluding the upper half first */
265annotation indomain_split;
266/** @group annotations.search.choice Bisect the domain, randomly selecting which half to exclude first */
267annotation indomain_split_random;
268/** @group annotations.search.choice Bisect the domain, excluding the lower half first */
269annotation indomain_reverse_split;
270/** @group annotations.search.choice
271 If the domain consists of several contiguous intervals, reduce the
272 domain to the first interval. Otherwise bisect the domain.
273 */
274annotation indomain_interval;
275/** @group annotations.search.choice Exclude the smallest value from the domain */
276annotation outdomain_min;
277/** @group annotations.search.choice Exclude the largest value from the domain */
278annotation outdomain_max;
279/** @group annotations.search.choice Exclude the middle value from the domain */
280annotation outdomain_median;
281/** @group annotations.search.choice Exclude a random value from the domain */
282annotation outdomain_random;
283
284/***
285 @groupdef annotations.search.explore Exploration strategy annotations
286*/
287
288/** @group annotations.search.explore Perform a complete search */
289annotation complete;
290
291/***
292 @groupdef annotations.search.restart Restart annotations
293*/
294
295/** @group annotations.search.restart Restart with Luby sequence scaled by \a scale */
296annotation restart_luby(int: scale);
297/** @group annotations.search.restart Restart with geometric sequence with parameters \a base and \a scale */
298annotation restart_geometric(float: base, int: scale);
299/** @group annotations.search.restart Restart with linear sequence scaled by \a scale */
300annotation restart_linear(int: scale);
301/** @group annotations.search.restart Restart after constant number of nodes \a scale */
302annotation restart_constant(int: scale);
303/** @group annotations.search.restart Do not restart */
304annotation restart_none;
305
306/***
307 @groupdef annotations.warmstart Warm start annotations
308
309 To be put on the solve item, similar to search annotations.
310 A variable can be mentioned several times and in different
311 annotations but only one of the values is taken
312*/
313
314/** @group annotations.warmstart Specify an array \a w of warm_start annotations
315 or other warm_start_array annotations. Can be useful to keep the annotation
316 order in FlatZinc for manual updating.
317
318 Note: if you have search annotations as well, put warm_starts into seq_search
319 in order to have precedence between both, which may matter.
320*/
321annotation warm_start_array( array[int] of ann: w );
322
323/** @group annotations.warmstart Specify warm start values \a v for an array of booleans \a x */
324annotation warm_start( array[int] of var bool: x, array[int] of bool: v );
325/** @group annotations.warmstart Specify warm start values \a v for an array of integers \a x */
326annotation warm_start( array[int] of var int: x, array[int] of int: v );
327/** @group annotations.warmstart Specify warm start values \a v for an array of floats \a x */
328annotation warm_start( array[int] of var float: x, array[int] of float: v );
329/** @group annotations.warmstart Specify warm start values \a v for an array of sets \a x */
330annotation warm_start( array[int] of var set of int: x, array[int] of set of int: v );
331
332
333/***
334 @groupdef annotations.warmstart.optvals Warm start annotations with optional values
335
336 The value arrays can contain <> elements (absent values).
337 The following decompositions eliminate those elements
338 because FlatZinc 1.6 does not support optionals.
339*/
340
341/** @group annotations.warmstart.optvals Specify warm start values \a v for an array of booleans \a x */
342annotation warm_start( array[int] of var bool: x, array[int] of opt bool: v ) =
343 if 0==length(x) \/ 0==length(v) then
344 warm_start( x, [] )
345 else
346 warm_start( [ x[i] | i in index_set(x) where
347 i-min(index_set(x))+min(index_set(v))>length(v) \/
348 occurs( v[ i-min(index_set(x))+min(index_set(v)) ] ) ],
349 [ deopt(v[i]) | i in index_set(v) where occurs(v[i]) ] )
350 endif;
351/** @group annotations.warmstart.optvals Specify warm start values \a v for an array of integers \a x */
352annotation warm_start( array[int] of var int: x, array[int] of opt int: v ) =
353 if 0==length(x) \/ 0==length(v) then
354 warm_start( x, [] )
355 else
356 warm_start( [ x[i] | i in index_set(x) where
357 i-min(index_set(x))+min(index_set(v))>length(v) \/
358 occurs( v[ i-min(index_set(x))+min(index_set(v)) ] ) ],
359 [ deopt(v[i]) | i in index_set(v) where occurs(v[i]) ] )
360 endif;
361/** @group annotations.warmstart.optvals Specify warm start values \a v for an array of floats \a x */
362annotation warm_start( array[int] of var float: x, array[int] of opt float: v ) =
363 if 0==length(x) \/ 0==length(v) then
364 warm_start( x, [] )
365 else
366 warm_start( [ x[i] | i in index_set(x) where
367 i-min(index_set(x))+min(index_set(v))>length(v) \/
368 occurs( v[ i-min(index_set(x))+min(index_set(v)) ] ) ],
369 [ deopt(v[i]) | i in index_set(v) where occurs(v[i]) ] )
370 endif;
371/** @group annotations.warmstart.optvals Specify warm start values \a v for an array of sets \a x */
372annotation warm_start( array[int] of var set of int: x, array[int] of opt set of int: v ) =
373 if 0==length(x) \/ 0==length(v) then
374 warm_start( x, [] )
375 else
376 warm_start( [ x[i] | i in index_set(x) where
377 i-min(index_set(x))+min(index_set(v))>length(v) \/
378 occurs( v[ i-min(index_set(x))+min(index_set(v)) ] ) ],
379 [ deopt(v[i]) | i in index_set(v) where occurs(v[i]) ] )
380 endif;
381
382
383
384/***
385 @groupdef optiontypes Option type support
386
387 These functions and predicates implement the standard library for working
388 with option types. Note that option type support is still incomplete.
389*/
390
391/** @group optiontypes Return value of \a x if \a x is not absent. Aborts
392 when evaluated on absent value. */
393function $T: deopt(opt $T: x);
394
395/** @group optiontypes Return value \a x unchanged (since \a x is guaranteed
396 to be non-optional). */
397function var $T: deopt(var $T: x) = x;
398
399/** @group optiontypes Test if \a x is not absent (always returns true) */
400test occurs(var $T: x) = true;
401/** @group optiontypes Test if \a x is not absent */
402test occurs(opt $T: x);
403/** @group optiontypes Test if \a x is absent (always returns false) */
404test absent(var $T: x) = false;
405/** @group optiontypes Test if \a x is absent */
406test absent(opt $T: x) = not occurs(x);
407
408/***
409 @groupdef optiontypes.bool Option type support for Booleans
410*/
411
412/** @group optiontypes.bool True iff \a x is not absent */
413function var bool : occurs(var opt bool: x) ::promise_total =
414 let {
415 var bool : b = occurs_internal(x);
416 var bool : dx = deopt_internal(x);
417 constraint (x = reverse_map(b,dx)) :: is_reverse_map;
418 } in b;
419
420/** @group optiontypes.bool Return value of \a x (assumes that \a x is not absent) */
421function var bool : deopt(var opt bool : x) ::promise_total =
422 let {
423 var bool : b = occurs_internal(x);
424 var bool : dx = deopt_internal(x);
425 constraint (x = reverse_map(b,dx)) :: is_reverse_map;
426 } in dx;
427
428/** @group optiontypes.bool True iff \a x is absent */
429predicate absent(var opt bool: x) = not occurs(x);
430
431function var bool: occurs_internal(var opt bool: x) ::promise_total =
432 let { var bool : b; } in b;
433function var bool : deopt_internal(var opt bool : x) ::promise_total =
434 let { var bool: y } in y;
435
436function var opt bool: reverse_map(var bool: occ, var bool: d);
437function opt bool: reverse_map(bool: occ, bool: d) ::promise_total =
438 if occ then d else <> endif;
439
440predicate bool_opt_eq(var opt bool: x, var opt bool: y) =
441 deopt(x)=deopt(y) /\ occurs(x)=occurs(y);
442
443/** @group optiontypes.bool True iff both \a b0 and \a b1 are absent or
444 both are present and have the same value. */
445predicate bool_eq(var opt bool: b0, var opt bool: b1) =
446 (absent(b0) /\ absent(b1))
447 \/ (occurs(b0) /\ occurs(b1) /\ deopt(b0)=deopt(b1));
448
449/** @group optiontypes.bool True iff \a b0 occurs and is equal to \a b1 */
450predicate bool_eq(var opt bool: b0, var bool: b1) =
451 occurs(b0) /\ deopt(b0)=b1;
452
453 /** @group optiontypes.bool True iff \a b1 occurs and is equal to \a b0 */
454predicate bool_eq(var bool: b0, var opt bool: b1) =
455 occurs(b1) /\ deopt(b1)=b0;
456
457/** @group optiontypes.bool True iff for any \p i, \a x[i] is absent or true */
458predicate forall (array[int] of var opt bool: x) =
459 forall ([absent(x[i]) \/ deopt(x[i]) | i in index_set(x)]);
460
461/** @group optiontypes.bool True iff for at least one \p i, \a x[i] occurs and is true */
462predicate exists (array[int] of var opt bool: x) =
463 exists ([occurs(x[i]) /\ deopt(x[i]) | i in index_set(x)]);
464
465% /** @group optiontypes.bool True iff \a x is absent or false */
466% function var bool: 'not'(var opt bool: x) = absent(x) \/ not deopt(x);
467
468% /** @group optiontypes.bool Return absent if \a idx is absent, otherwise return \a x[\a idx] */
469% function var opt bool: element(var opt int: idx, array[int] of var bool: x) =
470% if absent(idx) then <> else element(deopt(idx),x) endif;
471
472% /** @group optiontypes.bool Return absent if \a idx1 or \a idx2 is absent, otherwise return \a x[\a idx1, \a idx2] */
473% function var opt bool: element(var opt int: idx1, var opt int: idx2, array[int,int] of var bool: x) =
474% if absent(idx1) \/ absent(idx2) then <> else element(deopt(idx1),deopt(idx2),x) endif;
475
476% /** @group optiontypes.bool Return \a x[\a idx] */
477% function var opt bool: element(var int: idx, array[int] of var opt bool: x) =
478% let {
479% var opt bool: r;
480% constraint occurs(r) = element(idx,array1d(index_set(x),[occurs(x[i]) | i in index_set(x)]));
481% constraint deopt(r) = element(idx,array1d(index_set(x),[deopt(x[i]) | i in index_set(x)]));
482% } in r;
483
484% /** @group optiontypes.bool Return \a x[\a idx1, \a idx2] */
485% function var opt bool: element(var int: idx1, var int: idx2, array[int,int] of var opt bool: x) =
486% let {
487% var opt bool: r;
488% constraint occurs(r) = element(idx1,idx2,
489% array2d(index_set_1of2(x),index_set_2of2(x),[occurs(x[i,j]) | i in index_set_1of2(x), j in index_set_2of2(x)]));
490% constraint deopt(r) = element(idx1,idx2,
491% array2d(index_set_1of2(x),index_set_2of2(x),[deopt(x[i,j]) | i in index_set_1of2(x), j in index_set_2of2(x)]));
492% } in r;
493
494% /** @group optiontypes.bool Return absent if \a idx is absent, otherwise return \a x[\a idx] */
495% function var opt bool: element(var opt int: idx, array[int] of var opt bool: x) =
496% if absent(idx) then <> else element(deopt(idx),x) endif;
497
498% /** @group optiontypes.bool Return absent if \a idx1 or \a idx2 is absent, otherwise return \a x[\a idx1, \a idx2] */
499% function var opt bool: element(var opt int: idx1, var opt int: idx2, array[int,int] of var opt bool: x) =
500% if absent(idx1) \/ absent(idx2) then <> else element(deopt(idx1),deopt(idx2),x) endif;
501
502
503
504/***
505 @groupdef optiontypes.int Option type support for integers
506*/
507
508/** @group optiontypes.int True iff \a x is not absent */
509function var bool : occurs(var opt int : x) ::promise_total =
510 let {
511 var bool : b = occurs_internal(x);
512 var int : dx = deopt_internal(x);
513 constraint (x = reverse_map(b,dx)) :: is_reverse_map;
514 } in b;
515
516/** @group optiontypes.bool Return value of \a x (assumes that \a x is not absent) */
517function var int : deopt(var opt int : x) ::promise_total =
518 let {
519 var bool : b = occurs_internal(x);
520 var int : dx = deopt_internal(x);
521 constraint (x = reverse_map(b,dx)) :: is_reverse_map;
522 } in dx;
523
524/** @group optiontypes.bool True iff \a x is absent */
525function var bool: absent(var opt int: x) ::promise_total = not occurs(x);
526
527function var bool: occurs_internal(var opt int: x) ::promise_total =
528 let { var bool : b; } in b;
529function var int : deopt_internal(var opt int : x) ::promise_total =
530 let { var lb(x)..ub(x): y } in y;
531
532function var opt int: reverse_map(var bool: occ, var int: d);
533function opt int: reverse_map(bool: occ, int: d) ::promise_total =
534 if occ then d else <> endif;
535
536predicate var_dom(var opt int:x, set of int: s) =
537 let {
538 var int: dx = deopt(x);
539 set of int: new_dom = dom(dx) intersect s;
540 } in if new_dom = {} then absent(x) else dx in new_dom endif;
541
542predicate var_dom(array[$T] of var opt int: x, set of int: d) =
543 let { array[int] of var opt int: xx = array1d(x) }
544 in forall (i in index_set(xx)) (var_dom(xx[i],d));
545
546predicate int_opt_eq(var opt int: x, var opt int: y) =
547 deopt(x) = deopt(y) /\ occurs(x) = occurs(y);
548
549/** @group optiontypes.bool Search annotation for optional Boolean variables */
550annotation bool_search(array[int] of var opt bool: x, ann: a1, ann: a2, ann: a3) =
551 bool_search([if occurs(x[i]) then deopt(x[i]) else false endif | i in index_set(x)],a1,a2,a3);
552
553/** @group optiontypes.bool Search annotation for optional Boolean variables */
554annotation bool_search(array[int] of var opt bool: x, ann: a1, ann: a2) =
555 bool_search([if occurs(x[i]) then deopt(x[i]) else false endif | i in index_set(x)],a1,a2);
556
557/** @group optiontypes.int Weak comparison: true iff either \a x or \a y is absent, or both
558 occur and the value of \a x is greater than the value of \a y. */
559function var bool: '>'(var opt int: x, var opt int: y) = absent(x) \/ absent(y) \/ deopt(x) > deopt(y);
560/** @group optiontypes.int Weak comparison: true iff either \a x or \a y is absent, or both
561 occur and the value of \a x is greater than or equal to the value of \a y. */
562function var bool: '>='(var opt int: x, var opt int: y) = absent(x) \/ absent(y) \/ deopt(x) >= deopt(y);
563% /** @group optiontypes.int Weak comparison: true iff either \a x or \a y is absent, or both
564% occur and the value of \a x is less than the value of \a y. */
565% function var bool: '<'(var opt int: x, var opt int: y) = absent(x) \/ absent(y) \/ deopt(x) < deopt(y);
566% /** @group optiontypes.int Weak comparison: true iff either \a x or \a y is absent, or both
567% occur and the value of \a x is less than or equal to the value of \a y. */
568% function var bool: '<='(var opt int: x, var opt int: y) = absent(x) \/ absent(y) \/ deopt(x) <= deopt(y);
569
570/** @group optiontypes.int Weak comparison: true iff either \a x or \a y is absent, or both
571 occur and the value of \a x is greater than the value of \a y. */
572function bool: '>'(opt int: x, opt int: y) = absent(x) \/ absent(y) \/ deopt(x) > deopt(y);
573/** @group optiontypes.int Weak comparison: true iff either \a x or \a y is absent, or both
574 occur and the value of \a x is greater than or equal to the value of \a y. */
575function bool: '>='(opt int: x, opt int: y) = absent(x) \/ absent(y) \/ deopt(x) >= deopt(y);
576% /** @group optiontypes.int Weak comparison: true iff either \a x or \a y is absent, or both
577% occur and the value of \a x is less than the value of \a y. */
578% function bool: '<'(opt int: x, opt int: y) = absent(x) \/ absent(y) \/ deopt(x) < deopt(y);
579% /** @group optiontypes.int Weak comparison: true iff either \a x or \a y is absent, or both
580% occur and the value of \a x is less than or equal to the value of \a y. */
581% function bool: '<='(opt int: x, opt int: y) = absent(x) \/ absent(y) \/ deopt(x) <= deopt(y);
582
583% /** @group optiontypes.int Return minimum of elements in \a x that are not absent, or
584% absent if all elements in \a x are absent. */
585/*
586function var opt int: min(array[int] of var opt int: x) ::promise_total =
587 let {
588 var opt lb_array(x)..ub_array(x): m;
589 var lb_array(x)..ub_array(x): xmax;
590 constraint if ub(xmax) != infinity then xmax = ub(xmax) else forall (i in index_set(x)) (xmax >= deopt(x[i])) endif;
591 constraint occurs(m) <-> exists (i in index_set(x)) (occurs(x[i]));
592 constraint occurs(m) ->
593 deopt(m) = min([if occurs(xi) then deopt(xi) else xmax endif | xi in x]);
594 } in m;
595*/
596
597% /** @group optiontypes.int Return maximum of elements in \a x that are not absent, or
598% absent if all elements in \a x are absent.
599/*
600function var opt int: max(array[int] of var opt int: x) ::promise_total =
601 let {
602 var opt lb_array(x)..ub_array(x): m;
603 var lb_array(x)..ub_array(x): xmin;
604 constraint if lb(xmin) != -infinity then xmin = lb(xmin) else forall (i in index_set(x)) (xmin <= deopt(x[i])) endif;
605 constraint occurs(m) <-> exists (i in index_set(x)) (occurs(x[i]));
606 constraint occurs(m) ->
607 deopt(m) = max([if occurs(xi) then deopt(xi) else xmin endif | xi in x]);
608 } in m;
609*/
610
611/** @group optiontypes.int Weak addition. Return sum of \a x and \a y if both
612are present, otherwise return absent. */
613function var opt int: '~+'(var opt int: x, var opt int: y) ::promise_total =
614 let {
615 int: l = if lb(x)=-infinity \/ lb(y)=-infinity then -infinity else lb(x)+lb(y) endif;
616 int: u = if ub(x)=infinity \/ ub(y)=infinity then infinity else ub(x)+ub(y) endif;
617 var opt l..u: result;
618 constraint absent(x) \/ absent(y) -> result = <>;
619 constraint absent(x) \/ absent(y) \/ result = deopt(x)+deopt(y);
620 } in result;
621
622/** @group optiontypes.int Weak subtraction. Return difference of \a x and \a y if both
623are present, otherwise return absent. */
624function var opt int: '~-'(var opt int: x, var opt int: y) ::promise_total =
625 let {
626 int: l = if lb(x)=-infinity \/ ub(y)=infinity then -infinity else lb(x)-ub(y) endif;
627 int: u = if ub(x)=infinity \/ lb(y)=-infinity then infinity else ub(x)-lb(y) endif;
628 var opt l..u: result;
629 constraint absent(x) \/ absent(y) -> result = <>;
630 constraint absent(x) \/ absent(y) \/ result = deopt(x)-deopt(y);
631 } in result;
632
633/** @group optiontypes.int Weak multiplication. Return product of \a x and \a y if both
634are present, otherwise return absent. */
635function var opt int: '~*'(var opt int: x, var opt int: y) ::promise_total =
636 if absent(x) \/ absent(y) then <>
637 else deopt(x)*deopt(y) endif;
638
639/** @group optiontypes.int Weak equality. True if either \a x or \a y are absent, or
640present and equal.*/
641function var bool: '~='(var opt int: x, var opt int: y) ::promise_total =
642 absent(x) \/ absent(y) \/ deopt(x)=deopt(y);
643
644/** @group optiontypes.int Return optional 0/1 integer that is absent iff \a x
645 is absent, and 1 iff \a x occurs and is true. */
646function var opt int: bool2int(var opt bool: x) ::promise_total =
647 let {
648 var opt 0..1: xi;
649 constraint absent(xi)=absent(x);
650 constraint deopt(xi)=bool2int(deopt(x));
651 } in xi;
652
653/** @group optiontypes.int True iff both \a x and \a y are absent or
654 both are present and have the same value. */
655predicate int_eq(var opt int: x, var opt int: y) =
656 (absent(x) /\ absent(y))
657 \/ (occurs(x) /\ occurs(y) /\ (deopt(x)=deopt(y))::maybe_partial);
658
659/** @group optiontypes.int True iff only one of \a x and \a y is absent or
660 both are present and have different values. */
661predicate int_ne(var opt int : x, var opt int : y) =
662 (absent(x) != absent(y))
663 \/ (occurs(x) /\ occurs(y) /\ (deopt(x)!=deopt(y))::maybe_partial);
664
665% /** @group optiontypes.int Optional addition. Return sum of \a x and \a y, with absent replaced by 0. */
666% function var int: '+'(var opt int: x, var opt int: y) ::promise_total =
667% if occurs(x) then deopt(x) else 0 endif + if occurs(y) then deopt(y) else 0 endif;
668
669% /** @group optiontypes.int Optional addition. Return sum of \a x and \a y, with absent replaced by 0. */
670% function int: '+'(opt int: x, opt int: y) ::promise_total =
671% if occurs(x) then deopt(x) else 0 endif + if occurs(y) then deopt(y) else 0 endif;
672
673% /** @group optiontypes.int Optional subtraction. Return difference of \a x and \a y, with absent replaced by 0. */
674% function var int: '-'(var opt int: x, var opt int: y) ::promise_total =
675% if occurs(x) then deopt(x) else 0 endif - if occurs(y) then deopt(y) else 0 endif;
676
677% /** @group optiontypes.int Optional subtraction. Return difference of \a x and \a y, with absent replaced by 0. */
678% function int: '-'(opt int: x, opt int: y) ::promise_total =
679% if occurs(x) then deopt(x) else 0 endif - if occurs(y) then deopt(y) else 0 endif;
680
681% /** @group optiontypes.int Optional multiplication. Return product of \a x and \a y, with absent replaced by 1. */
682% function var int: '*'(var opt int: x, var opt int: y) ::promise_total =
683% if occurs(x) then deopt(x) else 1 endif * if occurs(y) then deopt(y) else 1 endif;
684
685% /** @group optiontypes.int Optional multiplication. Return product of \a x and \a y, with absent replaced by 1. */
686% function int: '*'(opt int: x, opt int: y) ::promise_total =
687% if occurs(x) then deopt(x) else 1 endif * if occurs(y) then deopt(y) else 1 endif;
688
689% /** @group optiontypes.int Optional division. Return \a x div \a y, with absent replaced by 1. */
690% function var int: 'div'(var opt int: x, var opt int: y) ::promise_total =
691% if occurs(x) then deopt(x) else 1 endif div if occurs(y) then deopt(y) else 1 endif;
692
693% /** @group optiontypes.int Optional division. Return \a x div \a y, with absent replaced by 1. */
694% function int: 'div'(opt int: x, opt int: y) ::promise_total =
695% if occurs(x) then deopt(x) else 1 endif div if occurs(y) then deopt(y) else 1 endif;
696
697/** @group optiontypes.int Optional modulo. Return \a x mod \a y, with absent replaced by 1. */
698function var int: 'mod'(var opt int: x, var opt int: y) ::promise_total =
699 if occurs(x) then deopt(x) else 1 endif mod if occurs(y) then deopt(y) else 1 endif;
700
701/** @group optiontypes.int Optional modulo. Return \a x mod \a y, with absent replaced by 1. */
702function int: 'mod'(opt int: x, opt int: y) ::promise_total =
703 if occurs(x) then deopt(x) else 1 endif mod if occurs(y) then deopt(y) else 1 endif;
704
705/** @group optiontypes.int Return sum of non-absent elements of \a x. */
706function var int: sum(array[int] of var opt int: x) =
707 sum (i in index_set(x)) (let { var int: dx = deopt(x[i]) } in if occurs(x[i]) then dx else 0 endif);
708
709/** @group optiontypes.int Return sum of non-absent elements of \a x. */
710function int: sum(array[int] of opt int: x) =
711 sum (i in index_set(x)) (if occurs(x[i]) then deopt(x[i]) else 0 endif);
712
713/** @group optiontypes.int Return product of non-absent elements of \a x. */
714function var int: product(array[int] of var opt int: x) =
715 product (i in index_set(x)) (let { var int: dx = deopt(x[i]) } in if occurs(x[i]) then dx else 1 endif);
716
717/** @group optiontypes.int Return product of non-absent elements of \a x. */
718function int: product(array[int] of opt int: x) =
719 product (i in index_set(x)) (if occurs(x[i]) then deopt(x[i]) else 1 endif);
720
721% /** @group optiontypes.int Return absent if \a idx is absent, otherwise return \a x[\a idx] */
722% function var opt int: element(var opt int: idx, array[int] of var int: x) =
723% if absent(idx) then <> else element(deopt(idx),x) endif;
724%
725% /** @group optiontypes.int Return absent if \a idx1 or \a idx2 is absent, otherwise return \a x[\a idx1, \a idx2] */
726% function var opt int: element(var opt int: idx1, var opt int: idx2, array[int,int] of var int: x) =
727% if absent(idx1) \/ absent(idx2) then <> else element(deopt(idx1),deopt(idx2),x) endif;
728%
729% /** @group optiontypes.int Return \a x[\a idx] */
730% function var opt int: element(var int: idx, array[int] of var opt int: x) =
731% let {
732% var opt int: r;
733% constraint occurs(r) = element(idx,array1d(index_set(x),[occurs(x[i]) | i in index_set(x)]));
734% constraint deopt(r) = element(idx,array1d(index_set(x),[deopt(x[i]) | i in index_set(x)]));
735% } in r;
736%
737% /** @group optiontypes.int Return \a x[\a idx1, \a idx2] */
738% function var opt int: element(var int: idx1, var int: idx2, array[int,int] of var opt int: x) =
739% let {
740% var opt int: r;
741% constraint occurs(r) = element(idx1,idx2,
742% array2d(index_set_1of2(x),index_set_2of2(x),[occurs(x[i,j]) | i in index_set_1of2(x), j in index_set_2of2(x)]));
743% constraint deopt(r) = element(idx1,idx2,
744% array2d(index_set_1of2(x),index_set_2of2(x),[deopt(x[i,j]) | i in index_set_1of2(x), j in index_set_2of2(x)]));
745% } in r;
746%
747% /** @group optiontypes.int Return absent if \a idx is absent, otherwise return \a x[\a idx] */
748% function var opt int: element(var opt int: idx, array[int] of var opt int: x) =
749% if absent(idx) then <> else element(deopt(idx),x) endif;
750%
751% /** @group optiontypes.int Return absent if \a idx1 or \a idx2 is absent, otherwise return \a x[\a idx1, \a idx2] */
752% function var opt int: element(var opt int: idx1, var opt int: idx2, array[int,int] of var opt int: x) =
753% if absent(idx1) \/ absent(idx2) then <> else element(deopt(idx1),deopt(idx2),x) endif;
754
755/** @group optiontypes.int Search annotation for optional integer variables */
756annotation int_search(array[int] of var opt int: x, ann: a1, ann: a2, ann: a3) =
757 int_search([if occurs(x[i]) then deopt(x[i]) else 0 endif | i in index_set(x)],a1,a2,a3);
758
759/** @group optiontypes.int Search annotation for optional integer variables */
760annotation int_search(array[int] of var opt int: x, ann: a1, ann: a2) =
761 int_search([if occurs(x[i]) then deopt(x[i]) else 0 endif | i in index_set(x)],a1,a2);
762
763/* Internal function used to optimize over option type objective */
764
765function var int: objective_deopt_(var opt int: x, bool: direction) =
766 let {
767 int: worst = if direction then lb(x)-1 else ub(x)+1 endif;
768 } in if occurs(x) then deopt(x) else worst endif;
769
770/* TODO: predicate to temporarily replace the output items */
771
772predicate output_this(array[int] of var int: arr);
773predicate solve_this(int: mode, var int: objective, array[int] of var int: x, int: varsel, int: valsel);
774predicate solve_this(int: mode, var int: objective);
775
776function int: sol(var int: x);
777
778/***
779 @groupdef options Compiler options
780*/
781
782/* @group options Whether to only generate domains that are contiguous ranges */
783/* opt bool: mzn_opt_only_range_domains; */
784
785/* @group options Check whether to only generate domains that are contiguous ranges */
786/* test mzn_check_only_range_domains() = */
787/* if absent(mzn_opt_only_range_domains) then false */
788/* else deopt(mzn_opt_only_range_domains) endif; */
789
790/* @group options If defined, this can be used to check that the MiniZinc compiler supports all the features used in the model. */
791/* opt int: mzn_min_version_required; */
792
793/* constraint assert(absent(mzn_min_version_required) \/ deopt(mzn_min_version_required) <= mzn_compiler_version(), "This model requires MiniZinc version "++mzn_version_to_string(deopt(mzn_min_version_required))++" but you are running version "++mzn_version_to_string(mzn_compiler_version())); */
794
795predicate set_in(array[$T] of var int: X, set of int: s) = forall(x in array1d(X)) (x in s);
796predicate int_eq(array[$T] of var int: X, int: s) = forall(x in array1d(X)) (x = s);
797predicate float_eq(array[$T] of var int: X, float: s) = forall(x in array1d(X)) (x = s);
798predicate int_le(array[$T] of var int: X, int: s) = forall(x in array1d(X)) (x <= s);
799predicate int_le(int:s, array[$T] of var int: X) = forall(x in array1d(X)) (x >= s);
800predicate float_le(array[$T] of var float: X, float: s) = forall(x in array1d(X)) (x <= s);
801predicate float_le(float:s, array[$T] of var float: X) = forall(x in array1d(X)) (x >= s);
802
803include "builtins.mzn";