Array constraints

Constraints that relate an array to one of its elements, to an extremum, or to a rearrangement of itself. The if_then_else family belongs here too: it picks an element as element does, by the first condition that holds rather than by an index.

Each is named for the type of the array’s elements, so int_array_element selects from an array of integers and bool_array_element from an array of Booleans.

There is one element constraint per element type, not two. FZnSO’s var int argument type accepts a constant, so an array of constants needs no separate identifier.

Wherever a constraint names a position in an array, an offset argument travels with that array and gives the number its first element is at, so index is read in the caller’s own numbering rather than in the flat list’s. Pass 1 for an array numbered from one; nothing here assumes it.

35 constraints

bool_array_arg_max

bool_array_arg_max(list of var bool: xs, int: offset, var int: index)

The index holds the position of the first element that holds.

$$\mathit{xs}_{\mathit{index} - \mathit{offset} + 1} \;\wedge\; \forall j < \mathit{index} : \neg \mathit{xs}_{j - \mathit{offset} + 1}$$

index is given in the caller’s numbering, which starts at offset.

bool_array_arg_min

bool_array_arg_min(list of var bool: xs, int: offset, var int: index)

The index holds the position of the first element that does not hold.

$$\neg \mathit{xs}_{\mathit{index} - \mathit{offset} + 1} \;\wedge\; \forall j < \mathit{index} : \mathit{xs}_{j - \mathit{offset} + 1}$$

index is given in the caller’s numbering, which starts at offset.

bool_array_arg_val

bool_array_arg_val(list of var bool: xs, int: offset, var bool: value, var int: index)

The index holds the first position at which the array takes the given value.

$$(\mathit{xs}_{\mathit{index} - \mathit{offset} + 1} \leftrightarrow \mathit{value}) \;\wedge\; \forall j < \mathit{index} : \neg (\mathit{xs}_{j - \mathit{offset} + 1} \leftrightarrow \mathit{value})$$

bool_array_element

bool_array_element(list of var bool: xs, int: offset, var int: index, var bool: value)

Selects the element of a Boolean array at a variable index.

$$\mathit{value} \leftrightarrow \mathit{xs}_{\mathit{index} - \mathit{offset} + 1}$$

bool_array_element_nd

bool_array_element_nd(list of var bool: xs, list of int: offsets, list of int: sizes, list of var int: indices, var bool: value)

Selects the element of a Boolean array of any number of dimensions, at a variable index per dimension.

$$\mathit{value} = \mathit{xs}_{1 + \sum_{d} (\mathit{indices}_d - \mathit{offsets}_d) \prod_{e > d} \mathit{sizes}_e}$$

offsets and sizes describe one dimension each and must be the same length as indices; xs holds the array flattened row-major, so the last dimension varies fastest. The one-dimensional case is this constraint with single-element lists, but bool_array_element is kept because a solver’s propagator for it is a different one.

bool_array_member

bool_array_member(list of var bool: xs, var bool: value)

also declarable as bool_array_member_reif and bool_array_member_imp

The value occurs somewhere in the array.

$$\exists i : \mathit{xs}_i \leftrightarrow \mathit{value}$$

bool_if_then_else

bool_if_then_else(list of var bool: conditions, list of var bool: values, var bool: result)

The result takes the value whose condition is the first that holds.

$$\forall i : \left( \mathit{conditions}_i \wedge \forall j < i : \neg \mathit{conditions}_j \right) \rightarrow \mathit{result} \leftrightarrow \mathit{values}_i$$

float_array_arg_max

float_array_arg_max(list of var float: xs, int: offset, var int: index)

The index holds the position of a largest element, choosing the first on a tie.

$$\mathit{xs}_{\mathit{index} - \mathit{offset} + 1} = \max_{j} \mathit{xs}_j \;\wedge\; \forall j < \mathit{index} : \mathit{xs}_{j - \mathit{offset} + 1} < \mathit{xs}_{\mathit{index} - \mathit{offset} + 1}$$

float_array_arg_min

float_array_arg_min(list of var float: xs, int: offset, var int: index)

The index holds the position of a smallest element, choosing the first on a tie.

$$\mathit{xs}_{\mathit{index} - \mathit{offset} + 1} = \min_{j} \mathit{xs}_j \;\wedge\; \forall j < \mathit{index} : \mathit{xs}_{j - \mathit{offset} + 1} > \mathit{xs}_{\mathit{index} - \mathit{offset} + 1}$$

float_array_arg_sort

float_array_arg_sort(list of var float: xs, int: offset, list of var int: permutation)

The permutation lists the positions of the array’s elements in sorted order.

$$\forall i < j : \mathit{xs}_{\mathit{permutation}_i - \mathit{offset} + 1} \leq \mathit{xs}_{\mathit{permutation}_j - \mathit{offset} + 1}$$

float_array_arg_val

float_array_arg_val(list of var float: xs, int: offset, var float: value, var int: index)

