# 4.2.1. Global constraints¶

These constraints represent high-level modelling abstractions, for which many solvers implement special, efficient inference algorithms.

## 4.2.1.2. Lexicographic constraints¶

```
predicate lex2(array [int,int] of var int: x)
```

Require adjacent rows and adjacent columns in the array `x` to be
lexicographically ordered. Adjacent rows and adjacent columns may be equal.

```
predicate lex_greater(array [int] of var bool: x,
array [int] of var bool: y)
```

Requires that the array `x` is strictly lexicographically greater than
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_greater(array [int] of var int: x,
array [int] of var int: y)
```

Requires that the array `x` is strictly lexicographically greater than
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_greater(array [int] of var float: x,
array [int] of var float: y)
```

Requires that the array `x` is strictly lexicographically greater than
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_greater(array [int] of var set of int: x,
array [int] of var set of int: y)
```

`x` is strictly lexicographically greater than
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_greatereq(array [int] of var bool: x,
array [int] of var bool: y)
```

Requires that the array `x` is lexicographically greater than or equal to
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_greatereq(array [int] of var int: x,
array [int] of var int: y)
```

Requires that the array `x` is lexicographically greater than or equal to
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_greatereq(array [int] of var float: x,
array [int] of var float: y)
```

Requires that the array `x` is lexicographically greater than or equal to
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_greatereq(array [int] of var set of int: x,
array [int] of var set of int: y)
```

`x` is lexicographically greater than or equal to
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_less(array [int] of var bool: x,
array [int] of var bool: y)
```

Requires that the array `x` is strictly lexicographically less than
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_less(array [int] of var int: x,
array [int] of var int: y)
```

Requires that the array `x` is strictly lexicographically less than
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_less(array [int] of var float: x,
array [int] of var float: y)
```

Requires that the array `x` is strictly lexicographically less than
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_less(array [int] of var set of int: x,
array [int] of var set of int: y)
```

`x` is strictly lexicographically less than
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_lesseq(array [int] of var bool: x,
array [int] of var bool: y)
```

Requires that the array `x` is lexicographically less than or equal to
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_lesseq(array [int] of var float: x,
array [int] of var float: y)
```

Requires that the array `x` is lexicographically less than or equal to
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_lesseq(array [int] of var int: x,
array [int] of var int: y)
```

Requires that the array `x` is lexicographically less than or equal to
array `y` . Compares them from first to last element, regardless of indices.

```
predicate lex_lesseq(array [int] of var set of int: x,
array [int] of var set of int: y)
```

`x` is lexicographically less than or equal to
array `y` . Compares them from first to last element, regardless of indices.

```
predicate strict_lex2(array [int,int] of var int: x)
```

Require adjacent rows and adjacent columns in the array `x` to be
lexicographically ordered. Adjacent rows and adjacent columns cannot be equal.

```
predicate value_precede(int: s, int: t, array [int] of var int: x)
```

Requires that `s` precede `t` in the array `x` .

Precedence means that if any element of `x`
is equal to `t` , then another element of `x` with a lower index is equal
to `s` .

```
predicate value_precede(int: s,
int: t,
array [int] of var set of int: x)
```

Requires that `s` precede `t` in the array `x` .

Precedence means that if an element of `x`
contains `t` but not `s` , then another element of `x` with lower index contains
`s` but not `t` .

```
predicate value_precede_chain(array [int] of int: c,
array [int] of var int: x)
```

Requires that `c` [ `i` ] precedes `c` [ `i` +1] in the array `x` .

Precedence means that if any element of `x`
is equal to `\a` c[ `i` +1], then another element of `x` with a lower index is equal
to `\a` c[ `i` ].

```
predicate value_precede_chain(array [int] of int: c,
array [int] of var set of int: x)
```

Requires that `c` [ `i` ] precedes `c` [ `i` +1] in the array `x` .

Precedence means that if an element of `x`
contains `\a` c[ `i` +1] but not `\a` c[ `i` ], then another element of `x` with lower index contains
`\a` c[ `i` ] but not `\a` c[ `i` +1].

## 4.2.1.3. Sorting constraints¶

```
function array [int] of var int: arg_sort(array [int] of var int: x)
```

Returns the permutation `p` which causes `x` to be in sorted order hence
`x` [ `p` [ `i` ]] <= `x` [ `p` [ `i` +1]].

