Describes a list of finite domain variables with a finite
automaton. True iff the finite automaton induced by Nodes and Arcs
(extended with Counters) accepts Signature. Sequence is a list of
terms, all of the same shape. Additional constraints must link
Sequence to Signature, if necessary. Nodes is a list of
source(Node) and sink(Node) terms. Arcs is a list of
arc(Node,Integer,Node) and arc(Node,Integer,Node,Exprs) terms that
denote the automaton's transitions. Each node is represented by an
arbitrary term. Transitions that are not mentioned go to an
implicit failure node. Exprs is a list of arithmetic expressions,
of the same length as Counters. In each expression, variables
occurring in Counters symbolically refer to previous counter
values, and variables occurring in Template refer to the current
element of Sequence. When a transition containing arithmetic
expressions is taken, each counter is updated according to the
result of the corresponding expression. When a transition without
arithmetic expressions is taken, all counters remain unchanged.
Counters is a list of variables. Initials is a list of finite
domain variables or integers denoting, in the same order, the
initial value of each counter. These values are related to Finals
according to the arithmetic expressions of the taken transitions.
The following example is taken from Beldiceanu, Carlsson, Debruyne
and Petit: "Reformulation of Global Constraints Based on
Constraints Checkers", Constraints 10(4), pp 339-362 (2005). It
relates a sequence of integers and finite domain variables to its
number of inflexions, which are switches between strictly ascending
and strictly descending subsequences:
sequence_inflexions(Vs, N) :-
variables_signature(Vs, Sigs),
automaton(Sigs, _, Sigs,
[source(s),sink(i),sink(j),sink(s)],
[arc(s,0,s), arc(s,1,j), arc(s,2,i),
arc(i,0,i), arc(i,1,j,[C+1]), arc(i,2,i),
arc(j,0,j), arc(j,1,j),
arc(j,2,i,[C+1])],
[C], [0], [N]).
variables_signature([], []).
variables_signature([V|Vs], Sigs) :-
variables_signature_(Vs, V, Sigs).
variables_signature_([], _, []).
variables_signature_([V|Vs], Prev, [S|Sigs]) :-
V #= Prev #<==> S #= 0,
Prev #< V #<==> S #= 1,
Prev #> V #<==> S #= 2,
variables_signature_(Vs, V, Sigs).
Example queries:
?- sequence_inflexions([1,2,3,3,2,1,3,0], N).
N = 3.
?- length(Ls, 5), Ls ins 0..1,
sequence_inflexions(Ls, 3), label(Ls).
Ls = [0, 1, 0, 1, 0] ;
Ls = [1, 0, 1, 0, 1].