The index holds the first position at which the array takes the given value.

$$\mathit{xs}_{\mathit{index} - \mathit{offset} + 1} = \mathit{value} \;\wedge\; \forall j < \mathit{index} : \mathit{xs}_{j - \mathit{offset} + 1} \neq \mathit{value}$$

float_array_element

float_array_element(list of var float: xs, int: offset, var int: index, var float: value)

Selects the element of a float array at a variable index.

$$\mathit{value} = \mathit{xs}_{\mathit{index} - \mathit{offset} + 1}$$

float_array_element_nd

float_array_element_nd(list of var float: xs, list of int: offsets, list of int: sizes, list of var int: indices, var float: value)

Selects the element of a float array of any number of dimensions, at a variable index per dimension.

$$\mathit{value} = \mathit{xs}_{1 + \sum_{d} (\mathit{indices}_d - \mathit{offsets}_d) \prod_{e > d} \mathit{sizes}_e}$$

offsets and sizes describe one dimension each and must be the same length as indices; xs holds the array flattened row-major, so the last dimension varies fastest. The one-dimensional case is this constraint with single-element lists, but float_array_element is kept because a solver’s propagator for it is a different one.

float_array_maximum

float_array_maximum(list of var float: xs, var float: value)

The value is the largest element of a non-empty array.

$$\mathit{value} = \max_{i} \mathit{xs}_i$$

float_array_member

float_array_member(list of var float: xs, var float: value)

also declarable as float_array_member_reif and float_array_member_imp

The value occurs somewhere in the array.

$$\exists i : \mathit{xs}_i = \mathit{value}$$

float_array_minimum

float_array_minimum(list of var float: xs, var float: value)

The value is the smallest element of a non-empty array.

$$\mathit{value} = \min_{i} \mathit{xs}_i$$

float_if_then_else

float_if_then_else(list of var bool: conditions, list of var float: values, var float: result)

The result takes the value whose condition is the first that holds.

$$\forall i : \left( \mathit{conditions}_i \wedge \forall j < i : \neg \mathit{conditions}_j \right) \rightarrow \mathit{result} = \mathit{values}_i$$

int_array_arg_max

int_array_arg_max(list of var int: xs, int: offset, var int: index)

The index holds the position of a largest element, choosing the first on a tie.

$$\mathit{xs}_{\mathit{index} - \mathit{offset} + 1} = \max_{j} \mathit{xs}_j \;\wedge\; \forall j < \mathit{index} : \mathit{xs}_{j - \mathit{offset} + 1} < \mathit{xs}_{\mathit{index} - \mathit{offset} + 1}$$

xs must be non-empty. index is given in the caller’s numbering, which starts at offset. Ties resolve to the lowest index, so the result is unique.

int_array_arg_min

int_array_arg_min(list of var int: xs, int: offset, var int: index)

The index holds the position of a smallest element, choosing the first on a tie.

$$\mathit{xs}_{\mathit{index} - \mathit{offset} + 1} = \min_{j} \mathit{xs}_j \;\wedge\; \forall j < \mathit{index} : \mathit{xs}_{j - \mathit{offset} + 1} > \mathit{xs}_{\mathit{index} - \mathit{offset} + 1}$$

xs must be non-empty. index is given in the caller’s numbering, which starts at offset.

int_array_arg_sort

int_array_arg_sort(list of var int: xs, int: offset, list of var int: permutation)

The permutation lists the positions of the array’s elements in sorted order.

$$\forall i < j : \mathit{xs}_{\mathit{permutation}_i - \mathit{offset} + 1} \leq \mathit{xs}_{\mathit{permutation}_j - \mathit{offset} + 1}$$

permutation holds positions in xs, numbered from offset. Ties resolve to the lower original position, so the result is unique.

int_array_arg_val

int_array_arg_val(list of var int: xs, int: offset, var int: value, var int: index)

The index holds the first position at which the array takes the given value.

$$\mathit{xs}_{\mathit{index} - \mathit{offset} + 1} = \mathit{value} \;\wedge\; \forall j < \mathit{index} : \mathit{xs}_{j - \mathit{offset} + 1} \neq \mathit{value}$$

int_array_element

int_array_element(list of var int: xs, int: offset, var int: index, var int: value)

Selects the element of an integer array at a variable index.

$$\mathit{value} = \mathit{xs}_{\mathit{index} - \mathit{offset} + 1}$$

int_array_element_nd

int_array_element_nd(list of var int: xs, list of int: offsets, list of int: sizes, list of var int: indices, var int: value)

Selects the element of a int array of any number of dimensions, at a variable index per dimension.

$$\mathit{value} = \mathit{xs}_{1 + \sum_{d} (\mathit{indices}_d - \mathit{offsets}_d) \prod_{e > d} \mathit{sizes}_e}$$

