this repo has no description
dekker.one
1/***
2 @groupdef builtins.logic Logical operations
3
4 Logical operations are the standard operators of Boolean logic.
5*/
6
7/** @group builtins.logic Return truth value of the negation of \a x */
8function bool: op_not(bool: x) = not x;
9/** @group builtins.logic Return truth value of the negation of \a x */
10function var bool: op_not(var bool: x) ::promise_total =
11 let {
12 var bool: y;
13 constraint bool_not(x, y);
14 } in y;
15
16/** @group builtins.compare Return if array \a x is equal to array \a y */
17function bool: op_equals(array[$T] of int: x,array[$T] of int: y) =
18 let {
19 array[int] of int: xx = array1d(x);
20 array[int] of int: yy = array1d(y);
21 } in
22 assert(index_sets_agree(x,y), "array index sets do not match",
23 forall (i in index_set(xx)) (xx[i]=yy[i])
24 );
25
26/** @group builtins.compare Return if array \a x is equal to array \a y */
27function var bool: op_equals(array[$T] of var int: x, array[$T] of var int: y) =
28 let {
29 array[int] of var int: xx = array1d(x);
30 array[int] of var int: yy = array1d(y);
31 } in
32 assert(index_sets_agree(x,y), "array index sets do not match",
33 forall (i in index_set(xx)) (xx[i]=yy[i])
34 );
35
36/** @group builtins.compare Return if array \a x is equal to array \a y */
37function bool: op_equals(array[$T] of bool: x, array[$T] of bool: y) =
38 let {
39 array[int] of bool: xx = array1d(x);
40 array[int] of bool: yy = array1d(y);
41 } in
42 assert(index_sets_agree(x,y), "array index sets do not match",
43 forall (i in index_set(xx)) (xx[i]=yy[i])
44 );
45
46/** @group builtins.compare Return if array \a x is equal to array \a y */
47function var bool: op_equals(array[$T] of var bool: x,array[$T] of var bool: y) =
48 let {
49 array[int] of var bool: xx = array1d(x);
50 array[int] of var bool: yy = array1d(y);
51 } in
52 assert(index_sets_agree(x,y), "array index sets do not match",
53 forall (i in index_set(xx)) (xx[i]=yy[i])
54 );
55
56
57/***
58 @groupdef builtins.arithmetic Arithmetic Builtins
59
60 These builtins implement arithmetic operations.
61*/
62
63predicate int_minus(var int:x, var int:y, var int:z);
64
65/** @group builtins.arithmetic Return \a -x */
66function int: op_minus(int: x) ::promise_total = -x;
67/** @group builtins.arithmetic Return \a x - \a y */
68function var int: op_minus(var int: x) ::promise_total =
69 let {
70 var int: y;
71 constraint int_minus(0,x,y);
72 } in y;
73
74/** @group builtins.arithmetic Return \a x - \a y */
75function int: op_minus(int: x, int: y) ::promise_total = x - y;
76/** @group builtins.arithmetic Return \a x - \a y */
77function var int: op_minus(var int: x, int: y) ::promise_total =
78 if y = 0 then
79 x
80 else
81 let {
82 var int: z;
83 constraint int_minus(x,y,z);
84 } in z
85 endif;
86/** @group builtins.arithmetic Return \a x - \a y */
87function var int: op_minus(var int: x, var int: y) ::promise_total =
88 let {
89 var int: z;
90 constraint int_minus(x, y, z);
91 } in z;
92/** @group builtins.arithmetic Return \a x + \a y */
93function int: op_plus(int: x, int: y) = x + y;
94/** @group builtins.arithmetic Return \a x + \a y */
95function var int: op_plus(int: x, var int: y) ::promise_total =
96 if x = 0 then
97 y
98 else
99 let {
100 var int: z;
101 constraint int_plus(x, y, z);
102 } in z
103 endif;
104/** @group builtins.arithmetic Return \a x + \a y */
105function var int: op_plus(var int: x, int: y) = op_plus(y, x);
106/** @group builtins.arithmetic Return \a x + \a y */
107function var int: op_plus(var int: x, var int: y) ::promise_total =
108 let {
109 var int: z;
110 constraint int_plus(x, y, z);
111 } in z;
112
113/** @group builtins.arithmetic Return \a x * \a y */
114function int: op_times(int: x, int: y) = x * y;
115function var int: op_times(int: x, var int: y) ::promise_total =
116 if x = 1 then
117 y
118 else
119 let {
120 var int: z;
121 constraint int_times(x, y, z);
122 } in z
123 endif;
124function var int: op_times(var int: x, int: y) = op_times(y, x);
125/** @group builtins.arithmetic Return \a x * \a y */
126function var int: op_times(var int: x, var int: y) ::promise_total =
127 let {
128 var int: z;
129 constraint int_times(x, y, z);
130 } in z;
131
132/* Negated versions of FlatZinc builtins */
133predicate int_lin_le_neg(array[int] of int: as, array[int] of var int: bs, int: c) =
134 int_lin_le([-a | a in as], bs, -c-1);
135predicate int_lin_eq_neg(array[int] of int: as, array[int] of var int: bs, int: c) =
136 int_lin_ne(as, bs, c);
137
138predicate pre_int_lin_eq(array[int] of int: as, array[int] of var int: bs, int: c) = if length(as)=0 then c=0 else int_lin_eq(as,bs,c) endif;
139
140predicate pre_int_lin_eq_neg(array[int] of int: as, array[int] of var int: bs, int: c) = if length(as)=0 then c!=0 else int_lin_ne(as,bs,c) endif;
141
142predicate pre_int_lin_le(array[int] of int: as, array[int] of var int: bs, int: c) = if length(as)=0 then 0<=c else int_lin_le(as,bs,c) endif;
143
144predicate pre_int_lin_le_neg(array[int] of int: as, array[int] of var int: bs, int: c) = if length(as)=0 then 0>c else int_lin_le_neg(as,bs,c) endif;
145
146
147/** @group builtins.arithmetic Return result of integer division \a x / \a y */
148function int: op_int_division(int: x, int: y) = x div y;
149/** @group builtins.arithmetic Return result of integer division \a x / \a y */
150function var int: op_int_division(var int: x, var int: y) =
151 if mzn_in_root_context(y) \/ not (0 in dom(y)) then div_t(x,y) else
152 let { constraint y != 0 } in div_mt(x,y) endif;
153
154/** @group builtins.arithmetic Return result of integer division \a x / \a y */
155function int: op_modulus(int: x, int: y) = x mod y;
156/** @group builtins.arithmetic Return result of integer division \a x / \a y */
157function var int: op_modulus(var int: x, var int: y) =
158 if mzn_in_root_context(y) \/ not (0 in dom(y)) then mod_t(x,y) else
159 let { constraint y != 0 } in mod_mt(x,y) endif;
160
161/** @group builtins.arithmetic Return result of floating point division \a x / \a y */
162function float: op_float_division(float: x, float: y) = x / y;
163/** @group builtins.arithmetic Return result of floating point division \a x / \a y */
164function var float: op_float_division(var float: x, var float: y) =
165 if mzn_in_root_context(y) \/ lb(y) > 0.0 \/ ub(y) < 0.0 then fldiv_t(x,y) else
166 let { constraint y != 0.0 } in fldiv_mt(x,y) endif;
167
168
169function int: internal_max(array[$U] of int: x);
170function int: internal_set_max(set of int: x);
171function bool: internal_max(array[$U] of bool: x);
172/** @group builtins.arithmetic Return maximum of \a x and \a y */
173function $T: max($T: x, $T: y) =
174 if x > y then
175 x
176 else
177 y
178 endif;
179/** @group builtins.arithmetic Return maximum of elements in set \a x */
180function int: max(set of int: x) = internal_set_max(x);
181/** @group builtins.arithmetic Return maximum of elements in array \a x */
182function int: max(array[$U] of int: x) = internal_max(array1d(x));
183/** @group builtins.arithmetic Return maximum of elements in array \a x */
184function bool: max(array[$U] of bool: x) = internal_max(array1d(x));
185
186function int: internal_min(array[$U] of int: x);
187function int: internal_set_min(set of int: x);
188function bool: internal_min(array[$U] of bool: x);
189/** @group builtins.arithmetic Return minimum of \a x and \a y */
190function $T: min($T: x, $T: y) =
191 if x < y then
192 x
193 else
194 y
195 endif;
196function int: min(set of int: x) = internal_set_min(x);
197function int: min(array[$U] of int: x) = internal_min(array1d(x));
198function bool: min(array[$U] of bool: x) = internal_min(array1d(x));
199
200predicate int_sum(array[int] of var int: xs, var int: x);
201/** @group builtins.arithmetic Return sum of elements in array \a x */
202function var int: sum_cc(array[$T] of var int: x) ::promise_total =
203 let {
204 array[int] of var int: xs = array1d(x);
205 var int: res;
206 constraint int_sum(xs, res);
207 } in res;
208
209function int: abs(int: x) =
210 if x<0 then
211 -x
212 else
213 x
214 endif;
215
216% ---------------
217
218/***
219 @groupdef builtins.ifthenelse Conditionals
220
221 These functions implement conditional (if-then-else-endif) constraints.
222*/
223
224/** @group builtins.ifthenelse Conditional constraint \(\{\a c[i]\land\not\exists \a c[1..i-1]\ \rightarrow\ y=x[i] \}\)
225
226 This constraint is generated by the compiler for if-then-else expressions.
227 The last entry in the \a c array is always the constant true, corresponding
228 to the else case.
229*/
230function var int: if_then_else(array[int] of var bool: c, array[int] of int: x) ::promise_total =
231 let {
232 var dom_array(x): y;
233 constraint fzn_if_then_else_int(c, x, y);
234 } in y;
235
236/** @group builtins.ifthenelse Conditional constraint \(\{\a c[i]\land\not\exists \a c[1..i-1]\ \rightarrow\ y=x[i] \}\)
237
238 This constraint is generated by the compiler for if-then-else expressions.
239 The last entry in the \a c array is always the constant true, corresponding
240 to the else case.
241*/
242function var int: if_then_else(array[int] of var bool: c, array[int] of var int: x) ::promise_total =
243 let {
244 var dom_array(x): y;
245 constraint fzn_if_then_else_var_int(c, x, y);
246 } in y;
247
248/** @group builtins.ifthenelse Conditional constraint \(\{\a c[i]\land\not\exists \a c[1..i-1]\ \rightarrow\ y=x[i] \}\)
249
250 This constraint is generated by the compiler for if-then-else expressions.
251 The last entry in the \a c array is always the constant true, corresponding
252 to the else case.
253*/
254function var bool: if_then_else(array[int] of var bool: c, array[int] of bool: x) ::promise_total =
255 let {
256 var bool: y;
257 constraint fzn_if_then_else_bool(c, x, y);
258 } in y;
259
260/** @group builtins.ifthenelse Conditional constraint \(\{\a c[i]\land\not\exists \a c[1..i-1]\ \rightarrow\ y=x[i] \}\)
261
262 This constraint is generated by the compiler for if-then-else expressions.
263 The last entry in the \a c array is always the constant true, corresponding
264 to the else case.
265*/
266function var bool: if_then_else(array[int] of var bool: c, array[int] of var bool: x) ::promise_total =
267 let {
268 var bool: y;
269 constraint fzn_if_then_else_var_bool(c, x, y);
270 } in y;
271
272/** @group builtins.ifthenelse Conditional partiality constraint
273
274 This constraint is generated by the compiler for if-then-else expressions
275 with potentially undefined cases.
276 The last entry in the \a c array is always the constant true, corresponding
277 to the else case.
278 The \a d[i] variable represents whether case
279 \p i is defined. Constrains that if \b is defined, then the selected case must be defined, and
280 if the selected case is undefined, then \a b must be undefined.
281*/
282function var bool: if_then_else_partiality(array[int] of var bool: c, array[int] of var bool: d) ::promise_total =
283 let {
284 var bool: b;
285 constraint fzn_if_then_else_partiality(c, d, b);
286 } in b;
287
288
289
290% Include solver-specific redefinitions for any FlatZinc built-ins.
291%
292include "fzn_if_then_else_int.mzn";
293include "fzn_if_then_else_var_int.mzn";
294include "fzn_if_then_else_bool.mzn";
295include "fzn_if_then_else_var_bool.mzn";
296include "fzn_if_then_else_partiality.mzn";
297% Include interpreter definitions always to be included
298include "mznasm_builtins.mzn";