MiniZinc Documentation - Standard Library

Functions and Predicates
predicate regular(array [int] of var int: x, int: Q, int: S, array [int,int] of int: d, int: q0, set of int: F) =
assert(Q > 0, "regular: \'Q\' must be greater than zero", assert(S > 0, "regular: \'S\' must be greater than zero", assert(index_set_1of2(d)==1..Q /\ index_set_2of2(d)== 1..S, "regular: the transition function \'d\' must be [1..Q,1..S]", assert(forall ( i in 1..Q, j in 1..S ) ( d[i, j] in 0..Q ), "regular: transition function \'d\' points to states outside 0..Q", assert(q0 in 1..Q, "regular: start state \'q0\' not in 1..Q", assert(F subset 1..Q, "regular: final states in \'F\' contain states outside 1..Q", let { int: m = min(index_set(x)), int: n = max(index_set(x))+1, array [m..n] of var 1..Q: a, } in ( a[m]==q0 /\ forall ( i in index_set(x) ) ( x[i] in 1..S /\ a[i+1]==d[a[i], x[i]] ) /\ a[n] in F)))))))
(standard decomposition from regular.mzn:8)

The sequence of values in array x (which must all be in the range 1..S) is accepted by the DFA of Q states with input 1..S and transition function d (which maps (1..Q, 1..S) -> 0..Q)) and initial state q0 (which must be in 1..Q) and accepting states F (which all must be in 1..Q). We reserve state 0 to be an always failing state.

predicate regular_nfa(array [int] of var int: x, int: Q, int: S, array [int,int] of set of int: d, int: q0, set of int: F) =
assert(Q > 0, "regular_nfa: \'Q\' must be greater than zero", assert(S > 0, "regular_nfa: \'S\' must be greater than zero", assert(index_set_1of2(d)==1..Q /\ index_set_2of2(d)==1..S, "regular_nfa: the transition function \'d\' must be [1..Q,1..S]", assert(forall ( i in 1..Q, j in 1..S ) ( d[i, j] subset 1..Q ), "regular_nfa: transition function \'d\' points to states outside 1..Q", assert(q0 in 1..Q, "regular: start state \'q0\' not in 1..Q", assert(F subset 1..Q, "regular: final states in \'F\' contain states outside 1..Q", let { int: m = min(index_set(x)), int: n = max(index_set(x))+1, array [m..n] of var 1..Q: a, } in ( a[m]==q0 /\ forall ( i in index_set(x) ) ( x[i] in 1..S /\ a[i+1] in d[a[i], x[i]] ) /\ a[n] in F)))))))
(standard decomposition from regular_nfa.mzn:8)

The sequence of values in array x (which must all be in the range 1..S) is accepted by the NFA of Q states with input 1..S and transition function d (which maps (1..Q, 1..S) -> set of 1..Q)) and initial state q0 (which must be in 1..Q) and accepting states F (which all must be in 1..Q).

predicate table(array [int] of var bool: x, array [int,int] of bool: t) =
assert(index_set_2of2(t)==index_set(x), "The second dimension of the table must equal the number of variables "++ "in the first argument", let { int: l = min(index_set(x)), int: u = max(index_set(x)), int: lt = min(index_set_1of2(t)), int: ut = max(index_set_1of2(t)), var lt..ut: i, array [l..u, lt..ut] of bool: t_transposed = array2d(l..u, lt.. ut, [ t[i, j] | j in l..u, i in lt..ut ]), } in ( forall ( j in l..u ) ( t_transposed[j, i]==x[j] ) ))
(standard decomposition from table_bool.mzn:6)

Represents the constraint x in t where we consider each row in t to be a tuple and t as a set of tuples.

predicate table(array [int] of var int: x, array [int,int] of int: t) =
assert(index_set_2of2(t)==index_set(x), "The second dimension of the table must equal the number of variables "++ "in the first argument", let { int: l = min(index_set(x)), int: u = max(index_set(x)), int: lt = min(index_set_1of2(t)), int: ut = max(index_set_1of2(t)), var lt..ut: i, array [l..u, lt..ut] of int: t_transposed = array2d(l..u, lt..ut, [ t[i, j] | j in l..u, i in lt..ut ]), } in ( forall ( j in l..u ) ( t_transposed[j, i]==x[j] ) ))
(standard decomposition from table_int.mzn:6)

Represents the constraint x in t where we consider each row in t to be a tuple and t as a set of tuples.