Generated on Sat Jun 2 2018 07:17:44 for Gecode by doxygen 1.8.13
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  DFA::DFA(int start, Transition t_spec[], int f_spec[], bool minimize) {
152  using namespace Int;
153  using namespace Extensional;
154  // Compute number of states and transitions
155  int n_states = start;
156  int n_trans = 0;
157  for (Transition* t = &t_spec[0]; t->i_state >= 0; t++) {
158  n_states = std::max(n_states,t->i_state);
159  n_states = std::max(n_states,t->o_state);
160  n_trans++;
161  }
162  for (int* f = &f_spec[0]; *f >= 0; f++)
163  n_states = std::max(n_states,*f);
164  n_states++;
165 
166  // Temporary structure for transitions
167  Transition* trans = heap.alloc<Transition>(n_trans);
168  for (int i = n_trans; i--; )
169  trans[i] = t_spec[i];
170  // Temporary structures for finals
171  int* final = heap.alloc<int>(n_states+1);
172  bool* is_final = heap.alloc<bool>(n_states+1);
173  int n_finals = 0;
174  for (int i = n_states+1; i--; )
175  is_final[i] = false;
176  for (int* f = &f_spec[0]; *f != -1; f++) {
177  is_final[*f] = true;
178  final[n_finals++] = *f;
179  }
180 
181  if (minimize) {
182  // Sort transitions by symbol and i_state
183  TransBySymbolI_State::sort(trans, n_trans);
184  Transition** idx = heap.alloc<Transition*>(n_trans+1);
185  // idx[i]...idx[i+1]-1 gives where transitions for symbol i start
186  int n_symbols = 0;
187  {
188  int j = 0;
189  while (j < n_trans) {
190  idx[n_symbols++] = &trans[j];
191  int s = trans[j].symbol;
192  while ((j < n_trans) && (s == trans[j].symbol))
193  j++;
194  }
195  idx[n_symbols] = &trans[j];
196  assert(j == n_trans);
197  }
198  // Map states to groups
199  int* s2g = heap.alloc<int>(n_states+1);
200  StateGroup* part = heap.alloc<StateGroup>(n_states+1);
201  GroupStates* g2s = heap.alloc<GroupStates>(n_states+1);
202  // Initialize: final states is group one, all other group zero
203  for (int i = n_states+1; i--; ) {
204  part[i].state = i;
205  part[i].group = is_final[i] ? 1 : 0;
206  s2g[i] = part[i].group;
207  }
208  // Important: the state n_state is the dead state, conceptually
209  // if there is no transition for a symbol and input state, it is
210  // assumed that there is an implicit transition to n_state
211 
212  // Set up the indexing data structure, sort by group
213  StateGroupByGroup::sort(part,n_states+1);
214  int n_groups;
215  if (part[0].group == part[n_states].group) {
216  // No final states, just one group
217  g2s[0].fst = &part[0]; g2s[0].lst = &part[n_states+1];
218  n_groups = 1;
219  } else {
220  int i = 0;
221  assert(part[0].group == 0);
222  do i++; while (part[i].group == 0);
223  g2s[0].fst = &part[0]; g2s[0].lst = &part[i];
224  g2s[1].fst = &part[i]; g2s[1].lst = &part[n_states+1];
225  n_groups = 2;
226  }
227 
228  // Do the refinement
229  {
230  int m_groups;
231  do {
232  m_groups = n_groups;
233  // Iterate over symbols
234  for (int sidx = n_symbols; sidx--; ) {
235  // Iterate over groups
236  for (int g = n_groups; g--; ) {
237  // Ignore singleton groups
238  if (g2s[g].lst-g2s[g].fst > 1) {
239  // Apply transitions to group states
240  // This exploits that both transitions as well as
241  // stategroups are sorted by (input) state
242  Transition* t = idx[sidx];
243  Transition* t_lst = idx[sidx+1];
244  for (StateGroup* sg = g2s[g].fst; sg<g2s[g].lst; sg++) {
245  while ((t < t_lst) && (t->i_state < sg->state))
246  t++;
247  // Compute group resulting from transition
248  if ((t < t_lst) && (t->i_state == sg->state))
249  sg->group = s2g[t->o_state];
250  else
251  sg->group = s2g[n_states]; // Go to dead state
252  }
253  // Sort group by groups from transitions
254  StateGroupByGroup::sort(g2s[g].fst,
255  static_cast<int>(g2s[g].lst-g2s[g].fst));
256  // Group must be split?
257  if (g2s[g].fst->group != (g2s[g].lst-1)->group) {
258  // Skip first group
259  StateGroup* sg = g2s[g].fst+1;
260  while ((sg-1)->group == sg->group)
261  sg++;
262  // Start splitting
263  StateGroup* lst = g2s[g].lst;
264  g2s[g].lst = sg;
265  while (sg < lst) {
266  s2g[sg->state] = n_groups;
267  g2s[n_groups].fst = sg++;
268  while ((sg < lst) && ((sg-1)->group == sg->group)) {
269  s2g[sg->state] = n_groups; sg++;
270  }
271  g2s[n_groups++].lst = sg;
272  }
273  }
274  }
275  }
276  }
277  } while (n_groups != m_groups);
278  // New start state
279  start = s2g[start];
280  // Compute new final states
281  n_finals = 0;
282  for (int g = n_groups; g--; )
283  for (StateGroup* sg = g2s[g].fst; sg < g2s[g].lst; sg++)
284  if (is_final[sg->state]) {
285  final[n_finals++] = g;
286  break;
287  }
288  // Compute representatives
289  int* s2r = heap.alloc<int>(n_states+1);
290  for (int i = n_states+1; i--; )
291  s2r[i] = -1;
292  for (int g = n_groups; g--; )
293  s2r[g2s[g].fst->state] = g;
294  // Clean transitions
295  int j = 0;
296  for (int i = 0; i<n_trans; i++)
297  if (s2r[trans[i].i_state] != -1) {
298  trans[j].i_state = s2g[trans[i].i_state];
299  trans[j].symbol = trans[i].symbol;
300  trans[j].o_state = s2g[trans[i].o_state];
301  j++;
302  }
303  n_trans = j;
304  n_states = n_groups;
305  heap.free<int>(s2r,n_states+1);
306  }
307  heap.free<GroupStates>(g2s,n_states+1);
308  heap.free<StateGroup>(part,n_states+1);
309  heap.free<int>(s2g,n_states+1);
310  heap.free<Transition*>(idx,n_trans+1);
311  }
312 
313  // Do a reachability analysis for all states starting from start state
315  int* state = heap.alloc<int>(n_states);
316  for (int i=n_states; i--; )
317  state[i] = SI_NONE;
318 
319  Transition** idx = heap.alloc<Transition*>(n_states+1);
320  {
321  // Sort all transitions according to i_state and create index structure
322  // idx[i]...idx[i+1]-1 gives where transitions for state i start
323  TransByI_State::sort(trans, n_trans);
324  {
325  int j = 0;
326  for (int i=0; i<n_states; i++) {
327  idx[i] = &trans[j];
328  while ((j < n_trans) && (i == trans[j].i_state))
329  j++;
330  }
331  idx[n_states] = &trans[j];
332  assert(j == n_trans);
333  }
334 
335  state[start] = SI_FROM_START;
336  visit.push(start);
337  while (!visit.empty()) {
338  int s = visit.pop();
339  for (Transition* t = idx[s]; t < idx[s+1]; t++)
340  if (!(state[t->o_state] & SI_FROM_START)) {
341  state[t->o_state] |= SI_FROM_START;
342  visit.push(t->o_state);
343  }
344  }
345  }
346 
347  // Do a reachability analysis for all states to a final state
348  {
349  // Sort all transitions according to o_state and create index structure
350  // idx[i]...idx[i+1]-1 gives where transitions for state i start
351  TransByO_State::sort(trans, n_trans);
352  {
353  int j = 0;
354  for (int i=0; i<n_states; i++) {
355  idx[i] = &trans[j];
356  while ((j < n_trans) && (i == trans[j].o_state))
357  j++;
358  }
359  idx[n_states] = &trans[j];
360  assert(j == n_trans);
361  }
362 
363  for (int i = n_finals; i--; ) {
364  state[final[i]] |= (SI_TO_FINAL | SI_FINAL);
365  visit.push(final[i]);
366  }
367  while (!visit.empty()) {
368  int s = visit.pop();
369  for (Transition* t = idx[s]; t < idx[s+1]; t++)
370  if (!(state[t->i_state] & SI_TO_FINAL)) {
371  state[t->i_state] |= SI_TO_FINAL;
372  visit.push(t->i_state);
373  }
374  }
375  }
376  heap.free<Transition*>(idx,n_states+1);
377  heap.free<int>(final,n_states+1);
378  heap.free<bool>(is_final,n_states+1);
379 
380  // Now all reachable states are known (also the final ones)
381  int* re = heap.alloc<int>(n_states);
382  for (int i = n_states; i--; )
383  re[i] = -1;
384 
385  // Renumber states
386  int m_states = 0;
387  // Start state gets zero
388  re[start] = m_states++;
389 
390  // Renumber final states
391  for (int i = n_states; i--; )
392  if ((state[i] == (SI_FINAL | SI_FROM_START | SI_TO_FINAL)) && (re[i] < 0))
393  re[i] = m_states++;
394  // If start state is final, final states start from zero, otherwise from one
395  int final_fst = (state[start] & SI_FINAL) ? 0 : 1;
396  int final_lst = m_states;
397  // final_fst...final_lst-1 are the final states
398 
399  // Renumber remaining states
400  for (int i = n_states; i--; )
401  if ((state[i] == (SI_FROM_START | SI_TO_FINAL)) && (re[i] < 0))
402  re[i] = m_states++;
403 
404  // Count number of remaining transitions
405  int m_trans = 0;
406  for (int i = n_trans; i--; )
407  if ((re[trans[i].i_state] >= 0) && (re[trans[i].o_state] >= 0))
408  m_trans++;
409 
410  // All done... Construct the automaton
411  DFAI* d = new DFAI(m_trans);
412  d->n_states = m_states;
413  d->n_trans = m_trans;
414  d->final_fst = final_fst;
415  d->final_lst = final_lst;
416  {
417  int j = 0;
418  Transition* r = &d->trans[0];
419  for (int i = 0; i<n_trans; i++)
420  if ((re[trans[i].i_state] >= 0) && (re[trans[i].o_state] >= 0)) {
421  r[j].symbol = trans[i].symbol;
422  r[j].i_state = re[trans[i].i_state];
423  r[j].o_state = re[trans[i].o_state];
424  j++;
425  }
426  TransBySymbol::sort(r,m_trans);
427  }
428  {
429  // Count number of symbols
430  unsigned int n_symbols = 0;
431  for (int i = 0; i<m_trans; ) {
432  int s = d->trans[i++].symbol;
433  n_symbols++;
434  while ((i<m_trans) && (d->trans[i].symbol == s))
435  i++;
436  }
437  d->n_symbols = n_symbols;
438  }
439  {
440  // Compute maximal degree
441  unsigned int max_degree = 0;
442  unsigned int* deg = heap.alloc<unsigned int>(m_states);
443 
444  // Compute in-degree per state
445  for (int i = m_states; i--; )
446  deg[i] = 0;
447  for (int i = m_trans; i--; )
448  deg[d->trans[i].o_state]++;
449  for (int i = m_states; i--; )
450  max_degree = std::max(max_degree,deg[i]);
451 
452  // Compute out-degree per state
453  for (int i = m_states; i--; )
454  deg[i] = 0;
455  for (int i = m_trans; i--; )
456  deg[d->trans[i].i_state]++;
457  for (int i = m_states; i--; )
458  max_degree = std::max(max_degree,deg[i]);
459 
460  heap.free<unsigned int>(deg,m_states);
461 
462  // Compute transitions per symbol
463  {
464  int i=0;
465  while (i < m_trans) {
466  int j=i++;
467  while ((i < m_trans) &&
468  (d->trans[j].symbol == d->trans[i].symbol))
469  i++;
470  max_degree = std::max(max_degree,static_cast<unsigned int>(i-j));
471  }
472  }
473 
474  d->max_degree = max_degree;
475  }
476 
477  d->fill();
478  object(d);
479  heap.free<int>(re,n_states);
480  heap.free<int>(state,n_states);
481  heap.free<Transition>(trans,n_trans);
482  }
483 
484  bool
485  DFA::equal(const DFA& d) const {
486  assert(n_states() == d.n_states());
487  assert(n_transitions() == d.n_transitions());
488  assert(n_symbols() == d.n_symbols());
489  assert(final_fst() == d.final_fst());
490  assert(final_lst() == d.final_lst());
491  DFA::Transitions me(*this);
492  DFA::Transitions they(d);
493  while (me()) {
494  if (me.i_state() != they.i_state())
495  return false;
496  if (me.symbol() != they.symbol())
497  return false;
498  if (me.o_state() != they.o_state())
499  return false;
500  ++me;
501  ++they;
502  }
503  return true;
504  }
505 
506 }
507 
508 // STATISTICS: int-prop
509 
static void sort(DFA::Transition t[], int n)
Definition: dfa.cpp:97
Sort transition array by symbol (value)
Definition: dfa.cpp:57
int i_state(void) const
Return in-state of current transition.
Definition: dfa.hpp:249
int symbol
symbol
Definition: int.hh:2035
NodeType t
Type of node.
Definition: bool-expr.cpp:230
int n_trans
Number of transitions.
Definition: dfa.hpp:49
int final_fst
First final state.
Definition: dfa.hpp:53
int final_fst(void) const
Return the number of the first final state.
Definition: dfa.hpp:163
static void sort(DFA::Transition t[], int n)
Definition: dfa.cpp:64
const FloatNum max
Largest allowed float value.
Definition: float.hh:844
static void sort(DFA::Transition t[], int n)
Definition: dfa.cpp:81
static void sort(StateGroup sg[], int n)
Definition: dfa.cpp:124
StateInfo
Information about states.
Definition: dfa.cpp:140
Sort transition array by output state.
Definition: dfa.cpp:90
State is not reachable.
Definition: dfa.cpp:141
State is reachable from start state.
Definition: dfa.cpp:142
#define forceinline
Definition: config.hpp:185
int i_state
input state
Definition: int.hh:2034
Stategroup is used to compute a partition of states.
Definition: dfa.cpp:107
Gecode::IntSet d(v, 7)
Transition * trans
The transitions.
Definition: dfa.hpp:59
static void sort(DFA::Transition t[], int n)
Definition: dfa.cpp:48
Deterministic finite automaton (DFA)
Definition: int.hh:2023
T * alloc(long unsigned int n)
Allocate block of n objects of type T from heap.
Definition: heap.hpp:431
Gecode::IntArgs i(4, 1, 2, 3, 4)
int n
Number of negative literals for node type.
Definition: bool-expr.cpp:234
int final_lst
Last final state.
Definition: dfa.hpp:55
GroupStates is used to index StateGroup by group
Definition: dfa.cpp:133
Sort transition array by input state.
Definition: dfa.cpp:41
int n_transitions(void) const
Return the number of transitions.
Definition: dfa.hpp:151
Specification of a DFA transition.
Definition: int.hh:2032
int o_state
output state Default constructor
Definition: int.hh:2036
unsigned int n_symbols
Number of symbols.
Definition: dfa.hpp:47
Final state is reachable from state.
Definition: dfa.cpp:143
Post propagator for SetVar SetOpType SetVar SetRelType r
Definition: set.hh:765
Post propagator for f(x \diamond_{\mathit{op}} y) \sim_r z \f$ void rel(Home home
Post propagator for SetVar SetOpType SetVar y
Definition: set.hh:765
void free(T *b, long unsigned int n)
Delete n objects starting at b.
Definition: heap.hpp:457
DFA(void)
Initialize for DFA accepting the empty word.
Definition: dfa.hpp:131
Heap heap
The single global heap.
Definition: heap.cpp:44
Sort transition array by symbol and then input states.
Definition: dfa.cpp:73
Stack with fixed number of elements.
void fill(void)
Fill hash table.
Definition: dfa.hpp:93
Data stored for a DFA.
Definition: dfa.hpp:42
Iterator for DFA transitions (sorted by symbols)
Definition: int.hh:2043
Sort groups stated by group and then state.
Definition: dfa.cpp:116
Post propagator for SetVar x
Definition: set.hh:765
int n_states
Number of states.
Definition: dfa.hpp:45
int n_states(void) const
Return the number of states.
Definition: dfa.hpp:139
bool operator()(const DFA::Transition &x, const DFA::Transition &y)
Definition: dfa.cpp:44
Gecode toplevel namespace
int final_lst(void) const
Return the number of the last final state.
Definition: dfa.hpp:169
unsigned int n_symbols(void) const
Return the number of symbols.
Definition: dfa.hpp:145
int symbol(void) const
Return symbol of current transition.
Definition: dfa.hpp:254
int o_state(void) const
Return out-state of current transition.
Definition: dfa.hpp:259
unsigned int max_degree
Maximal degree (in-degree and out-degree of any state) and maximal number of transitions per symbol...
Definition: dfa.hpp:51