4.2.5. FlatZinc builtins¶
These are the standard constraints that need to be supported by FlatZinc solvers (or redefined in the redefinitions.mzn file).
4.2.5.1. Integer FlatZinc builtins¶
predicate array_int_element(var int: b,
array [int] of int: as,
var int: c)
Constrains as [ b ] = c
predicate array_int_maximum(var int: m, array [int] of var int: x)
Constrains m to be the maximum value of the (non-empty) array x
predicate array_int_minimum(var int: m, array [int] of var int: x)
Constrains m to be the minimum value of the (non-empty) array x
predicate array_var_int_element(var int: b,
array [int] of var int: as,
var int: c)
Constrains as [ b ] = c
predicate int_abs(var int: a, var int: b)
Constrains b to be the absolute value of a
predicate int_div(var int: a, var int: b, var int: c)
Constrains a / b = c
predicate int_eq(var int: a, var int: b)
Constrains a to be equal to b
predicate int_eq_reif(var int: a, var int: b, var bool: r)
Constrains ( a = b ) \(\leftrightarrow\) r
predicate int_le(var int: a, var int: b)
Constrains a to be less than or equal to b
predicate int_le_reif(var int: a, var int: b, var bool: r)
Constrains ( a ≤ b ) \(\leftrightarrow\) r
predicate int_lin_eq(array [int] of int: as,
array [int] of var int: bs,
int: c)
Constrains \({\bf c} = \sum_i {\bf as}[i]*{\bf bs}[i]\)
predicate int_lin_eq_reif(array [int] of int: as,
array [int] of var int: bs,
int: c,
var bool: r)
Constrains \({\bf r} \leftrightarrow ({\bf c} = \sum_i {\bf as}[i]*{\bf bs}[i])\)
predicate int_lin_le(array [int] of int: as,
array [int] of var int: bs,
int: c)
Constrains \(\sum\) as [ i ]* bs [ i ] ≤ c
predicate int_lin_le_reif(array [int] of int: as,
array [int] of var int: bs,
int: c,
var bool: r)
Constrains r \(\leftrightarrow\) (\(\sum\) as [ i ]* bs [ i ] ≤ c )
predicate int_lin_ne(array [int] of int: as,
array [int] of var int: bs,
int: c)
Constrains \({\bf c} \neq \sum_i {\bf as}[i]*{\bf bs}[i]\)
predicate int_lin_ne_reif(array [int] of int: as,
array [int] of var int: bs,
int: c,
var bool: r)
Constrains \({\bf r} \leftrightarrow ({\bf c} \neq \sum_i {\bf as}[i]*{\bf bs}[i])\)
predicate int_lt(var int: a, var int: b)
Constrains a < b
predicate int_lt_reif(var int: a, var int: b, var bool: r)
Constrains r \(\leftrightarrow\) ( a < b )
predicate int_max(var int: a, var int: b, var int: c)
Constrains max( a , b ) = c
predicate int_min(var int: a, var int: b, var int: c)
Constrains min( a , b ) = c
predicate int_mod(var int: a, var int: b, var int: c)
Constrains a % b = c
predicate int_ne(var int: a, var int: b)
Constrains a ≠ b
predicate int_ne_reif(var int: a, var int: b, var bool: r)
r \(\leftrightarrow\) ( a ≠ b )
predicate int_plus(var int: a, var int: b, var int: c)
Constrains a + b = c
predicate int_pow(var int: x, var int: y, var int: z)
Constrains z = \({\bf x} ^ {{\bf y}}\)
predicate int_pow_fixed(var int: x, int: y, var int: z)
Constrains z = \({\bf x} ^ {{\bf y}}\)
predicate int_times(var int: a, var int: b, var int: c)
Constrains a * b = c
4.2.5.2. Bool FlatZinc builtins¶
predicate array_bool_and(array [int] of var bool: as, var bool: r)
Constrains \({\bf r} \leftrightarrow \bigwedge_i {\bf as}[i]\)
predicate array_bool_element(var int: b,
array [int] of bool: as,
var bool: c)
Constrains as [ b ] = c
predicate array_bool_or(array [int] of var bool: as, var bool: r)
Constrains \({\bf r} \leftrightarrow \bigvee_i {\bf as}[i]\)
predicate array_bool_xor(array [int] of var bool: as)
Constrains \(\oplus_i\ {\bf as}[i]\)
predicate array_var_bool_element(var int: b,
array [int] of var bool: as,
var bool: c)
Constrains as [ b ] = c
predicate bool2int(var bool: a, var int: b)
Constrains \({\bf b} \in \{0,1\}\) and \({\bf a} \leftrightarrow {\bf b}=1\)
predicate bool_and(var bool: a, var bool: b, var bool: r)
Constrains \({\bf r} \leftrightarrow {\bf a} \land {\bf b}\)
predicate bool_clause(array [int] of var bool: as,
array [int] of var bool: bs)
Constrains \(\bigvee_i {\bf as}[i] \lor \bigvee_j \lnot {\bf bs}[j]\)
predicate bool_eq(var bool: a, var bool: b)
Constrains a = b
predicate bool_eq_reif(var bool: a, var bool: b, var bool: r)
Constrains r \(\leftrightarrow\) ( a = b )
predicate bool_le(var bool: a, var bool: b)
Constrains a ≤ b
predicate bool_le_reif(var bool: a, var bool: b, var bool: r)
Constrains r \(\leftrightarrow\) ( a ≤ b )
predicate bool_lin_eq(array [int] of int: as,
array [int] of var bool: bs,
var int: c)
Constrains \({\bf c} = \sum_i {\bf as}[i]*{\bf bs}[i]\)
predicate bool_lin_le(array [int] of int: as,
array [int] of var bool: bs,
int: c)
Constrains \({\bf c} \leq \sum_i {\bf as}[i]*{\bf bs}[i]\)
predicate bool_lt(var bool: a, var bool: b)
Constrains a < b
predicate bool_lt_reif(var bool: a, var bool: b, var bool: r)
Constrains r \(\leftrightarrow\) ( a < b )
predicate bool_not(var bool: a, var bool: b)
Constrains a ≠ b
predicate bool_or(var bool: a, var bool: b, var bool: r)
Constrains \({\bf r} \leftrightarrow {\bf a} \lor {\bf b}\)
predicate bool_xor(var bool: a, var bool: b, var bool: r)
Constrains \({\bf r} \leftrightarrow {\bf a} \oplus {\bf b}\)
predicate bool_xor(var bool: a, var bool: b)
Constrains a \(\oplus\) b
4.2.5.3. Set FlatZinc builtins¶
predicate array_set_element(var int: b,
array [int] of set of int: as,
var set of int: c)
Constrains as [ b ] = c
predicate array_var_set_element(var int: b,
array [int] of var set of int: as,
var set of int: c)
Constrains as [ b ] = c
predicate set_card(var set of int: S, var int: x)
Constrains x = | S |
predicate set_diff(var set of int: x,
var set of int: y,
var set of int: r)
Constrains r = x \(\setminus\) y
predicate set_eq(var set of int: x, var set of int: y)
Constrains x = y
predicate set_eq_reif(var set of int: x,
var set of int: y,
var bool: r)
Constrains r \(\leftrightarrow\) ( x = y )
predicate set_in(var int: x, set of int: S)
Constrains x \(\in\) S
predicate set_in(var int: x, var set of int: S)
Constrains x \(\in\) S
predicate set_in_reif(var int: x, set of int: S, var bool: r)
Constrains \({\bf r} \leftrightarrow ({\bf x} \in {\bf S})\)
predicate set_in_reif(var int: x, var set of int: S, var bool: r)
Constrains \({\bf r} \leftrightarrow ({\bf x} \in {\bf S})\)
predicate set_intersect(var set of int: x,
var set of int: y,
var set of int: r)
Constrains r = x \(\cap\) y
predicate set_le(var set of int: x, var set of int: y)
Constrains x ≤ y (lexicographic order of the sorted lists of elements)
predicate set_le_reif(var set of int: x,
var set of int: y,
var bool: r)
Constrains \({\bf r} \leftrightarrow ({\bf x} \leq {\bf y})\) (lexicographic order of the sorted lists of elements)
predicate set_lt(var set of int: x, var set of int: y)
Constrains x < y (lexicographic order of the sorted lists of elements)
predicate set_lt_reif(var set of int: x,
var set of int: y,
var bool: r)
Constrains \({\bf r} \leftrightarrow ({\bf x} < {\bf y})\) (lexicographic order of the sorted lists of elements)
predicate set_ne(var set of int: x, var set of int: y)
Constrains x ≠ y
predicate set_ne_reif(var set of int: x,
var set of int: y,
var bool: r)
Constrains r \(\leftrightarrow\) ( x ≠ y )
predicate set_subset(var set of int: x, var set of int: y)
Constrains x \(\subseteq\) y
predicate set_subset_reif(var set of int: x,
var set of int: y,
var bool: r)
Constrains \({\bf r} \leftrightarrow ({\bf x} \subseteq {\bf y})\)
predicate set_superset(var set of int: x, var set of int: y)
Constrains x \(\supseteq\) y
predicate set_symdiff(var set of int: x,
var set of int: y,
var set of int: r)
Constrains r to be the symmetric difference of x and y
predicate set_union(var set of int: x,
var set of int: y,
var set of int: r)
Constrains r = x \(\cup\) y
4.2.5.4. Float FlatZinc builtins¶
predicate array_float_element(var int: b,
array [int] of float: as,
var float: c)
Constrains as [ b ] = c
predicate array_float_maximum(var int: m, array [int] of var int: x)
Constrains m to be the maximum value of the (non-empty) array x
predicate array_float_minimum(var int: m, array [int] of var int: x)
Constrains m to be the minimum value of the (non-empty) array x
predicate array_var_float_element(var int: b,
array [int] of var float: as,
var float: c)
Constrains as [ b ] = c
predicate float_abs(var float: a, var float: b)
Constrains b to be the absolute value of a
predicate float_acos(var float: a, var float: b)
Constrains b = acos( a )
predicate float_acosh(var float: a, var float: b)
Constrains b = acosh( a )
predicate float_asin(var float: a, var float: b)
Constrains b = asin( a )
predicate float_asinh(var float: a, var float: b)
Constrains b = asinh( a )
predicate float_atan(var float: a, var float: b)
Constrains b = atan( a )
predicate float_atanh(var float: a, var float: b)
Constrains b = atanh( a )
predicate float_cos(var float: a, var float: b)
Constrains b = cos( a )
predicate float_cosh(var float: a, var float: b)
Constrains b = cosh( a )
predicate float_div(var float: a, var float: b, var float: c)
Constrains a / b = c
predicate float_dom(var float: x, array [int] of float: as)
Constrains the domain of x using the values in as , using each pair of values as [2* i -1].. as [2* i ] for i in 1.. n /2 as a possible range
predicate float_eq(var float: a, var float: b)
Constrains a = b
predicate float_eq_reif(var float: a, var float: b, var bool: r)
Constrains r \(\leftrightarrow\) ( a = b )
predicate float_exp(var float: a, var float: b)
Constrains b = exp( a )
predicate float_in(var float: a, float: b, float: c)
Constrains \({\bf a} \in\ [ {\bf b}, {\bf c} ]\)
predicate float_in_reif(var float: a, float: b, float: c, var bool: r)
Constrains r \(\leftrightarrow\) \({\bf a} \in\ [ {\bf b}, {\bf c} ]\)
predicate float_le(var float: a, var float: b)
Constrains a ≤ b
predicate float_le_reif(var float: a, var float: b, var bool: r)
Constrains r \(\leftrightarrow\) ( a ≤ b )
predicate float_lin_eq(array [int] of float: as,
array [int] of var float: bs,
float: c)
Constrains \({\bf c} = \sum_i {\bf as}[i]*{\bf bs}[i]\)
predicate float_lin_eq_reif(array [int] of float: as,
array [int] of var float: bs,
float: c,
var bool: r)
Constrains \({\bf r} \leftrightarrow ({\bf c} = \sum_i {\bf as}[i]*{\bf bs}[i])\)
predicate float_lin_le(array [int] of float: as,
array [int] of var float: bs,
float: c)
Constrains \({\bf c} \leq \sum_i {\bf as}[i]*{\bf bs}[i]\)
predicate float_lin_le_reif(array [int] of float: as,
array [int] of var float: bs,
float: c,
var bool: r)
Constrains \({\bf r} \leftrightarrow ({\bf c} \leq \sum_i {\bf as}[i]*{\bf bs}[i])\)
predicate float_lin_lt(array [int] of float: as,
array [int] of var float: bs,
float: c)
Constrains \({\bf c} < \sum_i {\bf as}[i]*{\bf bs}[i]\)
predicate float_lin_lt_reif(array [int] of float: as,
array [int] of var float: bs,
float: c,
var bool: r)
Constrains \({\bf r} \leftrightarrow ({\bf c} < \sum_i {\bf as}[i]*{\bf bs}[i])\)
predicate float_lin_ne(array [int] of float: as,
array [int] of var float: bs,
float: c)
Constrains \({\bf c} \neq \sum_i {\bf as}[i]*{\bf bs}[i]\)
predicate float_lin_ne_reif(array [int] of float: as,
array [int] of var float: bs,
float: c,
var bool: r)
Constrains \({\bf r} \leftrightarrow ({\bf c} \neq \sum_i {\bf as}[i]*{\bf bs}[i])\)
predicate float_ln(var float: a, var float: b)
Constrains b = ln( a )
predicate float_log10(var float: a, var float: b)
Constrains b = log<sub>10</sub>( a )
predicate float_log2(var float: a, var float: b)
Constrains b = log<sub>2</sub>( a )
predicate float_lt(var float: a, var float: b)
Constrains a < b
predicate float_lt_reif(var float: a, var float: b, var bool: r)
Constrains r \(\leftrightarrow\) ( a < b )
predicate float_max(var float: a, var float: b, var float: c)
Constrains max( a , b ) = c
predicate float_min(var float: a, var float: b, var float: c)
Constrains min( a , b ) = c
predicate float_ne(var float: a, var float: b)
Constrains a ≠ b
predicate float_ne_reif(var float: a, var float: b, var bool: r)
Constrains r \(\leftrightarrow\) ( a ≠ b )
predicate float_plus(var float: a, var float: b, var float: c)
Constrains a + b = c
predicate float_pow(var float: x, var float: y, var float: z)
Constrains z = \({\bf x} ^ {{\bf y}}\)
predicate float_sin(var float: a, var float: b)
Constrains b = sin( a )
predicate float_sinh(var float: a, var float: b)
Constrains b = sinh( a )
predicate float_sqrt(var float: a, var float: b)
Constrains \({\bf b} = \sqrt{{\bf a}}\)
predicate float_tan(var float: a, var float: b)
Constrains b = tan( a )
predicate float_tanh(var float: a, var float: b)
Constrains b = tanh( a )
predicate float_times(var float: a, var float: b, var float: c)
Constrains a * b = c
predicate int2float(var int: x, var float: y)
Constrains y = x
4.2.5.5. FlatZinc builtins added in MiniZinc 2.0.0.¶
These functions and predicates define built-in operations of the MiniZinc language that have been added in MiniZinc 2.0.0. Solvers that support these natively need to include a file called redefinitions-2.0.mzn in their solver library that redefines these predicates as builtins.
predicate array_float_maximum(var float: m,
array [int] of var float: x)
Constrains m to be the maximum value in array x .
predicate array_float_minimum(var float: m,
array [int] of var float: x)
Constrains m to be the minimum value in array x .
predicate array_int_maximum(var int: m, array [int] of var int: x)
Constrains m to be the maximum value in array x .
predicate array_int_minimum(var int: m, array [int] of var int: x)
Constrains m to be the minimum value in array x .
predicate bool_clause_reif(array [int] of var bool: as,
array [int] of var bool: bs,
var bool: b)
Reified clause constraint. Constrains \({\bf b} \leftrightarrow \bigvee_i {\bf as}[i] \lor \bigvee_j \lnot {\bf bs}[j]\)
4.2.5.6. FlatZinc builtins added in MiniZinc 2.0.2.¶
These functions and predicates define built-in operations of the MiniZinc language that have been added in MiniZinc 2.0.2. Solvers that support these natively need to include a file called redefinitions-2.0.2.mzn in their solver library that redefines these predicates as builtins.
predicate array_var_bool_element_nonshifted(var int: idx,
array [int] of var bool: x,
var bool: c)
Element constraint on array with MiniZinc index set, constrains x [ idx ] = c This can be overridden in a solver that can perform the index calculation more efficiently than using a MiniZinc decomposition.
predicate array_var_float_element_nonshifted(var int: idx,
array [int] of var float: x,
var float: c)
Element constraint on array with MiniZinc index set, constrains x [ idx ] = c This can be overridden in a solver that can perform the index calculation more efficiently than using a MiniZinc decomposition.
predicate array_var_int_element_nonshifted(var int: idx,
array [int] of var int: x,
var int: c)
Element constraint on array with MiniZinc index set, constrains x [ idx ] = c This can be overridden in a solver that can perform the index calculation more efficiently than using a MiniZinc decomposition.
predicate array_var_set_element_nonshifted(var int: idx,
array [int] of var set of int: x,
var set of int: c)
Element constraint on array with MiniZinc index set, constrains x [ idx ] = c This can be overridden in a solver that can perform the index calculation more efficiently than using a MiniZinc decomposition.
4.2.5.7. FlatZinc builtins added in MiniZinc 2.1.0.¶
These functions and predicates define built-in operations of the MiniZinc language that have been added in MiniZinc 2.1.0. Solvers that support these natively need to include a file called redefinitions-2.1.0.mzn in their solver library that redefines these predicates as builtins.
predicate float_dom(var float: x, array [int] of float: as)
Constrains x to take one of the values in as
predicate float_in(var float: x, float: a, float: b)
Constrains a ≤ x ≤ b
4.2.5.8. FlatZinc builtins added in MiniZinc 2.1.1.¶
These functions and predicates define built-in operations of the MiniZinc language that have been added in MiniZinc 2.1.1. Solvers that support these natively need to include a file called redefinitions-2.1.1.mzn in their solver library that redefines these predicates as builtins.
function var $$E: max(var set of $$E: s)
Returns variable constrained to be equal to the maximum of the set s . An alternative implementation can be found in the comments of the source code.
function var $$E: min(var set of $$E: s)
Returns variable constrained to be equal to the minimum of the set s . An alternative implementation can be found in the comments of the source code.