MiniZinc Documentation - Standard Library

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

Functions and Predicates
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_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_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_set_element(var int: b, array [int] of set of int: as, var set of int: c)

Constrains as[b] = c

predicate array_var_bool_element(var int: b, array [int] of var bool: as, var bool: c)

Constrains as[b] = c

predicate array_var_float_element(var int: b, array [int] of var float: as, var float: c)

Constrains as[b] = c

predicate array_var_int_element(var int: b, array [int] of var int: as, var 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 bool2int(var bool: a, var int: b)

Constrains b ∈ {0,1} and ab=1

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

Constrains rab

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 ↔ (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 ↔ (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 ↔ (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 rab

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

Constrains rab

predicate bool_xor(var bool: a, var bool: b)

Constrains ab

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_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 ↔ (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 ↔ \( {\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 ↔ (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 = log10(a)

predicate float_log2(var float: a, var float: b)

Constrains b = log2(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 ↔ (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 ↔ (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

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) ↔ 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) ↔ 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 Σ 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 ↔ (Σ 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 ↔ (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 ↔ (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

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 − 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 ↔ (x = y)

predicate set_in(var int: x, set of int: S)

Constrains xS

predicate set_in(var int: x, var set of int: S)

Constrains xS

predicate set_in_reif(var int: x, set of int: S, var bool: r)

Constrains r ↔ (xS)

predicate set_in_reif(var int: x, var set of int: S, var bool: r)

Constrains r ↔ (xS)

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

Constrains r = x ∩ 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 ↔ (xy)

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

Constrains xy

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

Constrains r ↔ (xy)

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 ∪ y