/*
Decomposition of global constraint regular in Picat.
This is a translation of the MiniZinc decomposition of
regular, see below for some comments.
Note: Picat v0.4 includes a built-in regular/6.
Here's a description of the transition tables.
Note that input can never be 0 since it is used for no state.
Example: regexp 123*21
Transition = [
% inputs: 1 2 3
[2, 0, 0], % transitions from state 1: -2-> state 2 [start]
[0, 3, 0], % transitions from state 2: -3-> state 3 %
[0, 4, 3], % transitions from state 3: -3-> state 3, -2-> state 4
[5, 0, 0], % transitions from state 4: -1-> state 5 [final]
[0, 0, 0] % transitions from state 5: (none)
],
InitialState = 1,
AcceptingStates = [5]
The states are numbered from 1..Transition.length.
The initial state is in InitialState, i.e. the state Transition[InitialState].
The columns are the inputs (the column index), e.g. the first state ([2, 0, 0])
means that it only accept a "1" (first column), and then go to state 2 ([0, 3, 0],
which only accept a "2" (second column) and go to state 3 ([0, 4, 3]) with the
following meaning:
- if "1": not accepted
- if "2": goto state 4
- if "3": goto state 3 (loop)
And the DFA now goto through the states. The accepting state in this
example is only state 5 (AcceptingStates must be a list).
Model created by Hakan Kjellerstrand, hakank@gmail.com
See also my Picat page: http://www.hakank.org/picat/
*/
import util.
import cp.
main => go.
% Testing regexp 123*21
go ?=>
dfa(1,Transition,NStates,InputMax,InitialState,AcceptingStates),
% decision variables
N :: 2..10,
indomain(N),
println(n=N),
X = new_list(N),
X :: 1..3,
regular(X,NStates,InputMax,Transition,InitialState, AcceptingStates),
Vars = X,
solve([ff], Vars),
println('x '=X),
fail,
nl.
go => true.
%
% same as go/0 but we also get the state list (A)
% using regular2/7.
%
go1b ?=>
dfa(1,Transition,NStates,InputMax,InitialState,AcceptingStates),
% decision variables
N :: 2..10,
indomain(N),
println(n=N),
X = new_list(N),
X :: 1..3,
regular2(X,NStates,InputMax,Transition,InitialState, AcceptingStates,A),
Vars = X,
solve([ff], Vars),
println('x '=X),
println('A '=A),
fail,
nl.
go1b => true.
go2 ?=>
dfa(2,Transition,NStates,InputMax,InitialState,AcceptingStates),
N = 11,
X = new_list(N),
X :: 1..3,
regular(X,NStates,InputMax,Transition,InitialState, AcceptingStates),
Vars = X,
solve([ff], Vars),
println('x '=X),
fail,
nl.
go2 => true.
go3 ?=>
dfa(3,Transition,NStates,InputMax,InitialState,AcceptingStates),
N = 10,
X = new_list(N),
X :: 1..3,
regular(X,NStates,InputMax,Transition,InitialState, AcceptingStates),
Vars = X,
solve([ff], Vars),
println('x '=X),
fail,
nl.
go3 => true.
go4 ?=>
dfa(4,Transition,NStates,InputMax,InitialState,AcceptingStates),
N = 10,
X = new_list(N),
X :: 1..3,
regular(X,NStates,InputMax,Transition,InitialState, AcceptingStates),
Vars = X,
solve([ff], Vars),
println('x '=X),
fail,
nl.
go4 => true.
go5 ?=>
dfa(5,Transition,NStates,InputMax,InitialState,AcceptingStates),
N = 8,
X = new_list(N),
X :: 1..3,
regular(X,NStates,InputMax,Transition,InitialState, AcceptingStates),
Vars = X,
solve([ff], Vars),
println('x '=X),
fail,
nl.
go5 => true.
%
% same as go6/0 but also exposing A, the state array.
%
go6 ?=>
dfa(6,Transition,NStates,InputMax,InitialState,AcceptingStates),
N = 3,
X = new_list(N),
X :: 1..3,
regular(X,NStates,InputMax,Transition,InitialState, AcceptingStates),
Vars = X,
solve([ff], Vars),
println('x '=X),
fail,
nl.
go6 => true.
go6b ?=>
dfa(6,Transition,NStates,InputMax,InitialState,AcceptingStates),
N = 3,
X = new_list(N),
X :: 1..3,
regular2(X,NStates,InputMax,Transition,InitialState, AcceptingStates,A),
Vars = X,
solve([ff], Vars),
println('x '=X),
println('A '=A),
nl,
fail,
nl.
go6b => true.
%
% even number of 1s and 2s
%
go7 ?=>
dfa(7,Transition,NStates,InputMax,InitialState,AcceptingStates),
N = 10,
X = new_list(N),
X :: 1..2,
regular(X,NStates,InputMax,Transition,InitialState, AcceptingStates),
Vars = X,
solve([ff], Vars),
println('x '=X),
println(['1s'=sum([1 : E in X, E =1]),'2s'=sum([1 : E in X, E = 2])]),
fail,
nl.
go7 => true.
% Later note: Since v0.4, Picat includes a built-in regular/6 predicate
% (in part based on this decomposition).
%
/*
This is a translation of MiniZinc's regular constraint (defined in
lib/zinc/globals.mzn), via the Comet code refered above.
All comments are from the MiniZinc code.
"""
The sequence of values in array 'x' (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.
"""
x : IntVar array
Q : number of states
S : input_max
d : transition matrix
q0: initial state
F : accepting states
*/
my_regular(X, Q, S, D, Q0, F) =>
% """
% If x has index set m..n-1, then a[m] holds the initial state
% (q0), and a[i+1] holds the state we're in after processing
% x[i]. If a[n] is in F, then we succeed (ie. accept the string).
% """
M = 1,
N2 = X.length+1,
A = new_array(N2),
A :: 1..Q,
X :: 1..S, % """Do this in case it's a var."""
A[M] #= Q0, % Set a[0], initial state
foreach(I in 1..X.length)
% X[I] :: 1..S, % Do this in case it's a var.
% Here is MiniZinc's infamous matrix element
% which I try to translate here:
% a[i+1] = d[a[i], x[i]]
matrix_element(D,A[I], X[I], A[I+1])
end,
element(_,F,A[N2]).
% member(A[N2], F). % """Check the final state is in F."""
% A[N2] :: F. % """Check the final state is in F."""
%
% regular2/7 is the same as regular/6 but it also returns A,
% the state list. This might be handy for debugging or
% explorations.
%
regular2(X, Q, S, D, Q0, F,A) =>
% """
% If x has index set m..n-1, then a[m] holds the initial state
% (q0), and a[i+1] holds the state we're in after processing
% x[i]. If a[n] is in F, then we succeed (ie. accept the string).
% """
M = 1,
N2 = X.length+1,
A = new_array(N2),
A :: 1..Q,
X :: 1..S, % """Do this in case it's a var."""
A[M] #= Q0, % Set a[0], initial state
foreach(I in 1..X.length)
% X[I] :: 1..S, % """Do this in case it's a var."""
% This is MiniZinc's infamous matrix element which I try to
% translate to Picat:
% a[i+1] = d[a[i], x[i]]
matrix_element(D,A[I], X[I], A[I+1])
end,
member(A[N2], F). % """Check the final state is in F."""
% A[N2] :: F. % """Check the final state is in F."""
%
% diverse matrix_element/4 to test
%
%%
%% matrix_element/4
%% by Neng-Fa Zhou and Hakan Kjellerstrand
%%
matrix_element(M,I,J,Val) => matrix_element_cp(M,I,J,Val).
matrix_element_cp(M,I,J,Val),list(M) =>
list_matrix_to_array_matrix(M) = M1,
matrix_element_aux(M1,I,J,Val).
matrix_element_cp(M,I,J,Val),array(M) =>
matrix_element_aux(M,I,J,Val).
matrix_element_aux(M,I,J,Val) =>
NRows = M.length,
NCols = M[1].length,
if not valid_matrix(M,NRows,NCols) then
handle_exception($invalid_matrix(M),matrix_element)
end,
I :: 1..NRows,
J :: 1..NCols,
if ground(M) then
Table = [(R,C,M[R,C]) : R in 1..NRows, C in 1..NCols],
table_in((I,J,Val),Table)
else
wait_until_ij(M,I,J,Val)
end.
valid_matrix(M,NRows,NCols) =>
foreach(R in 2..NRows)
M[R].length==NCols
end.
% wait until I and J becomes non-var
wait_until_ij(_M,I,J,_Val),var(I),{ins(I),ins(J)} => true.
wait_until_ij(_M,_I,J,_Val),var(J),{ins(J)} => true.
wait_until_ij(M,I,J,Val) => Val=M[I,J].
%
% DFA examples
%
% regexp 123*21
dfa(1,Transition,NStates,InputMax,InitialState,AcceptingStates) =>
Transition = [
[2, 0, 0], % transitions from state 1: -2-> state 2
[0, 3, 0], % transitions from state 2: -3-> state 3 %
[0, 4, 3], % transitions from state 3: -3-> state 3, -2-> state 4
[5, 0, 0], % transitions from state 4: -1-> state 5
[0, 0, 0] % transitions from state 5: (none)
],
NStates = 5,
InputMax = 3,
InitialState = 1,
AcceptingStates = [5].
% This example is from
% "Handbook of Constraint programming", page 180
%
%
% ^(c+|a+b+a+){n}$
% ^(3+|1+2+1+){n}$
%
% Or: aa*bb* + cc*
%
% "It accepts the strings 'aaabaa' and 'cc', but not 'aacbba'."
%
dfa(2,Transition,NStates,InputMax,InitialState,AcceptingStates) =>
Transition = [
% inputs
% 1 2 3
[2,0,5], % 1 start
[2,3,0], % 2 loop + next
[4,3,0], % 3 next + loop
[4,0,0], % 4 loop + end state
[0,0,5] % 5 loop and end state
],
NStates = 5,
InputMax = 3,
AcceptingStates = [4,5],
InitialState = 1.
%
% Example1 from Choco http://www.emn.fr/x-info/choco-solver/doku.php?id=regular
%
% First example
% t.add(new Transition(0, 1, 1));
% t.add(new Transition(1, 1, 2));
% t.add(new Transition(2, 1, 3));
%
% t.add(new Transition(3, 3, 0));
% t.add(new Transition(0, 3, 0));
%
dfa(3,Transition,NStates,InputMax,InitialState,AcceptingStates) =>
Transition = [
[2, 0, 1], % 1
[3, 0, 0], % 2
[0, 4, 0], % 3
[0, 0, 1] % 4
],
NStates = Transition.length,
InputMax = 4,
InitialState = 1,
AcceptingStates = [4].
%
% Example2 from Choco http://www.emn.fr/x-info/choco-solver/doku.php?id=regular
%
% This is an all_equal constraint. The initial_state decides which
% values it will be
dfa(4,Transition,NStates,InputMax,InitialState,AcceptingStates) =>
Transition = [
[1, 0, 0, 0], % 1 (start)
[0, 2, 0, 0], % 2
[0, 0, 3, 0], % 3
[0, 0, 0, 4] % 4
],
NStates = Transition.length,
InputMax = 4,
InitialState = 3,
AcceptingStates = 1..4.
%
% Example3 from Choco http://www.emn.fr/x-info/choco-solver/doku.php?id=regular
%
% This is stretchPath, not regular
% lgt.add(new int[]{2, 2, 2}); // stretches of value 2 are exactly of size 2
% lgt.add(new int[]{0, 2, 2}); // stretches of value 0 are exactly of size 2
% lgt.add(new int[]{1, 2, 3}); // stretches of value 1 are at least of size 2 and at most 3
%
% This should be interpreted as:
% 0{2}1{2,3}2{2}
% for all permutations of 0,1,and 2.
% Or rather:
% 1{2}2{2,3}3{2}
% for all permutations of 1,2, and 3 since 0 is not allowed as an input value...
%
dfa(5,Transition,NStates,InputMax,InitialState,AcceptingStates) =>
Transition = [
[2, 4, 7], % 1 (start)
[3, 0, 0], % 2
[0, 4, 7], % 3 (end)
[0, 5, 0], % 4
[2, 6, 7], % 5 (end)
[2, 0, 7], % 6 (end)
[0, 0, 8], % 7
[2, 4, 0] % 8 (end)
],
NStates = Transition.length,
InputMax = 3,
InitialState = 1,
AcceptingStates = [3,5,6,8].
%
% All different.
% This works in principle (here is n=3), but the automaton will
% be forbiddingly large for larger arrays.
%
dfa(6,Transition,NStates,InputMax,InitialState,AcceptingStates) =>
Transition = [
% 1 2 3
[ 2, 7, 12], % 1 (start)
[ 0, 3, 5], % 2
[ 0, 0, 4], % 3
[ 0, 0, 0], % 4
[ 0, 6, 0], % 5
[ 0, 0, 0], % 6
[ 8, 0, 10], % 7
[ 0, 0, 9], % 8
[ 0, 0, 0], % 9
[11, 0, 0], % 10
[ 0, 0, 0], % 11
[13, 15, 0], % 12
[ 0, 14, 0], % 13
[ 0, 0, 0], % 14
[ 16, 0, 0], % 15
[ 0, 0, 0] % 16
],
NStates = Transition.length,
InputMax = 3,
InitialState = 1,
AcceptingStates = [4,6,9,11,14,16].
%
% "Need Regular Expression for Finite Automata: Even number of 1s and Even number of 0s"
% http://stackoverflow.com/questions/17420332/need-regular-expression-for-finite-automata-even-number-of-1s-and-even-number-o
%
% Q1 <- 1 -> Q2
% ^ ^
% | |
% 2 2
% | |
% v v
% Q4 <- 1 -> Q3
%
dfa(7,Transition,NStates,InputMax,InitialState,AcceptingStates) =>
Transition = [
% 1 2
[ 2, 4], % state 1 Q1 start, final
[ 1, 3], % state 2 Q2
[ 4, 2], % state 3 Q3
[ 3, 1] % state 4 Q4
],
NStates = Transition.length,
InputMax = 2,
InitialState = 1,
AcceptingStates = [1].