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.
◀predicate link_set_to_booleans(var set of int: s,
array [int] of var bool: b) =
assert(ub(s) subset index_set(b),
"link_set_to_booleans: the index set of b must be a superset of the possible values of s",
forall ( i in index_set(b) ) (
b[i] <-> i in s
))
(standard decomposition from link_set_to_booleans.mzn:7)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.