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: xs,
                   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: total_cost)

Requires that xs defines a path in the cost MDD with total edge weight total_cost.

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

cost_regular

predicate cost_regular(array [int] of var int: xs,
                       int: Q,
                       int: S,
                       array [int,int] of int: d,
                       int: q0,
                       set of int: F,
                       array [int,int] of int: cost,
                       var int: total_cost)

The sequence of values in array xs (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 cost, and total_cost is the sum of cost taken on the accepting path for xs.

mdd

predicate mdd(array [int] of var int: xs,
              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 xs 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(xs)+1
E: the number of edges
from: the leaving node (1..N)for each edge
label: the set of values of the xs 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: xs,
                     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 xs 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(xs)+1
E: the number of edges
from: the leaving node (1..N)for each edge
label: the set of values of the xs variable for each edge
to: the entering node for each edge, where 0 = T node

regular

1.  predicate regular(array [$$X] of var $$Val: xs,
                      array [$$State,$$Val] of opt $$State: d,
                      $$State: q0,
                      set of $$State: F)

2.  predicate regular(array [int] of var int: xs,
                      int: Q,
                      int: S,
                      array [int,int] of int: d,
                      int: q0,
                      set of int: F)

3.  predicate regular(array [int] of var int: xs,
                      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 $$E: xs, string: regexp)

The sequence of values in array xs is accepted by the DFA with transition function d, initial state q0 and accepting states F. The transition function maps states (from enumerated type State) and values (from type Val) to states, or the absent value if the transition is not possible.
The sequence of values in array xs (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 xs (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 xs is accepted by the regular expression regexp. 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 [$$X] of var $$Val: xs,
                          array [$$State,$$Val] of set of $$State: d,
                          $$State: q0,
                          set of $$State: F)

2.  predicate regular_nfa(array [int] of var int: xs,
                          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: xs,
                          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 xs is accepted by the NFA with transition function d, initial state q0 and accepting states F. The transition function maps states (from enumerated type State) and values (from type Val) to sets of states.
The sequence of values in array xs (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 xs (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: xs,
                    array [$$X,$$E] of bool: tuples)

2.  predicate table(array [$$E] of var int: xs,
                    array [$$X,$$E] of int: tuples)

3.  predicate table(array [$$E] of var opt int: xs,
                    array [$$X,$$E] of opt int: tuples)

1, 2.: Represents the constraint xs in tuples where we consider each row in tuples to be a tuple and tuples as a set of tuples.

Represents the constraint xs in tuples if the variable x_i and the value t_i occur where we consider each row in tuples to be a tuple and tuples as a set of tuples.