The permutation is the stable sort hence `x` [ `p` [ `i` ]] = `x` [ `p` [ `i` +1]] \(\rightarrow\) `p` [ `i` ] < `p` [ `i` +1].

```
function array [int] of var int: arg_sort(array [int] of var float: x)
```

Returns the permutation `p` which causes `x` to be in sorted order hence
`x` [ `p` [ `i` ]] <= `x` [ `p` [ `i` +1]].

The permutation is the stable sort hence `x` [ `p` [ `i` ]] = `x` [ `p` [ `i` +1]] \(\rightarrow\) `p` [ `i` ] < `p` [ `i` +1].

```
predicate arg_sort(array [int] of var int: x,
array [int] of var int: p)
```

Constrains `p` to be the permutation which causes `x` to be in sorted order hence
`x` [ `p` [ `i` ]] <= `x` [ `p` [ `i` +1]].

The permutation is the stable sort hence `x` [ `p` [ `i` ]] = `x` [ `p` [ `i` +1]] \(\rightarrow\) `p` [ `i` ] < `p` [ `i` +1].

```
predicate arg_sort(array [int] of var float: x,
array [int] of var int: p)
```

Constrains `p` to be the permutation which causes `x` to be in sorted order hence
`x` [ `p` [ `i` ]] <= `x` [ `p` [ `i` +1]].

`x` [ `p` [ `i` ]] = `x` [ `p` [ `i` +1]] \(\rightarrow\) `p` [ `i` ] < `p` [ `i` +1].

```
predicate decreasing(array [int] of var bool: x)
```

Requires that the array `x` is in decreasing order (duplicates are allowed).

```
predicate decreasing(array [int] of var float: x)
```

Requires that the array `x` is in decreasing order (duplicates are allowed).

```
predicate decreasing(array [int] of var int: x)
```

Requires that the array `x` is in decreasing order (duplicates are allowed).

```
predicate decreasing(array [int] of var set of int: x)
```

Requires that the array `x` is in decreasing order (duplicates are allowed).

```
predicate increasing(array [int] of var bool: x)
```

Requires that the array `x` is in increasing order (duplicates are allowed).

```
predicate increasing(array [int] of var float: x)
```

Requires that the array `x` is in increasing order (duplicates are allowed).

```
predicate increasing(array [int] of var int: x)
```

Requires that the array `x` is in increasing order (duplicates are allowed).

```
predicate increasing(array [int] of var set of int: x)
```

Requires that the array `x` is in increasing order (duplicates are allowed).

```
predicate sort(array [int] of var int: x, array [int] of var int: y)
```

Requires that the multiset of values in `x` are the same as the
multiset of values in `y` but `y` is in sorted order.

```
function array [int] of var int: sort(array [int] of var int: x)
```

Return a multiset of values that is the same as the
multiset of values in `x` but in sorted order.

## 4.2.1.4. Channeling constraints¶

```
predicate int_set_channel(array [int] of var int: x,
array [int] of var set of int: y)
```

Requires that array of int variables `x` and array of set variables `y`
are related such that ( `x` [ `i` ] = `j` ) ↔ ( `i` in `y` [ `j` ]).

```
predicate inverse(array [int] of var int: f,
array [int] of var int: invf)
```

Constrains two arrays of int variables, `f` and `invf` , to represent
inverse functions. All the values in each array must be within the index
set of the other array.

```
function array [int] of var int: inverse(array [int] of var int: f)
```

Given a function `f` represented as an array, return the inverse function.

```
predicate inverse_set(array [int] of var set of int: f,
array [int] of var set of int: invf)
```

Constrains two arrays of set of int variables, `f` and `invf` , so that
a `j` in f[ `i` ] iff `i` in invf[ `j` ]. All the values in each array’s sets
must be within the index set of the other array.

```
predicate link_set_to_booleans(var set of int: s,
array [int] of var bool: b)
```

Constrain the array of Booleans `b` to be a representation of the set `s` :
`i` in `s` ↔ `b` [ `i` ].

The index set of `b` must be a superset of the possible values of `s` .

## 4.2.1.5. Counting constraints¶

```
predicate among(var int: n, array [int] of var int: x, set of int: v)
```

Requires exactly `n` variables in `x` to take one of the values in `v` .

```
function var int: among(array [int] of var int: x, set of int: v)
```

Returns the number of variables in `x` that take one of the values in `v` .

```
predicate at_least(int: n, array [int] of var int: x, int: v)
```

