The following constraint provides a general way of defining any
constraint involving sequences whose *checker*, i.e. a procedure
that classifies ground instances as solutions or non-solutions, can be
expressed by a finite automaton, deterministic or nondeterministic,
extended with counter operations on its arcs. The point is that it is
very much easier to come up with such a checker than to come up with a
filtering algorithm for the constraint of interest. In the absence of
counters, it maintains domain consistency.

Corresponds to `regular/6`

in MiniZinc.

`automaton(`

`Signature`,`SourcesSinks`,`Arcs`)*since release 4.1*`automaton(`

`Sequence`,`Template`,`Signature`,`SourcesSinks`,`Arcs`,`Counters`,`Initial`,`Final`)`automaton(`

`Sequence`,`Template`,`Signature`,`SourcesSinks`,`Arcs`,`Counters`,`Initial`,`Final`,`Options`)*since release 4.1*-
The arguments are described below in terms of their abstract syntax:

`Sequence`The sequence of terms of interest; abstract grammar category

`sequence`.`Template`A template for an item of the sequence; abstract grammar category

`template`. Only relevant if some state transition involving counter arithmetic mentions a variable occurring in`Template`, in which case the corresponding term in a sequence element will be accessed.`Signature`The

*signature*of`Sequence`; abstract grammar category`signature`. The automaton is not driven by`Sequence`itself, but by`Signature`, which ranges over some alphabet, implicitly defined by the values used by`Arcs`. In addition to`automaton/[8,9]`

, you must call a constraint that maps`Sequence`to`Signature`.`SourcesSinks`The source and sink nodes of the automaton; abstract grammar category

`sourcessinks`.`Arcs`The arcs (transitions) of the automaton; abstract grammar category

`arcs`. Any transition not mentioned is assumed to go to an implicit failure node. An arc optionally contains expressions for updated counter values; by default, the counters remain unchanged. Conditional updates can be specified.`Counters`A list of variables, local to the constraint; abstract grammar category

`counters`.`Initial`A list of initial values, usually instantiated; abstract grammar category

`initial`.`Final`A list of final values, usually uninstantiated; abstract grammar category

`final`.`Options`Abstract grammar category

`options`; a list of zero or more of the following terms. All but the last option are implemented by adding auxiliary counters to the automaton including the necessary updates in the arcs:`valueprec(`

`First`,`Later`,`N`)*since release 4.1.3*-
`N`is unified with`n`, computed such that: if the value`Later`occurs in the`Signature`, then`First`occurs`n`times before the first occurrence of`Later`, otherwise`n=0`. `anystretchocc(`

`N`)*since release 4.1.3*-
`N`is unified with the number of (nonempty) stretches of any single value in the`Signature`. `stretchocc(`

`ValuePat`,`N`)*since release 4.1.3*-
`N`is unified with the number of stretches of values matching`ValuePat`(abstract grammar category`valuepat`) in the`Signature`. `stretchoccmod(`

`ValuePat`,`Mod`,`N`)*since release 4.1.3*-
`N`is unified with the number (modulo`Mod`) of stretches of values matching`ValuePat`(abstract grammar category`valuepat`) the`Signature`. `stretchmaxlen(`

`ValuePat`,`N`)*since release 4.1.3*-
`N`is unified with`n`, computed such that: if values matching`ValuePat`(abstract grammar category`valuepat`) occur the`Signature`, then`n`is the length of the longest such stretch, otherwise`n=0`. `stretchminlen(`

`ValuePat`,`N`)*since release 4.1.3*-
`N`is unified with`n`, computed such that: if values matching`ValuePat`(abstract grammar category`valuepat`) occur the`Signature`, then`n`is the length of the shortest such stretch, otherwise`n`is a large integer. `wordocc(`

`WordPat`,`N`)*since release 4.1.3*-
`N`is unified with the number of words matching`WordPat`(abstract grammar category`wordpat`) in the`Signature`. `wordoccmod(`

`WordPat`,`Mod`,`N`)*since release 4.1.3*-
`N`is unified with the number (modulo`Mod`) of words matching`WordPat`(abstract grammar category`wordpat`) in the`Signature`. `wordprefix(`

`WordPat`,`ZO`)*since release 4.1.3*-
If the prefix of the

`Signature`matches`WordPat`(abstract grammar category`wordpat`), then`ZO`is unified with 1, otherwise with 0. `wordsuffix(`

`WordPat`,`ZO`)*since release 4.1.3*-
If the suffix of the

`Signature`matches`WordPat`(abstract grammar category`wordpat`), then`ZO`is unified with 1, otherwise with 0. `state(`

`Map`,`StateSequence`)*since release 4.1*-
For a signature of length

`k`, the constraint is implemented by decomposition into`k`smaller constraints mapping an old state to a new state. The states are represented as domain variables.`StateSequence`forms the list of these`k+1`domain variables, starting with the initial state and ending with the final state.`Map`gives the interpretation of their values: it is a list of pairs`Node-Value`such that if the nth state variable`Sn`equals`Value`, then the automaton is in state`Node`having read`n`symbols. `counterseq(`

`CounterSequence`)*since release 4.2.1*-
Similarly to the list of states,

`CounterSequence`forms the list of the`k+1`instances of`Counters`, beginning with`Initial`and ending with`Final`.

Abstract syntax:

`sequence`::= `list of template`{all of which of the same shape} `template`::= `term`{most general shape of the `sequence`}{its variables should be local to the constraint} `signature`::= `list of variable``sourcessinks`::= `list of nodespec``nodespec`::= `source(`

