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)