Requires at least `n` variables in `x` to take the value `v` .

```
predicate at_least(int: n,
array [int] of var set of int: x,
set of int: v)
```

Requires at least `n` variables in `x` to take the value `v` .

```
predicate at_most(int: n, array [int] of var int: x, int: v)
```

Requires at most `n` variables in `x` to take the value `v` .

```
predicate at_most(int: n,
array [int] of var set of int: x,
set of int: v)
```

Requires at most `n` variables in `x` to take the value `v` .

```
predicate at_most1(array [int] of var set of int: s)
```

Requires that each pair of sets in `s` overlap in at most one element.

```
predicate count(array [int] of var int: x, var int: y, var int: c)
```

Constrains `c` to be the number of occurrences of `y` in `x` .

```
function var int: count(array [int] of var int: x, var int: y)
```

Returns the number of occurrences of `y` in `x` .

```
predicate count_eq(array [int] of var int: x, var int: y, var int: c)
```

Constrains `c` to be the number of occurrences of `y` in `x` .

```
predicate count_geq(array [int] of var int: x, var int: y, var int: c)
```

Constrains `c` to be greater than or equal to the number of occurrences
of `y` in `x` .

```
predicate count_gt(array [int] of var int: x, var int: y, var int: c)
```

Constrains `c` to be strictly greater than the number of occurrences
of `y` in `x` .

```
predicate count_leq(array [int] of var int: x, var int: y, var int: c)
```

Constrains `c` to be less than or equal to the number of occurrences
of `y` in `x` .

```
predicate count_lt(array [int] of var int: x, var int: y, var int: c)
```

Constrains `c` to be strictly less than the number of occurrences
of `y` in `x` .

```
predicate count_neq(array [int] of var int: x, var int: y, var int: c)
```

Constrains `c` to be not equal to the number of occurrences
of `y` in `x` .

```
predicate distribute(array [int] of var int: card,
array [int] of var int: value,
array [int] of var int: base)
```

Requires that `card` [ `i` ] is the number of occurences of `value` [ `i` ] in
`base` . The values in `value` need not be distinct.

```
function array [int] of var int: distribute(array [int] of var int: value,
array [int] of var int: base)
```

Returns an array of the number of occurences of `value` [ `i` ] in
`base` . The values in `value` need not be distinct.

```
predicate exactly(int: n, array [int] of var int: x, int: v)
```

Requires exactly `n` variables in `x` to take the value `v` .

```
predicate exactly(int: n,
array [int] of var set of int: x,
set of int: v)
```

Requires exactly `n` variables in `x` to take the value `v` .

```
predicate global_cardinality(array [int] of var int: x,
array [int] of int: cover,
array [int] of var int: counts)
```

Requires that the number of occurrences of `cover` [ `i` ] in `x` is `counts` [ `i` ].

```
function array [int] of var int: global_cardinality(array [int] of var int: x,
array [int] of int: cover)
```

Returns the number of occurrences of `cover` [ `i` ] in `x` .

```
predicate global_cardinality_closed(array [int] of var int: x,
array [int] of int: cover,
array [int] of var int: counts)
```

Requires that the number of occurences of `i` in `x` is `counts` [ `i` ].

The elements of `x` must take their values from `cover` .

```
function array [int] of var int: global_cardinality_closed(array [int] of var int: x,
array [int] of int: cover)
```

Returns an array with number of occurences of `i` in `x` .

The elements of `x` must take their values from `cover` .

```
predicate global_cardinality_low_up(array [int] of var int: x,
array [int] of int: cover,
array [int] of int: lbound,
array [int] of int: ubound)
```

Requires that for all `i` , the value `cover` [ `i` ] appears at least `lbound` [ `i` ]
and at most `ubound` [ `i` ] times in the array `x` .

```
predicate global_cardinality_low_up_closed(array [int] of var int: x,
array [int] of int: cover,
array [int] of int: lbound,
array [int] of int: ubound)
```

Requires that for all `i` , the value `cover` [ `i` ] appears at least `lbound` [ `i` ]
and at most `ubound` [ `i` ] times in the array `x` .

The elements of `x` must take their values from `cover` .

## 4.2.1.6. Packing constraints¶

```
predicate bin_packing(int: c,
array [int] of var int: bin,
array [int] of int: w)
```

Requires that each item `i` with weight `w` [ `i` ], be put into `bin` [ `i` ] such
that the sum of the weights of the items in each bin does not exceed the
capacity `c` .