offsets and sizes describe one dimension each and must be the same length as indices; xs holds the array flattened row-major, so the last dimension varies fastest. The one-dimensional case is this constraint with single-element lists, but int_array_element is kept because a solver’s propagator for it is a different one.

int_array_maximum

int_array_maximum(list of var int: xs, var int: value)

The value is the largest element of a non-empty array.

$$\mathit{value} = \max_{i} \mathit{xs}_i$$

xs must be non-empty. The binary maximum is this constraint with a two-element list.

int_array_member

int_array_member(list of var int: xs, var int: value)

also declarable as int_array_member_reif and int_array_member_imp

The value occurs somewhere in the array.

$$\exists i : \mathit{xs}_i = \mathit{value}$$

int_array_minimum

int_array_minimum(list of var int: xs, var int: value)

The value is the smallest element of a non-empty array.

$$\mathit{value} = \min_{i} \mathit{xs}_i$$

xs must be non-empty.

int_array_sort

int_array_sort(list of var int: xs, list of var int: ys)

The second array is the first sorted into non-decreasing order.

$$\left( \forall v : \lvert \{\, i \mid \mathit{xs}_i = v \,\} \rvert = \lvert \{\, i \mid \mathit{ys}_i = v \,\} \rvert \right) \;\wedge\; \forall i < j : \mathit{ys}_i \leq \mathit{ys}_j$$

xs and ys must have equal length.

int_array_write

int_array_write(list of var int: xs, int: offset, var int: index, var int: value, list of var int: result)

The result equals the array with one position overwritten.

$$\mathit{result}_j = \begin{cases} \mathit{value} & \text{if } j = \mathit{index} - \mathit{offset} + 1 \\ \mathit{xs}_j & \text{otherwise} \end{cases}$$

xs and result must have equal length. The array analogue of an assignment, for modelling state that changes step by step.

int_array_writes

int_array_writes(list of var int: xs, int: offset, list of var int: index, list of var int: value, list of var int: result)

also declarable as int_array_writes_reif and int_array_writes_imp

The result equals the array with several positions overwritten at once.

$$\left( \forall k : \mathit{result}_{\mathit{index}_k - \mathit{offset} + 1} = \mathit{value}_k \right) \wedge \forall j : \left( \forall k : \mathit{index}_k - \mathit{offset} + 1 \neq j \right) \rightarrow \mathit{result}_j = \mathit{xs}_j$$

index and value must have equal length, as must xs and result. Two writes to one position must agree; int_array_writes_sequential lets the later one win instead.

int_array_writes_sequential

int_array_writes_sequential(list of var int: xs, int: offset, list of var int: index, list of var int: value, list of var int: result)

The result equals the array with the writes applied in order, the last to a position winning.

$$\mathit{result}_j = \begin{cases} \mathit{value}_{k} & \text{where } k = \max \{\, k \mid \mathit{index}_k - \mathit{offset} + 1 = j \,\} \\ \mathit{xs}_j & \text{if no such } k \end{cases}$$

int_if_then_else

int_if_then_else(list of var bool: conditions, list of var int: values, var int: result)

The result takes the value whose condition is the first that holds.

$$\forall i : \left( \mathit{conditions}_i \wedge \forall j < i : \neg \mathit{conditions}_j \right) \rightarrow \mathit{result} = \mathit{values}_i$$

conditions and values must have equal length. With no condition holding the result is unconstrained; an else branch is a final condition fixed to true.

set_of_int_array_element

set_of_int_array_element(list of var set of int: xs, int: offset, var int: index, var set of int: value)

Selects the element of an array of sets at a variable index.

$$\mathit{value} = \mathit{xs}_{\mathit{index} - \mathit{offset} + 1}$$

set_of_int_array_element_nd

set_of_int_array_element_nd(list of var set of int: xs, list of int: offsets, list of int: sizes, list of var int: indices, var set of int: value)

Selects the element of a set array of any number of dimensions, at a variable index per dimension.

$$\mathit{value} = \mathit{xs}_{1 + \sum_{d} (\mathit{indices}_d - \mathit{offsets}_d) \prod_{e > d} \mathit{sizes}_e}$$

offsets and sizes describe one dimension each and must be the same length as indices; xs holds the array flattened row-major, so the last dimension varies fastest. The one-dimensional case is this constraint with single-element lists, but set_of_int_array_element is kept because a solver’s propagator for it is a different one.

set_of_int_array_member

set_of_int_array_member(list of var set of int: xs, var set of int: value)

also declarable as set_of_int_array_member_reif and set_of_int_array_member_imp

The value occurs somewhere in the array.

$$\exists i : \mathit{xs}_i = \mathit{value}$$

set_of_int_if_then_else

set_of_int_if_then_else(list of var bool: conditions, list of var set of int: values, var set of int: result)

The result takes the value whose condition is the first that holds.

$$\forall i : \left( \mathit{conditions}_i \wedge \forall j < i : \neg \mathit{conditions}_j \right) \rightarrow \mathit{result} = \mathit{values}_i$$