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