Assumptions:

- forall
`i`,`w`[`i`] >=0 `c`>=0

```
predicate bin_packing_capa(array [int] of int: c,
array [int] of var int: bin,
array [int] of int: w)
```

Requires that each item `i` with weight `w` [ `i` ], be put into `bin` [ `i` ] such
that the sum of the weights of the items in each bin `b` does not exceed the
capacity `c` [ `b` ].

Assumptions:

- forall
`i`,`w`[`i`] >=0 - forall
`b`,`c`[`b`] >=0

```
predicate bin_packing_load(array [int] of var int: load,
array [int] of var int: bin,
array [int] of int: w)
```

Requires that each item `i` with weight `w` [ `i` ], be put into `bin` [ `i` ] such
that the sum of the weights of the items in each bin `b` is equal to
`load` [ `b` ].

Assumptions:

- forall
`i`,`w`[`i`] >=0

```
function array [int] of var int: bin_packing_load(array [int] of var int: bin,
array [int] of int: w)
```

Returns the load of each bin resulting from packing each item `i` with
weight `w` [ `i` ] into `bin` [ `i` ], where the load is defined as
the sum of the weights of the items in each bin.

Assumptions:

- forall
`i`,`w`[`i`] >=0

```
predicate diffn(array [int] of var int: x,
array [int] of var int: y,
array [int] of var int: dx,
array [int] of var int: dy)
```

Constrains rectangles `i` , given by their origins ( `x` [ `i` ], `y` [ `i` ])
and sizes ( `dx` [ `i` ], `dy` [ `i` ]), to be non-overlapping. Zero-width
rectangles can still not overlap with any other rectangle.

```
predicate diffn_k(array [int,int] of var int: box_posn,
array [int,int] of var int: box_size)
```

Constrains `k` -dimensional boxes to be non-overlapping. For each box `i`
and dimension `j` , `box_posn` [ `i` , `j` ] is the base position of the box
in dimension `j` , and `box_size` [ `i` , `j` ] is the size in that dimension.
Boxes whose size is 0 in any dimension still cannot overlap with any other box.

```
predicate diffn_nonstrict(array [int] of var int: x,
array [int] of var int: y,
array [int] of var int: dx,
array [int] of var int: dy)
```

Constrains rectangles `i` , given by their origins ( `x` [ `i` ], `y` [ `i` ])
and sizes ( `dx` [ `i` ], `dy` [ `i` ]), to be non-overlapping. Zero-width
rectangles can be packed anywhere.

```
predicate diffn_nonstrict_k(array [int,int] of var int: box_posn,
array [int,int] of var int: box_size)
```

Constrains `k` -dimensional boxes to be non-overlapping. For each box `i`
and dimension `j` , `box_posn` [ `i` , `j` ] is the base position of the box
in dimension `j` , and `box_size` [ `i` , `j` ] is the size in that dimension.
Boxes whose size is 0 in at least one dimension can be packed anywhere.

```
predicate geost(int: k,
array [int,int] of int: rect_size,
array [int,int] of int: rect_offset,
array [int] of set of int: shape,
array [int,int] of var int: x,
array [int] of var int: kind)
```

A global non-overlap constraint for `k` dimensional objects. It enforces that no two objects overlap.

Parameters:

`k`: the number of dimensions`rect_size`: the size of each box in`k`dimensios`rect_offset`: the offset of each box from the base position in`k`dimensions`shape`: the set of rectangles defining the`i`-th shape. Assumption: Each pair of boxes in a shape must not overlap.`x`: the base position of each object.`x`[`i`,`j`] is the position of object`i`in. dimension`j`.`kind`: the shape used by each object.

```
predicate geost_bb(int: k,
array [int,int] of int: rect_size,
array [int,int] of int: rect_offset,
array [int] of set of int: shape,
array [int,int] of var int: x,
array [int] of var int: kind,
array [int] of var int: l,
array [int] of var int: u)
```

A global non-overlap constraint for `k` dimensional objects. It enforces that no two objects overlap, and that all objects fit within a global `k` dimensional bounding box.

Parameters:

`k`: the number of dimensions`rect_size`: the size of each box in`k`dimensios`rect_offset`: the offset of each box from the base position in`k`dimensions`shape`: the set of rectangles defining the`i`-th shape. Assumption: Each pair of boxes in a shape must not overlap.`x`: the base position of each object.`x`[`i`,`j`] is the position of object`i`in dimension`j`.`kind`: the shape used by each object.`l`: is an array of lower bounds,`l`[`i`] is the minimum bounding box for all objects in dimension`i`.`u`: is an array of upper bounds,`u`[`i`] is the maximum bounding box for all objects in dimension`i`.

