Generated on Mon May 10 06:46:43 2010 for Gecode by doxygen 1.6.3

reg.cpp

Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Christian Schulte <schulte@gecode.org>
00005  *
00006  *  Copyright:
00007  *     Christian Schulte, 2004
00008  *
00009  *  Last modified:
00010  *     $Date: 2009-11-03 17:23:42 +0100 (Tue, 03 Nov 2009) $ by $Author: schulte $
00011  *     $Revision: 10032 $
00012  *
00013  *  This file is part of Gecode, the generic constraint
00014  *  development environment:
00015  *     http://www.gecode.org
00016  *
00017  *  Permission is hereby granted, free of charge, to any person obtaining
00018  *  a copy of this software and associated documentation files (the
00019  *  "Software"), to deal in the Software without restriction, including
00020  *  without limitation the rights to use, copy, modify, merge, publish,
00021  *  distribute, sublicense, and/or sell copies of the Software, and to
00022  *  permit persons to whom the Software is furnished to do so, subject to
00023  *  the following conditions:
00024  *
00025  *  The above copyright notice and this permission notice shall be
00026  *  included in all copies or substantial portions of the Software.
00027  *
00028  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00029  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00030  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00031  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00032  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00033  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00034  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00035  *
00036  */
00037 
00038 #include <gecode/minimodel.hh>
00039 
00040 namespace Gecode {
00041 
00042   namespace MiniModel {
00043 
00044     class PosSet;
00048     typedef Support::BlockAllocator<PosSet> PosSetAllocator;
00049 
00050     class NodeInfo;
00051     class PosInfo;
00052 
00053   }
00054 
00056   class REG::Exp {
00057   public:
00059     unsigned int use_cnt;
00060     unsigned int _n_pos;
00064     enum ExpType {
00065       ET_SYMBOL,
00066       ET_CONC,
00067       ET_OR,
00068       ET_STAR
00069     };
00071     ExpType type;
00073     union {
00075       int  symbol;
00077       Exp* kids[2];
00078     } data;
00079 
00080     MiniModel::PosSet*
00081     followpos(MiniModel::PosSetAllocator&,MiniModel::PosInfo*);
00082     void inc(void);
00083     void dec(void);
00084     unsigned int n_pos(void) const;
00086     template<class Char, class Traits>
00087     std::basic_ostream<Char,Traits>&
00088     print(std::basic_ostream<Char,Traits>& os) const;
00089 
00090     static void* operator new(size_t);
00091     static void  operator delete(void*);
00092   private:
00093     void dispose(void);
00094   };
00095 
00096 
00097   /*
00098    * Operations on expression nodes
00099    *
00100    */
00101 
00102 
00103   forceinline void*
00104   REG::Exp::operator new(size_t s) {
00105     return heap.ralloc(s);
00106   }
00107   forceinline void
00108   REG::Exp::operator delete(void*) {
00109     // Deallocation happens in dispose
00110   }
00111 
00112   void
00113   REG::Exp::dispose(void) {
00114     Support::DynamicStack<Exp*,Heap> todo(heap);
00115     todo.push(this);
00116     while (!todo.empty()) {
00117       Exp* e = todo.pop();
00118       switch (e->type) {
00119       case ET_OR:
00120       case ET_CONC:
00121         if ((e->data.kids[1] != NULL) && (--e->data.kids[1]->use_cnt == 0))
00122           todo.push(e->data.kids[1]);
00123       case ET_STAR:
00124         if ((e->data.kids[0] != NULL) && (--e->data.kids[0]->use_cnt == 0))
00125           todo.push(e->data.kids[0]);
00126       default: ;
00127       }
00128       heap.rfree(e);
00129     }
00130   }
00131 
00132   forceinline void
00133   REG::Exp::inc(void) {
00134     if (this != NULL)
00135       use_cnt++;
00136   }
00137   forceinline void
00138   REG::Exp::dec(void) {
00139     if ((this != NULL) && (--use_cnt == 0))
00140       dispose();
00141   }
00142 
00143 
00144   forceinline unsigned int
00145   REG::Exp::n_pos(void) const {
00146     return (this != NULL) ? _n_pos : 0;
00147   }
00148 
00149 
00150   /*
00151    * Regular expressions
00152    *
00153    */
00154 
00155   forceinline
00156   REG::REG(Exp* f) : e(f) {}
00157 
00158   REG::REG(void) : e(NULL) {}
00159 
00160   REG::REG(const REG& r) : e(r.e) {
00161     e->inc();
00162   }
00163 
00164   const REG&
00165   REG::operator =(const REG& r) {
00166     if (&r != this) {
00167       r.e->inc();
00168       e->dec();
00169       e = r.e;
00170     }
00171     return *this;
00172   }
00173 
00174   REG::~REG(void) {
00175     e->dec();
00176   }
00177 
00178   REG::REG(int s) : e(new Exp) {
00179     e->use_cnt     = 1;
00180     e->_n_pos      = 1;
00181     e->type        = REG::Exp::ET_SYMBOL;
00182     e->data.symbol = s;
00183   }
00184 
00185   REG::REG(const IntArgs& x) {
00186     int n = x.size();
00187     if (n < 1)
00188       throw MiniModel::TooFewArguments("REG");
00189     Exp** a = heap.alloc<Exp*>(n);
00190     // Initialize with symbols
00191     for (int i=n; i--; ) {
00192       a[i] = new Exp();
00193       a[i]->use_cnt     = 1;
00194       a[i]->_n_pos      = 1;
00195       a[i]->type        = REG::Exp::ET_SYMBOL;
00196       a[i]->data.symbol = x[i];
00197     }
00198     // Build a balanced tree of alternative nodes
00199     for (int m=n; m>1; ) {
00200       if (m & 1) {
00201         m -= 1;
00202         Exp* e1 = a[m];
00203         Exp* e2 = a[0];
00204         a[0] = new Exp;
00205         a[0]->use_cnt      = 1;
00206         a[0]->_n_pos       = e1->n_pos() + e2->n_pos();
00207         a[0]->type         = REG::Exp::ET_OR;
00208         a[0]->data.kids[0] = e1;
00209         a[0]->data.kids[1] = e2;
00210       } else {
00211         m >>= 1;
00212         for (int i=0; i<m; i++) {
00213           Exp* e1 = a[2*i];
00214           Exp* e2 = a[2*i+1];
00215           a[i] = new Exp;
00216           a[i]->use_cnt      = 1;
00217           a[i]->_n_pos       = e1->n_pos() + e2->n_pos();
00218           a[i]->type         = REG::Exp::ET_OR;
00219           a[i]->data.kids[0] = e1;
00220           a[i]->data.kids[1] = e2;
00221         }
00222       }
00223     }
00224     e = a[0];
00225     heap.free<Exp*>(a,n);
00226   }
00227 
00228   REG
00229   REG::operator |(const REG& r2) {
00230     if (e == r2.e)
00231       return *this;
00232     Exp* f = new Exp();
00233     f->use_cnt      = 1;
00234     f->_n_pos       = e->n_pos() + r2.e->n_pos();
00235     f->type         = REG::Exp::ET_OR;
00236     f->data.kids[0] = e;    e->inc();
00237     f->data.kids[1] = r2.e; r2.e->inc();
00238     REG r(f);
00239     return r;
00240   }
00241 
00242   REG&
00243   REG::operator |=(const REG& r2) {
00244     if (e == r2.e)
00245       return *this;
00246     Exp* f = new Exp();
00247     f->use_cnt      = 1;
00248     f->_n_pos       = e->n_pos() + r2.e->n_pos();
00249     f->type         = REG::Exp::ET_OR;
00250     f->data.kids[0] = e;
00251     f->data.kids[1] = r2.e; r2.e->inc();
00252     e=f;
00253     return *this;
00254   }
00255 
00256   REG
00257   REG::operator +(const REG& r2) {
00258     if (e == NULL)    return r2;
00259     if (r2.e == NULL) return *this;
00260     Exp* f = new Exp();
00261     f->use_cnt      = 1;
00262     f->_n_pos       = e->n_pos() + r2.e->n_pos();
00263     f->type         = REG::Exp::ET_CONC;
00264     f->data.kids[0] = e;    e->inc();
00265     f->data.kids[1] = r2.e; r2.e->inc();
00266     REG r(f);
00267     return r;
00268   }
00269 
00270   REG&
00271   REG::operator +=(const REG& r2) {
00272     if (r2.e == NULL)
00273       return *this;
00274     if (e == NULL) {
00275       e=r2.e; e->inc();
00276     } else {
00277       Exp* f = new Exp();
00278       f->use_cnt      = 1;
00279       f->_n_pos       = e->n_pos() + r2.e->n_pos();
00280       f->type         = REG::Exp::ET_CONC;
00281       f->data.kids[0] = e;
00282       f->data.kids[1] = r2.e; r2.e->inc();
00283       e=f;
00284     }
00285     return *this;
00286   }
00287 
00288   REG
00289   REG::operator *(void) {
00290     if ((e == NULL) || (e->type == REG::Exp::ET_STAR))
00291       return *this;
00292     Exp* f = new Exp();
00293     f->use_cnt      = 1;
00294     f->_n_pos       = e->n_pos();
00295     f->type         = REG::Exp::ET_STAR;
00296     f->data.kids[0] = e; e->inc();
00297     REG r(f);
00298     return r;
00299   }
00300 
00301   REG
00302   REG::operator ()(unsigned int n, unsigned int m) {
00303     REG r;
00304     if ((n>m) || (m == 0))
00305       return r;
00306     if (n>0) {
00307       int i = n;
00308       REG r0 = *this;
00309       while (i>0)
00310         if (i & 1) {
00311           r = r0+r; i--;
00312         } else {
00313           r0 = r0+r0; i >>= 1;
00314         }
00315     }
00316     if (m > n) {
00317       int i = m-n;
00318       REG s0;
00319       s0 = s0 | *this;
00320       REG s;
00321       while (i>0)
00322         if (i & 1) {
00323           s = s0+s; i--;
00324         } else {
00325           s0 = s0+s0; i >>= 1;
00326         }
00327       r = r + s;
00328     }
00329     return r;
00330   }
00331 
00332   REG
00333   REG::operator ()(unsigned int n) {
00334     REG r;
00335     if (n > 0) {
00336       REG r0 = *this;
00337       int i = n;
00338       while (i>0)
00339         if (i & 1) {
00340           r = r0+r; i--;
00341         } else {
00342           r0 = r0+r0; i >>= 1;
00343         }
00344     }
00345     return r+**this;
00346   }
00347 
00348   REG
00349   REG::operator +(void) {
00350     return this->operator ()(1);
00351   }
00352 
00353 
00354   namespace MiniModel {
00355 
00356     /*
00357      * Sets of positions
00358      *
00359      */
00360 
00364     enum PosSetCmp {
00365       PSC_LE,
00366       PSC_EQ,
00367       PSC_GR
00368     };
00369 
00373     class PosSet : public Support::BlockClient<PosSet> {
00374       // Maintain sets of positions in inverse order
00375       // This makes the check whether the last position is included
00376       // more efficient.
00377     public:
00378       int pos; PosSet* next;
00379 
00380       PosSet(void);
00381       PosSet(int);
00382 
00383       bool in(int) const;
00384       static PosSetCmp cmp(PosSet*,PosSet*);
00385       static PosSet*   cup(PosSetAllocator&,PosSet*,PosSet*);
00386     };
00387 
00388 
00389     forceinline
00390     PosSet::PosSet(void) {}
00391     forceinline
00392     PosSet::PosSet(int p) : pos(p), next(NULL) {}
00393 
00394 
00395     forceinline bool
00396     PosSet::in(int p) const {
00397       for (const PosSet* ps = this; ps != NULL; ps = ps->next)
00398         if (ps->pos == p) {
00399           return true;
00400         } else if (ps->pos < p) {
00401           return false;
00402         }
00403       return false;
00404     }
00405 
00406     forceinline PosSetCmp
00407     PosSet::cmp(PosSet* ps1, PosSet* ps2) {
00408       while ((ps1 != NULL) && (ps2 != NULL)) {
00409         if (ps1 == ps2)
00410           return PSC_EQ;
00411         if (ps1->pos < ps2->pos)
00412           return PSC_LE;
00413         if (ps1->pos > ps2->pos)
00414           return PSC_GR;
00415         ps1 = ps1->next; ps2 = ps2->next;
00416       }
00417       if (ps1 == ps2)
00418         return PSC_EQ;
00419       return ps1 == NULL ? PSC_LE : PSC_GR;
00420     }
00421 
00422     PosSet*
00423     PosSet::cup(PosSetAllocator& psm, PosSet* ps1, PosSet* ps2) {
00424       PosSet*  ps;
00425       PosSet** p = &ps;
00426       while ((ps1 != NULL) && (ps2 != NULL)) {
00427         if (ps1 == ps2) {
00428           *p = ps1; return ps;
00429         }
00430         PosSet* n = new (psm) PosSet;
00431         *p = n; p = &n->next;
00432         if (ps1->pos == ps2->pos) {
00433           n->pos = ps1->pos;
00434           ps1 = ps1->next; ps2 = ps2->next;
00435         } else if (ps1->pos > ps2->pos) {
00436           n->pos = ps1->pos; ps1 = ps1->next;
00437         } else {
00438           n->pos = ps2->pos; ps2 = ps2->next;
00439         }
00440       }
00441       *p = (ps1 != NULL) ? ps1 : ps2;
00442       return ps;
00443     }
00444 
00445 
00447     class NodeInfo {
00448     public:
00449       bool    nullable;
00450       PosSet* firstpos;
00451       PosSet* lastpos;
00452       NodeInfo(bool n=false, PosSet* fp=NULL, PosSet* lp=NULL);
00453     };
00454 
00456     class ExpInfo {
00457     public:
00458       REG::Exp* exp;
00459       bool open;
00460       ExpInfo(REG::Exp* e=NULL);
00461     };
00462     
00467     class PosInfo {
00468     public:
00469       int     symbol;
00470       PosSet* followpos;
00471     };
00472 
00473     forceinline
00474     NodeInfo::NodeInfo(bool n, PosSet* fp, PosSet* lp)
00475       : nullable(n), firstpos(fp), lastpos(lp) {}
00476 
00477     forceinline
00478     ExpInfo::ExpInfo(REG::Exp* e)
00479       : exp(e), open(true) {}
00480 
00481   }
00482 
00483   forceinline MiniModel::PosSet*
00484   REG::Exp::followpos(MiniModel::PosSetAllocator& psm,
00485                       MiniModel::PosInfo* pi) {
00486     int p=0;
00487 
00488     using MiniModel::PosSet;
00489     using MiniModel::NodeInfo;
00490     using MiniModel::ExpInfo;
00491 
00492     Support::DynamicStack<ExpInfo,Heap> todo(heap);
00493     Support::DynamicStack<NodeInfo,Heap> done(heap);
00494 
00495     // Start with first expression to be processed
00496     todo.push(ExpInfo(this));
00497 
00498     do {
00499       if (todo.top().exp == NULL) {
00500         todo.pop();
00501         done.push(NodeInfo(true,NULL,NULL));
00502       } else {
00503         switch (todo.top().exp->type) {
00504         case ET_SYMBOL:
00505           {
00506             pi[p].symbol = todo.pop().exp->data.symbol;
00507             PosSet* ps = new (psm) PosSet(p++);
00508             done.push(NodeInfo(false,ps,ps));
00509           }
00510           break;
00511         case ET_STAR:
00512           if (todo.top().open) {
00513             // Evaluate subexpression recursively
00514             todo.top().open = false;
00515             todo.push(todo.top().exp->data.kids[0]);
00516           } else {
00517             todo.pop();
00518             NodeInfo ni = done.pop();
00519             for (PosSet* ps = ni.lastpos; ps != NULL; ps = ps->next)
00520               pi[ps->pos].followpos =
00521                 PosSet::cup(psm,pi[ps->pos].followpos,ni.firstpos);
00522             done.push(NodeInfo(true,ni.firstpos,ni.lastpos));
00523           }
00524           break;
00525         case ET_CONC:
00526           if (todo.top().open) {
00527             // Evaluate subexpressions recursively
00528             todo.top().open = false;
00529             REG::Exp* e = todo.top().exp;
00530             todo.push(e->data.kids[1]);
00531             todo.push(e->data.kids[0]);
00532           } else {
00533             todo.pop();
00534             NodeInfo ni1 = done.pop();
00535             NodeInfo ni0 = done.pop();
00536             for (PosSet* ps = ni0.lastpos; ps != NULL; ps = ps->next)
00537               pi[ps->pos].followpos =
00538                 PosSet::cup(psm,pi[ps->pos].followpos,ni1.firstpos);
00539             done.push(NodeInfo(ni0.nullable & ni1.nullable,
00540                                ni0.nullable ? 
00541                                PosSet::cup(psm,ni0.firstpos,ni1.firstpos) : ni0.firstpos,
00542                                ni1.nullable ? 
00543                                PosSet::cup(psm,ni0.lastpos,ni1.lastpos) : ni1.lastpos));
00544           }
00545           break;
00546         case ET_OR:
00547           if (todo.top().open) {
00548             // Evaluate subexpressions recursively
00549             todo.top().open = false;
00550             REG::Exp* e = todo.top().exp;
00551             todo.push(e->data.kids[1]);
00552             todo.push(e->data.kids[0]);
00553           } else {
00554             todo.pop();
00555             NodeInfo ni1 = done.pop();
00556             NodeInfo ni0 = done.pop();
00557             done.push(NodeInfo(ni0.nullable | ni1.nullable,
00558                                PosSet::cup(psm,ni0.firstpos,ni1.firstpos),
00559                                PosSet::cup(psm,ni0.lastpos,ni1.lastpos)));
00560           }
00561           break;
00562         default: GECODE_NEVER;
00563         }
00564       }
00565     } while (!todo.empty());
00566     return done.top().firstpos;
00567   }
00568 
00569     
00570   namespace MiniModel {
00571 
00572     class StateNode;
00573 
00577     typedef Support::BlockAllocator<StateNode> StatePoolAllocator;
00578 
00582     class StateNode : public Support::BlockClient<StateNode> {
00583     public:
00584       PosSet*    pos;
00585       int        state;
00586       StateNode* next;
00587       StateNode* left;
00588       StateNode* right;
00589     };
00590 
00594     class StatePool {
00595     public:
00596       int   n_states;
00597       StateNode  root;
00598       StateNode* next;
00599       StateNode* all;
00600 
00601       StatePool(PosSet*);
00602 
00603       StateNode* pop(void);
00604       bool empty(void) const;
00605 
00606       int state(StatePoolAllocator&, PosSet*);
00607     };
00608 
00609     forceinline
00610     StatePool::StatePool(PosSet* ps) {
00611       next     = &root;
00612       all      = NULL;
00613       n_states = 1;
00614       root.pos   = ps;
00615       root.state = 0;
00616       root.next  = NULL;
00617       root.left  = NULL;
00618       root.right = NULL;
00619     }
00620 
00621     forceinline StateNode*
00622     StatePool::pop(void) {
00623       StateNode* n = next;
00624       next = n->next;
00625       n->next = all;
00626       all = n;
00627       return n;
00628     }
00629 
00630     forceinline bool
00631     StatePool::empty(void) const {
00632       return next == NULL;
00633     }
00634 
00635     forceinline int
00636     StatePool::state(StatePoolAllocator& spm, PosSet* ps) {
00637       int d = 0;
00638       StateNode** p = NULL;
00639       StateNode*  n = &root;
00640       do {
00641         switch (PosSet::cmp(ps,n->pos)) {
00642         case PSC_EQ: return n->state;
00643         case PSC_LE: p = &n->left;  n = *p; break;
00644         case PSC_GR: p = &n->right; n = *p; break;
00645         default: GECODE_NEVER;
00646         }
00647         d++;
00648       } while (n != NULL);
00649       n = new (spm) StateNode; *p = n;
00650       n->pos   = ps;
00651       n->state = n_states++;
00652       n->next  = next;
00653       n->left  = NULL;
00654       n->right = NULL;
00655       next = n;
00656       return n->state;
00657     }
00658 
00662     class SymbolsInc {
00663     public:
00664       forceinline bool
00665       operator ()(int x, int y) {
00666         return x < y;
00667       }
00668       forceinline static void
00669       sort(int s[], int n) {
00670         SymbolsInc o;
00671         Support::quicksort<int,SymbolsInc>(s,n,o);
00672       }
00673     };
00674 
00675 
00680     class TransitionBag {
00681     private:
00682       Support::DynamicArray<DFA::Transition,Heap> t;
00683       int n;
00684     public:
00685       TransitionBag(void);
00686       void add(int,int,int);
00687       void finish(void);
00688       DFA::Transition* transitions(void);
00689     };
00690 
00691     forceinline
00692     TransitionBag::TransitionBag(void) : t(heap), n(0) {}
00693 
00694     forceinline void
00695     TransitionBag::add(int i_state, int symbol, int o_state) {
00696       t[n].i_state = i_state;
00697       t[n].symbol  = symbol;
00698       t[n].o_state = o_state;
00699       n++;
00700     }
00701 
00702     forceinline void
00703     TransitionBag::finish(void) {
00704       t[n].i_state = -1;
00705     }
00706 
00707     forceinline DFA::Transition*
00708     TransitionBag::transitions(void) {
00709       return &t[0];
00710     }
00711 
00712 
00717     class FinalBag {
00718     private:
00719       Support::DynamicArray<int,Heap> f;
00720       int n;
00721     public:
00722       FinalBag(void);
00723       void add(int);
00724       void finish(void);
00725       int* finals(void);
00726     };
00727 
00728     forceinline
00729     FinalBag::FinalBag(void) : f(heap), n(0) {}
00730 
00731     forceinline void
00732     FinalBag::add(int state) {
00733       f[n++] = state;
00734     }
00735 
00736     forceinline void
00737     FinalBag::finish(void) {
00738       f[n] = -1;
00739     }
00740 
00741     forceinline int*
00742     FinalBag::finals(void) {
00743       return &f[0];
00744     }
00745 
00746   }
00747 
00748   REG::operator DFA(void) {
00749     using MiniModel::PosSetAllocator;
00750     using MiniModel::StatePoolAllocator;
00751     using MiniModel::PosInfo;
00752     using MiniModel::PosSet;
00753     using MiniModel::NodeInfo;
00754 
00755     using MiniModel::StatePool;
00756     using MiniModel::StateNode;
00757 
00758     using MiniModel::TransitionBag;
00759     using MiniModel::FinalBag;
00760 
00761     using MiniModel::SymbolsInc;
00762 
00763     PosSetAllocator    psm;
00764     StatePoolAllocator spm;
00765     REG r = *this + REG(Int::Limits::max+1);
00766     int n_pos = r.e->n_pos();
00767 
00768     PosInfo* pi = heap.alloc<PosInfo>(n_pos);
00769     for (int i=n_pos; i--; )
00770       pi[i].followpos = NULL;
00771 
00772     PosSet* firstpos = r.e->followpos(psm,&pi[0]);
00773 
00774     // Compute symbols
00775     int* symbols = heap.alloc<int>(n_pos);
00776     for (int i=n_pos; i--; )
00777       symbols[i] = pi[i].symbol;
00778 
00779     SymbolsInc::sort(&symbols[0],n_pos-1);
00780     int n_symbols = 1;
00781     for (int i = 1; i<n_pos-1; i++)
00782       if (symbols[i-1] != symbols[i])
00783         symbols[n_symbols++] = symbols[i];
00784 
00785     // Compute states and transitions
00786     TransitionBag tb;
00787     StatePool sp(firstpos);
00788     while (!sp.empty()) {
00789       StateNode* sn = sp.pop();
00790       for (int i = n_symbols; i--; ) {
00791         PosSet* u = NULL;
00792         for (PosSet* ps = sn->pos; ps != NULL; ps = ps->next)
00793           if (pi[ps->pos].symbol == symbols[i])
00794             u = PosSet::cup(psm,u,pi[ps->pos].followpos);
00795         if (u != NULL)
00796           tb.add(sn->state,symbols[i],sp.state(spm,u));
00797       }
00798     }
00799     tb.finish();
00800 
00801     // Compute final states
00802     FinalBag fb;
00803     for (StateNode* n = sp.all; n != NULL; n = n->next)
00804       if (n->pos->in(n_pos-1))
00805         fb.add(n->state);
00806     fb.finish();
00807 
00808     heap.free<PosInfo>(pi,n_pos);
00809     heap.free<int>(symbols,n_pos);
00810     return DFA(0,tb.transitions(),fb.finals(),true);
00811   }
00812 
00813 }
00814 
00815 // STATISTICS: minimodel-any
00816