4.2.2.9. 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: N: the number of nodes, the root node is node 1 level: the level of each node, the root is level 1, T is level length(x)+1 E: the number of edges from: the leaving node (1..N)for each edge label: the set of value of the x variable for each edge cost: the cost for each edge to: the entering node for each edge, where 0 = T node totalcost: the total cost of the path defined by x

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: N: the number of nodes, the root node is node 1 level: the level of each node, the root is level 1, T is level length(x)+1 E: the number of edges from: the leaving node (1..N)for each edge label: the set of values of the x variable for each edge to: the entering node for each edge, where 0 = T node

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: N: the number of nodes, the root node is node 1 level: the level of each node, the root is level 1, T is level length(x)+1 E: the number of edges from: the leaving node (1..N)for each edge label: the set of values of the x variable for each edge to: the entering node for each edge, where 0 = T node

regular¶

 1. predicate regular(array [int] of var int: x, int: Q, int: S, array [int,int] of int: d, int: q0, set of int: F) 2. 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) 3. predicate regular(array [int] of var int: x, string: r)  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. The sequence of values in array x (which must all be in the set S) is accepted by the DFA of Q states with input S and transition function d (which maps (1..Q, 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. The sequence of values in array x is accepted by the regular expression r. This constraint generates its DFA equivalent. Regular expressions can use the following syntax: Selection: Concatenation: “12 34”, 12 followed by 34. (Characters are assumed to be the part of the same number unless split by syntax or whitespace.) Union: “7|11”, a 7 or 11. Groups: “7(6|8)”, a 7 followed by a 6 or an 8. Wildcard: “.”, any value within the domain. Classes: “[3-6 7]”, a 3,4,5,6, or 7. Negated classes: “[^3 5]”, any value within the domain except for a 3 or a 5. Quantifiers: Asterisk: “12*”, 0 or more times a 12. Question mark: “5?”, 0 or 1 times a 5. (optional) Plus sign: “42+”, 1 or more time a 42. Exact: “1{3}”, exactly 3 times a 1. At least: “9{5,}”, 5 or more times a 9. Between: “7{3,5}”, at least 3 times, but at most 5 times a 7. Members of enumerated types can be used in place of any integer (e.g., “A B”, A followed by B). Enumerated identifiers still use whitespace for concatenation.

regular_nfa¶

 1. 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) 2. 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)  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). The sequence of values in array x (which must all be in the range S) is accepted by the NFA of Q states with input S and transition function d (which maps (1..Q, 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).

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)  1, 2. Represents the constraint x in t where we consider each row in t to be a tuple and t as a set of tuples. Represents the constraint x in t if the variable x_i and the value t_i occur where we consider each row in t to be a tuple and t as a set of tuples.