```
predicate geost_smallest_bb(int: k,
array [int,int] of int: rect_size,
array [int,int] of int: rect_offset,
array [int] of set of int: shape,
array [int,int] of var int: x,
array [int] of var int: kind,
array [int] of var int: l,
array [int] of var int: u)
```

A global non-overlap constraint for `k` dimensional objects. It enforces that no two objects overlap, and that all objects fit within a global `k` dimensional bounding box. In addition, it enforces that the bounding box is the smallest one containing all objects, i.e., each of the `2k` boundaries is touched by at least by one object.

Parameters:

`k`: the number of dimensions`rect_size`: the size of each box in`k`dimensios`rect_offset`: the offset of each box from the base position in`k`dimensions`shape`: the set of rectangles defining the`i`-th shape. Assumption: Each pair of boxes in a shape must not overlap.`x`: the base position of each object.`x`[`i`,`j`] is the position of object`i`in dimension`j`.`kind`: the shape used by each object.`l`: is an array of lower bounds,`l`[`i`] is the minimum bounding box for all objects in dimension`i`.`u`: is an array of upper bounds,`u`[`i`] is the maximum bounding box for all objects in dimension`i`.

```
predicate knapsack(array [int] of int: w,
array [int] of int: p,
array [int] of var int: x,
var int: W,
var int: P)
```

Requires that items are packed in a knapsack with certain weight and profit restrictions.

Assumptions:

- Weights
wand profitspmust be non-negativew,pandxmust have the same index sets

Parameters:

`w`: weight of each type of item`p`: profit of each type of item`x`: number of items of each type that are packed`W`: sum of sizes of all items in the knapsack`P`: sum of profits of all items in the knapsack

## 4.2.1.7. Scheduling constraints¶

```
predicate alternative(var opt int: s0,
var int: d0,
array [int] of var opt int: s,
array [int] of var int: d)
```

Alternative constraint for optional tasks. Task ( `s0` , `d0` ) spans the
optional tasks ( `s` [ `i` ], `d` [ `i` ]) in the array arguments
and at most one can occur

```
predicate cumulative(array [int] of var int: s,
array [int] of var int: d,
array [int] of var int: r,
var int: b)
```

Requires that a set of tasks given by start times `s` , durations `d` , and
resource requirements `r` , never require more than a global resource bound
`b` at any one time.

Assumptions:

- forall
`i`,`d`[`i`] >= 0 and`r`[`i`] >= 0

```
predicate cumulative(array [int] of var opt int: s,
array [int] of var int: d,
array [int] of var int: r,
var int: b)
```

Requires that a set of tasks given by start times `s` , durations `d` , and
resource requirements `r` , never require more than a global resource bound
`b` at any one time. Start times are optional variables, so
that absent tasks do not need to be scheduled.

Assumptions:
- forall `i` , `d` [ `i` ] >= 0 and `r` [ `i` ] >= 0

```
predicate disjunctive(array [int] of var int: s,
array [int] of var int: d)
```

Requires that a set of tasks given by start times `s` and durations `d`
do not overlap in time. Tasks with duration 0 can be scheduled at any time,
even in the middle of other tasks.

Assumptions:

- forall
`i`,`d`[`i`] >= 0

```
predicate disjunctive(array [int] of var opt int: s,
array [int] of var int: d)
```

Requires that a set of tasks given by start times `s` and durations `d`
do not overlap in time. Tasks with duration 0 can be scheduled at any time,
even in the middle of other tasks. Start times are optional variables, so
that absent tasks do not need to be scheduled.

Assumptions:

- forall
`i`,`d`[`i`] >= 0

```
predicate disjunctive_strict(array [int] of var int: s,
array [int] of var int: d)
```

Requires that a set of tasks given by start times `s` and durations `d`
do not overlap in time. Tasks with duration 0 CANNOT be scheduled at any time,
but only when no other task is running.

Assumptions:

- forall
`i`,`d`[`i`] >= 0

```
predicate disjunctive_strict(array [int] of var opt int: s,
array [int] of var int: d)
```

