MiniZinc Documentation - Standard Library

Functions and Predicates
predicate lex2(array [int,int] of var int: x) =
let { int: lbx1 = min(index_set_1of2(x)), int: ubx1 = max(index_set_1of2(x)), int: lbx2 = min(index_set_2of2(x)), int: ubx2 = max(index_set_2of2(x)), } in ( forall ( i in lbx1+1..ubx1 ) ( lex_lesseq([ x[i-1, j] | j in index_set_2of2(x) ], [ x[i, j] | j in index_set_2of2(x) ]) ) /\ forall ( j in lbx2+1..ubx2 ) ( lex_lesseq([ x[i, j-1] | i in index_set_1of2(x) ], [ x[i, j] | i in index_set_1of2(x) ]) ))
(standard decomposition from lex2.mzn:7)

Require adjacent rows and adjacent columns in the array x to be lexicographically ordered. Adjacent rows and adjacent columns may be equal.

predicate lex_greater(array [int] of var bool: x, array [int] of var bool: y) =
lex_less(y, x)
(standard decomposition from lex_greater.mzn:7)

Requires that the array x is strictly lexicographically greater than array y. Compares them from first to last element, regardless of indices.

predicate lex_greater(array [int] of var int: x, array [int] of var int: y) =
lex_less(y, x)
(standard decomposition from lex_greater.mzn:15)

Requires that the array x is strictly lexicographically greater than array y. Compares them from first to last element, regardless of indices.

predicate lex_greater(array [int] of var float: x, array [int] of var float: y) =
lex_less(y, x)
(standard decomposition from lex_greater.mzn:23)

Requires that the array x is strictly lexicographically greater than array y. Compares them from first to last element, regardless of indices.

predicate lex_greater(array [int] of var set of int: x, array [int] of var set of int: y) =
lex_less(y, x)
(standard decomposition from lex_greater.mzn:31)

Requires that the array x is strictly lexicographically greater than array y. Compares them from first to last element, regardless of indices.

predicate lex_greatereq(array [int] of var bool: x, array [int] of var bool: y) =
lex_lesseq(y, x)
(standard decomposition from lex_greatereq.mzn:7)

Requires that the array x is lexicographically greater than or equal to array y. Compares them from first to last element, regardless of indices.

predicate lex_greatereq(array [int] of var int: x, array [int] of var int: y) =
lex_lesseq(y, x)
(standard decomposition from lex_greatereq.mzn:15)

Requires that the array x is lexicographically greater than or equal to array y. Compares them from first to last element, regardless of indices.

predicate lex_greatereq(array [int] of var float: x, array [int] of var float: y) =
lex_lesseq(y, x)
(standard decomposition from lex_greatereq.mzn:23)

Requires that the array x is lexicographically greater than or equal to array y. Compares them from first to last element, regardless of indices.

predicate lex_greatereq(array [int] of var set of int: x, array [int] of var set of int: y) =
lex_lesseq(y, x)
(standard decomposition from lex_greatereq.mzn:31)

Requires that the array x is lexicographically greater than or equal to array y. Compares them from first to last element, regardless of indices.

predicate lex_less(array [int] of var bool: x, array [int] of var bool: y) =
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)), int: size = max(ux-lx, uy-ly), array [0..size+1] of var bool: b, } in ( b[0] /\ forall ( i in 0..size ) ( b[i]==(x[lx+i]<=y[ly+i] /\ (x[lx+i] < y[ly+i] \/ b[i+1])) ) /\ b[size+1]==(ux-lx < uy-ly))
(standard decomposition from lex_less_bool.mzn:6)

Requires that the array x is strictly lexicographically less than array y. Compares them from first to last element, regardless of indices.

predicate lex_less(array [int] of var int: x, array [int] of var int: y) =
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)), int: size = max(ux-lx, uy-ly), array [0..size+1] of var bool: b, } in ( b[0] /\ forall ( i in 0..size ) ( b[i]==(x[lx+i]<=y[ly+i] /\ (x[lx+i] < y[ly+i] \/ b[i+1])) ) /\ b[size+1]==(ux-lx < uy-ly))
(standard decomposition from lex_less_int.mzn:6)

Requires that the array x is strictly lexicographically less than array y. Compares them from first to last element, regardless of indices.

predicate lex_less(array [int] of var float: x, array [int] of var float: y) =
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)), int: size = max(ux-lx, uy-ly), array [0..size+1] of var bool: b, } in ( b[0] /\ forall ( i in 0..size ) ( b[i]==(x[lx+i]<=y[ly+i] /\ (x[lx+i] < y[ly+i] \/ b[i+1])) ) /\ b[size+1]==(ux-lx < uy-ly))
(standard decomposition from lex_less_float.mzn:6)

Requires that the array x is strictly lexicographically less than array y. Compares them from first to last element, regardless of indices.

predicate lex_less(array [int] of var set of int: x, array [int] of var set of int: y) =
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)), int: size = max(ux-lx, uy-ly), array [0..size+1] of var bool: b, } in ( b[0] /\ forall ( i in 0..size ) ( b[i]==(x[lx+i]<=y[ly+i] /\ (x[lx+i] < y[ly+i] \/ b[i+1])) ) /\ b[size+1]==(ux-lx < uy-ly))
(standard decomposition from lex_less_set.mzn:6)

Requires that the array x is strictly lexicographically less than array y. Compares them from first to last element, regardless of indices.