`node`){an initial state} | `sink(`

`node`){an accept state} `node`::= `term``arcs`::= `list of arc``arc`::= `arc(`

`node`,`integer`,`node`){from node, integer, to node} | `arc(`

`node`,`integer`,`node`,`exprs`){ `exprs`correspond to new counter values}| `arc(`

`node`,`integer`,`node`,`conditional`)`conditional`::= `(cond -> exprs)`| `(conditional ; conditional)``exprs`::= `list of Expr`{of same length as `counters`}{ `Expr`as defined in Syntax of Arithmetic Expressions}{over `counters`,`template`and constants}{variables occurring in `counters`correspond to old counter values}{variables occurring in `template`refer to the current element of`sequence`}`cond`::= `constraint`{over `counters`,`template`and constants}{must be reifiable or `true`

}`counters`::= `list of variable`{should be local to the constraint} `initial`::= `list of dvar`{of same length as `counters`}`final`::= `list of dvar`{of same length as `counters`}`option`::= `state(`

`list of term`,`list of dvar`)| `valueprec(`

`integer`,`integer`,`dvar`)| `anystretchocc(`

`dvar`)| `stretchocc(`

`valuepat`,`dvar`)| `stretchoccmod(`

`valuepat`,`dvar`,`integer`)| `stretchmaxlen(`

`valuepat`,`dvar`)| `stretchminlen(`

`valuepat`,`dvar`)| `wordocc(`

`wordpat`,`dvar`)| `wordoccmod(`

`wordpat`,`dvar`,`integer`)| `wordprefix(`

`wordpat`,`dvar`)| `wordsuffix(`

`wordpat`,`dvar`)`valuepat`::= `integer`| `list of integer`{alternatives} | `valuepat``/`

`valuepat`{alternatives} `wordpat`::= `list of valuepat``dvar`::= `variable or integer`If no counters are used, then the arguments

`Counters`,`Initial`and`Final`should be`[]`

. The arguments`Template`and`Sequence`are only relevant if some`Expr`mentions a variable in`Template`, in which case the corresponding position in`Sequence`will be used at that point.The constraint holds for a ground instance

`Sequence`if:-
`Signature`is the signature corresponding to`Sequence`. - The finite automaton encoded by
`SourcesSinks`and`Arcs`stops in an accept state. - Any counter arithmetic on the transitions map their
`Initial`values to the`Final`values. - Any extra constraint imposed by
`Options`are true.

Here is an example. Suppose that you want to define the predicate

`inflexion(`

which should hold if`N`,`L`,`Opt`)`L`is a list of domain variables, and`N`is the number of times that the sequence order switches between strictly increasing and strictly decreasing. For example, the sequence`[1,1,4,8,8,2,7,1]`

switches order three times.Such a constraint is conveniently expressed by a finite automaton over the alphabet

`[<,=,>]`

denoting the order between consecutive list elements. A counter is incremented when the order switches, and is mapped to the first argument of the constraint. The automaton could look as follows:

Automaton for`inflexion/3`

The following piece of code encodes this using

`automaton/9`

. The auxiliary predicate`inflexion_signature/2`

maps the sequence to a signature where the consecutive element order is encoded over the alphabet`[0,1,2]`

. We use one counter with initial value 0 and final value`N`(an argument of`inflexion/3`

). Two transitions increment the counter. All states are accept states.inflexion(N, Vars, Opt) :- inflexion_signature(Vars, Sign), automaton(Sign, _, Sign, [source(s),sink(i),sink(j),sink(s)], [arc(s,1,s ), arc(s,2,i ), arc(s,0,j ), arc(i,1,i ), arc(i,2,i ), arc(i,0,j,[C+1]), arc(j,1,j ), arc(j,0,j ), arc(j,2,i,[C+1])], [C],[0],[N],Opt). inflexion_signature([], []). inflexion_signature([_], []) :- !. inflexion_signature([X,Y|Ys], [S|Ss]) :- S in 0..2, X #> Y #<=> S #= 0, X #= Y #<=> S #= 1, X #< Y #<=> S #= 2, inflexion_signature([Y|Ys], Ss).

Some queries:

/* count the #inflections of a ground string */ | ?-

`inflexion(N, [1,1,4,8,8,2,7,1], []).`N = 3 ? RET yes/* find strings with two inflections */ | ?-

`length(L,4), domain(L,0,1),``inflexion(2,L,[]), labeling([],L).`L = [0,1,0,1] ?`;`L = [1,0,1,0] ?`;`no/* find strings that are strictly increasing, strictly decreasing or all equal */ | ?-

`length(L,4), domain(L,0,3),``inflexion(I,L,[anystretchocc(1)]), labeling([],L).`I = 0, L = [0,0,0,0] ?`;`I = 0, L = [0,1,2,3] ?`;`I = 0, L = [1,1,1,1] ?`;`I = 0, L = [2,2,2,2] ?`;`I = 0, L = [3,2,1,0] ?`;`I = 0, L = [3,3,3,3] ?`;`no/* find strings that contain an increase followed by a decrease */ | ?-

`length(L,4), domain(L,0,1),``inflexion(I,L,[wordocc([2,0],1)]), labeling([],L).`I = 1, L = [0,0,1,0] ?`;`I = 1, L = [0,1,0,0] ?`;`I = 2, L = [0,1,0,1] ?`;`I = 2, L = [1,0,1,0] ?`;`noThis constraint uses techniques from [Beldiceanu, Carlsson & Petit 04] and [Beldiceanu, Carlsson, Flener & Pearson 10].

Send feedback on this subject.