From ac037cbb966285b724c8bbf776195855dc4a558f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 23 May 2013 23:22:12 -0700 Subject: New MFS package. --- src/opt/sfm/sfmInt.h | 56 +++++++++++++++++++++++++++++++++------------------- 1 file changed, 36 insertions(+), 20 deletions(-) (limited to 'src/opt/sfm/sfmInt.h') diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h index d52b46e4..e2833121 100644 --- a/src/opt/sfm/sfmInt.h +++ b/src/opt/sfm/sfmInt.h @@ -55,33 +55,37 @@ struct Sfm_Ntk_t_ int nNodes; // internal nodes int nObjs; // total objects // user data - Vec_Wec_t * vFanins; // fanins Vec_Str_t * vFixed; // persistent objects Vec_Wrd_t * vTruths; // truth tables + Vec_Wec_t vFanins; // fanins // attributes - Vec_Wec_t * vFanouts; // fanouts - Vec_Int_t * vLevels; // logic level - Vec_Int_t vTravIds; // traversal IDs + Vec_Wec_t vFanouts; // fanouts + Vec_Int_t vLevels; // logic level + Vec_Int_t vCounts; // fanin counters Vec_Int_t vId2Var; // ObjId -> SatVar Vec_Int_t vVar2Id; // SatVar -> ObjId Vec_Wec_t * vCnfs; // CNFs Vec_Int_t * vCover; // temporary + // traversal IDs + Vec_Int_t vTravIds; // traversal IDs + Vec_Int_t vTravIds2;// traversal IDs int nTravIds; // traversal IDs + int nTravIds2;// traversal IDs // window int iNode; Vec_Int_t * vLeaves; // leaves Vec_Int_t * vRoots; // roots Vec_Int_t * vNodes; // internal Vec_Int_t * vTfo; // TFO (excluding iNode) + Vec_Int_t * vDivs; // divisors // SAT solving int nSatVars; // the number of variables sat_solver * pSat1; // SAT solver for the on-set sat_solver * pSat0; // SAT solver for the off-set // intermediate data - Vec_Int_t * vDivs; // divisors + Vec_Int_t * vDivIds; // divisors indexes Vec_Int_t * vLits; // literals - Vec_Int_t * vFani; // iterator fanins - Vec_Int_t * vFano; // iterator fanouts + Vec_Int_t * vDiffs; // differences Vec_Wec_t * vClauses; // CNF clauses for the node Vec_Int_t * vFaninMap;// mapping fanins into their SAT vars }; @@ -89,26 +93,38 @@ struct Sfm_Ntk_t_ #define SFM_SAT_UNDEC 0x1234567812345678 #define SFM_SAT_SAT 0x8765432187654321 -//////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// -#define Sfm_NtkForEachNode( p, i ) for ( i = p->nPis; i + p->nPos < p->nObjs; i++ ) -#define Sfm_NodeForEachFanin( p, Node, Fan, i ) for ( p->vFani = Vec_WecEntry(p->vFanins, Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFani, i)), 1); i++ ) -#define Sfm_NodeForEachFanout( p, Node, Fan, i ) for ( p->vFano = Vec_WecEntry(p->vFanouts, Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFano, i)), 1); i++ ) +static inline int Sfm_ObjIsPi( Sfm_Ntk_t * p, int i ) { return i < p->nPis; } +static inline int Sfm_ObjIsPo( Sfm_Ntk_t * p, int i ) { return i + p->nPos >= p->nObjs; } +static inline int Sfm_ObjIsNode( Sfm_Ntk_t * p, int i ) { return i >= p->nPis && i + p->nPos < p->nObjs; } + +static inline Vec_Int_t * Sfm_ObjFiArray( Sfm_Ntk_t * p, int i ) { return Vec_WecEntry(&p->vFanins, i); } +static inline Vec_Int_t * Sfm_ObjFoArray( Sfm_Ntk_t * p, int i ) { return Vec_WecEntry(&p->vFanouts, i); } -static inline int Sfm_ObjIsPi( Sfm_Ntk_t * p, int i ) { return i < p->nPis; } -static inline int Sfm_ObjIsPo( Sfm_Ntk_t * p, int i ) { return i + p->nPos < p->nObjs; } -static inline int Sfm_ObjIsNode( Sfm_Ntk_t * p, int i ) { return i >= p->nPis && i + p->nPos < p->nObjs; } +static inline int Sfm_ObjFaninNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Sfm_ObjFiArray(p, i)); } +static inline int Sfm_ObjFanoutNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Sfm_ObjFoArray(p, i)); } -static inline int Sfm_ObjFaninNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Vec_WecEntry(p->vFanins, i)); } -static inline int Sfm_ObjFanoutNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Vec_WecEntry(p->vFanouts, i)); } +static inline int Sfm_ObjFanin( Sfm_Ntk_t * p, int i, int k ) { return Vec_IntEntry(Sfm_ObjFiArray(p, i), k); } +static inline int Sfm_ObjFanout( Sfm_Ntk_t * p, int i, int k ) { return Vec_IntEntry(Sfm_ObjFoArray(p, i), k); } -static inline int Sfm_ObjSatVar( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry(&p->vId2Var, iObj); } +static inline int Sfm_ObjSatVar( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry(&p->vId2Var, iObj); } static inline void Sfm_ObjSetSatVar( Sfm_Ntk_t * p, int iObj, int Num ) { assert(Sfm_ObjSatVar(p, iObj) == -1); Vec_IntWriteEntry(&p->vId2Var, iObj, Num); Vec_IntWriteEntry(&p->vVar2Id, Num, iObj); } static inline void Sfm_ObjCleanSatVar( Sfm_Ntk_t * p, int Num ) { assert(Sfm_ObjSatVar(p, Vec_IntEntry(&p->vVar2Id, Num)) != -1); Vec_IntWriteEntry(&p->vId2Var, Vec_IntEntry(&p->vVar2Id, Num), Num); Vec_IntWriteEntry(&p->vVar2Id, Num, -1); } static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p, int nSize ) { int i; for ( i = 1; i < nSize; i++ ) Sfm_ObjCleanSatVar( p, i ); } +static inline int Sfm_ObjLevel( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry(&p->vLevels, iObj); } + +static inline int Sfm_ObjUpdateFaninCount( Sfm_Ntk_t * p, int iObj ) { return Vec_IntAddToEntry(&p->vCounts, iObj, -1); } +static inline void Sfm_ObjResetFaninCount( Sfm_Ntk_t * p, int iObj ) { Vec_IntWriteEntry(&p->vCounts, iObj, Sfm_ObjFaninNum(p, iObj)-1); } + + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#define Sfm_NtkForEachNode( p, i ) for ( i = p->nPis; i + p->nPos < p->nObjs; i++ ) +#define Sfm_NodeForEachFanin( p, Node, Fan, i ) for ( i = 0; i < Sfm_ObjFaninNum(p, Node) && ((Fan = Sfm_ObjFanin(p, Node, i)), 1); i++ ) +#define Sfm_NodeForEachFanout( p, Node, Fan, i ) for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ ) //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// @@ -124,7 +140,7 @@ extern Sfm_Ntk_t * Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPo /*=== sfmSat.c ==========================================================*/ extern word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit ); /*=== sfmWin.c ==========================================================*/ -extern int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode ); +extern int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose ); extern void Sfm_NtkWin2Sat( Sfm_Ntk_t * p ); -- cgit v1.2.3