36 namespace Gecode {
namespace Int {
namespace Extensional {
50 Support::quicksort<DFA::Transition,TransByI_State>(
t,
n,tbis);
66 Support::quicksort<DFA::Transition,TransBySymbol>(
t,
n,tbs);
83 Support::quicksort<DFA::Transition,TransBySymbolI_State>(
t,
n,tbsi);
99 Support::quicksort<DFA::Transition,TransByO_State>(
t,
n,tbos);
126 Support::quicksort<StateGroup,StateGroupByGroup>(sg,
n,o);
154 using namespace Extensional;
158 int n_states = start;
161 n_states =
std::max(n_states,
t->i_state);
162 n_states =
std::max(n_states,
t->o_state);
165 for (
int*
f = &f_spec[0]; *
f >= 0;
f++)
171 for (
int i=0;
i<n_trans;
i++)
172 trans[
i] = t_spec[
i];
174 int*
final = region.
alloc<
int>(n_states+1);
175 bool* is_final = region.
alloc<
bool>(n_states+1);
177 for (
int i=0;
i<n_states+1;
i++)
179 for (
int*
f = &f_spec[0]; *
f != -1;
f++) {
181 final[n_finals++] = *
f;
192 while (j < n_trans) {
193 idx[n_symbols++] = &trans[j];
195 while ((j < n_trans) && (s == trans[j].
symbol))
198 idx[n_symbols] = &trans[j];
199 assert(j == n_trans);
202 int* s2g = region.
alloc<
int>(n_states+1);
203 StateGroup* part = region.
alloc<StateGroup>(n_states+1);
204 GroupStates* g2s = region.
alloc<GroupStates>(n_states+1);
206 for (
int i=0;
i<n_states+1;
i++) {
208 part[
i].group = is_final[
i] ? 1 : 0;
209 s2g[
i] = part[
i].group;
218 if (part[0].group == part[n_states].group) {
220 g2s[0].fst = &part[0]; g2s[0].lst = &part[n_states+1];
224 assert(part[0].group == 0);
225 do i++;
while (part[i].group == 0);
226 g2s[0].fst = &part[0]; g2s[0].lst = &part[
i];
227 g2s[1].fst = &part[
i]; g2s[1].lst = &part[n_states+1];
237 for (
int sidx = n_symbols; sidx--; ) {
239 for (
int g = n_groups; g--; ) {
241 if (g2s[g].lst-g2s[g].fst > 1) {
247 for (StateGroup* sg = g2s[g].fst; sg<g2s[g].lst; sg++) {
248 while ((t < t_lst) && (t->
i_state < sg->state))
251 if ((t < t_lst) && (t->
i_state == sg->state))
254 sg->group = s2g[n_states];
258 static_cast<int>(g2s[g].lst-g2s[g].fst));
260 if (g2s[g].fst->group != (g2s[g].lst-1)->group) {
262 StateGroup* sg = g2s[g].fst+1;
263 while ((sg-1)->group == sg->group)
266 StateGroup* lst = g2s[g].lst;
269 s2g[sg->state] = n_groups;
270 g2s[n_groups].fst = sg++;
271 while ((sg < lst) && ((sg-1)->group == sg->group)) {
272 s2g[sg->state] = n_groups; sg++;
274 g2s[n_groups++].lst = sg;
280 }
while (n_groups != m_groups);
285 for (
int g = n_groups; g--; )
286 for (StateGroup* sg = g2s[g].fst; sg < g2s[g].lst; sg++)
287 if (is_final[sg->state]) {
288 final[n_finals++] = g;
292 int* s2r = region.
alloc<
int>(n_states+1);
293 for (
int i=0;
i<n_states+1;
i++)
295 for (
int g=0; g<n_groups; g++)
296 s2r[g2s[g].fst->state] = g;
299 for (
int i = 0;
i<n_trans;
i++)
300 if (s2r[trans[
i].i_state] != -1) {
302 trans[j].symbol = trans[
i].symbol;
303 trans[j].o_state = s2g[trans[
i].o_state];
313 int* state = region.
alloc<
int>(n_states);
314 for (
int i=0;
i<n_states;
i++)
324 for (
int i=0;
i<n_states;
i++) {
326 while ((j < n_trans) && (
i == trans[j].i_state))
329 idx[n_states] = &trans[j];
330 assert(j == n_trans);
335 while (!visit.
empty()) {
340 visit.
push(
t->o_state);
352 for (
int i=0;
i<n_states;
i++) {
354 while ((j < n_trans) && (
i == trans[j].o_state))
357 idx[n_states] = &trans[j];
358 assert(j == n_trans);
361 for (
int i=0;
i<n_finals;
i++) {
363 visit.
push(
final[
i]);
365 while (!visit.
empty()) {
370 visit.
push(
t->i_state);
376 int* re = region.
alloc<
int>(n_states);
377 for (
int i=0;
i<n_states;
i++)
383 re[start] = m_states++;
386 for (
int i=n_states;
i--; )
390 int final_fst = (state[start] &
SI_FINAL) ? 0 : 1;
391 int final_lst = m_states;
395 for (
int i=n_states;
i--; )
401 for (
int i=n_trans;
i--; )
402 if ((re[trans[
i].i_state] >= 0) && (re[trans[
i].
o_state] >= 0))
414 for (
int i = 0;
i<n_trans;
i++)
415 if ((re[trans[
i].i_state] >= 0) && (re[trans[
i].o_state] >= 0)) {
417 r[j].
i_state = re[trans[
i].i_state];
418 r[j].
o_state = re[trans[
i].o_state];
425 unsigned int n_symbols = 0;
426 for (
int i = 0;
i<m_trans; ) {
436 unsigned int max_degree = 0;
437 unsigned int* deg = region.
alloc<
unsigned int>(m_states);
440 for (
int i=0;
i<m_states;
i++)
442 for (
int i=0;
i<m_trans;
i++)
444 for (
int i=0;
i<m_states;
i++)
445 max_degree =
std::max(max_degree,deg[
i]);
448 for (
int i=0; i<m_states; i++)
450 for (
int i=0; i<m_trans; i++)
452 for (
int i=0; i<m_states; i++)
453 max_degree =
std::max(max_degree,deg[i]);
458 while (i < m_trans) {
460 while ((i < m_trans) &&
463 max_degree =
std::max(max_degree,static_cast<unsigned int>(i-j));
475 init(start,t_spec,f_spec,minimize);
478 DFA::DFA(
int start, std::initializer_list<Transition> tl,
479 std::initializer_list<int> fl,
bool minimize) {
481 int nt =
static_cast<int>(tl.size());
482 int nf =
static_cast<int>(fl.size());
490 int* fs = reg.
alloc<
int>(nf + 1);
493 for (
const int&
f : fl)
497 init(start,ts,fs,minimize);
501 DFA::equal(
const DFA&
d)
const {
510 if (me.i_state() != they.
i_state())
512 if (me.symbol() != they.
symbol())
514 if (me.o_state() != they.
o_state())
void push(const T &x)
Push element x on top of stack.
static void sort(DFA::Transition t[], int n)
Sort transition array by symbol (value)
int i_state(void) const
Return in-state of current transition.
int n_trans
Number of transitions.
int final_fst
First final state.
int final_fst(void) const
Return the number of the first final state.
void init(int s, Transition t[], int f[], bool minimize=true)
Initialize DFA.
static void sort(DFA::Transition t[], int n)
const FloatNum max
Largest allowed float value.
static void sort(DFA::Transition t[], int n)
T * alloc(long unsigned int n)
Allocate block of n objects of type T from region.
static void sort(StateGroup sg[], int n)
StateInfo
Information about states.
Sort transition array by output state.
bool empty(void) const
Test whether stack is empty.
State is reachable from start state.
Stategroup is used to compute a partition of states.
Transition * trans
The transitions.
static void sort(DFA::Transition t[], int n)
Deterministic finite automaton (DFA)
int n
Number of negative literals for node type.
int final_lst
Last final state.
Gecode::IntArgs i({1, 2, 3, 4})
GroupStates is used to index StateGroup by group
Sort transition array by input state.
int n_transitions(void) const
Return the number of transitions.
Specification of a DFA transition.
int o_state
output state Default constructor
unsigned int n_symbols
Number of symbols.
Final state is reachable from state.
Post propagator for SetVar SetOpType SetVar SetRelType r
Post propagator for f(x \diamond_{\mathit{op}} y) \sim_r z \f$ void rel(Home home
Post propagator for SetVar SetOpType SetVar y
DFA(void)
Initialize for DFA accepting the empty word.
Sort transition array by symbol and then input states.
Stack with fixed number of elements.
void fill(void)
Fill hash table.
Iterator for DFA transitions (sorted by symbols)
T pop(void)
Pop topmost element from stack and return it.
Sort groups stated by group and then state.
Post propagator for SetVar x
int n_states
Number of states.
int n_states(void) const
Return the number of states.
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
Gecode toplevel namespace
int final_lst(void) const
Return the number of the last final state.
unsigned int n_symbols(void) const
Return the number of symbols.
int symbol(void) const
Return symbol of current transition.
int o_state(void) const
Return out-state of current transition.
unsigned int max_degree
Maximal degree (in-degree and out-degree of any state) and maximal number of transitions per symbol...