predicate lex_lesseq(array [int] of var bool: x, array [int] of var bool: y) =
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)), int: size = max(ux-lx, uy-ly), array [0..size] of var bool: b, } in ( b[0] /\ forall ( i in 0..size ) ( b[i]==(x[lx+i]<=y[ly+i] /\ if i==size then true else x[lx+i] < y[ly+i] \/ b[i+1] endif) ))
(standard decomposition from lex_lesseq_bool.mzn:6)

Requires that the array x is lexicographically less than or equal to array y. Compares them from first to last element, regardless of indices.

predicate lex_lesseq(array [int] of var float: x, array [int] of var float: y) =
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)), int: size = max(ux-lx, uy-ly), array [0..size] of var bool: b, } in ( b[0] /\ forall ( i in 0..size ) ( b[i]==(x[lx+i]<=y[ly+i] /\ if i==size then true else x[lx+i] < y[ly+i] \/ b[i+1] endif) ))
(standard decomposition from lex_lesseq_float.mzn:6)

Requires that the array x is lexicographically less than or equal to array y. Compares them from first to last element, regardless of indices.

predicate lex_lesseq(array [int] of var int: x, array [int] of var int: y) =
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)), int: size = max(ux-lx, uy-ly), array [0..size] of var bool: b, } in ( b[0] /\ forall ( i in 0..size ) ( b[i]==(x[lx+i]<=y[ly+i] /\ if i==size then true else x[lx+i] < y[ly+i] \/ b[i+1] endif) ))
(standard decomposition from lex_lesseq_int.mzn:6)

Requires that the array x is lexicographically less than or equal to array y. Compares them from first to last element, regardless of indices.

predicate lex_lesseq(array [int] of var set of int: x, array [int] of var set of int: y) =
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)), int: size = max(ux-lx, uy-ly), array [0..size] of var bool: b, } in ( b[0] /\ forall ( i in 0..size ) ( b[i]==(x[lx+i]<=y[ly+i] /\ if i==size then true else x[lx+i] < y[ly+i] \/ b[i+1] endif) ))
(standard decomposition from lex_lesseq_set.mzn:6)

Requires that the array x is lexicographically less than or equal to array y. Compares them from first to last element, regardless of indices.

predicate strict_lex2(array [int,int] of var int: x) =
let { int: lbx1 = min(index_set_1of2(x)), int: ubx1 = max(index_set_1of2(x)), int: lbx2 = min(index_set_2of2(x)), int: ubx2 = max(index_set_2of2(x)), } in ( forall ( i in lbx1+1..ubx1 ) ( lex_less([ x[i-1, j] | j in index_set_2of2(x) ], [ x[i, j] | j in index_set_2of2(x) ]) ) /\ forall ( j in lbx2+1..ubx2 ) ( lex_less([ x[i, j-1] | i in index_set_1of2(x) ], [ x[i, j] | i in index_set_1of2(x) ]) ))
(standard decomposition from strict_lex2.mzn:7)

Require adjacent rows and adjacent columns in the array x to be lexicographically ordered. Adjacent rows and adjacent columns cannot be equal.

predicate value_precede(int: s, int: t, array [int] of var int: x) =
let { int: imin = min(index_set(x)), int: imax = max(index_set(x)), array [imin..imax+1] of var bool: b, } in ( forall ( i in imin..imax ) ( let { var bool: xis = x[i]==s, } in ( (xis -> b[i+1]==true) /\ (not xis -> b[i]==b[i+1]) /\ (not b[i] -> x[i]!=t)) ) /\ b[imin]==false)
(standard decomposition from value_precede_int.mzn:1)

Requires that s precede t in the array x.

Precedence means that if any element of x is equal to t, then another element of x with a lower index is equal to s.

predicate value_precede(int: s, int: t, array [int] of var set of int: x) =
let { int: imin = min(index_set(x)), int: imax = max(index_set(x)), array [imin..imax+1] of var bool: b, } in ( forall ( i in imin..imax ) ( let { var bool: xis = s in x[i] /\ not (t in x[i]), } in ( (xis -> b[i+1]==true) /\ (not xis -> b[i]==b[i+1]) /\ (not b[i] -> s in x[i] \/ not (t in x[i]))) ) /\ b[imin]==false)
(standard decomposition from value_precede_set.mzn:1)

Requires that s precede t in the array x.

Precedence means that if an element of x contains t but not s, then another element of x with lower index contains s but not t.

predicate value_precede_chain(array [int] of int: c, array [int] of var int: x) =
forall ( i in min(index_set(c))+1..max(index_set(c)) ) ( value_precede(c[i-1], c[i], x) )
(standard decomposition from value_precede_chain_int.mzn:3)

Requires that c[i] precedes c[i +1] in the array x.

Precedence means that if any element of x is equal to \a c[i +1], then another element of x with a lower index is equal to \a c[i].

predicate value_precede_chain(array [int] of int: c, array [int] of var set of int: x) =
forall ( i in min(index_set(c))+1..max(index_set(c)) ) ( value_precede(c[i-1], c[i], x) )
(standard decomposition from value_precede_chain_set.mzn:3)

Requires that c[i] precedes c[i +1] in the array x.

Precedence means that if an element of x contains \a c[i +1] but not \a c[i], then another element of x with lower index contains \a c[i] but not \a c[i +1].