Version abc70906

12 files changed, 143 insertions, 116 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 931e0930..cd6bdfd4 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -39,6 +39,7 @@ extern "C" {
 #include "aig.h"
 #include "dar.h"
 #include "satSolver.h"
+#include "bar.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -126,6 +127,7 @@ struct Fra_Man_t_
     // mapping AIG into FRAIG
     int              nFramesAll;        // the number of timeframes used
     Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
+    int              nSizeAlloc;        // allocated size of the arrays for timeframe nodes
     // equivalence classes 
     Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
     // simulation info
@@ -144,7 +146,7 @@ struct Fra_Man_t_
     sint64           nInsLimitGlobal;   // resource limit
     Vec_Ptr_t **     pMemFanins;        // the arrays of fanins for some FRAIG nodes
     int *            pMemSatNums;       // the array of SAT numbers for some FRAIG nodes
-    int              nSizeAlloc;        // allocated size of the arrays
+    int              nMemAlloc;         // allocated size of the arrays for FRAIG varnums and fanins
     Vec_Ptr_t *      vTimeouts;         // the nodes, for which equivalence checking timed out
     // statistics
     int              nSimRounds;
@@ -240,7 +242,7 @@ extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pO
 extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
 extern int                 Fra_FraigMiterStatus( Aig_Man_t * p );
 extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
-extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig );
+extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
 extern Aig_Man_t *         Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax );
 /*=== fraImp.c ========================================================*/
 extern Vec_Int_t *         Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
@@ -259,7 +261,7 @@ extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int n
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
 extern Fra_Man_t *         Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
-extern void                Fra_ManClean( Fra_Man_t * p );
+extern void                Fra_ManClean( Fra_Man_t * p, int nNodesMax );
 extern Aig_Man_t *         Fra_ManPrepareComb( Fra_Man_t * p );
 extern void                Fra_ManFinalizeComb( Fra_Man_t * p );
 extern void                Fra_ManStop( Fra_Man_t * p );
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index 648d08c4..1df25c0a 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -187,8 +187,8 @@ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
     p->nPref = nPref;
     p->nDepth = nDepth;
     p->nFramesAll = nPref + nDepth;
-    p->pObjToFrames  = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
-    memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
+    p->pObjToFrames  = ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) );
+    memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * Aig_ManObjNumMax(pAig) );
     return p;
 }
 
@@ -231,7 +231,8 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
     int i, k, f;
 
     // start the fraig package
-    pAigFrames = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * p->nFramesAll );
+    pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll );
+    pAigFrames->pName = Aig_UtilStrsav( p->pAig->pName );
     // create PI nodes for the frames
     for ( f = 0; f < p->nFramesAll; f++ )
         Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 3e3392c7..a03fa6e5 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -60,8 +60,8 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
     p = ALLOC( Fra_Cla_t, 1 );
     memset( p, 0, sizeof(Fra_Cla_t) );
     p->pAig = pAig;
-    p->pMemRepr  = ALLOC( Aig_Obj_t *, (Aig_ManObjIdMax(pAig) + 1) );
-    memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(pAig) + 1) );
+    p->pMemRepr  = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
+    memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
     p->vClasses     = Vec_PtrAlloc( 100 );
     p->vClasses1    = Vec_PtrAlloc( 100 );
     p->vClassesTemp = Vec_PtrAlloc( 100 );
@@ -112,8 +112,8 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
 {
     Aig_Obj_t * pObj;
     int i;
-    Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 );
-    memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) );
+    Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) );
+    memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) );
     if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
     {
         Aig_ManForEachObj( p->pAig, pObj, i )
@@ -277,7 +277,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
     int i, k, nTableSize, nEntries, nNodes, iEntry;
 
     // allocate the hash table hashing simulation info into nodes
-    nTableSize = Aig_PrimeCudd( Aig_ManObjIdMax(p->pAig) + 1 );
+    nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
     ppTable = ALLOC( Aig_Obj_t *, nTableSize ); 
     ppNexts = ALLOC( Aig_Obj_t *, nTableSize ); 
     memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
@@ -643,8 +643,8 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
     // perform combinational simulation
     pComb = Fra_SmlSimulateComb( p->pAig, 32 );
     // compute the weight of each node in the classes
-    pWeights = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );
-    memset( pWeights, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) );
+    pWeights = ALLOC( int, Aig_ManObjNumMax(p->pAig) );
+    memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
     Aig_ManForEachObj( p->pAig, pObj, i )
     { 
         pRepr = Fra_ClassObjRepr( pObj );
@@ -798,9 +798,10 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
     assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
     assert( nFramesK > 0 );
     // start the fraig package
-    pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * nFramesAll );
+    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
+    pManFraig->pName = Aig_UtilStrsav( p->pAig->pName );
     // allocate place for the node mapping
