4.2.6. FlatZinc builtins

These are the standard constraints that need to be supported by FlatZinc solvers (or redefined in the redefinitions.mzn file).

4.2.6.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 ( ab ) \(\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 ab

predicate int_ne_reif(var int: a, var int: b, var bool: r)

r \(\leftrightarrow\) ( ab )

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_times(var int: a, var int: b, var int: c)

Constrains a * b = c

4.2.6.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 \({\bf r} \leftrightarrow \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 ab

predicate bool_le_reif(var bool: a, var bool: b, var bool: r)

Constrains r \(\leftrightarrow\) ( ab )

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 ab

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.6.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 xy (lexicographic order)

predicate set_lt(var set of int: x, var set of int: y)

Constrains x < y (lexicographic order)

predicate set_ne(var set of int: x, var set of int: y)

Constrains xy

predicate set_ne_reif(var set of int: x,
                      var set of int: y,
                      var bool: r)

Constrains r \(\leftrightarrow\) ( xy )

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_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.6.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 ab

predicate float_le_reif(var float: a, var float: b, var bool: r)

Constrains r \(\leftrightarrow\) ( ab )

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 ab

predicate float_ne_reif(var float: a, var float: b, var bool: r)

Constrains r \(\leftrightarrow\) ( ab )

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.6.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 .

More…

predicate array_float_minimum(var float: m,
                              array [int] of var float: x)

Constrains m to be the minimum value in array x .

More…

predicate array_int_maximum(var int: m, array [int] of var int: x)

Constrains m to be the maximum value in array x .

More…

predicate array_int_minimum(var int: m, array [int] of var int: x)

Constrains m to be the minimum value in array x .

More…

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]\)

More…

4.2.6.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.

More…

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.

More…

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.

More…

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.

More…

4.2.6.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

More…

predicate float_in(var float: x, float: a, float: b)

Constrains axb

More…

4.2.6.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.

More…

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.

More…