Version abc70727

1 files changed, 89 insertions, 45 deletions

diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 0e583d6c..e109df56 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -53,6 +53,37 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
     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->nTimeFrames      =       0;  // the number of timeframes to unroll
+    pPars->fConeBias        =       1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the default solving parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ParamsDefaultSeq( 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     = 1000000;  // conflict limit at a node
+    pPars->nBTLimitMiter    =  500000;  // conflict limit at an output
+    pPars->nTimeFrames      =       1;  // the number of timeframes to unroll
+    pPars->fConeBias        =       0;
 }
 
 /**Function*************************************************************
@@ -74,47 +105,36 @@ 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->pManFraig  = Aig_ManStartFrom( pManAig );
-    assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManFraig) );
+    p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1;
+    p->nFrames    = pPars->nTimeFrames + 1;
     // allocate simulation info
-    p->nSimWords  = pPars->nSimWords;
-    p->pSimWords  = ALLOC( unsigned, (Aig_ManObjIdMax(pManAig) + 1) * p->nSimWords );
+    p->nSimWords  = pPars->nSimWords * p->nFrames;
+    p->pSimWords  = ALLOC( unsigned, p->nSizeAlloc * p->nSimWords * p->nFrames );
     // clean simulation info of the constant node
-    memset( p->pSimWords, 0, sizeof(unsigned) * ((Aig_ManPiNum(pManAig) + 1) * p->nSimWords) );
+    memset( p->pSimWords, 0, sizeof(unsigned) * p->nSizeAlloc * p->nSimWords * p->nFrames );
     // allocate storage for sim pattern
     p->nPatWords  = Aig_BitWordNum( Aig_ManPiNum(pManAig) );
     p->pPatWords  = ALLOC( unsigned, p->nPatWords ); 
     p->pPatScores = ALLOC( int, 32 * p->nSimWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
-    p->vClasses   = Vec_PtrAlloc( 100 );
-    p->vClasses1  = Vec_PtrAlloc( 100 );
-    p->vClassOld  = Vec_PtrAlloc( 100 );
-    p->vClassNew  = Vec_PtrAlloc( 100 );
-    p->vClassesTemp = Vec_PtrAlloc( 100 );
+    p->vTimeouts  = Vec_PtrAlloc( 100 );
+    // equivalence classes
+    p->pCla       = Fra_ClassesStart( pManAig );
     // allocate other members
-    p->nSizeAlloc = Aig_ManObjIdMax(pManAig) + 1;
-    p->pMemFraig  = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
-    memset( p->pMemFraig, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
-    p->pMemRepr  = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
-    memset( p->pMemRepr, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
-    p->pMemReprFra  = ALLOC( Aig_Obj_t *, p->nSizeAlloc );
-    memset( p->pMemReprFra, 0, p->nSizeAlloc * sizeof(Aig_Obj_t *) );
-    p->pMemFanins  = ALLOC( Vec_Ptr_t *, p->nSizeAlloc );
-    memset( p->pMemFanins, 0, p->nSizeAlloc * sizeof(Vec_Ptr_t *) );
-    p->pMemSatNums  = ALLOC( int, p->nSizeAlloc );
-    memset( p->pMemSatNums, 0, p->nSizeAlloc * sizeof(int) );
+    p->pMemFraig  = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFrames );
+    memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFrames );
+    p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFrames );
+    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFrames );
+    p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFrames );
+    memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFrames );
     // set random number generator
     srand( 0xABCABC );
-    // make sure the satisfying assignment is node assigned
-    assert( p->pManFraig->pData == NULL );
-    // connect AIG managers to the FRAIG manager
-    Fra_ManPrepare( p );
     return p;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Prepares managers by transfering pointers to the objects.]
+  Synopsis    [Prepares the new manager to begin fraiging.]
 
   Description []
                
@@ -123,24 +143,54 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_ManPrepare( Fra_Man_t * p )
+Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
 {
+    Aig_Man_t * pManFraig;
     Aig_Obj_t * pObj;
     int i;
-    // set the pointers to the manager
-    Aig_ManForEachObj( p->pManFraig, pObj, i )
-        pObj->pData = p;
+    assert( p->pManFraig == NULL );
     // set the pointer to the manager
     Aig_ManForEachObj( p->pManAig, pObj, i )
         pObj->pData = p;
+    // start the fraig package
+    pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 );
     // set the pointers to the available fraig nodes
-    Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), Aig_ManConst1(p->pManFraig) );
+    Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) );
     Aig_ManForEachPi( p->pManAig, pObj, i )
-        Fra_ObjSetFraig( pObj, Aig_ManPi(p->pManFraig, i) );
+        Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
+    // set the pointers to the manager
+    Aig_ManForEachObj( pManFraig, pObj, i )
+        pObj->pData = p;
+    // make sure the satisfying assignment is node assigned
+    assert( pManFraig->pData == NULL );
+    return pManFraig;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Finalizes the combinational miter after fraiging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ManFinalizeComb( Fra_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    // add the POs
+    Aig_ManForEachPo( p->pManAig, pObj, i )
+        Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) );
+    // postprocess
+    Aig_ManCleanMarkB( p->pManFraig );
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Stops the fraiging manager.]
 
   Description []
@@ -158,19 +208,13 @@ void Fra_ManStop( Fra_Man_t * p )
             Vec_PtrFree( p->pMemFanins[i] );
     if ( p->pPars->fVerbose )
         Fra_ManPrint( p );
-    if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
-    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
-    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
-    if ( p->vClasses1 )    Vec_PtrFree( p->vClasses1 );
-    if ( p->vClasses )     Vec_PtrFree( p->vClasses );
-    if ( p->vPiVars )      Vec_PtrFree( p->vPiVars );
-    if ( p->pSat )         sat_solver_delete( p->pSat );
-    FREE( p->pMemSatNums );
-    FREE( p->pMemFanins );
-    FREE( p->pMemRepr );
-    FREE( p->pMemReprFra );
+    if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts );
+    if ( p->vPiVars )   Vec_PtrFree( p->vPiVars );
+    if ( p->pSat )      sat_solver_delete( p->pSat );
+    if ( p->pCla  )     Fra_ClassesStop( p->pCla );
     FREE( p->pMemFraig );
-    FREE( p->pMemClasses );
+    FREE( p->pMemFanins );
+    FREE( p->pMemSatNums );
     FREE( p->pPatScores );
     FREE( p->pPatWords );
     FREE( p->pSimWords );
@@ -197,7 +241,7 @@ void Fra_ManPrint( Fra_Man_t * p )
     printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
         p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
     printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", 
-        Aig_ManNodeNum(p->pManFraig), p->nNodesMiter, Aig_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
+        p->pManFraig? Aig_ManNodeNum(p->pManFraig) : -1, p->nNodesMiter, Aig_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
     if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
     PRT( "AIG simulation  ", p->timeSim  );
     PRT( "AIG traversal   ", p->timeTrav  );