-    ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p->pAig) + 1 );
+    ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
     Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
     // create latches for the first frame
     Aig_ManForEachLoSeq( p->pAig, pObj, i )
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 94beb61a..b390edbe 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -267,7 +267,7 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
 ***********************************************************************/
 void Fra_FraigSweep( Fra_Man_t * p )
 {
-    ProgressBar * pProgress;
+    Bar_Progress_t * pProgress;
     Aig_Obj_t * pObj, * pObjNew;
     int i, k = 0, Pos = 0;
     // fraig latch outputs
@@ -280,10 +280,10 @@ void Fra_FraigSweep( Fra_Man_t * p )
     if ( p->pPars->fLatchCorr )
         return;
     // fraig internal nodes
-    pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
+    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
     Aig_ManForEachNode( p->pManAig, pObj, i )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Bar_ProgressUpdate( pProgress, i, NULL );
         // derive and remember the new fraig node
         pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) );
         Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew );
@@ -296,7 +296,7 @@ void Fra_FraigSweep( Fra_Man_t * p )
         if ( p->pPars->fUseImps )
             Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
     }
-    Extra_ProgressBarStop( pProgress );
+    Bar_ProgressStop( pProgress );
     // try to prove the outputs of the miter
     p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
 //    Fra_MiterStatus( p->pManFraig );
@@ -331,8 +331,8 @@ clk = clock();
     p->pManFraig = Fra_ManPrepareComb( p );
     p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
     Fra_SmlSimulate( p, 0 );
-    if ( p->pPars->fChoicing )
-        Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
+//    if ( p->pPars->fChoicing )
+//        Aig_ManReprStart( p->pManFraig, Aig_ManObjNumMax(p->pManAig) );
     // collect initial states
     p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
     p->nNodesBeg = Aig_ManNodeNum(pManAig);
@@ -346,10 +346,12 @@ clk = clock();
     Fra_ManFinalizeComb( p );
     if ( p->pPars->fChoicing )
     {
-        int clk2 = clock();
+int clk2 = clock();
         Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
-        pManAigNew = Aig_ManDupRepr( p->pManAig );
-        Aig_ManCreateChoices( pManAigNew );
+        pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
+        Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) );
+        Aig_ManTransferRepr( pManAigNew, p->pManAig );
+        Aig_ManMarkValidChoices( pManAigNew );
         Aig_ManStop( p->pManFraig );
         p->pManFraig = NULL;
 p->timeTrav += clock() - clk2;
@@ -359,14 +361,6 @@ p->timeTrav += clock() - clk2;
         Aig_ManCleanup( p->pManFraig );
         pManAigNew = p->pManFraig;
         p->pManFraig = NULL;
-/*
-        Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
-        pManAigNew = Aig_ManDupRepr( p->pManAig );
-//        Aig_ManCreateChoices( pManAigNew );
-        Aig_ManCleanup( pManAigNew );
-        Aig_ManStop( p->pManFraig );
-        p->pManFraig = NULL;
-*/
     }
 p->timeTotal = clock() - clk;
     // collect final stats
@@ -388,16 +382,16 @@ p->timeTotal = clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig )
+Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
 {
     Fra_Par_t Pars, * pPars = &Pars; 
     Fra_ParamsDefault( pPars );
-    pPars->nBTLimitNode = 1000;
-    pPars->fVerbose     = 0;
-    pPars->fProve       = 0;
+    pPars->nBTLimitNode = nConfMax;
+    pPars->fChoicing    = 1;
     pPars->fDoSparse    = 1;
     pPars->fSpeculate   = 0;
-    pPars->fChoicing    = 1;
+    pPars->fProve       = 0;
+    pPars->fVerbose     = 0;
     return Fra_FraigPerform( pManAig, pPars );
 }
  
@@ -418,11 +412,11 @@ Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
     Fra_Par_t Pars, * pPars = &Pars; 
     Fra_ParamsDefault( pPars );
     pPars->nBTLimitNode = nConfMax;
