Functions and Predicates

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

let {
var 0..length(x): n,
constraint among(n, x, v),
} in (n)

(standard decomposition from among_fn.mzn:6)Returns the number of variables in x that take one of the values in v.

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

n==sum ( i in index_set(x) ) ( bool2int(x[i] in v) )

(standard decomposition from among.mzn:4)Requires exactly n variables in x to take one of the values in v.

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

sum ( i in index_set(x) ) ( bool2int(x[i]==v) )>=n

(standard decomposition from at_least_int.mzn:5)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) =

sum ( i in index_set(x) ) ( bool2int(x[i]==v) )>=n

(standard decomposition from at_least_set.mzn:5)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) =

sum ( i in index_set(x) ) ( bool2int(x[i]==v) )<=n

(standard decomposition from at_most_int.mzn:5)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) =

sum ( i in index_set(x) ) ( bool2int(x[i]==v) )<=n

(standard decomposition from at_most_set.mzn:5)Requires at most n variables in x to take the value v.

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

forall ( i, j in index_set(s) where i < j ) (
card(s[i] intersect s[j])<=1
)

(standard decomposition from at_most1.mzn:4)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) =

let {
var 0..length(x): c,
constraint count(x, y, c),
} in (c)

(standard decomposition from count_fn.mzn:6)Returns the number of occurrences of y in x.

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

c==sum ( i in index_set(x) ) ( bool2int(x[i]==y) )

(standard decomposition from count_eq.mzn:4)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) =

c==sum ( i in index_set(x) ) ( bool2int(x[i]==y) )

(standard decomposition from count_eq.mzn:4)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) =

c>=sum ( i in index_set(x) ) ( bool2int(x[i]==y) )

(standard decomposition from count_geq.mzn:5)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) =

c > sum ( i in index_set(x) ) ( bool2int(x[i]==y) )

(standard decomposition from count_gt.mzn:5)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) =

c<=sum ( i in index_set(x) ) ( bool2int(x[i]==y) )

(standard decomposition from count_leq.mzn:5)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) =

c < sum ( i in index_set(x) ) ( bool2int(x[i]==y) )

(standard decomposition from count_lt.mzn:5)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) =

c!=sum ( i in index_set(x) ) ( bool2int(x[i]==y) )

(standard decomposition from count_neq.mzn:5)Constrains c to be not equal to the number of occurrences of y in x.

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

let {
array [index_set(value)] of var 0..length(base): card,
constraint distribute(card, value, base),
} in (card)

(standard decomposition from distribute_fn.mzn:7)Returns an array of the number of occurences of value[i] in base. The values in value need not be distinct.

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

assert(index_set(card)==index_set(value),
"distribute: card and value arrays must have identical index sets",
forall ( i in index_set(card) ) (
card[i]==sum ( j in index_set(base) ) (
bool2int(value[i]==base[j])
)
))

(standard decomposition from distribute.mzn:5)Requires that card[i] is 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) =

n==sum ( i in index_set(x) ) ( bool2int(x[i]==v) )

(standard decomposition from exactly_int.mzn:5)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) =

n==sum ( i in index_set(x) ) ( bool2int(x[i]==v) )

(standard decomposition from exactly_set.mzn:5)Requires exactly n variables in x to take the value v.

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

let {
array [index_set(cover)] of var 0..length(x): counts,
constraint global_cardinality(x, cover, counts),
} in (counts)

(standard decomposition from global_cardinality_fn.mzn:6)Returns the number of occurrences of cover[i] in x.

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

assert(index_set(cover)==index_set(counts),
"global_cardinality: cover and counts must have identical index sets",
forall ( i in index_set(cover) ) (
count(x, cover[i], counts[i])
) /\
length(x)>=sum(counts))

(standard decomposition from global_cardinality.mzn:6)Requires that the number of occurrences of cover[i] in x is counts[i].

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

let {
array [index_set(cover)] of var 0..length(x): counts,
constraint global_cardinality_closed(x, cover, counts),
} in (counts)

(standard decomposition from global_cardinality_closed_fn.mzn:8)Returns an array with number of occurences of i in x.

The elements of x must take their values from cover.

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

assert(index_set(cover)==index_set(counts),
"global_cardinality_closed: "++
"cover and counts must have identical index sets", forall ( i in
index_set(x) ) ( x[i] in
{ d | d in cover } ) /\
global_cardinality(x, cover, counts) /\ length(x)==
sum(counts))

(standard decomposition from global_cardinality_closed.mzn:6)Requires that the number of occurences of i in x is counts[i].

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) =

forall ( i in index_set(cover) ) (
sum ( j in index_set(x) ) ( bool2int(x[j]==cover[i])
) in lbound[i]..ubound[i]
)

(standard decomposition from global_cardinality_low_up.mzn:5)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) =

forall ( i in index_set(x) ) ( x[i] in { d | d in array2set(cover) }
) /\
global_cardinality_low_up(x, cover, lbound, ubound) /\
length(x) in sum(lbound)..sum(ubound)

(standard decomposition from global_cardinality_low_up_closed.mzn:7)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.