# 4.2.1. Global constraints¶

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

## 4.2.1.1. Counting constraints¶

These constraints count and restrict how many times certain values occur
in an array of variables. MiniZinc will automatically generate the basic counting
constraints below from expressions such as `count(i in x)(i=c) <= d`, so you
can write models in this much more readable style instead of using these
predicates. However, if your model
contains multiple counting constraints over the same array, constraints
like `distribute` or `global_cardinality` below may be useful.

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

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

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

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

```
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_eq(array [int] of var int: x, int: y, int: c)
```

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

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

Returns 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_geq(array [int] of var int: x, int: y, 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_gt(array [int] of var int: x, int: y, 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_leq(array [int] of var int: x, int: y, 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_lt(array [int] of var int: x, int: y, 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 count_neq(array [int] of var int: x, int: y, 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 occurrences 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 occurrences of `value` [ `i` ] in
`base` . The values in `value` need not be distinct.

```
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 occurrences of `cover` [ `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 occurrences of `cover` [ `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.3. 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 seq_precede_chain(array [int] of var int: x)
```

Requires that `i` precedes `i` +1 in the array `x` for all positive `i` .

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

Requires that `i` appears in a set in array `x` before `i` +1 for all positive `i`

```
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 opt 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 `c` [ `i` +1], then another element of `x` with a lower index is equal
to `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 `c` [ `i` +1] but not `c` [ `i` ], then another element of `x` with lower index contains
`c` [ `i` ] but not `c` [ `i` +1].

## 4.2.1.4. 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.

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

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

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

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

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

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

## 4.2.1.5. 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` ) \(\leftrightarrow\) ( `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 [$$E] of var $$F: inverse(array [$$F] of var $$E: f)
```

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

```
function array [$$E] of $$F: inverse(array [$$F] of $$E: f)
```

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

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

If the `i` th variable of the collection `X` is assigned to `j` and if `j` is in the index set of `Y` then the `j` th variable of the collection `Y` is assigned to `i` .

Conversely, if the `j` th variable of the collection `Y` is assigned to `i` and if `i` is in the index set of `X` then the `i` th variable of the collection `X` is assigned to `j` .

```
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` \(\leftrightarrow\) `b` [ `i` ].

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

## 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`dimensions`rect_offset`: the offset of each box from the base position in`k`dimensions`shape`: the set of rectangles defining the`i`-th shape.`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`dimensions`rect_offset`: the offset of each box from the base position in`k`dimensions`shape`: the set of rectangles defining the`i`-th shape.`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_nonoverlap_k(array [int] of var int: x1,
array [int] of int: w1,
array [int] of var int: x2,
array [int] of int: w2)
```

A global non-overlap constraint for `2` dimensional objects. It enforces that no two objects overlap
and zero-length objects do not appear in the middle of other objects.

Parameters:

`x1`: first coordinate of each object`w2`: width in first dimension for each object`x2`: second coordinate of each object`w2`: width in second dimension for each object

```
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`dimensions`rect_offset`: the offset of each box from the base position in`k`dimensions`shape`: the set of rectangles defining the`i`-th shape.`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
`w`and profits`p`must be non-negative `w`,`p`and`x`must 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. Graph constraints¶

```
predicate bounded_dpath(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
var int: s,
var int: t,
array [int] of var bool: ns,
array [int] of var bool: es,
var int: K)
```

Constrains the subgraph `ns` and `es` of a given directed graph to be a path from `s` to `t` of weight `K` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`w`: the weight of each edge`s`: the source node (which may be variable)`t`: the dest node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph`K`: the cost of the path

```
predicate bounded_dpath(array [int] of $$N: from,
array [int] of $$N: to,
array [int] of int: w,
var $$N: s,
var $$N: t,
array [$$N] of var bool: ns,
array [int] of var bool: es,
var int: K)
```

Constrains the subgraph `ns` and `es` of a given directed graph to be a path from `s` to `t` of weight `K` .

Parameters:

`from`: the leaving node for each edge`to`: the entering node for each edge`w`: the weight of each edge`s`: the source node (which may be variable)`t`: the dest node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph`K`: the cost of the path

```
predicate bounded_path(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
var int: s,
var int: t,
array [int] of var bool: ns,
array [int] of var bool: es,
var int: K)
```

Constrains the subgraph `ns` and `es` of a given undirected graph to be a path from `s` to `t` of weight `K` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`w`: the weight of each edge`s`: the source node (which may be variable)`t`: the dest node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph`K`: the cost of the path

```
predicate bounded_path(array [int] of $$N: from,
array [int] of $$N: to,
array [int] of int: w,
var $$N: s,
var $$N: t,
array [$$N] of var bool: ns,
array [int] of var bool: es,
var int: K)
```

Constrains the subgraph `ns` and `es` of a given undirected graph to be a path from `s` to `t` of weight `K` .

Parameters:

`from`: the leaving node for each edge`to`: the entering node for each edge`w`: the weight of each edge`s`: the source node (which may be variable)`t`: the dest node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph`K`: the cost of the path

```
predicate connected(array [int] of $$N: from,
array [int] of $$N: to,
array [$$N] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given undirected graph to be connected.

Parameters:

`from`: is the leaving node for each edge`to`: is the entering node for each edge`ns`: is a Boolean for each node whether it is in the subgraph`es`: is a Boolean for each edge whether it is in the subgraph

```
predicate d_weighted_spanning_tree(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
var int: r,
array [int] of var bool: es,
var int: K)
```

Constrains the set of edges `es` of a given directed graph to be a weighted spanning tree rooted at `r` of weight `W` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`w`: the weight of each edge`r`: the root node (which may be variable)`es`: a Boolean for each edge whether it is in the subgraph`K`: the weight of the tree

```
predicate dag(array [int] of $$N: from,
array [int] of $$N: to,
array [$$N] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given directed graph to be a DAG.

Parameters:

`from`: the leaving node for each edge`to`: the entering node for each edge`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate dconnected(array [int] of $$N: from,
array [int] of $$N: to,
array [$$N] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given directed graph to be connected.

Parameters:

`from`: the leaving node for each edge`to`: the entering node for each edge`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate dpath(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: s,
var int: t,
array [int] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given directed graph to be a path from `s` to `t` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`s`: the source node (which may be variable)`t`: the dest node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate dpath(array [int] of $$N: from,
array [int] of $$N: to,
var $$N: s,
var $$N: t,
array [$$N] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given directed graph to be a path from `s` to `t` .

Parameters:

`from`: the leaving node for each edge`to`: the entering node for each edge`s`: the source node (which may be variable)`t`: the dest node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate dreachable(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given directed graph to be reachable from `r` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`r`: the root node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate dreachable(array [int] of $$N: from,
array [int] of $$N: to,
var $$N: r,
array [$$N] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given directed graph to be reachable from `r` .

Parameters:

`from`: the leaving node for each edge`to`: the entering node for each edge`r`: the root node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate dsteiner(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es,
var int: K)
```

Constrains the subgraph `ns` and `es` of a given directed graph to be a weighted spanning tree rooted at `r` of weight `W` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`w`: the weight of each edge`r`: the root node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph`K`: the weight of the tree

```
predicate dtree(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given directed graph to be a tree rooted at `r` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`r`: the root node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate dtree(array [int] of $$N: from,
array [int] of $$N: to,
var $$N: r,
array [$$N] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given directed graph to be at tree rooted at `r` .

Parameters:

`from`: the leaving node for each edge`to`: the entering node for each edge`r`: the root node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate path(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: s,
var int: t,
array [int] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given undirected graph to be a path from `s` to `t` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`s`: the source node (which may be variable)`t`: the dest node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate path(array [int] of $$N: from,
array [int] of $$N: to,
var $$N: s,
var $$N: t,
array [$$N] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given undirected graph to be a path from `s` to `t` .

Parameters:

`from`: the leaving node for each edge`to`: the entering node for each edge`s`: the source node (which may be variable)`t`: the dest node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate reachable(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given undirected graph to be reachable from `r` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`r`: the root node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate reachable(array [int] of $$N: from,
array [int] of $$N: to,
var $$N: r,
array [$$N] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given undirected graph to be reachable from `r` .

Parameters:

`from`: the leaving node for each edge`to`: the entering node for each edge`r`: the root node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate steiner(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
array [int] of var bool: ns,
array [int] of var bool: es,
var int: K)
```

Constrains the set of edges `es` of a given undirected graph to be a weighted spanning tree of weight `W` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`w`: the weight of each edge`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph`K`: the weight of the tree

```
predicate subgraph(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of var bool: ns,
array [int] of var bool: es)
```

Constrains that `ns` and `es` is a subgraph of a given directed graph.

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate subgraph(array [int] of $$N: from,
array [int] of $$N: to,
array [$$N] of var bool: ns,
array [int] of var bool: es)
```

Constrains that `ns` and `es` is a subgraph of a given directed graph.

Parameters:

`from`: the leaving node for each edge`to`: the entering node for each edge`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate tree(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given undirected graph to be a tree rooted at `r` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`r`: the root node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate tree(array [int] of $$N: from,
array [int] of $$N: to,
var $$N: r,
array [$$N] of var bool: ns,
array [int] of var bool: es)
```

Constrains the subgraph `ns` and `es` of a given undirected graph to be at tree rooted at `r` .

Parameters:

`from`: the leaving node for each edge`to`: the entering node for each edge`r`: the root node (which may be variable)`ns`: a Boolean for each node whether it is in the subgraph`es`: a Boolean for each edge whether it is in the subgraph

```
predicate weighted_spanning_tree(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
array [int] of var bool: es,
var int: K)
```

Constrains the set of edges `es` of a given undirected graph to be a weighted spanning tree of weight `W` .

Parameters:

`N`: the number of nodes in the given graph`E`: the number of edges in the given graph`from`: the leaving node 1..`N`for each edge`to`: the entering node 1..`N`for each edge`w`: the weight of each edge`es`: a Boolean for each edge whether it is in the subgraph`K`: the weight of the tree

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

```
predicate cost_mdd(array [int] of var int: x,
int: N,
array [int] of int: level,
int: E,
array [int] of int: from,
array [int] of set of int: label,
array [int] of int: cost,
array [int] of int: to,
var int: totalcost)
```

Requires that `x` defines a path in the cost MDD with total edge weight `totalcost` .

Parameters:

`N`: the number of nodes, the root node is node 1`level`: the level of each node, the root is level 1, T is level`length`(x)+1`E`: the number of edges`from`: the leaving node (1..`N`)for each edge`label`: the set of value of the x variable for each edge`cost`: the cost for each edge`to`: the entering node for each edge, where 0 = T node`totalcost`: the total cost of the path defined by`x`

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

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. Each edge has an associated cost `c` ,
and `C` is the sum of costs taken on the accepting path for `x` .

```
predicate mdd(array [int] of var int: x,
int: N,
array [int] of int: level,
int: E,
array [int] of int: from,
array [int] of set of int: label,
array [int] of int: to)
```

Requires that `x` defines a path from root to true node T through the (deterministic) MDD defined by

The MDD must be deterministic, i.e., there cannot be two edges with the same label leaving the same node.

Parameters:

`N`: the number of nodes, the root node is node 1`level`: the level of each node, the root is level 1, T is level`length`(x)+1`E`: the number of edges`from`: the leaving node (1..`N`)for each edge`label`: the set of values of the`x`variable for each edge`to`: the entering node for each edge, where 0 = T node

```
predicate mdd_nondet(array [int] of var int: x,
int: N,
array [int] of int: level,
int: E,
array [int] of int: from,
array [int] of set of int: label,
array [int] of int: to)
```

Requires that `x` defines a path from root to true node T through the (nondeterministic) MDD defined by

The MDD can be nondeterministic, i.e., there can be two edges with the same label leaving the same node.

Parameters:

`N`: the number of nodes, the root node is node 1`level`: the level of each node, the root is level 1, T is level`length`(x)+1`E`: the number of edges`from`: the leaving node (1..`N`)for each edge`label`: the set of values of the`x`variable for each edge`to`: the entering node for each edge, where 0 = T node

```
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,
int: Q,
set of 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 set `S` )
is accepted by the DFA of `Q` states with input `S` and transition
function `d` (which maps (1.. `Q` , `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 regular_nfa(array [int] of var int: x,
int: Q,
set of 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 `S` )
is accepted by the NFA of `Q` states with input `S` and transition
function `d` (which maps (1.. `Q` , `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.

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

Represents the constraint `x` in `t` if the variable `x_i` and the value
`t_i` occur where we consider each row in `t` to be a tuple and `t` as a
set of tuples.

## 4.2.1.10. Machine learning constraints¶

```
predicate neural_net(array [int] of var float: inputs,
array [int] of int: input_ids,
array [int] of var float: outputs,
array [int] of int: output_ids,
array [int] of float: bias,
array [int] of float: edge_weight,
array [int] of int: edge_parent,
array [int] of int: first_edge,
NEURON_TYPE: neuron_type)
```

constrain the output layer of a neural net to take the value defined by the input layer.
the arguments are
`inputs` : an array of float variables
`input_ids` : array[int] of node
`outputs` : an array of float variables
`output_ids` : array[int] of node
`bias` : array[node] of float
`edge_weight` : array[edge] of float (dummy one at end!)
`edge_parent` : array[edge] of neuron (start neuron for edge)
`first_edge` : array[node] of 1..m+1
`neuron_type` : { NT_RELU, NT_STEP, NT_LINEAR, NT_SOFTPLUS }

## 4.2.1.11. Deprecated constraints¶

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

This constraint is deprecated. Use count(i in x)(i=v) >= n instead.

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

This constraint is deprecated. Use count(i in x)(i=v) <= n instead.

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

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

This constraint is deprecated. Use count(i in x)(i=v) = n instead.

## 4.2.1.12. Other declarations¶

```
function var $$E: arg_max(array [$$E] 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 $$E: arg_max(array [$$E] of var bool: x)
```

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

```
function var $$E: arg_max(array [$$E] 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 $$E: arg_min(array [$$E] 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 $$E: arg_min(array [$$E] of var bool: x)
```

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

```
function var $$E: arg_min(array [$$E] 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 bool: 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 bool: 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` .

```
function var float: piecewise_linear(var float: x,
array [int] of float: xi,
array [int] of float: vi)
```

Return a piecewise-linear interpolation
of the given point sequence as a function of `x`

```
predicate piecewise_linear(var float: x,
var float: y,
array [int] of float: xi,
array [int] of float: vi)
```

Constrains `y` ( `x` ) to be a piecewise-linear interpolation of
the provided point sequence.

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

```
predicate sum_set(array [int] of int: vs,
array [int] of int: ws,
var set of int: x,
var int: s)
```

Requires that the sum of the weights `ws` [ `i1` ].. `ws` [ `iN` ] equals `s` ,
where `vs` [ `i1` ].. `vs` [ `iN` ] are the elements appearing in set `x`