-    pPars->fVerbose     = 0;
-    pPars->fProve       = 0;
+    pPars->fChoicing    = 0;
     pPars->fDoSparse    = 1;
     pPars->fSpeculate   = 0;
-    pPars->fChoicing    = 0;
+    pPars->fProve       = 0;
+    pPars->fVerbose     = 0;
     pFraig = Fra_FraigPerform( pManAig, pPars );
     return pFraig;
 } 
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index 5e4b8c28..d8bf4e48 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -64,8 +64,8 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
 {
     Aig_Obj_t * pObj;
     int i, * pnBits; 
-    pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );  
-    memset( pnBits, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) );
+    pnBits = ALLOC( int, Aig_ManObjNumMax(p->pAig) );  
+    memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
     Aig_ManForEachObj( p->pAig, pObj, i )
         pnBits[i] = Fra_SmlCountOnesOne( p, i );
     return pnBits;
@@ -325,7 +325,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
     int CostMin = AIG_INFINITY, CostMax = 0;
     int i, k, Imp, CostRange, clk = clock();
-    assert( Aig_ManObjIdMax(p->pManAig) + 1 < (1 << 15) );
+    assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 53dbdbb6..14fba9ba 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -133,7 +133,8 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
     assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
 
     // start the fraig package
-    pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFramesAll );
+    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
+    pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
     pManFraig->nRegs = p->pManAig->nRegs;
     // create PI nodes for the frames
     for ( f = 0; f < p->nFramesAll; f++ )
@@ -194,7 +195,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
     Aig_ManForEachObj( p, pObj, i )
         pObj->pData = pObj;
     // iterate and add objects
-    nNodesOld = Aig_ManObjIdMax(p);
+    nNodesOld = Aig_ManObjNumMax(p);
     pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
     for ( f = 0; f < nFrames; f++ )
     {
@@ -372,11 +373,14 @@ PRT( "Time", clock() - clk );
             if ( p->pSat == NULL )
                 printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
         }
-
+ 
         // set the pointers to the manager
         Aig_ManForEachObj( p->pManFraig, pObj, i )
             pObj->pData = p;
 
