MiniZinc Documentation - Standard Library

Functions and Predicates
predicate int_set_channel(array [int] of var int: x, array [int] of var set of int: y) =
forall ( i in index_set(x) ) ( x[i] in index_set(y) ) /\ forall ( j in index_set(y) ) ( y[j] subset index_set(x) ) /\ forall ( i in index_set(x), j in index_set(y) ) ( x[i]==j <-> i in y[j] )
(standard decomposition from int_set_channel.mzn:5)

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

function array [int] of var int: inverse(array [int] of var int: f) =
let { array [lb_array(f)..ub_array(f)] of var index_set(f): invf, constraint inverse(f, invf), } in (invf)
(standard decomposition from inverse_fn.mzn:6)

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

predicate inverse(array [int] of var int: f, array [int] of var int: invf) =
forall ( i in index_set(f), j in index_set(invf) ) ( f[i] in index_set(invf) /\ invf[j] in index_set(f) /\ (j==f[i] <-> i==invf[j]) )
(standard decomposition from inverse.mzn:6)

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.

predicate inverse_set(array [int] of var set of int: f, array [int] of var set of int: invf) =
forall ( i in index_set(f) ) ( f[i] subset index_set(invf) ) /\ forall ( j in index_set(invf) ) ( invf[j] subset index_set(f) ) /\ forall ( i in index_set(f), j in index_set(invf) ) ( j in f[i] <-> i in invf[j] )
(standard decomposition from inverse_set.mzn:6)

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.