Version abc70906

1 files changed, 56 insertions, 56 deletions

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 );