summaryrefslogtreecommitdiffstats
path: root/src/aig/fra/fraMan.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/fra/fraMan.c')
-rw-r--r--src/aig/fra/fraMan.c134
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 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 08:17:01 +0000