Requires that a set of tasks given by start times `s` and durations `d`
do not overlap in time. Tasks with duration 0 CANNOT be scheduled at any time,
but only when no other task is running. Start times are optional variables, so
that absent tasks do not need to be scheduled.

Assumptions:

- forall
`i`,`d`[`i`] >= 0

```
predicate span(var opt int: s0,
var int: d0,
array [int] of var opt int: s,
array [int] of var int: d)
```

Span constraint for optional tasks. Task ( `s0` , `d0` ) spans the optional
tasks ( `s` [ `i` ], `d` [ `i` ]) in the array arguments.

## 4.2.1.8. Extensional constraints (table, regular etc.)¶

```
predicate regular(array [int] of var int: x,
int: Q,
int: S,
array [int,int] of int: d,
int: q0,
set of int: F)
```

The sequence of values in array `x` (which must all be in the range 1.. `S` )
is accepted by the DFA of `Q` states with input 1.. `S` and transition
function `d` (which maps (1.. `Q` , 1.. `S` ) -> 0.. `Q` )) and initial state `q0`
(which must be in 1.. `Q` ) and accepting states `F` (which all must be in
1.. `Q` ). We reserve state 0 to be an always failing state.

```
predicate regular(array [int] of var int: x, string: r)
```

The sequence of values in array `x` is accepted by the regular
expression `r` . This constraint generates it’s DFA equivalent.

Regular expressions can use the following syntax:

- Selection:
- Concatenation: “12 34”, 12 followed by 34. (Characters are assumed to be the part of the same number unless split by syntax or whitespace.)
- Union: “7|11”, a 7 or 11.
- Groups: “7(6|8)”, a 7 followed by a 6 or an 8.
- Wildcard: “.”, any value within the domain.
- Classes: “[3-6 7]”, a 3,4,5,6, or 7.
- Negated classes: “[^3 5]”, any value within the domain except for a 3 or a 5.

- Quantifiers:
- Asterisk: “12*”, 0 or more times a 12.
- Question mark: “5?”, 0 or 1 times a 5. (optional)
- Plus sign: “42+”, 1 or more time a 42.
- Exact: “1{3}”, exactly 3 times a 1.
- At least: “9{5,}”, 5 or more times a 9.
- Between: “7{3,5}”, at least 3 times, but at most 5 times a 7.

Members of enumerated types can be used in place of any integer (e.g., “A B”, A followed by B). Enumerated identifiers still use whitespace for concatenation.

```
predicate regular_nfa(array [int] of var int: x,
int: Q,
int: S,
array [int,int] of set of int: d,
int: q0,
set of int: F)
```

The sequence of values in array `x` (which must all be in the range 1.. `S` )
is accepted by the NFA of `Q` states with input 1.. `S` and transition
function `d` (which maps (1.. `Q` , 1.. `S` ) -> set of 1.. `Q` )) and initial state `q0`
(which must be in 1.. `Q` ) and accepting states `F` (which all must be in
1.. `Q` ).

```
predicate table(array [int] of var bool: x, array [int,int] of bool: t)
```

Represents the constraint `x` in `t` where we
consider each row in `t` to be a tuple and `t` as a set of tuples.

```
predicate table(array [int] of var int: x, array [int,int] of int: t)
```

Represents the constraint `x` in `t` where we
consider each row in `t` to be a tuple and `t` as a set of tuples.

## 4.2.1.9. Other declarations¶

```
function var int: arg_max(array [int] of var int: x)
```

Returns the index of the maximum value in the array `x` .
When breaking ties the least index is returned.

```
function var int: arg_max(array [int] of var float: x)
```

Returns the index of the maximum value in the array `x` .
When breaking ties the least index is returned.

```
function var int: arg_min(array [int] of var int: x)
```

Returns the index of the minimum value in the array `x` .
When breaking ties the least index is returned.

```
function var int: arg_min(array [int] of var float: x)
```

Returns the index of the minimum value in the array `x` .
When breaking ties the least index is returned.

```
predicate circuit(array [int] of var int: x)
```

Constrains the elements of `x` to define a circuit where `x` [ `i` ] = `j` means
that `j` is the successor of `i` .

```
predicate disjoint(var set of int: s1, var set of int: s2)
```

Requires that sets `s1` and `s2` do not intersect.

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

Constrains `m` to be the maximum of the values in `x` .

Assumptions: | `x` | > 0.

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

Constrains `m` to be the maximum of the values in `x` .

Assumptions: | `x` | > 0.

