diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-27 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-27 08:01:00 -0700 |
commit | a8a80d9a1a84c2c5f605f6630dc804f3631e7a9f (patch) | |
tree | e48831dc8c36a01683f1d73324e8c48af1db5b5c /src/aig/fra/fra.h | |
parent | 054e2cd3a8ab4ada55db4def2d6ce7d309341e07 (diff) | |
download | abc-a8a80d9a1a84c2c5f605f6630dc804f3631e7a9f.tar.gz abc-a8a80d9a1a84c2c5f605f6630dc804f3631e7a9f.tar.bz2 abc-a8a80d9a1a84c2c5f605f6630dc804f3631e7a9f.zip |
Version abc70727
Diffstat (limited to 'src/aig/fra/fra.h')
-rw-r--r-- | src/aig/fra/fra.h | 97 |
1 files changed, 59 insertions, 38 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 127882ea..13e79a0e 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -49,6 +49,7 @@ extern "C" { //////////////////////////////////////////////////////////////////////// typedef struct Fra_Par_t_ Fra_Par_t; +typedef struct Fra_Cla_t_ Fra_Cla_t; typedef struct Fra_Man_t_ Fra_Man_t; // FRAIG parameters @@ -65,8 +66,26 @@ struct Fra_Par_t_ int fProve; // prove the miter outputs int fVerbose; // verbose output int fDoSparse; // skip sparse functions + int fConeBias; // bias variables in the cone (good for unsat runs) int nBTLimitNode; // conflict limit at a node int nBTLimitMiter; // conflict limit at an output + int nTimeFrames; // the number of timeframes to unroll +}; + +// FRAIG equivalence classes +struct Fra_Cla_t_ +{ + Aig_Man_t * pAig; // the original AIG manager + Aig_Obj_t ** pMemRepr; // pointers to representatives of each node + Vec_Ptr_t * vClasses; // equivalence classes + Vec_Ptr_t * vClasses1; // equivalence class of Const1 node + Vec_Ptr_t * vClassesTemp; // temporary storage for new classes + Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes + Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used + Vec_Ptr_t * vClassOld; // old equivalence class after splitting + Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting + int nPairs; // the number of pairs of nodes + int fRefinement; // set to 1 when refinement has happened }; // FRAIG manager @@ -77,6 +96,9 @@ struct Fra_Man_t_ // AIG managers Aig_Man_t * pManAig; // the starting AIG manager Aig_Man_t * pManFraig; // the final AIG manager + // mapping AIG into FRAIG + int nFrames; // the number of timeframes used + Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes // simulation info unsigned * pSimWords; // memory for simulation information int nSimWords; // the number of simulation words @@ -85,27 +107,17 @@ struct Fra_Man_t_ unsigned * pPatWords; // the counter example int * pPatScores; // the scores of each pattern // equivalence classes - Vec_Ptr_t * vClasses; // equivalence classes - Vec_Ptr_t * vClasses1; // equivalence class of Const1 node - Vec_Ptr_t * vClassesTemp; // temporary storage for new classes - Aig_Obj_t ** pMemClasses; // memory allocated for equivalence classes - Aig_Obj_t ** pMemClassesFree; // memory allocated for equivalence classes to be used - Vec_Ptr_t * vClassOld; // old equivalence class after splitting - Vec_Ptr_t * vClassNew; // new equivalence class(es) after splitting - int nPairs; // the number of pairs of nodes + Fra_Cla_t * pCla; // representation of (candidate) equivalent nodes // equivalence checking sat_solver * pSat; // SAT solver int nSatVars; // the number of variables currently used Vec_Ptr_t * vPiVars; // the PIs of the cone used sint64 nBTLimitGlobal; // resource limit sint64 nInsLimitGlobal; // resource limit - // 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 + 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 + Vec_Ptr_t * vTimeouts; // the nodes, for which equivalence checking timed out // statistics int nSimRounds; int nNodesMiter; @@ -140,23 +152,23 @@ struct Fra_Man_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -static inline unsigned * Fra_ObjSim( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; } +static inline unsigned * Fra_ObjSim( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id; } static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ 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 Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFrames*pObj->Id + i]; } +static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFrames*pObj->Id + i] = pNode; } + +static inline Vec_Ptr_t * Fra_ObjFaninVec( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]; } +static inline void Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins ) { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins; } + +static inline int Fra_ObjSatNum( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id]; } +static inline void Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num ) { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num; } -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; } +static inline Aig_Obj_t * Fra_ClassObjRepr( Aig_Obj_t * pObj ) { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id]; } +static inline void Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; } -static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; } -static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; } +static inline Aig_Obj_t * Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL; } +static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL; } //////////////////////////////////////////////////////////////////////// /// ITERATORS /// @@ -167,31 +179,40 @@ static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_I //////////////////////////////////////////////////////////////////////// /*=== fraClass.c ========================================================*/ -extern void Fra_PrintClasses( Fra_Man_t * p ); -extern void Fra_CreateClasses( Fra_Man_t * p ); -extern int Fra_RefineClasses( Fra_Man_t * p ); -extern int Fra_RefineClasses1( Fra_Man_t * p ); +extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ); +extern void Fra_ClassesStop( Fra_Cla_t * p ); +extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ); +extern void Fra_ClassesPrint( Fra_Cla_t * p ); +extern void Fra_ClassesPrepare( Fra_Cla_t * p ); +extern int Fra_ClassesRefine( Fra_Cla_t * p ); +extern int Fra_ClassesRefine1( Fra_Cla_t * p ); +extern int Fra_ClassesCountLits( Fra_Cla_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 * pPars ); -extern Aig_Man_t * Fra_Choice( Aig_Man_t * pManAig ); +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 void Fra_FraigSweep( Fra_Man_t * pManAig ); /*=== fraDfs.c ========================================================*/ -extern int Fra_CheckTfi( Fra_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld ); +/*=== fraInd.c ========================================================*/ +extern Aig_Man_t * Fra_Induction( Aig_Man_t * p, int nFrames, int fVerbose ); /*=== fraMan.c ========================================================*/ 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_ManPrepare( Fra_Man_t * p ); +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 ); extern void Fra_ManPrint( Fra_Man_t * p ); /*=== fraSat.c ========================================================*/ extern int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); /*=== fraSim.c ========================================================*/ -extern int Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj ); -extern int Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); +extern int Fra_NodeHasZeroSim( Aig_Obj_t * pObj ); +extern int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ); +extern unsigned Fra_NodeHashSims( Aig_Obj_t * pObj ); extern void Fra_SavePattern( Fra_Man_t * p ); -extern void Fra_Simulate( Fra_Man_t * p ); +extern void Fra_Simulate( Fra_Man_t * p, int fInit ); extern void Fra_Resimulate( Fra_Man_t * p ); extern int Fra_CheckOutputSims( Fra_Man_t * p ); |