Counting constraints

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