Functions and Predicates

◀function array [int] of var int: arg_sort(array [int] of var int: x) =

if length(x)==0 then
[] else let {
int: l = min(index_set(x)),
int: u = max(index_set(x)),
array [1..u-l+1] of var l..u: p,
constraint arg_sort_int(x, p),
} in (p) endif

(standard decomposition from arg_sort.mzn:7)Returns the permutation p which causes x to be in sorted order hence x[p[i]] <= x[p[i+1]]. The permutation is the stable sort hence x[p[i]] = x[p[i+1]] \(\rightarrow\) p[i] < p[i+1].

◀function array [int] of var int: arg_sort(array [int] of var float: x) =

if length(x)==0 then
[] else let {
int: l = min(index_set(x)),
int: u = max(index_set(x)),
array [1..u-l+1] of var l..u: p,
constraint arg_sort_float(x, p),
} in (p) endif

(standard decomposition from arg_sort.mzn:24)◀predicate arg_sort(array [int] of var int: x,
array [int] of var int: p) =

assert(index_set(p)==1..length(x),
"arg_sort_int: second argument must have index 1..length(first argument)",
alldifferent(p) /\
forall ( j in 1..length(x)-1 ) (
x[p[j]]<=x[p[j+1]] /\ (x[p[j]]==x[p[j+1]] -> p[j] < p[j+1])
))

(standard decomposition from arg_sort_int.mzn:3)Constrains p to be the permutation which causes x to be in sorted order hence x[p[i]] <= x[p[i+1]]. The permutation is the stable sort hence x[p[i]] = x[p[i+1]] \(\rightarrow\) p[i] < p[i+1].

◀predicate arg_sort(array [int] of var float: x,
array [int] of var int: p) =

assert(index_set(p)==1..length(x),
"arg_sort_float: second argument must have index 1..length(first argument)",
alldifferent(p) /\
forall ( j in 1..length(x)-1 ) (
x[p[j]]<=x[p[j+1]] /\ (x[p[j]]==x[p[j+1]] -> p[j] < p[j+1])
))

(standard decomposition from arg_sort_float.mzn:3)◀predicate decreasing(array [int] of var bool: x) =

forall ( i in index_set(x) diff {min(index_set(x))} ) ( x[i-1]>=x[i] )

(standard decomposition from decreasing_bool.mzn:5)Requires that the array x is in decreasing order (duplicates are allowed).

◀predicate decreasing(array [int] of var float: x) =

forall ( i in index_set(x) diff {min(index_set(x))} ) ( x[i-1]>=x[i] )

(standard decomposition from decreasing_float.mzn:5)Requires that the array x is in decreasing order (duplicates are allowed).

◀predicate decreasing(array [int] of var int: x) =

forall ( i in index_set(x) diff {min(index_set(x))} ) ( x[i-1]>=x[i] )

(standard decomposition from decreasing_int.mzn:5)Requires that the array x is in decreasing order (duplicates are allowed).

◀predicate decreasing(array [int] of var set of int: x) =

forall ( i in index_set(x) diff {min(index_set(x))} ) ( x[i-1]>=x[i] )

(standard decomposition from decreasing_set.mzn:5)Requires that the array x is in decreasing order (duplicates are allowed).

◀predicate increasing(array [int] of var bool: x) =

forall ( i in index_set(x) diff {min(index_set(x))} ) ( x[i-1]<=x[i] )

(standard decomposition from increasing_bool.mzn:5)Requires that the array x is in increasing order (duplicates are allowed).

◀predicate increasing(array [int] of var float: x) =

forall ( i in index_set(x) diff {min(index_set(x))} ) ( x[i-1]<=x[i] )

(standard decomposition from increasing_float.mzn:5)Requires that the array x is in increasing order (duplicates are allowed).

◀predicate increasing(array [int] of var int: x) =

forall ( i in index_set(x) diff {min(index_set(x))} ) ( x[i-1]<=x[i] )

(standard decomposition from increasing_int.mzn:5)Requires that the array x is in increasing order (duplicates are allowed).

◀predicate increasing(array [int] of var set of int: x) =

forall ( i in index_set(x) diff {min(index_set(x))} ) ( x[i-1]<=x[i] )

(standard decomposition from increasing_set.mzn:5)Requires that the array x is in increasing order (duplicates are allowed).

◀function array [int] of var int: sort(array [int] of var int: x) =

let {
array [1..length(x)] of var lb_array(x)..ub_array(x): y,
constraint sort(x, y),
} in (y)

(standard decomposition from sort_fn.mzn:7)Return a multiset of values that is the same as the multiset of values in x but in sorted order.

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

assert(card(index_set(x))==card(index_set(y)),
"sort: x and y must be same sized arrays", let {
int: lx =
min(index_set(x)),
int: ux =
max(index_set(x)),
int: ly =
min(index_set(y)),
int: uy =
max(index_set(y)),
array [lx..ux] of
var ly..uy: p,
} in (
forall ( i in
index_set(x) ) ( y[p[i]]==x[i] ) /\ alldifferent(p) /\
increasing(y)))

(standard decomposition from sort.mzn:8)Requires that the multiset of values in x are the same as the multiset of values in y but y is in sorted order.