Generated on Tue Mar 24 2020 14:04:04 for Gecode by doxygen 1.8.17
dfa.cpp
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Christian Schulte <schulte@gecode.org>
5  *
6  * Copyright:
7  * Christian Schulte, 2004
8  *
9  * This file is part of Gecode, the generic constraint
10  * development environment:
11  * http://www.gecode.org
12  *
13  * Permission is hereby granted, free of charge, to any person obtaining
14  * a copy of this software and associated documentation files (the
15  * "Software"), to deal in the Software without restriction, including
16  * without limitation the rights to use, copy, modify, merge, publish,
17  * distribute, sublicense, and/or sell copies of the Software, and to
18  * permit persons to whom the Software is furnished to do so, subject to
19  * the following conditions:
20  *
21  * The above copyright notice and this permission notice shall be
22  * included in all copies or substantial portions of the Software.
23  *
24  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
25  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
26  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
27  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
28  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
29  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
30  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
31  *
32  */
33 
34 #include <gecode/int.hh>
35 
36 namespace Gecode { namespace Int { namespace Extensional {
37 
42  public:
43  forceinline bool
45  return x.i_state < y.i_state;
46  }
47  forceinline static void
48  sort(DFA::Transition t[], int n) {
49  TransByI_State tbis;
50  Support::quicksort<DFA::Transition,TransByI_State>(t,n,tbis);
51  }
52  };
53 
57  class TransBySymbol {
58  public:
59  forceinline bool
61  return x.symbol < y.symbol;
62  }
63  forceinline static void
64  sort(DFA::Transition t[], int n) {
65  TransBySymbol tbs;
66  Support::quicksort<DFA::Transition,TransBySymbol>(t,n,tbs);
67  }
68  };
69 
74  public:
75  forceinline bool
77  return ((x.symbol < y.symbol) ||
78  ((x.symbol == y.symbol) && (x.i_state < y.i_state)));
79  }
80  forceinline static void
81  sort(DFA::Transition t[], int n) {
83  Support::quicksort<DFA::Transition,TransBySymbolI_State>(t,n,tbsi);
84  }
85  };
86 
91  public:
92  forceinline bool
94  return x.o_state < y.o_state;
95  }
96  forceinline static void
97  sort(DFA::Transition t[], int n) {
98  TransByO_State tbos;
99  Support::quicksort<DFA::Transition,TransByO_State>(t,n,tbos);
100  }
101  };
102 
103 
107  class StateGroup {
108  public:
109  int state;
110  int group;
111  };
112 
117  public:
118  forceinline bool
119  operator ()(const StateGroup& x, const StateGroup& y) {
120  return ((x.group < y.group) ||
121  ((x.group == y.group) && (x.state < y.state)));
122  }
123  static void
124  sort(StateGroup sg[], int n) {
126  Support::quicksort<StateGroup,StateGroupByGroup>(sg,n,o);
127  }
128  };
129 
133  class GroupStates {
134  public:
137  };
138 
140  enum StateInfo {
141  SI_NONE = 0,
144  SI_FINAL = 4
145  };
146 
147 }}}
148 
149 namespace Gecode {
150 
151  void
152  DFA::init(int start, Transition t_spec[], int f_spec[], bool minimize) {
153  using namespace Int;
154  using namespace Extensional;
155  Region region;
156 
157  // Compute number of states and transitions
158  int n_states = start;
159  int n_trans = 0;
160  for (Transition* t = &t_spec[0]; t->i_state >= 0; t++) {
161  n_states = std::max(n_states,t->i_state);
162  n_states = std::max(n_states,t->o_state);
163  n_trans++;
164  }
165  for (int* f = &f_spec[0]; *f >= 0; f++)
167  n_states++;
168 
169  // Temporary structure for transitions
170  Transition* trans = region.alloc<Transition>(n_trans);
171  for (int i=0; i<n_trans; i++)
172  trans[i] = t_spec[i];
173  // Temporary structures for finals
174  int* final = region.alloc<int>(n_states+1);
175  bool* is_final = region.alloc<bool>(n_states+1);
176  int n_finals = 0;
177  for (int i=0; i<n_states+1; i++)
178  is_final[i] = false;
179  for (int* f = &f_spec[0]; *f != -1; f++) {
180  is_final[*f] = true;
181  final[n_finals++] = *f;
182  }
183 
184  if (minimize) {
185  // Sort transitions by symbol and i_state
186  TransBySymbolI_State::sort(trans, n_trans);
187  Transition** idx = region.alloc<Transition*>(n_trans+1);
188  // idx[i]...idx[i+1]-1 gives where transitions for symbol i start
189  int n_symbols = 0;
190  {
191  int j = 0;
192  while (j < n_trans) {
193  idx[n_symbols++] = &trans[j];
194  int s = trans[j].symbol;
195  while ((j < n_trans) && (s == trans[j].symbol))
196  j++;
197  }
198  idx[n_symbols] = &trans[j];
199  assert(j == n_trans);
200  }
201  // Map states to groups
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);
205  // Initialize: final states is group one, all other group zero
206  for (int i=0; i<n_states+1; i++) {
207  part[i].state = i;
208  part[i].group = is_final[i] ? 1 : 0;
209  s2g[i] = part[i].group;
210  }
211  // Important: the state n_state is the dead state, conceptually
212  // if there is no transition for a symbol and input state, it is
213  // assumed that there is an implicit transition to n_state
214 
215  // Set up the indexing data structure, sort by group
217  int n_groups;
218  if (part[0].group == part[n_states].group) {
219  // No final states, just one group
220  g2s[0].fst = &part[0]; g2s[0].lst = &part[n_states+1];
221  n_groups = 1;
222  } else {
223  int i = 0;
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];
228  n_groups = 2;
229  }
230 
231  // Do the refinement
232  {
233  int m_groups;
234  do {
235  m_groups = n_groups;
236  // Iterate over symbols
237  for (int sidx = n_symbols; sidx--; ) {
238  // Iterate over groups
239  for (int g = n_groups; g--; ) {
240  // Ignore singleton groups
241  if (g2s[g].lst-g2s[g].fst > 1) {
242  // Apply transitions to group states
243  // This exploits that both transitions as well as
244  // stategroups are sorted by (input) state
245  Transition* t = idx[sidx];
246  Transition* t_lst = idx[sidx+1];
247  for (StateGroup* sg = g2s[g].fst; sg<g2s[g].lst; sg++) {
248  while ((t < t_lst) && (t->i_state < sg->state))
249  t++;
250  // Compute group resulting from transition
251  if ((t < t_lst) && (t->i_state == sg->state))
252  sg->group = s2g[t->o_state];
253  else
254  sg->group = s2g[n_states]; // Go to dead state
255  }
256  // Sort group by groups from transitions
257  StateGroupByGroup::sort(g2s[g].fst,
258  static_cast<int>(g2s[g].lst-g2s[g].fst));
259  // Group must be split?
260  if (g2s[g].fst->group != (g2s[g].lst-1)->group) {
261  // Skip first group
262  StateGroup* sg = g2s[g].fst+1;
263  while ((sg-1)->group == sg->group)
264  sg++;
265  // Start splitting
266  StateGroup* lst = g2s[g].lst;
267  g2s[g].lst = sg;
268  while (sg < 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++;
273  }
274  g2s[n_groups++].lst = sg;
275  }
276  }
277  }
278  }
279  }
280  } while (n_groups != m_groups);
281  // New start state
282  start = s2g[start];
283  // Compute new final states
284  n_finals = 0;
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;
289  break;
290  }
291  // Compute representatives
292  int* s2r = region.alloc<int>(n_states+1);
293  for (int i=0; i<n_states+1; i++)
294  s2r[i] = -1;
295  for (int g=0; g<n_groups; g++)
296  s2r[g2s[g].fst->state] = g;
297  // Clean transitions
298  int j = 0;
299  for (int i = 0; i<n_trans; i++)
300  if (s2r[trans[i].i_state] != -1) {
301  trans[j].i_state = s2g[trans[i].i_state];
302  trans[j].symbol = trans[i].symbol;
303  trans[j].o_state = s2g[trans[i].o_state];
304  j++;
305  }
306  n_trans = j;
307  n_states = n_groups;
308  }
309  }
310 
311  // Do a reachability analysis for all states starting from start state
313  int* state = region.alloc<int>(n_states);
314  for (int i=0; i<n_states; i++)
315  state[i] = SI_NONE;
316 
317  Transition** idx = region.alloc<Transition*>(n_states+1);
318  {
319  // Sort all transitions according to i_state and create index structure
320  // idx[i]...idx[i+1]-1 gives where transitions for state i start
321  TransByI_State::sort(trans, n_trans);
322  {
323  int j = 0;
324  for (int i=0; i<n_states; i++) {
325  idx[i] = &trans[j];
326  while ((j < n_trans) && (i == trans[j].i_state))
327  j++;
328  }
329  idx[n_states] = &trans[j];
330  assert(j == n_trans);
331  }
332 
333  state[start] = SI_FROM_START;
334  visit.push(start);
335  while (!visit.empty()) {
336  int s = visit.pop();
337  for (Transition* t = idx[s]; t < idx[s+1]; t++)
338  if (!(state[t->o_state] & SI_FROM_START)) {
339  state[t->o_state] |= SI_FROM_START;
340  visit.push(t->o_state);
341  }
342  }
343  }
344 
345  // Do a reachability analysis for all states to a final state
346  {
347  // Sort all transitions according to o_state and create index structure
348  // idx[i]...idx[i+1]-1 gives where transitions for state i start
349  TransByO_State::sort(trans, n_trans);
350  {
351  int j = 0;
352  for (int i=0; i<n_states; i++) {
353  idx[i] = &trans[j];
354  while ((j < n_trans) && (i == trans[j].o_state))
355  j++;
356  }
357  idx[n_states] = &trans[j];
358  assert(j == n_trans);
359  }
360 
361  for (int i=0; i<n_finals; i++) {
362  state[final[i]] |= (SI_TO_FINAL | SI_FINAL);
363  visit.push(final[i]);
364  }
365  while (!visit.empty()) {
366  int s = visit.pop();
367  for (Transition* t = idx[s]; t < idx[s+1]; t++)
368  if (!(state[t->i_state] & SI_TO_FINAL)) {
369  state[t->i_state] |= SI_TO_FINAL;
370  visit.push(t->i_state);
371  }
372  }
373  }
374 
375  // Now all reachable states are known (also the final ones)
376  int* re = region.alloc<int>(n_states);
377  for (int i=0; i<n_states; i++)
378  re[i] = -1;
379 
380  // Renumber states
381  int m_states = 0;
382  // Start state gets zero
383  re[start] = m_states++;
384 
385  // Renumber final states
386  for (int i=n_states; i--; )
387  if ((state[i] == (SI_FINAL | SI_FROM_START | SI_TO_FINAL)) && (re[i] < 0))
388  re[i] = m_states++;
389  // If start state is final, final states start from zero, otherwise from one
390  int final_fst = (state[start] & SI_FINAL) ? 0 : 1;
391  int final_lst = m_states;
392  // final_fst...final_lst-1 are the final states
393 
394  // Renumber remaining states
395  for (int i=n_states; i--; )
396  if ((state[i] == (SI_FROM_START | SI_TO_FINAL)) && (re[i] < 0))
397  re[i] = m_states++;
398 
399  // Count number of remaining transitions
400  int m_trans = 0;
401  for (int i=n_trans; i--; )
402  if ((re[trans[i].i_state] >= 0) && (re[trans[i].o_state] >= 0))
403  m_trans++;
404 
405  // All done... Construct the automaton
406  DFAI* d = new DFAI(m_trans);
407  d->n_states = m_states;
408  d->n_trans = m_trans;
409  d->final_fst = final_fst;
410  d->final_lst = final_lst;
411  {
412  int j = 0;
413  Transition* r = &d->trans[0];
414  for (int i = 0; i<n_trans; i++)
415  if ((re[trans[i].i_state] >= 0) && (re[trans[i].o_state] >= 0)) {
416  r[j].symbol = trans[i].symbol;
417  r[j].i_state = re[trans[i].i_state];
418  r[j].o_state = re[trans[i].o_state];
419  j++;
420  }
421  TransBySymbol::sort(r,m_trans);
422  }
423  {
424  // Count number of symbols
425  unsigned int n_symbols = 0;
426  for (int i = 0; i<m_trans; ) {
427  int s = d->trans[i++].symbol;
428  n_symbols++;
429  while ((i<m_trans) && (d->trans[i].symbol == s))
430  i++;
431  }
432  d->n_symbols = n_symbols;
433  }
434  {
435  // Compute maximal degree
436  unsigned int max_degree = 0;
437  unsigned int* deg = region.alloc<unsigned int>(m_states);
438 
439  // Compute in-degree per state
440  for (int i=0; i<m_states; i++)
441  deg[i] = 0;
442  for (int i=0; i<m_trans; i++)
443  deg[d->trans[i].o_state]++;
444  for (int i=0; i<m_states; i++)
446 
447  // Compute out-degree per state
448  for (int i=0; i<m_states; i++)
449  deg[i] = 0;
450  for (int i=0; i<m_trans; i++)
451  deg[d->trans[i].i_state]++;
452  for (int i=0; i<m_states; i++)
454 
455  // Compute transitions per symbol
456  {
457  int i=0;
458  while (i < m_trans) {
459  int j=i++;
460  while ((i < m_trans) &&
461  (d->trans[j].symbol == d->trans[i].symbol))
462  i++;
463  max_degree = std::max(max_degree,static_cast<unsigned int>(i-j));
464  }
465  }
466 
467  d->max_degree = max_degree;
468  }
469 
470  d->fill();
471  object(d);
472  }
473 
474  DFA::DFA(int start, Transition t_spec[], int f_spec[], bool minimize) {
475  init(start,t_spec,f_spec,minimize);
476  }
477 
478  DFA::DFA(int start, std::initializer_list<Transition> tl,
479  std::initializer_list<int> fl, bool minimize) {
480  Region reg;
481  int nt = static_cast<int>(tl.size());
482  int nf = static_cast<int>(fl.size());
483  Transition* ts = reg.alloc<Transition>(nt + 1);
484  {
485  int i=0;
486  for (const Transition& t : tl)
487  ts[i++] = t;
488  ts[nt].i_state = -1;
489  }
490  int* fs = reg.alloc<int>(nf + 1);
491  {
492  int i=0;
493  for (const int& f : fl)
494  fs[i++] = f;
495  fs[nf] = -1;
496  }
497  init(start,ts,fs,minimize);
498  }
499 
500  bool
501  DFA::equal(const DFA& d) const {
502  assert(n_states() == d.n_states());
503  assert(n_transitions() == d.n_transitions());
504  assert(n_symbols() == d.n_symbols());
505  assert(final_fst() == d.final_fst());
506  assert(final_lst() == d.final_lst());
507  DFA::Transitions me(*this);
508  DFA::Transitions they(d);
509  while (me()) {
510  if (me.i_state() != they.i_state())
511  return false;
512  if (me.symbol() != they.symbol())
513  return false;
514  if (me.o_state() != they.o_state())
515  return false;
516  ++me;
517  ++they;
518  }
519  return true;
520  }
521 
522 }
523 
524 // STATISTICS: int-prop
525 
Post propagator for SetVar x
Definition: set.hh:767
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:767
Sort transition array by output state.
Definition: dfa.cpp:90
static void sort(DFA::Transition t[], int n)
Definition: dfa.cpp:48
Sort transition array by symbol and then input states.
Definition: dfa.cpp:73
StateInfo
Information about states.
Definition: dfa.cpp:140
int i_state
input state
Definition: int.hh:2060
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
Definition: dfa.cpp:44
Sort transition array by symbol (value)
Definition: dfa.cpp:57
@ SI_NONE
State is not reachable.
Definition: dfa.cpp:141
Stack with fixed number of elements.
T * alloc(long unsigned int n)
Allocate block of n objects of type T from region.
Definition: region.hpp:386
SharedHandle::Object * object(void) const
Access to the shared object.
NodeType t
Type of node.
Definition: bool-expr.cpp:230
int final_fst(void) const
Return the number of the first final state.
Definition: dfa.hpp:163
int state
Definition: dfa.cpp:109
DFA(void)
Initialize for DFA accepting the empty word.
Definition: dfa.hpp:131
int n_transitions(void) const
Return the number of transitions.
Definition: dfa.hpp:151
int symbol
symbol
Definition: int.hh:2061
@ SI_FINAL
State is final.
Definition: dfa.cpp:144
static void sort(StateGroup sg[], int n)
Definition: dfa.cpp:124
static void sort(DFA::Transition t[], int n)
Definition: dfa.cpp:81
Sort transition array by input state.
Definition: dfa.cpp:41
Gecode toplevel namespace
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
Definition: dfa.cpp:93
@ SI_FROM_START
State is reachable from start state.
Definition: dfa.cpp:142
unsigned int n_symbols(void) const
Return the number of symbols.
Definition: dfa.hpp:145
Specification of a DFA transition.
Definition: int.hh:2058
Handle to region.
Definition: region.hpp:55
GroupStates is used to index StateGroup by group
Definition: dfa.cpp:133
int o_state
output state Default constructor
Definition: int.hh:2062
Post propagator for SetVar SetOpType SetVar SetRelType r
Definition: set.hh:767
bool empty(void) const
Test whether stack is empty.
void sort(TaskViewArray< TaskView > &t)
Sort task view array t according to sto and inc (increasing or decreasing)
Definition: sort.hpp:133
Stategroup is used to compute a partition of states.
Definition: dfa.cpp:107
T pop(void)
Pop topmost element from stack and return it.
Iterator for DFA transitions (sorted by symbols)
Definition: int.hh:2069
unsigned int max_degree(void) const
Return maximal degree (in-degree and out-degree) of any state.
Definition: dfa.hpp:157
Sort groups stated by group and then state.
Definition: dfa.cpp:116
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
Definition: dfa.cpp:76
static void sort(DFA::Transition t[], int n)
Definition: dfa.cpp:97
@ SI_TO_FINAL
Final state is reachable from state.
Definition: dfa.cpp:143
int n_states(void) const
Return the number of states.
Definition: dfa.hpp:139
StateGroup * fst
Definition: dfa.cpp:135
Data stored for a DFA.
Definition: dfa.hpp:42
StateGroup * lst
Definition: dfa.cpp:136
Deterministic finite automaton (DFA)
Definition: int.hh:2049
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
Definition: dfa.cpp:60
int final_lst(void) const
Return the number of the last final state.
Definition: dfa.hpp:169
Gecode::IntSet d(v, 7)
void push(const T &x)
Push element x on top of stack.
#define forceinline
Definition: config.hpp:185
bool operator()(const StateGroup &x, const StateGroup &y)
Definition: dfa.cpp:119
static void sort(DFA::Transition t[], int n)
Definition: dfa.cpp:64
int group
Definition: dfa.cpp:110
Post propagator for f(x \diamond_{\mathit{op}} y) \sim_r z \f$ void rel(Home home
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:234
void init(int s, Transition t[], int f[], bool minimize=true)
Initialize DFA.
Definition: dfa.cpp:152
Gecode::IntArgs i({1, 2, 3, 4})
const FloatNum max
Largest allowed float value.
Definition: float.hh:844