automaton(Signature, SourcesSinks, Arcs) since release 4.1automaton(Sequence, Template, Signature, SourcesSinks, Arcs, Counters, Initial, Final)automaton(Sequence, Template, Signature, SourcesSinks, Arcs, Counters, Initial, Final, Options) since release 4.1- 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, 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, 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, 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), 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), 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, 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(N,L,Opt) which should hold if 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/3The 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] ? ;
no
This constraint uses techniques from [Beldiceanu, Carlsson & Petit 04] and [Beldiceanu, Carlsson, Flener & Pearson 10].