Functions and Predicates
◀predicate all_different(array [int] of var int: x) =
forall ( i, j in index_set(x) where i < j ) ( x[i]!=x[j] )
(standard decomposition from all_different_int.mzn:5)Constrain the array of integers x to be all different.
◀predicate all_different(array [int] of var set of int: x) =
forall ( i, j in index_set(x) where i < j ) ( x[i]!=x[j] )
(standard decomposition from all_different_set.mzn:5)Constrain the array of sets of integers x to be all different.
◀predicate all_disjoint(array [int] of var set of int: S) =
forall ( i, j in index_set(S) where i < j ) ( disjoint(S[i], S[j]) )
(standard decomposition from all_disjoint.mzn:4)Constrain the array of sets of integers S to be pairwise disjoint.
◀predicate all_equal(array [int] of var int: x) =
forall ( i, j in index_set(x) where i < j ) ( x[i]==x[j] )
(standard decomposition from all_equal_int.mzn:1)Constrain the array of integers x to be all equal
◀predicate all_equal(array [int] of var set of int: x) =
forall ( i, j in index_set(x) where i < j ) ( x[i]==x[j] )
(standard decomposition from all_equal_set.mzn:1)Constrain the array of sets of integers x to be all different
◀predicate alldifferent_except_0(array [int] of var int: vs) =
forall ( i, j in index_set(vs) where i < j ) (
vs[i]!=0 /\ vs[j]!=0 -> vs[i]!=vs[j]
)
(standard decomposition from alldifferent_except_0.mzn:5)Constrain the array of integers vs to be all different except those elements that are assigned the value 0.
◀function var int: nvalue(array [int] of var int: x) =
let {
var 0..length(x): n,
constraint nvalue(n, x),
} in (n)
(standard decomposition from nvalue_fn.mzn:6)Returns the number of distinct values in x.
◀predicate nvalue(var int: n, array [int] of var int: x) =
let {
int: lx = lb_array(x),
int: ux = ub_array(x),
} in (
n==sum ( j in lx..ux ) (
bool2int(exists ( i in index_set(x) ) ( x[i]==j ))
))
(standard decomposition from nvalue.mzn:4)Requires that the number of distinct values in x is n.
◀predicate symmetric_all_different(array [int] of var int: x) =
all_different(x) /\
forall ( i, j in index_set(x) where i!=j ) ( x[i]==j -> x[j]==i )
(standard decomposition from symmetric_all_different.mzn:8)Requires the array of integers x to be all different, and for all i, x[i]=j \(\rightarrow\) x[j]=i.