+        // prepare solver for fraiging the last timeframe
+        Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) );
+
         // transfer PI/LO variable numbers
         Aig_ManForEachObj( p->pManFraig, pObj, i )
         {
@@ -402,12 +406,14 @@ PRT( "Time", clock() - clk );
         p->nSatCallsRecent = 0;
         p->nSatCallsSkipped = 0;
         Fra_FraigSweep( p );
+        // remove FRAIG and SAT solver
+        Aig_ManStop( p->pManFraig );   p->pManFraig = NULL;
+        sat_solver_delete( p->pSat );  p->pSat = NULL; 
+        memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
 //        printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
         assert( p->vTimeouts == NULL );
         if ( p->vTimeouts )
            printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
-        // cleanup
-        Fra_ManClean( p );
         // check if refinement has happened
 //        p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
         if ( p->pCla->fRefinement && 
@@ -435,7 +441,7 @@ clk2 = clock();
 //    Fra_ClassesPrint( p->pCla, 1 );
     Fra_ClassesSelectRepr( p->pCla );
     Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
-    pManAigNew = Aig_ManDupRepr( pManAig );
+    pManAigNew = Aig_ManDupRepr( pManAig, 0 );
     // add implications to the manager
     if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
         Fra_ImpRecordInManager( p, pManAigNew );
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index c3b5504e..e73d610f 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -509,7 +509,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
     Fra_Man_t * pTemp;
     Aig_Man_t * pAigPart, * pAigNew = NULL;
     Vec_Int_t * vPart;
-    Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
+//    Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
     int i, nIter, clk = clock(), clk2, clk3;
     if ( Aig_ManNodeNum(pAig) == 0 )
     {
@@ -622,7 +622,7 @@ clk2 = clock();
     if ( fReprSelect )
         Fra_ClassesSelectRepr( p->pCla );
     Fra_ClassesCopyReprs( p->pCla, NULL );
-    pAigNew = Aig_ManDupRepr( p->pAig );
+    pAigNew = Aig_ManDupRepr( p->pAig, 0 );
     Aig_ManSeqCleanup( pAigNew );
 //    Aig_ManCountMergeRegs( pAigNew );
 p->timeUpdate += clock() - clk2;
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 97282e98..f505b0c2 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -42,20 +42,20 @@
 void Fra_ParamsDefault( Fra_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Fra_Par_t) );
-    pPars->nSimWords        =      32;  // the number of words in the simulation info
-    pPars->dSimSatur        =   0.005;  // the ratio of refined classes when saturation is reached
-    pPars->fPatScores       =       0;  // enables simulation pattern scoring
-    pPars->MaxScore         =      25;  // max score after which resimulation is used
-    pPars->fDoSparse        =       1;  // skips sparse functions
-//    pPars->dActConeRatio    =    0.05;  // the ratio of cone to be bumped
-//    pPars->dActConeBumpMax  =     5.0;  // the largest bump of activity
-    pPars->dActConeRatio    =     0.3;  // the ratio of cone to be bumped
-    pPars->dActConeBumpMax  =    10.0;  // the largest bump of activity
-    pPars->nBTLimitNode     =     100;  // conflict limit at a node
-    pPars->nBTLimitMiter    =  500000;  // conflict limit at an output
-    pPars->nFramesK         =       0;  // the number of timeframes to unroll
-    pPars->fConeBias        =       1;
-    pPars->fRewrite         =       0;
+    pPars->nSimWords        =       32;  // the number of words in the simulation info
+    pPars->dSimSatur        =    0.005;  // the ratio of refined classes when saturation is reached
+    pPars->fPatScores       =        0;  // enables simulation pattern scoring
+    pPars->MaxScore         =       25;  // max score after which resimulation is used
+    pPars->fDoSparse        =        1;  // skips sparse functions
+//    pPars->dActConeRatio    =     0.05;  // the ratio of cone to be bumped
+//    pPars->dActConeBumpMax  =      5.0;  // the largest bump of activity
+    pPars->dActConeRatio    =      0.3;  // the ratio of cone to be bumped
+    pPars->dActConeBumpMax  =     10.0;  // the largest bump of activity
+    pPars->nBTLimitNode     =      100;  // conflict limit at a node
+    pPars->nBTLimitMiter    =   500000;  // conflict limit at an output
+    pPars->nFramesK         =        0;  // the number of timeframes to unroll
+    pPars->fConeBias        =        1;
+    pPars->fRewrite         =        0;
 }
 
 /**Function*************************************************************
@@ -72,20 +72,20 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
 void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Fra_Par_t) );
-    pPars->nSimWords        =       1;  // the number of words in the simulation info
-    pPars->dSimSatur        =   0.005;  // the ratio of refined classes when saturation is reached
-    pPars->fPatScores       =       0;  // enables simulation pattern scoring
-    pPars->MaxScore         =      25;  // max score after which resimulation is used
-    pPars->fDoSparse        =       1;  // skips sparse functions
-    pPars->dActConeRatio    =     0.3;  // the ratio of cone to be bumped
-    pPars->dActConeBumpMax  =    10.0;  // the largest bump of activity
-    pPars->nBTLimitNode     =10000000;  // conflict limit at a node
-    pPars->nBTLimitMiter    =  500000;  // conflict limit at an output
-    pPars->nFramesK         =       1;  // the number of timeframes to unroll
-    pPars->fConeBias        =       0;
-    pPars->fRewrite         =       0;
-    pPars->fLatchCorr       =       0;
-}
+    pPars->nSimWords        =        1;  // the number of words in the simulation info
+    pPars->dSimSatur        =    0.005;  // the ratio of refined classes when saturation is reached
+    pPars->fPatScores       =        0;  // enables simulation pattern scoring
+    pPars->MaxScore         =       25;  // max score after which resimulation is used
+    pPars->fDoSparse        =        1;  // skips sparse functions
+    pPars->dActConeRatio    =      0.3;  // the ratio of cone to be bumped
+    pPars->dActConeBumpMax  =     10.0;  // the largest bump of activity
+    pPars->nBTLimitNode     = 10000000;  // conflict limit at a node
+    pPars->nBTLimitMiter    =   500000;  // conflict limit at an output
+    pPars->nFramesK         =        1;  // the number of timeframes to unroll
+    pPars->fConeBias        =        0;
+    pPars->fRewrite         =        0;
+    pPars->fLatchCorr       =        0;
+} 
 
 /**Function*************************************************************
 
@@ -108,7 +108,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     memset( p, 0, sizeof(Fra_Man_t) );
     p->pPars      = pPars;
     p->pManAig    = pManAig;
-    p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1;
+    p->nSizeAlloc = Aig_ManObjNumMax( pManAig );
     p->nFramesAll = pPars->nFramesK + 1;
     // allocate storage for sim pattern
     p->nPatWords  = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
@@ -119,10 +119,6 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     // allocate other members
     p->pMemFraig  = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
     memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
-    p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFramesAll + 10000 );
-    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFramesAll + 10000 );
-    p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFramesAll + 10000 );
-    memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFramesAll + 10000 );
     // set random number generator
     srand( 0xABCABC );
     // set the pointer to the manager
@@ -142,24 +138,24 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_ManClean( Fra_Man_t * p )
+void Fra_ManClean( Fra_Man_t * p, int nNodesMax )
 {
-    int i, Limit;
-
-    Limit = Aig_ManObjIdMax(p->pManFraig) + 1;
-    for ( i = 0; i < Limit; i++ )
+    int i;
+    // remove old arrays
+    for ( i = 0; i < p->nMemAlloc; i++ )
         if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
             Vec_PtrFree( p->pMemFanins[i] );
-
-    memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
-    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * Limit );
-    memset( p->pMemSatNums, 0, sizeof(int) * Limit );
-
-    Aig_ManStop( p->pManFraig );   
-    p->pManFraig = NULL;
-
-    sat_solver_delete( p->pSat );  
-    p->pSat = NULL; 
+    // realloc for the new size
+    if ( p->nMemAlloc < nNodesMax )
+    {
+        int nMemAllocNew = nNodesMax + 5000;
+        p->pMemFanins = REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew );
+        p->pMemSatNums = REALLOC( int, p->pMemSatNums, nMemAllocNew );
+        p->nMemAlloc = nMemAllocNew;
+    }
+    // prepare for the new run
+    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
+    memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
 }
 
 /**Function*************************************************************
@@ -180,7 +176,8 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
     int i;
     assert( p->pManFraig == NULL );
     // start the fraig package
-    pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 );
+    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) );
+    pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
     pManFraig->nRegs    = p->pManAig->nRegs;
     pManFraig->nAsserts = p->pManAig->nAsserts;
     // set the pointers to the available fraig nodes
@@ -190,6 +187,12 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
     // set the pointers to the manager
     Aig_ManForEachObj( pManFraig, pObj, i )
         pObj->pData = p;
+    // allocate memory for mapping FRAIG nodes into SAT numbers and fanins
+    p->nMemAlloc = p->nSizeAlloc;
+    p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nMemAlloc );
+    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
+    p->pMemSatNums = ALLOC( int, p->nMemAlloc );
+    memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
     // make sure the satisfying assignment is node assigned
     assert( pManFraig->pData == NULL );
     return pManFraig;
@@ -231,7 +234,6 @@ void Fra_ManFinalizeComb( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_ManStop( Fra_Man_t * p )
 {
-    int i;
     if ( p->pPars->fVerbose )
         Fra_ManPrint( p );
     // save mapping from original nodes into FRAIG nodes
@@ -242,9 +244,7 @@ void Fra_ManStop( Fra_Man_t * p )
         p->pManAig->pObjCopies = p->pMemFraig;
         p->pMemFraig = NULL;
     }
-    for ( i = 0; i < p->nSizeAlloc; i++ )
-        if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
-            Vec_PtrFree( p->pMemFanins[i] );
+    Fra_ManClean( p, 0 );
     if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts );
     if ( p->vPiVars )   Vec_PtrFree( p->vPiVars );
     if ( p->pSat )      sat_solver_delete( p->pSat );
@@ -271,14 +271,14 @@ void Fra_ManStop( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_ManPrint( Fra_Man_t * p )
 {
-    double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
+    double nMemory = 1.0*Aig_ManObjNumMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
     printf( "SimWord = %d. Round = %d.  Mem = %0.2f Mb.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
         p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) );
     printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n", 
         p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) );
     printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
-        p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, 
-        p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
+        p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), 
+        p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
     if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
     PRT( "AIG simulation  ", p->pSml->timeSim  );
     PRT( "AIG traversal   ", p->timeTrav );
diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c
index 23b6dd1d..691b2b3d 100644
--- a/src/aig/fra/fraPart.c
+++ b/src/aig/fra/fraPart.c
@@ -41,7 +41,7 @@
 ***********************************************************************/
 void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
 {
-    ProgressBar * pProgress;
+    Bar_Progress_t * pProgress;
     Vec_Vec_t * vSupps, * vSuppsIn;
     Vec_Ptr_t * vSuppsNew;
     Vec_Int_t * vSupNew, * vSup, * vSup2, * vTemp;//, * vSupIn;
@@ -86,10 +86,10 @@ clk = clock();
     vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) );
     vOverNew  = Vec_IntAlloc( Aig_ManPoNum(p) );
     vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) );
