diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-26 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-26 08:01:00 -0700 |
commit | 054e2cd3a8ab4ada55db4def2d6ce7d309341e07 (patch) | |
tree | a951eeeafa90dc555cb6442151761190e0b5af6a /src/aig/fra/fra.h | |
parent | 64dc240b904adafee78e2a66a1fc31b717f8985f (diff) | |
download | abc-054e2cd3a8ab4ada55db4def2d6ce7d309341e07.tar.gz abc-054e2cd3a8ab4ada55db4def2d6ce7d309341e07.tar.bz2 abc-054e2cd3a8ab4ada55db4def2d6ce7d309341e07.zip |
Version abc70726
Diffstat (limited to 'src/aig/fra/fra.h')
-rw-r--r-- | src/aig/fra/fra.h | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 7f2df105..127882ea 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -60,6 +60,7 @@ struct Fra_Par_t_ int MaxScore; // max score after which resimulation is used double dActConeRatio; // the ratio of cone to be bumped double dActConeBumpMax; // the largest bump in activity + int fChoicing; // enables choicing int fSpeculate; // use speculative reduction int fProve; // prove the miter outputs int fVerbose; // verbose output @@ -101,6 +102,7 @@ struct Fra_Man_t_ // various data members Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes Aig_Obj_t ** pMemRepr; // memory allocated for points to the node representatives + Aig_Obj_t ** pMemReprFra; // memory allocated for points to the node representatives in the FRAIG Vec_Ptr_t ** pMemFanins; // the arrays of fanins int * pMemSatNums; // the array of SAT numbers int nSizeAlloc; // allocated size of the arrays @@ -118,7 +120,9 @@ struct Fra_Man_t_ int nSatProof; int nSatFails; int nSatFailsReal; - int nSpeculs; + int nSpeculs; + int nChoices; + int nChoicesFake; // runtime int timeSim; int timeTrav; @@ -141,11 +145,13 @@ static inline unsigned Fra_ObjRandomSim() { return (rand() << static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]; } static inline Aig_Obj_t * Fra_ObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]; } +static inline Aig_Obj_t * Fra_ObjReprFra( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemReprFra[pObj->Id]; } static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; } static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; } static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id] = pNode; } static inline void Fra_ObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id] = pNode; } +static inline void Fra_ObjSetReprFra( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemReprFra[pObj->Id] = pNode; } static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; } static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; } @@ -160,8 +166,6 @@ static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_I /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== fraAnd.c ========================================================*/ -extern void Fra_Sweep( Fra_Man_t * p ); /*=== fraClass.c ========================================================*/ extern void Fra_PrintClasses( Fra_Man_t * p ); extern void Fra_CreateClasses( Fra_Man_t * p ); @@ -170,7 +174,10 @@ extern int Fra_RefineClasses1( Fra_Man_t * p ); /*=== fraCnf.c ========================================================*/ extern void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); /*=== fraCore.c ========================================================*/ -extern Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pParams ); +extern Aig_Man_t * Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars ); +extern Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig ); +/*=== fraDfs.c ========================================================*/ +extern int Fra_CheckTfi( Fra_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams ); |