4.2.2.12. Extensional constraints (table, regular etc.)
In this section: cost_mdd, cost_regular, mdd, mdd_nondet, regular, regular_nfa, table.
cost_mdd
predicate cost_mdd(array [int] of var int: x,
int: N,
array [int] of int: level,
int: E,
array [int] of int: from,
array [int] of set of int: label,
array [int] of int: cost,
array [int] of int: to,
var int: totalcost)
|
Requires that x defines a path in the cost MDD with total edge weight totalcost. Parameters:
|
cost_regular
predicate cost_regular(array [int] of var int: x,
int: Q,
int: S,
array [int,int] of int: d,
int: q0,
set of int: F,
array [int,int] of int: c,
var int: C)
|
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. Each edge has an associated cost c, and C is the sum of costs taken on the accepting path for x. |
mdd
predicate mdd(array [int] of var int: x,
int: N,
array [int] of int: level,
int: E,
array [int] of int: from,
array [int] of set of int: label,
array [int] of int: to)
|
Requires that x defines a path from root to true node T through the (deterministic) Multivalued Decision Diagram (MDD) defined by the parameters. The MDD must be deterministic, i.e., there cannot be two edges with the same label leaving the same node. Parameters:
|
mdd_nondet
predicate mdd_nondet(array [int] of var int: x,
int: N,
array [int] of int: level,
int: E,
array [int] of int: from,
array [int] of set of int: label,
array [int] of int: to)
|
Requires that x defines a path from root to true node T through the (nondeterministic) Multivalued Decision Diagram (MDD) defined by the parameters. The MDD can be nondeterministic, i.e., there can be two edges with the same label leaving the same node. Parameters:
|
regular
1. predicate regular(array [int] of var $$Val: x,
array [$$State,$$Val] of opt $$State: d,
$$State: q0,
set of $$State: F)
2. predicate regular(array [int] of var int: x,
int: Q,
int: S,
array [int,int] of int: d,
int: q0,
set of int: F)
3. predicate regular(array [int] of var int: x,
int: Q,
set of int: S,
array [int,int] of int: d,
int: q0,
set of int: F)
4. predicate regular(array [int] of var int: x, string: r)
|
|
regular_nfa
1. predicate regular_nfa(array [int] of var $$Val: x,
array [$$State,$$Val] of set of $$State: d,
$$State: q0,
set of $$State: F)
2. 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)
3. predicate regular_nfa(array [int] of var int: x,
int: Q,
set of int: S,
array [int,int] of set of int: d,
int: q0,
set of int: F)
|
|
table
1. predicate table(array [$$E] of var bool: x, array [int,$$E] of bool: t)
2. predicate table(array [$$E] of var int: x, array [int,$$E] of int: t)
3. predicate table(array [int] of var opt int: x,
array [int,int] of opt int: t)
|
|