-    pProgress = Extra_ProgressBarStart( stdout, Aig_ManPoNum(p) );
+    pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) );
     Aig_ManForEachPo( p, pObj, i )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Bar_ProgressUpdate( pProgress, i, NULL );
         // get old supports
         vSup = Vec_VecEntry( vSupps, i );
         if ( Vec_IntSize(vSup) < 2 )
@@ -152,7 +152,7 @@ clk = clock();
         printf( "\n" );
 */
     }
-    Extra_ProgressBarStop( pProgress );
+    Bar_ProgressStop( pProgress );
 PRT( "Scanning", clock() - clk );
 
     // print cumulative statistics
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index bc8ef08a..e1cc4c32 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -18,6 +18,7 @@
 
 ***********************************************************************/
 
+#include <math.h>
 #include "fra.h"
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 88c552dc..0146ac5a 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "fra.h"
+#include "ioa.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -100,7 +101,7 @@ PRT( "Time", clock() - clkTotal );
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose, int fVeryVerbose )
+int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
 {
     Aig_Man_t * pNew, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
@@ -116,7 +117,9 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose,
 
     // perform sequential cleanup
 clk = clock();
+    if ( pNew->nRegs )
     pNew = Aig_ManReduceLaches( pNew, 0 );
+    if ( pNew->nRegs )
     pNew = Aig_ManConstReduce( pNew, 0 );
     if ( fVerbose )
     {
@@ -126,7 +129,7 @@ PRT( "Time", clock() - clk );
     }
 
     // perform forward retiming
-    if ( fRetimeFirst )
+    if ( fRetimeFirst && pNew->nRegs )
     {
 clk = clock();
     pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
@@ -141,6 +144,8 @@ PRT( "Time", clock() - clk );
     
     // run latch correspondence
 clk = clock();
+    if ( pNew->nRegs )
+    {
     pNew = Aig_ManDup( pTemp = pNew, 1 );
     Aig_ManStop( pTemp );
     pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter );
@@ -151,6 +156,7 @@ clk = clock();
             nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
     }
+    }
 
     // perform fraiging
 clk = clock();
