Vars represents the variables that are to be satisfied for this constraint. It can be one collection of variables (or integers), or a collection of a collections of variables (or integers), if the constraint is to be satisfied by more than one collection of variables. Each collection can be of different size, i.e. have different number of variables. Posting the constraint with multiple collections of variables is logically equivalent to posting individual constraint with the same DFA for each collection, but should be more efficient as the same is shared by all the collections.
A collection of variables in Vars represents a sequence (i.e. they are ordered), and the DFA describes the values that can be taken by the sequence of variables, starting from the first variable, the DFA starts at the Start state, and moves to the next variable in the sequence via a transition given in Transition. A transition is a triple (from,to,input) that specifies the move from one state of the DFA to another (from,to), accompanied by the labelling of the original variable with the value specified by input. A transition is specified using the named structure trans(f,l,t), for the transition from state f to t (states are non-negative integers), and l is the input -- the integer value a variable is labelled to by the transition. The DFA is deterministic in that there should be at most a single transition for for each unique input and from state.
In addition to the transitions, the DFA requires a unique start state, which is given by Start, and must terminate in one of the final states, which is given in Finals as a collection of values. The Transitions, Start and Finals are mapped onto the data structures for representing a DFA in Gecode. Note however that for Gecode, both the final states and the Transitions must be terminated with a dummy entry (finals with a -1 state, and transitions with a transition with a -1 for the from state), these dummy entries are added by gfd before the constraint is passed to Gecode, so the user should not supply these entries.
The possible values for a sequence of variables can also be specified by regular/2, and using regular expression is probably more convenient. Both constraints map to same underlying implementation. For a sequence of fixed length, the solutions can also be specified using the table/2 constraint.
ConsistencyModule is the optional module specification to give the consistency level for the propagation for this constraint: gfd_gac for generalised arc consistency (domain consistency).
This constraint is implemented in Gecode as the extensional() constraint with the variant that takes a DFA as an argument.
[eclipse 7]: L = [A,B,C,D,E], extensional(L, [trans(0,0,0),trans(0,1,1),trans(1,0,0)], 0, [0]), labeling(L), writeln(L), fail. [0, 0, 0, 0, 0] [0, 0, 0, 1, 0] [0, 0, 1, 0, 0] [0, 1, 0, 0, 0] [0, 1, 0, 1, 0] [1, 0, 0, 0, 0] [1, 0, 0, 1, 0] [1, 0, 1, 0, 0] No (0.00s cpu)