diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-08-02 20:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-08-02 20:01:00 -0700 |
| commit | b8dea8ff0510ee7be465f5fe50994ecb58b9b30a (patch) | |
| tree | bfa6f6d88e01d51a9b1224a03e199c0efd199898 /src/aig/dch/dchInt.h | |
| parent | cbb7ff8642236fbc21576dec7b57b9e4cb7e60ef (diff) | |
| download | abc-b8dea8ff0510ee7be465f5fe50994ecb58b9b30a.tar.gz abc-b8dea8ff0510ee7be465f5fe50994ecb58b9b30a.tar.bz2 abc-b8dea8ff0510ee7be465f5fe50994ecb58b9b30a.zip | |
Version abc80802_2
Diffstat (limited to 'src/aig/dch/dchInt.h')
| -rw-r--r-- | src/aig/dch/dchInt.h | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h index a71cba69..e9a6f2e4 100644 --- a/src/aig/dch/dchInt.h +++ b/src/aig/dch/dchInt.h @@ -63,8 +63,10 @@ struct Dch_Man_t_ int * pSatVars; // mapping of each node into its SAT var Vec_Ptr_t * vUsedNodes; // nodes whose SAT vars are assigned int nRecycles; // the number of times SAT solver was recycled + int nCallsSince; // the number of calls since the last recycle Vec_Ptr_t * vFanins; // fanins of the CNF node - Vec_Ptr_t * vRoots; // the roots of the current equiv class + Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate + Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate // solver cone size int nConeThis; int nConeMax; @@ -95,6 +97,12 @@ struct Dch_Man_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +static inline int Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; } +static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; } + +static inline Aig_Obj_t * Dch_ObjFraig( Aig_Obj_t * pObj ) { return pObj->pData; } +static inline void Dch_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { pObj->pData = pNode; } + static inline int Dch_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) { return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig); @@ -105,9 +113,6 @@ static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) ); } -static inline int Dch_ObjSatNum( Dch_Man_t * p, Aig_Obj_t * pObj ) { return p->pSatVars[pObj->Id]; } -static inline void Dch_ObjSetSatNum( Dch_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num; } - //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -126,6 +131,7 @@ extern void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData, int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ); extern void Dch_ClassesStop( Dch_Cla_t * p ); extern int Dch_ClassesLitNum( Dch_Cla_t * p ); +extern Aig_Obj_t ** Dch_ClassesReadClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize ); extern void Dch_ClassesPrint( Dch_Cla_t * p, int fVeryVerbose ); extern void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs ); extern int Dch_ClassesRefine( Dch_Cla_t * p ); @@ -143,7 +149,10 @@ extern void Dch_ManSatSolverRecycle( Dch_Man_t * p ); extern int Dch_NodesAreEquiv( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 ); /*=== dchSim.c ===================================================*/ extern Dch_Cla_t * Dch_CreateCandEquivClasses( Aig_Man_t * pAig, int nWords, int fVerbose ); -/*=== dchSim.c ===================================================*/ +/*=== dchSimSat.c ===================================================*/ +extern void Dch_ManResimulateCex( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ); +extern void Dch_ManResimulateCex2( Dch_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ); +/*=== dchSweep.c ===================================================*/ extern void Dch_ManSweep( Dch_Man_t * p ); #ifdef __cplusplus |