@@ -166,7 +172,7 @@ PRT( "Time", clock() - clk );
     // perform seq sweeping while increasing the number of frames
     RetValue = Fra_FraigMiterStatus( pNew );
     if ( RetValue == -1 )
-    for ( nFrames = 1; ; nFrames *= 2 )
+    for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
     {
 clk = clock();
         pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
@@ -203,19 +209,35 @@ clk = clock();
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
         }
+        if ( pNew->nRegs )
+        pNew = Aig_ManConstReduce( pNew, 0 );
     }
+
     // get the miter status
     RetValue = Fra_FraigMiterStatus( pNew );
-    Aig_ManStop( pNew );
 
     // report the miter
     if ( RetValue == 1 )
+    {
         printf( "Networks are equivalent.   " );
+PRT( "Time", clock() - clkTotal );
+    }
     else if ( RetValue == 0 )
+    {
         printf( "Networks are NOT EQUIVALENT.   " );
+PRT( "Time", clock() - clkTotal );
+    }
     else
+    {
+        static int Counter = 1;
+        char pFileName[1000];
         printf( "Networks are UNDECIDED.   " );
 PRT( "Time", clock() - clkTotal );
+        sprintf( pFileName, "sm%03d.aig", Counter++ );
+        Ioa_WriteAiger( pNew, pFileName, 0 );
+        printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
+    }
+    Aig_ManStop( pNew );
     return RetValue;
 }
 
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 0b93fb73..d6f6d74a 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -703,7 +703,7 @@ printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(
 Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
 {
     Fra_Sml_t * p;
-    p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * (nPref + nFrames) * nWordsFrame );
+    p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
     memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
     p->pAig        = pAig;
     p->nPref       = nPref;