this repo has no description
dekker.one
1%-----------------------------------------------------------------------------%
2%
3% FlatZinc builtins
4%
5% This section contains declarations for the standard FlatZinc builtins.
6% They can be redefined by providing a custom redefinitions.mzn in the
7% solver globals library.
8%
9
10/***
11 @groupdef flatzinc FlatZinc builtins
12
13 These are the standard constraints that need to be supported by FlatZinc
14 solvers (or redefined in the redefinitions.mzn file).
15*/
16
17/***
18 @groupdef flatzinc.int Integer FlatZinc builtins
19*/
20
21/** @group flatzinc.int Constrains \a b to be the absolute value of \a a */
22predicate int_abs(var int: a, var int: b);
23/** @group flatzinc.int Constrains \a a to be equal to \a b */
24predicate int_eq(var int: a, var int: b);
25/** @group flatzinc.int Constrains (\a a=\a b) \( \leftrightarrow \) \a r */
26predicate int_eq_reif(var int: a, var int: b, var bool: r);
27/** @group flatzinc.int Constrains \a a to be less than or equal to \a b */
28predicate int_le(var int: a, var int: b);
29/** @group flatzinc.int Constrains (\a a ≤ \a b) \( \leftrightarrow \) \a r */
30predicate int_le_reif(var int: a, var int: b, var bool: r);
31/** @group flatzinc.int Constrains \( \a c = \sum_i \a as[i]*\a bs[i] \) */
32predicate int_lin_eq(array[int] of int: as, array[int] of var int: bs, int: c);
33/** @group flatzinc.int Constrains \( \a r \leftrightarrow (\a c = \sum_i \a as[i]*\a bs[i]) \) */
34predicate int_lin_eq_reif(array[int] of int: as, array[int] of var int: bs,int: c, var bool: r);
35/** @group flatzinc.int Constrains \( \a c \neq \sum_i \a as[i]*\a bs[i] \) */
36predicate int_lin_ne(array[int] of int: as, array[int] of var int: bs, int: c);
37/** @group flatzinc.int Constrains \( \a r \leftrightarrow (\a c \neq \sum_i \a as[i]*\a bs[i]) \) */
38predicate int_lin_ne_reif(array[int] of int: as, array[int] of var int: bs,int: c, var bool: r);
39
40/** @group flatzinc.int Constrains \( \sum \) \a as[\p i]*\a bs[\p i] ≤ \a c */
41predicate int_lin_le(array[int] of int: as, array[int] of var int: bs, int: c);
42/** @group flatzinc.int Constrains \a r \( \leftrightarrow \) (\( \sum \) \a as[\p i]*\a bs[\p i] ≤ \a c) */
43predicate int_lin_le_reif(array[int] of int: as, array[int] of var int: bs,int: c, var bool: r);
44/** @group flatzinc.int Constrains \a a ≠ \a b */
45predicate int_ne(var int: a, var int: b);
46/** @group flatzinc.int \a r \( \leftrightarrow \) (\a a ≠ \a b) */
47predicate int_ne_reif(var int: a, var int: b, var bool: r);
48/** @group flatzinc.int Constrains \a a + \a b = \a c */
49predicate int_plus(var int: a, var int: b, var int: c);
50/** @group flatzinc.int Constrains \a a / \a b = \a c */
51predicate int_div(var int: a, var int: b, var int: c);
52/** @group flatzinc.int Constrains \a a < \a b */
53predicate int_lt(var int: a, var int: b);
54/** @group flatzinc.int Constrains \a r \( \leftrightarrow \) (\a a < \a b) */
55predicate int_lt_reif(var int: a, var int: b, var bool: r);
56/** @group flatzinc.int Constrains max(\a a, \a b) = \a c */
57predicate int_max(var int: a, var int: b, var int: c);
58/** @group flatzinc.int Constrains min(\a a, \a b) = \a c */
59predicate int_min(var int: a, var int: b, var int: c);
60/** @group flatzinc.int Constrains \a a % \a b = \a c */
61predicate int_mod(var int: a, var int: b, var int: c);
62/** @group flatzinc.int Constrains \a a * \a b = \a c */
63predicate int_times(var int: a, var int: b, var int: c);
64/** @group flatzinc.int Constrains \a z = \(\a x ^ {\a y}\) */
65predicate int_pow(var int: x, var int: y, var int: z);
66
67/***
68 @groupdef flatzinc.bool Bool FlatZinc builtins
69*/
70
71/** @group flatzinc.bool Constrains \( \a b \in \{0,1\} \) and \( \a a \leftrightarrow \a b=1 \) */
72predicate bool2int(var bool: a, var int: b);
73/** @group flatzinc.bool Constrains \( \a r \leftrightarrow \a a \land \a b \) */
74predicate bool_and(var bool: a, var bool: b, var bool: r);
75/** @group flatzinc.bool Constrains \( \bigvee_i \a as[i] \lor \bigvee_j \lnot \a bs[j] \) */
76predicate bool_clause(array[int] of var bool: as, array[int] of var bool: bs);
77
78/** @group flatzinc.bool Constrains \a a = \a b */
79predicate bool_eq(var bool: a, var bool: b);
80/** @group flatzinc.bool Constrains \a r \( \leftrightarrow \) (\a a = \a b) */
81predicate bool_eq_reif(var bool: a, var bool: b, var bool: r);
82/** @group flatzinc.bool Constrains \a a ≤ \a b */
83predicate bool_le(var bool: a, var bool: b);
84/** @group flatzinc.bool Constrains \a r \( \leftrightarrow \) (\a a ≤ \a b) */
85predicate bool_le_reif(var bool: a, var bool: b, var bool: r);
86/** @group flatzinc.bool Constrains \( \a c = \sum_i \a as[i]*\a bs[i] \) */
87predicate bool_lin_eq(array[int] of int: as, array[int] of var bool: bs, var int: c);
88/** @group flatzinc.bool Constrains \( \a c \leq \sum_i \a as[i]*\a bs[i] \) */
89predicate bool_lin_le(array[int] of int: as, array[int] of var bool: bs, int: c);
90/** @group flatzinc.bool Constrains \a a < \a b */
91predicate bool_lt(var bool: a, var bool: b);
92/** @group flatzinc.bool Constrains \a r \( \leftrightarrow \) (\a a < \a b) */
93predicate bool_lt_reif(var bool: a, var bool: b, var bool: r);
94/** @group flatzinc.bool Constrains \a a ≠ \a b */
95predicate bool_not(var bool: a, var bool: b);
96/** @group flatzinc.bool Constrains \( \a r \leftrightarrow \a a \lor \a b \) */
97predicate bool_or(var bool: a, var bool: b, var bool: r);
98/** @group flatzinc.bool Constrains \( \a r \leftrightarrow \a a \oplus \a b \) */
99predicate bool_xor(var bool: a, var bool: b, var bool: r);
100/** @group flatzinc.bool Constrains \a a \( \oplus \) \a b */
101predicate bool_xor(var bool: a, var bool: b);
102
103/***
104 @groupdef flatzinc.set Set FlatZinc builtins
105*/
106
107/** @group flatzinc.set Constrains \a x \( \in \) \a S */
108predicate set_in(var int: x, set of int: S);
109/** @group flatzinc.set Constrains \a x \( \in \) \a S */
110predicate set_in(var int: x, var set of int: S);
111/** @group flatzinc.set Constrains \a x = |\a S| */
112predicate set_card(var set of int: S, var int: x);
113/** @group flatzinc.set Constrains \( \a r \leftrightarrow (\a x \in \a S) \) */
114predicate set_in_reif(var int: x, set of int: S, var bool: r);
115/** @group flatzinc.set Constrains \( \a r \leftrightarrow (\a x \in \a S) \) */
116predicate set_in_reif(var int: x, var set of int: S, var bool: r);
117/** @group flatzinc.set Constrains \a x \( \subseteq \) \a y */
118predicate set_subset(var set of int: x, var set of int: y);
119/** @group flatzinc.set Constrains \a x \( \supseteq \) \a y */
120predicate set_superset(var set of int: x, var set of int: y);
121/** @group flatzinc.set Constrains \( \a r \leftrightarrow (\a x \subseteq \a y) \) */
122predicate set_subset_reif(var set of int: x, var set of int: y, var bool: r);
123/** @group flatzinc.set Constrains \a x ≤ \a y (lexicographic order) */
124predicate set_le(var set of int: x, var set of int: y);
125/** @group flatzinc.set Constrains \a x < \a y (lexicographic order) */
126predicate set_lt(var set of int: x, var set of int: y);
127/** @group flatzinc.set Constrains \a x = \a y */
128predicate set_eq(var set of int: x, var set of int: y);
129/** @group flatzinc.set Constrains \a r \( \leftrightarrow \) (\a x = \a y) */
130predicate set_eq_reif(var set of int: x, var set of int: y, var bool: r);
131/** @group flatzinc.set Constrains \a x ≠ \a y */
132predicate set_ne(var set of int: x, var set of int: y);
133/** @group flatzinc.set Constrains \a r \( \leftrightarrow \) (\a x ≠ \a y) */
134predicate set_ne_reif(var set of int: x, var set of int: y, var bool: r);
135/** @group flatzinc.set Constrains \a r = \a x \( \cap \) \a y */
136predicate set_intersect(var set of int: x, var set of int: y, var set of int: r);
137/** @group flatzinc.set Constrains \a r = \a x \( \cup \) \a y */
138predicate set_union(var set of int: x, var set of int: y, var set of int: r);
139/** @group flatzinc.set Constrains \a r = \a x \( \setminus \) \a y */
140predicate set_diff(var set of int: x, var set of int: y, var set of int: r);
141/** @group flatzinc.set Constrains \a r to be the symmetric difference of \a x and \a y */
142predicate set_symdiff(var set of int: x, var set of int: y, var set of int: r);
143
144/***
145 @groupdef flatzinc.float Float FlatZinc builtins
146*/
147
148/** @group flatzinc.float Constrains \a b to be the absolute value of \a a */
149predicate float_abs(var float: a, var float: b);
150/** @group flatzinc.float Constrains \a b = acos(\a a) */
151predicate float_acos(var float: a, var float: b);
152/** @group flatzinc.float Constrains \a b = acosh(\a a) */
153predicate float_acosh(var float: a, var float: b);
154/** @group flatzinc.float Constrains \a b = asin(\a a) */
155predicate float_asin(var float: a, var float: b);
156/** @group flatzinc.float Constrains \a b = asinh(\a a) */
157predicate float_asinh(var float: a, var float: b);
158/** @group flatzinc.float Constrains \a b = atan(\a a) */
159predicate float_atan(var float: a, var float: b);
160/** @group flatzinc.float Constrains \a b = atanh(\a a) */
161predicate float_atanh(var float: a, var float: b);
162/** @group flatzinc.float Constrains \a b = cos(\a a) */
163predicate float_cos(var float: a, var float: b);
164/** @group flatzinc.float Constrains \a b = cosh(\a a) */
165predicate float_cosh(var float: a, var float: b);
166/** @group flatzinc.float Constrains \a b = exp(\a a) */
167predicate float_exp(var float: a, var float: b);
168/** @group flatzinc.float Constrains \a b = ln(\a a) */
169predicate float_ln(var float: a, var float: b);
170/** @group flatzinc.float Constrains \a b = log<sub>10</sub>(\a a) */
171predicate float_log10(var float: a, var float: b);
172/** @group flatzinc.float Constrains \a b = log<sub>2</sub>(\a a) */
173predicate float_log2(var float: a, var float: b);
174/** @group flatzinc.float Constrains \(\a b = \sqrt{\a a}\) */
175predicate float_sqrt(var float: a, var float: b);
176/** @group flatzinc.float Constrains \a z = \(\a x ^ {\a y}\) */
177predicate float_pow(var float: x, var float: y, var float: z);
178/** @group flatzinc.float Constrains \a b = sin(\a a) */
179predicate float_sin(var float: a, var float: b);
180/** @group flatzinc.float Constrains \a b = sinh(\a a) */
181predicate float_sinh(var float: a, var float: b);
182/** @group flatzinc.float Constrains \a b = tan(\a a) */
183predicate float_tan(var float: a, var float: b);
184/** @group flatzinc.float Constrains \a b = tanh(\a a) */
185predicate float_tanh(var float: a, var float: b);
186
187/** @group flatzinc.float Constrains \a a = \a b */
188predicate float_eq(var float: a, var float: b);
189/** @group flatzinc.float Constrains \a r \( \leftrightarrow \) (\a a = \a b) */
190predicate float_eq_reif(var float: a, var float: b, var bool: r);
191/** @group flatzinc.float Constrains \a a ≤ \a b */
192predicate float_le(var float: a, var float: b);
193/** @group flatzinc.float Constrains \a r \( \leftrightarrow \) (\a a ≤ \a b) */
194predicate float_le_reif(var float: a, var float: b, var bool: r);
195/** @group flatzinc.float Constrains \a a < \a b */
196predicate float_lt(var float: a, var float: b);
197/** @group flatzinc.float Constrains \a r \( \leftrightarrow \) (\a a < \a b) */
198predicate float_lt_reif(var float: a, var float: b, var bool: r);
199/** @group flatzinc.float Constrains \a a ≠ \a b */
200predicate float_ne(var float: a, var float: b);
201/** @group flatzinc.float Constrains \a r \( \leftrightarrow \) (\a a ≠ \a b) */
202predicate float_ne_reif(var float: a, var float: b, var bool: r);
203/** @group flatzinc.float Constrains \( \a a \in\ [ \a b, \a c ] \) */
204predicate float_in(var float: a, float: b, float: c);
205/** @group flatzinc.float Constrains \a r \( \leftrightarrow \) \( \a a \in\ [ \a b, \a c ] \) */
206predicate float_in_reif(var float: a, float: b, float: c, var bool: r);
207/** @group flatzinc.float Constrains the domain of \a x using the values in \a as, using each
208 pair of values \a as[2*\p i-1]..\a as[2*\p i] for \p i in 1..\p n/2 as a possible range
209 */
210predicate float_dom(var float: x, array[int] of float: as);
211
212/** @group flatzinc.float Constrains \( \a c = \sum_i \a as[i]*\a bs[i] \) */
213predicate float_lin_eq(array[int] of float: as, array[int] of var float: bs, float: c);
214/** @group flatzinc.float Constrains \( \a r \leftrightarrow (\a c = \sum_i \a as[i]*\a bs[i]) \) */
215predicate float_lin_eq_reif(array[int] of float: as, array[int] of var float: bs, float: c, var bool: r);
216/** @group flatzinc.float Constrains \( \a c \leq \sum_i \a as[i]*\a bs[i] \) */
217predicate float_lin_le(array[int] of float: as, array[int] of var float: bs, float: c);
218/** @group flatzinc.float Constrains \( \a r \leftrightarrow (\a c \leq \sum_i \a as[i]*\a bs[i]) \) */
219predicate float_lin_le_reif(array[int] of float: as, array[int] of var float: bs, float: c, var bool: r);
220/** @group flatzinc.float Constrains \( \a c < \sum_i \a as[i]*\a bs[i] \) */
221predicate float_lin_lt(array[int] of float: as, array[int] of var float: bs, float: c);
222/** @group flatzinc.float Constrains \( \a r \leftrightarrow (\a c < \sum_i \a as[i]*\a bs[i]) \) */
223predicate float_lin_lt_reif(array[int] of float: as, array[int] of var float: bs, float: c, var bool: r);
224/** @group flatzinc.float Constrains \( \a c \neq \sum_i \a as[i]*\a bs[i] \) */
225predicate float_lin_ne(array[int] of float: as, array[int] of var float: bs, float: c);
226/** @group flatzinc.float Constrains \( \a r \leftrightarrow (\a c \neq \sum_i \a as[i]*\a bs[i]) \) */
227predicate float_lin_ne_reif(array[int] of float: as, array[int] of var float: bs, float: c, var bool: r);
228
229/** @group flatzinc.float Constrains max(\a a, \a b) = \a c */
230predicate float_max(var float: a, var float: b, var float: c);
231/** @group flatzinc.float Constrains min(\a a, \a b) = \a c */
232predicate float_min(var float: a, var float: b, var float: c);
233/** @group flatzinc.float Constrains \a a + \a b = \a c */
234predicate float_plus(var float: a, var float: b, var float: c);
235/** @group flatzinc.float Constrains \a a / \a b = \a c */
236predicate float_div(var float: a, var float: b, var float: c);
237/** @group flatzinc.float Constrains \a a * \a b = \a c */
238predicate float_times(var float: a, var float: b, var float: c);
239
240/** @group flatzinc.float Constrains \a y=\a x */
241predicate int2float(var int: x, var float: y);
242
243
244% Array constraints
245
246/** @group flatzinc.bool Constrains \( \a r \leftrightarrow \bigwedge_i \a as[i]\) */
247predicate array_bool_and(array[int] of var bool: as, var bool: r);
248/** @group flatzinc.bool Constrains \( \a r \leftrightarrow \bigvee_i \a as[i]\) */
249predicate array_bool_or(array[int] of var bool: as, var bool: r);
250/** @group flatzinc.bool Constrains \( \a r \leftrightarrow \oplus_i\ \a as[i]\) */
251predicate array_bool_xor(array[int] of var bool: as);
252/** @group flatzinc.bool Constrains \a as[\a b] = \a c */
253predicate array_bool_element(var int: b, array[int] of bool: as, var bool: c);
254/** @group flatzinc.int Constrains \a as[\a b] = \a c */
255predicate array_int_element(var int: b, array[int] of int: as, var int: c);
256/** @group flatzinc.float Constrains \a as[\a b] = \a c */
257predicate array_float_element(var int: b, array[int] of float: as, var float: c);
258/** @group flatzinc.set Constrains \a as[\a b] = \a c */
259predicate array_set_element(var int: b, array[int] of set of int: as, var set of int: c);
260/** @group flatzinc.bool Constrains \a as[\a b] = \a c */
261predicate array_var_bool_element(var int: b, array[int] of var bool: as, var bool: c);
262/** @group flatzinc.int Constrains \a as[\a b] = \a c */
263predicate array_var_int_element(var int: b, array[int] of var int: as, var int: c);
264/** @group flatzinc.float Constrains \a as[\a b] = \a c */
265predicate array_var_float_element(var int: b, array[int] of var float: as, var float: c);
266/** @group flatzinc.set Constrains \a as[\a b] = \a c */
267predicate array_var_set_element(var int: b, array[int] of var set of int: as, var set of int: c);
268/** @group flatzinc.int Constrains \a m to be the maximum value of the (non-empty)
269 array \a x */
270predicate array_int_maximum(var int: m, array[int] of var int: x);
271/** @group flatzinc.float Constrains \a m to be the maximum value of the (non-empty)
272 array \a x */
273predicate array_float_maximum(var int: m, array[int] of var int: x);
274/** @group flatzinc.int Constrains \a m to be the minimum value of the (non-empty)
275 array \a x */
276predicate array_int_minimum(var int: m, array[int] of var int: x);
277/** @group flatzinc.float Constrains \a m to be the minimum value of the (non-empty)
278 array \a x */
279predicate array_float_minimum(var int: m, array[int] of var int: x);