| /**CFile**************************************************************** |
| |
| FileName [sscInt.h] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [Choice computation for tech-mapping.] |
| |
| Synopsis [Internal declarations.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 29, 2008.] |
| |
| Revision [$Id: sscInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #ifndef ABC__aig__ssc__sscInt_h |
| #define ABC__aig__ssc__sscInt_h |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// INCLUDES /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| #include "aig/gia/gia.h" |
| #include "sat/bsat/satSolver.h" |
| #include "ssc.h" |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// PARAMETERS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_HEADER_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// BASIC TYPES /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| // choicing manager |
| typedef struct Ssc_Man_t_ Ssc_Man_t; |
| struct Ssc_Man_t_ |
| { |
| // user data |
| Ssc_Pars_t * pPars; // choicing parameters |
| Gia_Man_t * pAig; // subject AIG |
| Gia_Man_t * pCare; // care set AIG |
| // internal data |
| Gia_Man_t * pFraig; // resulting AIG |
| sat_solver * pSat; // recyclable SAT solver |
| Vec_Int_t * vId2Var; // mapping of each node into its SAT var |
| Vec_Int_t * vVar2Id; // mapping of each SAT var into its node |
| Vec_Int_t * vPivot; // one SAT pattern |
| int nSatVarsPivot; // the number of variables for constraints |
| int nSatVars; // the current number of variables |
| // temporary storage |
| Vec_Int_t * vFront; // supergate fanins |
| Vec_Int_t * vFanins; // supergate fanins |
| Vec_Int_t * vPattern; // counter-example |
| Vec_Int_t * vDisPairs; // disproved pairs |
| // SAT calls statistics |
| int nSimRounds; // the number of simulation rounds |
| int nRecycles; // the number of times SAT solver was recycled |
| int nCallsSince; // the number of calls since the last recycle |
| int nSatCalls; // the number of SAT calls |
| int nSatCallsUnsat; // the number of unsat SAT calls |
| int nSatCallsSat; // the number of sat SAT calls |
| int nSatCallsUndec; // the number of undec SAT calls |
| // runtime stats |
| abctime timeSimInit; // simulation and class computation |
| abctime timeSimSat; // simulation of the counter-examples |
| abctime timeCnfGen; // generation of CNF |
| abctime timeSat; // total SAT time |
| abctime timeSatSat; // sat |
| abctime timeSatUnsat; // unsat |
| abctime timeSatUndec; // undecided |
| abctime timeOther; // other runtime |
| abctime timeTotal; // total runtime |
| }; |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// MACRO DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| static inline int Ssc_ObjSatVar( Ssc_Man_t * p, int iObj ) { return Vec_IntEntry(p->vId2Var, iObj); } |
| static inline void Ssc_ObjSetSatVar( Ssc_Man_t * p, int iObj, int Num ) { Vec_IntWriteEntry(p->vId2Var, iObj, Num); Vec_IntWriteEntry(p->vVar2Id, Num, iObj); } |
| static inline void Ssc_ObjCleanSatVar( Ssc_Man_t * p, int Num ) { Vec_IntWriteEntry(p->vId2Var, Vec_IntEntry(p->vVar2Id, Num), Num); Vec_IntWriteEntry(p->vVar2Id, Num, 0); } |
| |
| static inline int Ssc_ObjFraig( Ssc_Man_t * p, Gia_Obj_t * pObj ) { return pObj->Value; } |
| static inline void Ssc_ObjSetFraig( Gia_Obj_t * pObj, int iNode ) { pObj->Value = iNode; } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /*=== sscClass.c =================================================*/ |
| extern void Ssc_GiaClassesInit( Gia_Man_t * p ); |
| extern int Ssc_GiaClassesRefine( Gia_Man_t * p ); |
| extern void Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs ); |
| extern int Ssc_GiaSimClassRefineOneBit( Gia_Man_t * p, int i ); |
| /*=== sscCnf.c ===================================================*/ |
| extern void Ssc_CnfNodeAddToSolver( Ssc_Man_t * p, Gia_Obj_t * pObj ); |
| /*=== sscCore.c ==================================================*/ |
| /*=== sscSat.c ===================================================*/ |
| extern void Ssc_ManSatSolverRecycle( Ssc_Man_t * p ); |
| extern void Ssc_ManStartSolver( Ssc_Man_t * p ); |
| extern Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p ); |
| extern int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iObj, int fCompl ); |
| /*=== sscSim.c ===================================================*/ |
| extern void Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords ); |
| extern void Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot ); |
| extern int Ssc_GiaTransferPiPattern( Gia_Man_t * pAig, Gia_Man_t * pCare, Vec_Int_t * vPivot ); |
| extern void Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat ); |
| extern void Ssc_GiaSimRound( Gia_Man_t * p ); |
| extern Vec_Int_t * Ssc_GiaFindPivotSim( Gia_Man_t * p ); |
| extern int Ssc_GiaEstimateCare( Gia_Man_t * p, int nWords ); |
| /*=== sscUtil.c ===================================================*/ |
| extern Gia_Man_t * Ssc_GenerateOneHot( int nVars ); |
| |
| |
| ABC_NAMESPACE_HEADER_END |
| |
| |
| |
| #endif |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
