/**CFile**************************************************************** FileName [dchInt.h] SystemName [ABC: Logic synthesis and verification system.] PackageName [Choice computation for tech-mapping.] Synopsis [External declarations.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 29, 2008.] Revision [$Id: dchInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $] ***********************************************************************/ #ifndef ABC__aig__dch__dchInt_h #define ABC__aig__dch__dchInt_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include "aig/aig/aig.h" #include "sat/bsat/satSolver.h" #include "dch.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// // equivalence classes typedef struct Dch_Cla_t_ Dch_Cla_t; // choicing manager typedef struct Dch_Man_t_ Dch_Man_t; struct Dch_Man_t_ { // parameters Dch_Pars_t * pPars; // choicing parameters // AIGs used in the package // Vec_Ptr_t * vAigs; // user-given AIGs Aig_Man_t * pAigTotal; // intermediate AIG Aig_Man_t * pAigFraig; // final AIG // equivalence classes Dch_Cla_t * ppClasses; // equivalence classes of nodes Aig_Obj_t ** pReprsProved; // equivalences proved // SAT solving sat_solver * pSat; // recyclable SAT solver int nSatVars; // the counter of SAT variables 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 * 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; // SAT calls statistics int nSatCalls; // the number of SAT calls int nSatProof; // the number of proofs int nSatFailsReal; // the number of timeouts int nSatCallsUnsat; // the number of unsat SAT calls int nSatCallsSat; // the number of sat SAT calls // choice node statistics int nLits; // the number of lits in the cand equiv classes int nReprs; // the number of proved equivalent pairs int nEquivs; // the number of final equivalences int nChoices; // the number of final choice nodes // runtime stats abctime timeSimInit; // simulation and class computation abctime timeSimSat; // simulation of the counter-examples abctime timeSat; // solving SAT abctime timeSatSat; // sat abctime timeSatUnsat; // unsat abctime timeSatUndec; // undecided abctime timeChoice; // choice computation abctime timeOther; // other runtime abctime timeTotal; // total runtime }; //////////////////////////////////////////////////////////////////////// /// 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 (Aig_Obj_t *)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); } static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) { assert( !Dch_ObjIsConst1Cand( pAig, pObj ) ); Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) ); } //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// /*=== dchAig.c ===================================================*/ /*=== dchChoice.c ===================================================*/ extern int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig ); extern int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig ); extern Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig, int fSkipRedSupps ); /*=== dchClass.c =================================================*/ extern Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig ); extern void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData, unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *), int (*pFuncNodeIsConst)(void *,Aig_Obj_t *), 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 ); extern int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive ); extern void Dch_ClassesCollectOneClass( Dch_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vRoots ); extern void Dch_ClassesCollectConst1Group( Dch_Cla_t * p, Aig_Obj_t * pObj, int nNodes, Vec_Ptr_t * vRoots ); extern int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive ); /*=== dchCnf.c ===================================================*/ extern void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj ); /*=== dchMan.c ===================================================*/ extern Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars ); extern void Dch_ManStop( Dch_Man_t * p ); extern void Dch_ManSatSolverRecycle( Dch_Man_t * p ); /*=== dchSat.c ===================================================*/ 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 ); /*=== 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 ); ABC_NAMESPACE_HEADER_END #endif //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////