4.2.3.1. Integer FlatZinc builtins

In this section: array_int_element, array_var_int_element, int_abs, int_div, int_eq, int_eq_reif, int_le, int_le_reif, int_lin_eq, int_lin_eq_reif, int_lin_le, int_lin_le_reif, int_lin_ne, int_lin_ne_reif, int_lt, int_lt_reif, int_max, int_min, int_mod, int_ne, int_ne_reif, int_plus, int_pow, int_times, set_in.

array_int_element

predicate array_int_element(var int: idx,
                            array [int] of int: xs,
                            var int: y)

Constrains xs[idx] = y

array_var_int_element

predicate array_var_int_element(var int: idx,
                                array [int] of var int: xs,
                                var int: y)

Constrains xs[idx] = y

int_abs

predicate int_abs(var int: x, var int: y)

Constrains y to be the absolute value of x

int_div

predicate int_div(var int: x, var int: y, var int: z)

Constrains x / y = z, where z is rounded to the value closest to zero (i.e., truncated).

int_eq

predicate int_eq(var int: x, var int: y)

Constrains x to be equal to y

int_eq_reif

predicate int_eq_reif(var int: x, var int: y, var bool: b)

Constrains (x=y) \(\leftrightarrow\) b

int_le

predicate int_le(var int: x, var int: y)

Constrains x to be less than or equal to y

int_le_reif

predicate int_le_reif(var int: x, var int: y, var bool: b)

Constrains (x ≤ y) \(\leftrightarrow\) b

int_lin_eq

predicate int_lin_eq(array [int] of int: as,
                     array [int] of var int: xs,
                     int: y)

Constrains \({\bf y} = \sum_i {\bf as}[i]*{\bf xs}[i]\)

int_lin_eq_reif

predicate int_lin_eq_reif(array [int] of int: as,
                          array [int] of var int: xs,
                          int: y,
                          var bool: b)

Constrains \({\bf b} \leftrightarrow ({\bf y} = \sum_i {\bf as}[i]*{\bf xs}[i])\)

int_lin_le

predicate int_lin_le(array [int] of int: as,
                     array [int] of var int: xs,
                     int: y)

Constrains \(\sum\) as[i]*xs[i] ≤ y

int_lin_le_reif

predicate int_lin_le_reif(array [int] of int: as,
                          array [int] of var int: xs,
                          int: y,
                          var bool: b)

Constrains b \(\leftrightarrow\) (\(\sum\) as[i]*xs[i] ≤ y)

int_lin_ne

predicate int_lin_ne(array [int] of int: as,
                     array [int] of var int: xs,
                     int: y)

Constrains \({\bf y} \neq \sum_i {\bf as}[i]*{\bf xs}[i]\)

int_lin_ne_reif

predicate int_lin_ne_reif(array [int] of int: as,
                          array [int] of var int: xs,
                          int: y,
                          var bool: b)

Constrains \({\bf b} \leftrightarrow ({\bf y} \neq \sum_i {\bf as}[i]*{\bf xs}[i])\)

int_lt

predicate int_lt(var int: x, var int: y)

Constrains x < y

int_lt_reif

predicate int_lt_reif(var int: x, var int: y, var bool: b)

Constrains b \(\leftrightarrow\) (x < y)

int_max

predicate int_max(var int: x, var int: y, var int: z)

Constrains max(x, y) = z

int_min

predicate int_min(var int: x, var int: y, var int: z)

Constrains min(x, y) = z

int_mod

predicate int_mod(var int: x, var int: y, var int: z)

Constrains x % y = z

int_ne

predicate int_ne(var int: x, var int: y)

Constrains x ≠ y

int_ne_reif

predicate int_ne_reif(var int: x, var int: y, var bool: b)

b \(\leftrightarrow\) (x ≠ y)

int_plus

predicate int_plus(var int: x, var int: y, var int: z)

Constrains x + y = z

int_pow

predicate int_pow(var int: x, var int: y, var int: z)

Constrains z = \({\bf x} ^ {{\bf y}}\), {bf z} is constrained to 1 div pow(x, abs(y)) when \({\bf y} < 0\)

int_times

predicate int_times(var int: x, var int: y, var int: z)

Constrains x * y = z

set_in

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

Constrains x \(\in\) s