```
predicate maximum_arg(array [int] of var int: x, var int: i)
```

Constrain `i` to be the index of the maximum value in the array `x` .
When breaking ties the least index is returned.

Assumption: | `x` | > 0

```
predicate maximum_arg(array [int] of var float: x, var int: i)
```

Constrain `i` to be the index of the maximum value in the array `x` .
When breaking ties the least index is returned.

Assumption: | `x` | > 0

```
predicate member(array [int] of var bool: x, var bool: y)
```

Requires that `y` occurs in the array `x` .

```
predicate member(array [int] of var float: x, var float: y)
```

Requires that `y` occurs in the array `x` .

```
predicate member(array [int] of var int: x, var int: y)
```

Requires that `y` occurs in the array `x` .

```
predicate member(array [int] of var set of int: x, var set of int: y)
```

Requires that `y` occurs in the array `x` .

```
predicate member(var set of int: x, var int: y)
```

Requires that `y` occurs in the set `x` .

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

Constrains `m` to be the minimum of the values in `x` .

Assumptions: | `x` | > 0.

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

Constrains `m` to be the minimum of the values in `x` .

Assumptions: | `x` | > 0.

```
predicate minimum_arg(array [int] of var int: x, var int: i)
```

Constrain `i` to be the index of the minimum value in the array `x` .
When breaking ties the least index is returned.

Assumption: | `x` | > 0

```
predicate minimum_arg(array [int] of var float: x, var int: i)
```

Constrain `i` to be the index of the minimum value in the array `x` .
When breaking ties the least index is returned.

Assumption: | `x` | > 0

```
predicate network_flow(array [int,1..2] of int: arc,
array [int] of int: balance,
array [int] of var int: flow)
```

Defines a network flow constraint.

Parameters:

`arc`: a directed arc of the flow network. Arc`i`connects node`arc`[`i`,1] to node`arc`[`i`,2].`balance`: the difference between input and output flow for each node.`flow`: the flow going through each arc.

```
predicate network_flow_cost(array [int,1..2] of int: arc,
array [int] of int: balance,
array [int] of int: weight,
array [int] of var int: flow,
var int: cost)
```

Defines a network flow constraint with cost.

Parameters:

`arc`: a directed arc of the flow network. Arc`i`connects node`arc`[`i`,1] to node`arc`[`i`,2].`balance`: the difference between input and output flow for each node.`weight`: the unit cost of the flow through the arc.`flow`: the flow going through each arc.`cost`: the overall cost of the flow.

```
predicate partition_set(array [int] of var set of int: S,
set of int: universe)
```

Constrains the sets in array `S` to partition the `universe` .

```
predicate range(array [int] of var int: x,
var set of int: s,
var set of int: t)
```

Requires that the image of function `x` (represented as an array) on set
of values `s` is `t` . ub( `s` ) must be a subset of index_set( `x` ) otherwise an
assertion failure will occur.

```
function var set of int: range(array [int] of var int: x,
var set of int: s)
```

Returns the image of function `x` (represented as an array) on set
of values `s` . ub( `s` ) must be a subset of index_set( `x` ) otherwise an
assertion failure will occur.

```
predicate roots(array [int] of var int: x,
var set of int: s,
var set of int: t)
```

Requires that `x` [ `i` ] in `t` for all `i` in `s`

```
function var set of int: roots(array [int] of var int: x,
var set of int: t)
```

Returns `s` such that `x` [ `i` ] in `t` for all `i` in `s`

```
predicate sliding_sum(int: low,
int: up,
int: seq,
array [int] of var int: vs)
```

Requires that in each subsequence `vs` [ `i` ], …, `vs` [ `i` + `seq` - 1] the sum of the
values belongs to the interval [ `low` , `up` ].

```
predicate subcircuit(array [int] of var int: x)
```

Constrains the elements of `x` to define a subcircuit where `x` [ `i` ] = `j`
means that `j` is the successor of `i` and `x` [ `i` ] = `i` means that `i`
is not in the circuit.

```
predicate sum_pred(var int: i,
array [int] of set of int: sets,
array [int] of int: cs,
var int: s)
```

Requires that the sum of `cs` [ `i1` ].. `cs` [ `iN` ] equals `s` ,
where `i1` .. `iN` are the elements of the `i` th set in `sets` .

Nb: not called ‘sum’ as in the constraints catalog because ‘sum’ is a MiniZinc built-in function.