diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-28 14:29:56 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-03-28 14:29:56 -0700 |
| commit | fdfb8888911220cbd7e6774dda1f90f3c9637fd5 (patch) | |
| tree | 97224cb817f3690838484328b52e390c02e0580f | |
| parent | 2ccd0f9b85cb42d3e6e894a71cd8e962b2d3bd12 (diff) | |
| download | abc-fdfb8888911220cbd7e6774dda1f90f3c9637fd5.tar.gz abc-fdfb8888911220cbd7e6774dda1f90f3c9637fd5.tar.bz2 abc-fdfb8888911220cbd7e6774dda1f90f3c9637fd5.zip | |
Experiments with don't-cares.
| -rw-r--r-- | src/base/acb/acb.h | 348 | ||||
| -rw-r--r-- | src/base/acb/acbAbc.c | 18 | ||||
| -rw-r--r-- | src/base/acb/acbMfs.c | 395 | ||||
| -rw-r--r-- | src/base/acb/acbUtil.c | 250 | ||||
| -rw-r--r-- | src/sat/cnf/cnfMan.c | 2 |
5 files changed, 538 insertions, 475 deletions
diff --git a/src/base/acb/acb.h b/src/base/acb/acb.h index 0877a025..6954010b 100644 --- a/src/base/acb/acb.h +++ b/src/base/acb/acb.h @@ -30,6 +30,7 @@ #include "misc/util/utilNam.h" #include "misc/vec/vecHash.h" #include "aig/miniaig/abcOper.h" +#include "misc/vec/vecQue.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -70,7 +71,6 @@ struct Acb_Ntk_t_ Vec_Str_t vObjType; // type Vec_Int_t vObjFans; // fanin offsets Vec_Int_t vFanSto; // fanin storage - Vec_Wec_t vFanouts; // fanouts // optional Vec_Int_t vObjCopy; // copy Vec_Int_t vObjFunc; // function @@ -88,19 +88,20 @@ struct Acb_Ntk_t_ Vec_Int_t vLevelR; // level Vec_Int_t vPathD; // path Vec_Int_t vPathR; // path - Vec_Wec_t vClauses; - Vec_Wec_t vCnfs; - Vec_Int_t vCover; + Vec_Flt_t vCounts; // priority counts + Vec_Wec_t vFanouts; // fanouts + Vec_Wec_t vCnfs; // CNF // other - Vec_Int_t vArray0; - Vec_Int_t vArray1; - Vec_Int_t vArray2; + Vec_Que_t * vQue; // temporary + Vec_Int_t vCover; // temporary + Vec_Int_t vArray0; // temporary + Vec_Int_t vArray1; // temporary + Vec_Int_t vArray2; // temporary }; // design struct Acb_Man_t_ { - // design names char * pName; // design name char * pSpec; // spec file name Abc_Nam_t * pStrs; // string manager @@ -185,7 +186,7 @@ static inline int Acb_NtkNodeNum( Acb_Ntk_t * p ) { r static inline int Acb_NtkSeqNum( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vSeq); } static inline void Acb_NtkCleanObjCopies( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjCopy, Vec_StrCap(&p->vObjType), -1); } -static inline void Acb_NtkCleanObjFuncs( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjFunc, Vec_StrCap(&p->vObjType), 0); } +static inline void Acb_NtkCleanObjFuncs( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjFunc, Vec_StrCap(&p->vObjType), -1); } static inline void Acb_NtkCleanObjWeights( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjWeight,Vec_StrCap(&p->vObjType), 0); } static inline void Acb_NtkCleanObjTruths( Acb_Ntk_t * p ) { Vec_WrdFill(&p->vObjTruth, Vec_StrCap(&p->vObjType), 0); } static inline void Acb_NtkCleanObjNames( Acb_Ntk_t * p ) { Vec_IntFill(&p->vObjName, Vec_StrCap(&p->vObjType), 0); } @@ -196,114 +197,127 @@ static inline void Acb_NtkCleanObjLevelD( Acb_Ntk_t * p ) { V static inline void Acb_NtkCleanObjLevelR( Acb_Ntk_t * p ) { Vec_IntFill(&p->vLevelR, Vec_StrCap(&p->vObjType), 0); } static inline void Acb_NtkCleanObjPathD( Acb_Ntk_t * p ) { Vec_IntFill(&p->vPathD, Vec_StrCap(&p->vObjType), 0); } static inline void Acb_NtkCleanObjPathR( Acb_Ntk_t * p ) { Vec_IntFill(&p->vPathR, Vec_StrCap(&p->vObjType), 0); } - -static inline int Acb_NtkHasObjCopies( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjCopy) > 0; } -static inline int Acb_NtkHasObjFuncs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjFunc) > 0; } -static inline int Acb_NtkHasObjWeights( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjWeight)> 0; } -static inline int Acb_NtkHasObjTruths( Acb_Ntk_t * p ) { return Vec_WrdSize(&p->vObjTruth) > 0; } -static inline int Acb_NtkHasObjNames( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjName) > 0; } -static inline int Acb_NtkHasObjRanges( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjRange) > 0; } -static inline int Acb_NtkHasObjTravs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjTrav) > 0; } -static inline int Acb_NtkHasObjAttrs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjAttr) > 0; } -static inline int Acb_NtkHasObjLevelD( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vLevelD) > 0; } -static inline int Acb_NtkHasObjLevelR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vLevelR) > 0; } -static inline int Acb_NtkHasObjPathD( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathD) > 0; } -static inline int Acb_NtkHasObjPathR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathR) > 0; } - -static inline void Acb_NtkFreeObjCopies( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjCopy); } -static inline void Acb_NtkFreeObjFuncs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjFunc); } -static inline void Acb_NtkFreeObjWeights( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjWeight); } -static inline void Acb_NtkFreeObjTruths( Acb_Ntk_t * p ) { Vec_WrdErase(&p->vObjTruth); } -static inline void Acb_NtkFreeObjNames( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjName); } -static inline void Acb_NtkFreeObjRanges( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjRange); } -static inline void Acb_NtkFreeObjTravs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjTrav); } -static inline void Acb_NtkFreeObjAttrs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjAttr); } -static inline void Acb_NtkFreeObjLevelD( Acb_Ntk_t * p ) { Vec_IntErase(&p->vLevelD); } -static inline void Acb_NtkFreeObjLevelR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vLevelR); } -static inline void Acb_NtkFreeObjPathD( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathD); } -static inline void Acb_NtkFreeObjPathR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathR); } - -static inline Acb_ObjType_t Acb_ObjType( Acb_Ntk_t * p, int i ) { assert(i>0); return (Acb_ObjType_t)(int)(unsigned char)Vec_StrEntry(&p->vObjType, i); } -static inline void Acb_ObjCleanType( Acb_Ntk_t * p, int i ) { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)ABC_OPER_NONE ); } -static inline int Acb_TypeIsSeq( Acb_ObjType_t Type ) { return Type >= ABC_OPER_RAM && Type <= ABC_OPER_DFFRS; } -static inline int Acb_TypeIsUnary( Acb_ObjType_t Type ) { return Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_BIT_INV || Type == ABC_OPER_LOGIC_NOT || Type == ABC_OPER_ARI_MIN || Type == ABC_OPER_ARI_SQRT || Type == ABC_OPER_ARI_ABS || (Type >= ABC_OPER_RED_AND && Type <= ABC_OPER_RED_NXOR); } -static inline int Acb_TypeIsMux( Acb_ObjType_t Type ) { return Type == ABC_OPER_BIT_MUX || Type == ABC_OPER_SEL_NMUX || Type == ABC_OPER_SEL_SEL || Type == ABC_OPER_SEL_PSEL; } - -static inline int Acb_ObjIsCi( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CI; } -static inline int Acb_ObjIsCo( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CO; } -static inline int Acb_ObjIsCio( Acb_Ntk_t * p, int i ) { return Acb_ObjIsCi(p, i) || Acb_ObjIsCo(p, i); } -static inline int Acb_ObjIsFon( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_FON; } -static inline int Acb_ObjIsBox( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_BOX; } -static inline int Acb_ObjIsGate( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_GATE; } -static inline int Acb_ObjIsSlice( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_SLICE; } -static inline int Acb_ObjIsConcat( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CONCAT; } -static inline int Acb_ObjIsUnary( Acb_Ntk_t * p, int i ) { return Acb_TypeIsUnary(Acb_ObjType(p, i)); } +static inline void Acb_NtkCleanObjCounts( Acb_Ntk_t * p ) { Vec_FltFill(&p->vCounts, Vec_StrCap(&p->vObjType), 0); } +static inline void Acb_NtkCleanObjFanout( Acb_Ntk_t * p ) { Vec_WecInit(&p->vFanouts, Vec_StrCap(&p->vObjType) ); } +static inline void Acb_NtkCleanObjCnfs( Acb_Ntk_t * p ) { Vec_WecInit(&p->vCnfs, Vec_StrCap(&p->vObjType) ); } + +static inline int Acb_NtkHasObjCopies( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjCopy) > 0; } +static inline int Acb_NtkHasObjFuncs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjFunc) > 0; } +static inline int Acb_NtkHasObjWeights( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjWeight)> 0; } +static inline int Acb_NtkHasObjTruths( Acb_Ntk_t * p ) { return Vec_WrdSize(&p->vObjTruth) > 0; } +static inline int Acb_NtkHasObjNames( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjName) > 0; } +static inline int Acb_NtkHasObjRanges( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjRange) > 0; } +static inline int Acb_NtkHasObjTravs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjTrav) > 0; } +static inline int Acb_NtkHasObjAttrs( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vObjAttr) > 0; } +static inline int Acb_NtkHasObjLevelD( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vLevelD) > 0; } +static inline int Acb_NtkHasObjLevelR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vLevelR) > 0; } +static inline int Acb_NtkHasObjPathD( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathD) > 0; } +static inline int Acb_NtkHasObjPathR( Acb_Ntk_t * p ) { return Vec_IntSize(&p->vPathR) > 0; } +static inline int Acb_NtkHasObjCounts( Acb_Ntk_t * p ) { return Vec_FltSize(&p->vCounts) > 0; } +static inline int Acb_NtkHasObjFanout( Acb_Ntk_t * p ) { return Vec_WecSize(&p->vFanouts) > 0; } +static inline int Acb_NtkHasObjCnfs( Acb_Ntk_t * p ) { return Vec_WecSize(&p->vCnfs) > 0; } + +static inline void Acb_NtkFreeObjCopies( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjCopy); } +static inline void Acb_NtkFreeObjFuncs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjFunc); } +static inline void Acb_NtkFreeObjWeights( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjWeight); } +static inline void Acb_NtkFreeObjTruths( Acb_Ntk_t * p ) { Vec_WrdErase(&p->vObjTruth); } +static inline void Acb_NtkFreeObjNames( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjName); } +static inline void Acb_NtkFreeObjRanges( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjRange); } +static inline void Acb_NtkFreeObjTravs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjTrav); } +static inline void Acb_NtkFreeObjAttrs( Acb_Ntk_t * p ) { Vec_IntErase(&p->vObjAttr); } +static inline void Acb_NtkFreeObjLevelD( Acb_Ntk_t * p ) { Vec_IntErase(&p->vLevelD); } +static inline void Acb_NtkFreeObjLevelR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vLevelR); } +static inline void Acb_NtkFreeObjPathD( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathD); } +static inline void Acb_NtkFreeObjPathR( Acb_Ntk_t * p ) { Vec_IntErase(&p->vPathR); } +static inline void Acb_NtkFreeObjCounts( Acb_Ntk_t * p ) { Vec_FltErase(&p->vCounts); } +static inline void Acb_NtkFreeObjFanout( Acb_Ntk_t * p ) { Vec_WecErase(&p->vFanouts); } +static inline void Acb_NtkFreeObjCnfs( Acb_Ntk_t * p ) { Vec_WecErase(&p->vCnfs); } + +static inline Acb_ObjType_t Acb_ObjType( Acb_Ntk_t * p, int i ) { assert(i>0); return (Acb_ObjType_t)(int)(unsigned char)Vec_StrEntry(&p->vObjType, i); } +static inline void Acb_ObjCleanType( Acb_Ntk_t * p, int i ) { assert(i>0); Vec_StrWriteEntry( &p->vObjType, i, (char)ABC_OPER_NONE ); } +static inline int Acb_TypeIsSeq( Acb_ObjType_t Type ) { return Type >= ABC_OPER_RAM && Type <= ABC_OPER_DFFRS; } +static inline int Acb_TypeIsUnary( Acb_ObjType_t Type ) { return Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_BIT_INV || Type == ABC_OPER_LOGIC_NOT || Type == ABC_OPER_ARI_MIN || Type == ABC_OPER_ARI_SQRT || Type == ABC_OPER_ARI_ABS || (Type >= ABC_OPER_RED_AND && Type <= ABC_OPER_RED_NXOR); } +static inline int Acb_TypeIsMux( Acb_ObjType_t Type ) { return Type == ABC_OPER_BIT_MUX || Type == ABC_OPER_SEL_NMUX || Type == ABC_OPER_SEL_SEL || Type == ABC_OPER_SEL_PSEL; } + +static inline int Acb_ObjIsCi( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CI; } +static inline int Acb_ObjIsCo( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CO; } +static inline int Acb_ObjIsCio( Acb_Ntk_t * p, int i ) { return Acb_ObjIsCi(p, i) || Acb_ObjIsCo(p, i); } +static inline int Acb_ObjIsFon( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_FON; } +static inline int Acb_ObjIsBox( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_BOX; } +static inline int Acb_ObjIsGate( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_GATE; } +static inline int Acb_ObjIsSlice( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_SLICE; } +static inline int Acb_ObjIsConcat( Acb_Ntk_t * p, int i ) { return Acb_ObjType(p, i) == ABC_OPER_CONCAT; } +static inline int Acb_ObjIsUnary( Acb_Ntk_t * p, int i ) { return Acb_TypeIsUnary(Acb_ObjType(p, i)); } -static inline int Acb_ObjFanOffset( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vObjFans, i); } -static inline int * Acb_ObjFanins( Acb_Ntk_t * p, int i ) { return Vec_IntEntryP(&p->vFanSto, Acb_ObjFanOffset(p, i)); } -static inline int Acb_ObjFanin( Acb_Ntk_t * p, int i, int k ) { return Acb_ObjFanins(p, i)[k+1]; } -static inline int Acb_ObjFaninNum( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[0]; } -static inline int Acb_ObjFanoutNum( Acb_Ntk_t * p, int i ) { return Vec_IntSize( Vec_WecEntry(&p->vFanouts, i) ); } -static inline Vec_Int_t * Acb_ObjFanoutVec( Acb_Ntk_t * p, int i ) { return Vec_WecEntry( &p->vFanouts, i ); } -static inline int Acb_ObjFanin0( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[1]; } -static inline int Acb_ObjCioId( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[2]; } +static inline int Acb_ObjFanOffset( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vObjFans, i); } +static inline int * Acb_ObjFanins( Acb_Ntk_t * p, int i ) { return Vec_IntEntryP(&p->vFanSto, Acb_ObjFanOffset(p, i)); } +static inline int Acb_ObjFanin( Acb_Ntk_t * p, int i, int k ) { return Acb_ObjFanins(p, i)[k+1]; } +static inline int Acb_ObjFaninNum( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[0]; } +static inline int Acb_ObjFanoutNum( Acb_Ntk_t * p, int i ) { return Vec_IntSize( Vec_WecEntry(&p->vFanouts, i) ); } +static inline Vec_Int_t * Acb_ObjFanoutVec( Acb_Ntk_t * p, int i ) { return Vec_WecEntry( &p->vFanouts, i ); } +static inline int Acb_ObjFanin0( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[1]; } +static inline int Acb_ObjCioId( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[2]; } -static inline int Acb_ObjCopy( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjCopies(p) ); return Vec_IntGetEntryFull(&p->vObjCopy, i); } -static inline int Acb_ObjFunc( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjFuncs(p) ); return Vec_IntGetEntry(&p->vObjFunc, i); } -static inline int Acb_ObjWeight( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjWeights(p) );return Vec_IntGetEntry(&p->vObjWeight, i); } -static inline word Acb_ObjTruth( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdGetEntry(&p->vObjTruth, i); } -static inline word * Acb_ObjTruthP( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdEntryP(&p->vObjTruth, i); } -static inline int Acb_ObjName( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjNames(p) ); return Vec_IntGetEntry(&p->vObjName, i); } -static inline char * Acb_ObjNameStr( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkStr(p, Acb_ObjName(p, i)); } -static inline int Acb_ObjAttr( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_NtkHasObjAttrs(p) ? Vec_IntGetEntry(&p->vObjAttr, i) : 0; } -static inline int Acb_ObjAttrSize( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntry(&p->vAttrSto, Acb_ObjAttr(p, i)) : 0; } -static inline int * Acb_ObjAttrArray( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntryP(&p->vAttrSto, Acb_ObjAttr(p, i)+1) : NULL; } -static inline int Acb_ObjAttrValue( Acb_Ntk_t * p, int i, int x ) { int k, s = Acb_ObjAttrSize(p, i), * a = Acb_ObjAttrArray(p, i); for ( k = 0; k < s; k += 2) if (a[k] == x) return a[k+1]; return 0; } -static inline int Acb_ObjLevelD( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vLevelD, i); } -static inline int Acb_ObjLevelR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vLevelR, i); } -static inline int Acb_ObjPathD( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathD, i); } -static inline int Acb_ObjPathR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathR, i); } - -static inline void Acb_ObjSetCopy( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjCopy(p, i) == -1); Vec_IntSetEntry( &p->vObjCopy, i, x ); } -static inline void Acb_ObjSetFunc( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjFunc(p, i) == 0); Vec_IntSetEntry( &p->vObjFunc, i, x ); } -static inline void Acb_ObjSetWeight( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjWeight(p, i) == 0); Vec_IntSetEntry( &p->vObjWeight, i, x ); } -static inline void Acb_ObjSetTruth( Acb_Ntk_t * p, int i, word x ) { assert(Acb_ObjTruth(p, i) == 0);Vec_WrdSetEntry( &p->vObjTruth, i, x ); } -static inline void Acb_ObjSetName( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjName(p, i) == 0); Vec_IntSetEntry( &p->vObjName, i, x ); } -static inline void Acb_ObjSetAttrs( Acb_Ntk_t * p, int i, int * a, int s ) { assert(Acb_ObjAttr(p, i) == 0); if ( !a ) return; Vec_IntSetEntry(&p->vObjAttr, i, Vec_IntSize(&p->vAttrSto)); Vec_IntPush(&p->vAttrSto, s); Vec_IntPushArray(&p->vAttrSto, a, s); } -static inline int Acb_ObjSetLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vLevelD, i, x ); return x; } -static inline int Acb_ObjSetLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vLevelR, i, x ); return x; } -static inline int Acb_ObjSetPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vPathD, i, x ); return x; } -static inline int Acb_ObjSetPathR( Acb_Ntk_t * p, int i, int x ) { Vec_IntSetEntry( &p->vPathR, i, x ); return x; } -static inline int Acb_ObjUpdateLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelD, i, x ); return x; } -static inline int Acb_ObjUpdateLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelR, i, x ); return x; } -static inline int Acb_ObjAddToPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathD, i, x ); return x; } -static inline int Acb_ObjAddToPathR( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathR, i, x ); return x; } - -static inline int Acb_ObjNtkId( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjFanin(p, i, Acb_ObjFaninNum(p, i)) : 0; } -static inline Acb_Ntk_t * Acb_ObjNtk( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkNtk(p, Acb_ObjNtkId(p, i)); } -static inline int Acb_ObjIsSeq( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjNtk(p, i)->fSeq : Acb_TypeIsSeq(Acb_ObjType(p, i)); } - -static inline int Acb_ObjRangeId( Acb_Ntk_t * p, int i ) { return Acb_NtkHasObjRanges(p) ? Vec_IntGetEntry(&p->vObjRange, i) : 0; } -static inline int Acb_ObjRange( Acb_Ntk_t * p, int i ) { return Abc_Lit2Var( Acb_ObjRangeId(p, i) ); } -static inline int Acb_ObjLeft( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeLeft(p, Acb_ObjRange(p, i)); } -static inline int Acb_ObjRight( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeRight(p, Acb_ObjRange(p, i)); } -static inline int Acb_ObjSigned( Acb_Ntk_t * p, int i ) { return Abc_LitIsCompl(Acb_ObjRangeId(p, i)); } -static inline int Acb_ObjRangeSize( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeSize(p, Acb_ObjRange(p, i)); } -static inline void Acb_ObjSetRangeSign( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntSetEntry(&p->vObjRange, i, x); } -static inline void Acb_ObjSetRange( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntSetEntry(&p->vObjRange, i, Abc_Var2Lit(x,0)); } -static inline void Acb_ObjHashRange( Acb_Ntk_t * p, int i, int l, int r ) { Acb_ObjSetRange( p, i, Acb_NtkHashRange(p, l, r) ); } -static inline int Acb_ObjRangeSign( Acb_Ntk_t * p, int i ) { return Abc_Var2Lit( Acb_ObjRangeSize(p, i), Acb_ObjSigned(p, i) ); } - -static inline int Acb_ObjTravId( Acb_Ntk_t * p, int i ) { return Vec_IntGetEntry(&p->vObjTrav, i); } -static inline int Acb_ObjTravIdDiff( Acb_Ntk_t * p, int i ) { return p->nObjTravs - Vec_IntGetEntry(&p->vObjTrav, i); } -static inline int Acb_ObjIsTravIdCur( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs; } -static inline int Acb_ObjIsTravIdPrev( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs-1; } -static inline int Acb_ObjIsTravIdDiff( Acb_Ntk_t * p, int i, int d ) { return Acb_ObjTravId(p, i) == p->nObjTravs-d; } -static inline int Acb_ObjSetTravIdCur( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdCur(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs); return r; } -static inline int Acb_ObjSetTravIdPrev( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdPrev(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-1); return r; } -static inline int Acb_ObjSetTravIdDiff( Acb_Ntk_t * p, int i, int d ) { int r = Acb_ObjTravIdDiff(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-d); return r; } -static inline int Acb_NtkTravId( Acb_Ntk_t * p ) { return p->nObjTravs; } -static inline void Acb_NtkIncTravId( Acb_Ntk_t * p ) { if ( !Acb_NtkHasObjTravs(p) ) Acb_NtkCleanObjTravs(p); p->nObjTravs++; } +static inline int Acb_ObjCopy( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjCopies(p) ); return Vec_IntEntry(&p->vObjCopy, i); } +static inline int Acb_ObjFunc( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjFuncs(p) ); return Vec_IntEntry(&p->vObjFunc, i); } +static inline int Acb_ObjWeight( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjWeights(p) );return Vec_IntEntry(&p->vObjWeight, i); } +static inline word Acb_ObjTruth( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdEntry(&p->vObjTruth, i); } +static inline word * Acb_ObjTruthP( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjTruths(p) ); return Vec_WrdEntryP(&p->vObjTruth, i); } +static inline int Acb_ObjName( Acb_Ntk_t * p, int i ) { assert(i>0); assert( Acb_NtkHasObjNames(p) ); return Vec_IntEntry(&p->vObjName, i); } +static inline char * Acb_ObjNameStr( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkStr(p, Acb_ObjName(p, i)); } +static inline int Acb_ObjAttr( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_NtkHasObjAttrs(p) ? Vec_IntEntry(&p->vObjAttr, i) : 0; } +static inline int Acb_ObjAttrSize( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntry(&p->vAttrSto, Acb_ObjAttr(p, i)) : 0; } +static inline int * Acb_ObjAttrArray( Acb_Ntk_t * p, int i ) { assert(i>=0); return Acb_ObjAttr(p, i) ? Vec_IntEntryP(&p->vAttrSto, Acb_ObjAttr(p, i)+1) : NULL; } +static inline int Acb_ObjAttrValue( Acb_Ntk_t * p, int i, int x ) { int k, s = Acb_ObjAttrSize(p, i), * a = Acb_ObjAttrArray(p, i); for ( k = 0; k < s; k += 2) if (a[k] == x) return a[k+1]; return 0; } +static inline int Acb_ObjLevelD( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vLevelD, i); } +static inline int Acb_ObjLevelR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vLevelR, i); } +static inline int Acb_ObjPathD( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathD, i); } +static inline int Acb_ObjPathR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathR, i); } +static inline float Acb_ObjCounts( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_FltEntry(&p->vCounts, i); } +static inline Vec_Int_t * Acb_ObjFanout( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_WecEntry(&p->vFanouts, i); } +static inline Vec_Str_t * Acb_ObjCnfs( Acb_Ntk_t * p, int i ) { assert(i>0); return (Vec_Str_t *)Vec_WecEntry(&p->vCnfs, i); } + +static inline void Acb_ObjSetCopy( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjCopy(p, i) == -1); Vec_IntWriteEntry( &p->vObjCopy, i, x ); } +static inline void Acb_ObjSetFunc( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjFunc(p, i) == -1); Vec_IntWriteEntry( &p->vObjFunc, i, x ); } +static inline void Acb_ObjSetWeight( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjWeight(p, i)== 0); Vec_IntWriteEntry( &p->vObjWeight, i, x ); } +static inline void Acb_ObjSetTruth( Acb_Ntk_t * p, int i, word x ) { assert(Acb_ObjTruth(p, i) == 0); Vec_WrdWriteEntry( &p->vObjTruth, i, x ); } +static inline void Acb_ObjSetName( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjName(p, i) == 0); Vec_IntWriteEntry( &p->vObjName, i, x ); } +static inline void Acb_ObjSetAttrs( Acb_Ntk_t * p, int i, int * a, int s ) { assert(Acb_ObjAttr(p, i) == 0); if ( !a ) return; Vec_IntWriteEntry(&p->vObjAttr, i, Vec_IntSize(&p->vAttrSto)); Vec_IntPush(&p->vAttrSto, s); Vec_IntPushArray(&p->vAttrSto, a, s); } +static inline int Acb_ObjSetLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vLevelD, i, x ); return x; } +static inline int Acb_ObjSetLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vLevelR, i, x ); return x; } +static inline int Acb_ObjSetPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vPathD, i, x ); return x; } +static inline int Acb_ObjSetPathR( Acb_Ntk_t * p, int i, int x ) { Vec_IntWriteEntry( &p->vPathR, i, x ); return x; } +static inline float Acb_ObjSetCounts( Acb_Ntk_t * p, int i, float x ) { Vec_FltWriteEntry( &p->vCounts, i, x ); return x; } +static inline int Acb_ObjUpdateLevelD( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelD, i, x ); return x; } +static inline int Acb_ObjUpdateLevelR( Acb_Ntk_t * p, int i, int x ) { Vec_IntUpdateEntry( &p->vLevelR, i, x ); return x; } +static inline int Acb_ObjAddToPathD( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathD, i, x ); return x; } +static inline int Acb_ObjAddToPathR( Acb_Ntk_t * p, int i, int x ) { Vec_IntAddToEntry( &p->vPathR, i, x ); return x; } + +static inline int Acb_ObjNtkId( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjFanin(p, i, Acb_ObjFaninNum(p, i)) : 0; } +static inline Acb_Ntk_t * Acb_ObjNtk( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_NtkNtk(p, Acb_ObjNtkId(p, i)); } +static inline int Acb_ObjIsSeq( Acb_Ntk_t * p, int i ) { assert(i>0); return Acb_ObjIsBox(p, i) ? Acb_ObjNtk(p, i)->fSeq : Acb_TypeIsSeq(Acb_ObjType(p, i)); } + +static inline int Acb_ObjRangeId( Acb_Ntk_t * p, int i ) { return Acb_NtkHasObjRanges(p) ? Vec_IntEntry(&p->vObjRange, i) : 0; } +static inline int Acb_ObjRange( Acb_Ntk_t * p, int i ) { return Abc_Lit2Var( Acb_ObjRangeId(p, i) ); } +static inline int Acb_ObjLeft( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeLeft(p, Acb_ObjRange(p, i)); } +static inline int Acb_ObjRight( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeRight(p, Acb_ObjRange(p, i)); } +static inline int Acb_ObjSigned( Acb_Ntk_t * p, int i ) { return Abc_LitIsCompl(Acb_ObjRangeId(p, i)); } +static inline int Acb_ObjRangeSize( Acb_Ntk_t * p, int i ) { return Acb_NtkRangeSize(p, Acb_ObjRange(p, i)); } +static inline void Acb_ObjSetRangeSign( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntWriteEntry(&p->vObjRange, i, x); } +static inline void Acb_ObjSetRange( Acb_Ntk_t * p, int i, int x ) { assert(Acb_NtkHasObjRanges(p)); Vec_IntWriteEntry(&p->vObjRange, i, Abc_Var2Lit(x,0)); } +static inline void Acb_ObjHashRange( Acb_Ntk_t * p, int i, int l, int r ) { Acb_ObjSetRange( p, i, Acb_NtkHashRange(p, l, r) ); } +static inline int Acb_ObjRangeSign( Acb_Ntk_t * p, int i ) { return Abc_Var2Lit( Acb_ObjRangeSize(p, i), Acb_ObjSigned(p, i) ); } + +static inline int Acb_ObjTravId( Acb_Ntk_t * p, int i ) { return Vec_IntEntry(&p->vObjTrav, i); } +static inline int Acb_ObjTravIdDiff( Acb_Ntk_t * p, int i ) { return p->nObjTravs - Vec_IntEntry(&p->vObjTrav, i); } +static inline int Acb_ObjIsTravIdCur( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs; } +static inline int Acb_ObjIsTravIdPrev( Acb_Ntk_t * p, int i ) { return Acb_ObjTravId(p, i) == p->nObjTravs-1; } +static inline int Acb_ObjIsTravIdDiff( Acb_Ntk_t * p, int i, int d ) { return Acb_ObjTravId(p, i) == p->nObjTravs-d; } +static inline int Acb_ObjSetTravIdCur( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdCur(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs); return r; } +static inline int Acb_ObjSetTravIdPrev( Acb_Ntk_t * p, int i ) { int r = Acb_ObjIsTravIdPrev(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-1); return r; } +static inline int Acb_ObjSetTravIdDiff( Acb_Ntk_t * p, int i, int d ) { int r = Acb_ObjTravIdDiff(p, i); Vec_IntWriteEntry(&p->vObjTrav, i, p->nObjTravs-d); return r; } +static inline int Acb_NtkTravId( Acb_Ntk_t * p ) { return p->nObjTravs; } +static inline void Acb_NtkIncTravId( Acb_Ntk_t * p ) { if ( !Acb_NtkHasObjTravs(p) ) Acb_NtkCleanObjTravs(p); p->nObjTravs++; } //////////////////////////////////////////////////////////////////////// /// ITERATORS /// @@ -393,6 +407,13 @@ static inline void Acb_ObjAddFanin( Acb_Ntk_t * p, int iObj, int iFanin ) assert( pFanins[ 1 + pFanins[0] ] == -1 ); pFanins[ 1 + pFanins[0]++ ] = iFanin; } +static inline void Acb_ObjAddFanins( Acb_Ntk_t * p, int iObj, Vec_Int_t * vFanins ) +{ + int i, iFanin; + if ( vFanins ) + Vec_IntForEachEntry( vFanins, iFanin, i ) + Acb_ObjAddFanin( p, iObj, iFanin ); +} static inline void Acb_ObjSetNtkId( Acb_Ntk_t * p, int iObj, int iNtk ) // should be called after fanins are added { int * pFanins = Acb_ObjFanins( p, iObj ); @@ -438,6 +459,23 @@ static inline int Acb_ObjAlloc( Acb_Ntk_t * p, Acb_ObjType_t Type, int nFans, in assert( !Acb_ObjIsBox(p, iObj) || nFons > 0 ); for ( i = 0; i < nFons; i++ ) Acb_ObjAddFanin( p, Acb_ObjAlloc(p, ABC_OPER_FON, 1, 0), iObj ); + // extend storage + if ( Acb_NtkHasObjCopies(p) ) Vec_IntPush(&p->vObjCopy , -1); + if ( Acb_NtkHasObjFuncs(p) ) Vec_IntPush(&p->vObjFunc , -1); + if ( Acb_NtkHasObjWeights(p)) Vec_IntPush(&p->vObjWeight, 0); + if ( Acb_NtkHasObjTruths(p) ) Vec_WrdPush(&p->vObjTruth , 0); + if ( Acb_NtkHasObjNames(p) ) Vec_IntPush(&p->vObjName , 0); + if ( Acb_NtkHasObjRanges(p) ) Vec_IntPush(&p->vObjRange , 0); + if ( Acb_NtkHasObjTravs(p) ) Vec_IntPush(&p->vObjTrav , 0); + if ( Acb_NtkHasObjAttrs(p) ) Vec_IntPush(&p->vObjAttr , 0); + if ( Acb_NtkHasObjLevelD(p) ) Vec_IntPush(&p->vLevelD , 0); + if ( Acb_NtkHasObjLevelR(p) ) Vec_IntPush(&p->vLevelR , 0); + if ( Acb_NtkHasObjPathD(p) ) Vec_IntPush(&p->vPathD , 0); + if ( Acb_NtkHasObjPathR(p) ) Vec_IntPush(&p->vPathR , 0); + if ( Acb_NtkHasObjCounts(p) ) Vec_FltPush(&p->vCounts , 0); + if ( Acb_NtkHasObjFanout(p) ) Vec_WecPushLevel(&p->vFanouts); + if ( Acb_NtkHasObjCnfs(p) ) Vec_WecPushLevel(&p->vCnfs); + if ( p->vQue ) Vec_QueSetPriority( p->vQue, Vec_FltArrayP(&p->vCounts) ); return iObj; } static inline int Acb_ObjDup( Acb_Ntk_t * pNew, Acb_Ntk_t * p, int i ) @@ -455,6 +493,25 @@ static inline void Acb_ObjDelete( Acb_Ntk_t * p, int iObj ) Acb_ObjForEachFon( p, iObj, i ) Acb_ObjCleanType( p, i ); } +static inline void Acb_ObjAddFaninFanout( Acb_Ntk_t * p, int iObj ) +{ + int k, iFanin, * pFanins; + Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) + Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj ); +} +static inline void Acb_ObjRemoveFaninFanout( Acb_Ntk_t * p, int iObj ) +{ + int k, iFanin, * pFanins; + Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) + Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj ); +} +static inline void Acb_NtkCreateFanout( Acb_Ntk_t * p ) +{ + int iObj; + Acb_NtkCleanObjFanout( p ); + Acb_NtkForEachObj( p, iObj ) + Acb_ObjAddFaninFanout( p, iObj ); +} /**Function************************************************************* @@ -492,7 +549,6 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p ) Vec_StrErase( &p->vObjType ); Vec_IntErase( &p->vObjFans ); Vec_IntErase( &p->vFanSto ); - Vec_WecErase( &p->vFanouts ); // optional Vec_IntErase( &p->vObjCopy ); Vec_IntErase( &p->vObjFunc ); @@ -510,7 +566,12 @@ static inline void Acb_NtkFree( Acb_Ntk_t * p ) Vec_IntErase( &p->vLevelR ); Vec_IntErase( &p->vPathD ); Vec_IntErase( &p->vPathR ); + Vec_FltErase( &p->vCounts ); + Vec_WecErase( &p->vFanouts ); + Vec_WecErase( &p->vCnfs ); // other + Vec_QueFreeP( &p->vQue ); + Vec_IntErase( &p->vCover ); Vec_IntErase( &p->vArray0 ); Vec_IntErase( &p->vArray1 ); Vec_IntErase( &p->vArray2 ); @@ -572,42 +633,6 @@ static inline Vec_Int_t * Acb_NtkCollect( Acb_Ntk_t * p ) Vec_IntPush( vObjs, iObj ); return vObjs; } -static inline int Acb_NtkIsSeq( Acb_Ntk_t * p ) -{ - int iObj; - if ( p->fSeq ) - return 1; - if ( p->fComb ) - return 0; - assert( !p->fSeq && !p->fComb ); - Acb_NtkForEachBox( p, iObj ) - if ( Acb_ObjIsBox(p, iObj) ) - { - if ( Acb_NtkIsSeq( Acb_ObjNtk(p, iObj) ) ) - { - p->fSeq = 1; - return 1; - } - } - else if ( Acb_ObjIsSeq(p, iObj) ) - { - p->fSeq = 1; - return 1; - } - p->fComb = 1; - return 0; -} -static inline void Acb_NtkPrepareSeq( Acb_Ntk_t * p ) -{ - int iObj; - assert( Acb_NtkSeqNum(p) == 0 ); - if ( !Acb_NtkIsSeq(p) ) - return; - Acb_NtkForEachBox( p, iObj ) - if ( Acb_ObjIsSeq(p, iObj) ) - Vec_IntPush( &p->vSeq, iObj ); - // Acb_NtkObjOrder( p, &p->vSeq, NULL ); -} static inline Acb_Ntk_t * Acb_NtkDup( Acb_Man_t * pMan, Acb_Ntk_t * p, Vec_Int_t * vObjs ) { Acb_Ntk_t * pNew; @@ -684,6 +709,7 @@ static inline int Acb_NtkMemory( Acb_Ntk_t * p ) nMem += (int)Vec_IntMemory(&p->vNtkObjs ); nMem += (int)Vec_IntMemory(&p->vTargets ); // other + nMem += (int)Vec_IntMemory(&p->vCover ); nMem += (int)Vec_IntMemory(&p->vArray0 ); nMem += (int)Vec_IntMemory(&p->vArray1 ); nMem += (int)Vec_IntMemory(&p->vArray2 ); @@ -774,12 +800,6 @@ static inline Acb_Man_t * Acb_ManDup( Acb_Man_t * p, Vec_Int_t*(* pFuncOrder)(Ac pNew->iRoot = Acb_ManNtkNum(pNew); return pNew; } -static inline void Acb_ManPrepareSeq( Acb_Man_t * p ) -{ - Acb_Ntk_t * pNtk; int i; - Acb_ManForEachNtk( p, pNtk, i ) - Acb_NtkPrepareSeq( pNtk ); -} static inline void Acb_ManFree( Acb_Man_t * p ) { Acb_Ntk_t * pNtk; int i; @@ -939,8 +959,16 @@ static inline void Acb_ManPrintStats( Acb_Man_t * p, int nModules, int fVerbose /*=== acbUtil.c =============================================================*/ -extern void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj ); -extern void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp ); +extern Vec_Int_t * Acb_ObjCollectTfi( Acb_Ntk_t * p, int iObj, int fTerm ); +extern Vec_Int_t * Acb_ObjCollectTfo( Acb_Ntk_t * p, int iObj, int fTerm ); + +extern int Acb_ObjComputeLevelD( Acb_Ntk_t * p, int iObj ); +extern int Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo ); +extern void Acb_NtkUpdateLevelD( Acb_Ntk_t * p, int iObj ); +extern void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj ); + +extern void Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp ); +extern void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp ); ABC_NAMESPACE_HEADER_END diff --git a/src/base/acb/acbAbc.c b/src/base/acb/acbAbc.c index 169532e5..9be3bdab 100644 --- a/src/base/acb/acbAbc.c +++ b/src/base/acb/acbAbc.c @@ -46,15 +46,25 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p ) { + int fTrack = 1; Acb_Man_t * pMan = Acb_ManAlloc( Abc_NtkSpec(p), 1, NULL, NULL, NULL, NULL ); int i, k, NameId = Abc_NamStrFindOrAdd( pMan->pStrs, Abc_NtkName(p), NULL ); Acb_Ntk_t * pNtk = Acb_NtkAlloc( pMan, NameId, Abc_NtkCiNum(p), Abc_NtkCoNum(p), Abc_NtkObjNum(p) ); Abc_Obj_t * pObj, * pFanin; assert( Abc_NtkIsSopLogic(p) ); + pNtk->nFaninMax = 6; + if ( fTrack ) Vec_IntFill( &pNtk->vArray2, Abc_NtkObjNumMax(p), -1 ); Abc_NtkForEachCi( p, pObj, i ) + { pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 ); + if ( fTrack ) Vec_IntWriteEntry( &pNtk->vArray2, pObj->iTemp, Abc_ObjId(pObj) ); + } Abc_NtkForEachNode( p, pObj, i ) + { pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_LUT, Abc_ObjFaninNum(pObj), 0 ); + if ( fTrack ) Vec_IntWriteEntry( &pNtk->vArray2, pObj->iTemp, Abc_ObjId(pObj) ); +// printf( "%d -> %d\n%s", i, pObj->iTemp, (char *)pObj->pData ); + } Abc_NtkForEachCo( p, pObj, i ) pObj->iTemp = Acb_ObjAlloc( pNtk, ABC_OPER_CO, 1, 0 ); Abc_NtkForEachNode( p, pObj, i ) @@ -199,8 +209,8 @@ void Acb_ParSetDefault( Acb_Par_t * pPars ) { memset( pPars, 0, sizeof(Acb_Par_t) ); pPars->nLutSize = 4; // LUT size - pPars->nTfoLevMax = 3; // the maximum fanout levels - pPars->nTfiLevMax = 3; // the maximum fanin levels + pPars->nTfoLevMax = 1; // the maximum fanout levels + pPars->nTfiLevMax = 2; // the maximum fanin levels pPars->nFanoutMax = 10; // the maximum number of fanouts pPars->nDivMax = 16; // the maximum divisor count pPars->nTabooMax = 4; // the minimum MFFC size @@ -208,7 +218,7 @@ void Acb_ParSetDefault( Acb_Par_t * pPars ) pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run pPars->nNodesMax = 0; // the maximum number of nodes to try pPars->iNodeOne = 0; // one particular node to try - pPars->fArea = 0; // performs optimization for area + pPars->fArea = 1; // performs optimization for area pPars->fMoreEffort = 0; // enables using more effort pPars->fVerbose = 0; // enable basic stats pPars->fVeryVerbose = 0; // enable detailed stats @@ -230,7 +240,7 @@ Abc_Ntk_t * Abc_NtkOptMfse( Abc_Ntk_t * pNtk, Acb_Par_t * pPars ) extern void Acb_NtkOpt( Acb_Ntk_t * p, Acb_Par_t * pPars ); Abc_Ntk_t * pNtkNew; Acb_Ntk_t * p = Acb_NtkFromAbc( pNtk ); - //Acb_NtkOpt( p, pPars ); + Acb_NtkOpt( p, pPars ); pNtkNew = Acb_NtkToAbc( pNtk, p ); Acb_ManFree( p->pDesign ); return pNtkNew; diff --git a/src/base/acb/acbMfs.c b/src/base/acb/acbMfs.c index 7b86a686..a536a08b 100644 --- a/src/base/acb/acbMfs.c +++ b/src/base/acb/acbMfs.c @@ -94,7 +94,8 @@ Vec_Wec_t * Acb_DeriveCnfForWindow( Acb_Ntk_t * p, Vec_Int_t * vWin, int PivotVa { if ( Abc_LitIsCompl(iObj) && i < PivotVar ) continue; - vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, iObj ); + iObj = Abc_Lit2Var(iObj); + vCnfBase = Acb_ObjCnfs( p, iObj ); if ( Vec_StrSize(vCnfBase) > 0 ) continue; if ( vCnf == NULL ) @@ -163,7 +164,10 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) Vec_Int_t * vLits = Vec_IntAlloc( 1000 ); // mark new SAT variables Vec_IntForEachEntry( vWinObjs, iObj, i ) - Acb_ObjSetCopy( p, i, iObj ); + { + Acb_ObjSetFunc( p, Abc_Lit2Var(iObj), i ); +//printf( "Node %d -> SAT var %d\n", Vec_IntEntry(&p->vArray2, Abc_Lit2Var(iObj)), i ); + } // add clauses for all nodes Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntForEachEntry( vWinObjs, iObjLit, i ) @@ -175,8 +179,8 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) // collect SAT variables Vec_IntClear( vFaninVars ); Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) - Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iFanin) ); - Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) ); + Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iFanin) ); + Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iObj) ); // derive CNF for the node Acb_TranslateCnf( vClas, vLits, (Vec_Str_t *)Vec_WecEntry(vCnfs, iObj), vFaninVars, -1 ); } @@ -188,8 +192,8 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) // collect SAT variables Vec_IntClear( vFaninVars ); Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) - Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iFanin) + (iFanin > PivotVar) * nTfoSize ); - Vec_IntPush( vFaninVars, Acb_ObjCopy(p, iObj) + nTfoSize ); + Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iFanin) + (Acb_ObjFunc(p, iFanin) > PivotVar) * nTfoSize ); + Vec_IntPush( vFaninVars, Acb_ObjFunc(p, iObj) + nTfoSize ); // derive CNF for the node Acb_TranslateCnf( vClas, vLits, (Vec_Str_t *)Vec_WecEntry(vCnfs, iObj), vFaninVars, PivotVar ); } @@ -204,13 +208,13 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) continue; iObj = Abc_Lit2Var(iObjLit); // add clauses - Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 0), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 0) ); + Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 1), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 0) ); Vec_IntPush( vClas, Vec_IntSize(vLits) ); - Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 1), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 0) ); + Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 0), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 0) ); Vec_IntPush( vClas, Vec_IntSize(vLits) ); - Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 0), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 1) ); + Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 0), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 1) ); Vec_IntPush( vClas, Vec_IntSize(vLits) ); - Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjCopy(p, iObj), 1), Abc_Var2Lit(Acb_ObjCopy(p, iObj) + nTfoSize, 0), Abc_Var2Lit(nVars, 1) ); + Vec_IntPushThree( vLits, Abc_Var2Lit(Acb_ObjFunc(p, iObj), 1), Abc_Var2Lit(Acb_ObjFunc(p, iObj) + nTfoSize, 1), Abc_Var2Lit(nVars, 1) ); Vec_IntPush( vClas, Vec_IntSize(vLits) ); Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars++, 0) ); } @@ -222,7 +226,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) Vec_IntFree( vFaninVars ); // undo SAT variables Vec_IntForEachEntry( vWinObjs, iObj, i ) - Vec_IntWriteEntry( &p->vObjCopy, iObj, -1 ); + Vec_IntWriteEntry( &p->vObjFunc, Abc_Lit2Var(iObj), -1 ); // create CNF structure pCnf = ABC_CALLOC( Cnf_Dat_t, 1 ); pCnf->nVars = nVarsAll; @@ -235,6 +239,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) // cleanup Vec_IntFree( vClas ); Vec_IntFree( vLits ); + //Cnf_DataPrint( pCnf, 1 ); return pCnf; } @@ -252,7 +257,7 @@ Cnf_Dat_t * Acb_NtkWindow2Cnf( Acb_Ntk_t * p, Vec_Int_t * vWinObjs, int Pivot ) ***********************************************************************/ sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, int nTimes ) { - int n, i, RetValue, nRounds = nTimes <= 2 ? nTimes-1 : nTimes; + int n, i, RetValue, nRounds = nTimes <= 2 ? nTimes-1 : 2; Vec_Int_t * vFlips = Cnf_DataCollectFlipLits( pCnf, PivotVar ); sat_solver * pSat = sat_solver_new(); sat_solver_setnvars( pSat, nTimes * pCnf->nVars + nRounds * nDivs + 1 ); @@ -283,7 +288,7 @@ sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, in { int BaseA = n * pCnf->nVars; int BaseB = ((n + 1) % nTimes) * pCnf->nVars; - int BaseC = nTimes * pCnf->nVars + n * nDivs; + int BaseC = nTimes * pCnf->nVars + (n & 1) * nDivs; for ( i = 0; i < nDivs; i++ ) sat_solver_add_buffer_enable( pSat, BaseA + i, BaseB + i, BaseC + i, 0 ); } @@ -298,6 +303,92 @@ sat_solver * Acb_NtkWindow2Solver( Cnf_Dat_t * pCnf, int PivotVar, int nDivs, in } + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkPrintVec( Acb_Ntk_t * p, Vec_Int_t * vVec, char * pName ) +{ + int i; + printf( "%s: ", pName ); + for ( i = 0; i < vVec->nSize; i++ ) + printf( "%d ", Vec_IntEntry(&p->vArray2, vVec->pArray[i]) ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Collects divisors in a non-topo order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax ) +{ + Vec_Int_t * vDivs = Vec_IntAlloc( 100 ); + Vec_Int_t * vFront = Vec_IntAlloc( 100 ); + int i, k, iFanin, * pFanins; + // mark taboo nodes + Acb_NtkIncTravId( p ); + assert( !Acb_ObjIsCio(p, Pivot) ); + Acb_ObjSetTravIdCur( p, Pivot ); + for ( i = 0; i < nTaboo; i++ ) + { + assert( !Acb_ObjIsCio(p, pTaboo[i]) ); + if ( Acb_ObjSetTravIdCur( p, pTaboo[i] ) ) + assert( 0 ); + } + // collect non-taboo fanins of pivot but do not use them as frontier + Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k ) + if ( !Acb_ObjSetTravIdCur( p, iFanin ) ) + Vec_IntPush( vDivs, iFanin ); + // collect non-taboo fanins of taboo nodes and use them as frontier + for ( i = 0; i < nTaboo; i++ ) + Acb_ObjForEachFaninFast( p, pTaboo[i], pFanins, iFanin, k ) + if ( !Acb_ObjSetTravIdCur( p, iFanin ) ) + { + Vec_IntPush( vDivs, iFanin ); + if ( !Acb_ObjIsCio(p, iFanin) ) + Vec_IntPush( vFront, iFanin ); + } + // select divisors incrementally + while ( Vec_IntSize(vFront) > 0 && Vec_IntSize(vDivs) < nDivsMax ) + { + // select the topmost + int iObj, iObjMax = -1, LevelMax = -1; + Vec_IntForEachEntry( vFront, iObj, k ) + if ( LevelMax < Acb_ObjLevelD(p, iObj) ) + LevelMax = Acb_ObjLevelD(p, (iObjMax = iObj)); + assert( iObjMax > 0 ); + Vec_IntRemove( vFront, iObjMax ); + // expand the topmost + Acb_ObjForEachFaninFast( p, iObjMax, pFanins, iFanin, k ) + if ( !Acb_ObjSetTravIdCur( p, iFanin ) ) + { + Vec_IntPush( vDivs, iFanin ); + if ( !Acb_ObjIsCio(p, iFanin) ) + Vec_IntPush( vFront, iFanin ); + } + } + Vec_IntFree( vFront ); + // sort them by level + Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vLevelD ); + return vDivs; +} + /**Function************************************************************* Synopsis [Marks TFO of divisors.] @@ -314,7 +405,8 @@ void Acb_ObjMarkTfo_rec( Acb_Ntk_t * p, int iObj, int Pivot, int nTfoLevMax, int int iFanout, i; if ( Acb_ObjSetTravIdCur(p, iObj) ) return; - if ( Acb_ObjLevelD(p, iObj) > nTfoLevMax || Acb_ObjFanoutNum(p, iObj) >= nFanMax || iObj == Pivot ) +//printf( "Labeling %d.\n", Vec_IntEntry(&p->vArray2, iObj) ); + if ( Acb_ObjLevelD(p, iObj) > nTfoLevMax || Acb_ObjFanoutNum(p, iObj) > nFanMax || iObj == Pivot ) return; Acb_ObjForEachFanout( p, iObj, iFanout, i ) Acb_ObjMarkTfo_rec( p, iFanout, Pivot, nTfoLevMax, nFanMax ); @@ -323,6 +415,7 @@ void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax { int i, iObj; Acb_NtkIncTravId( p ); + Acb_ObjSetTravIdCur( p, Pivot ); Vec_IntForEachEntry( vDivs, iObj, i ) Acb_ObjMarkTfo_rec( p, iObj, Pivot, nTfoLevMax, nFanMax ); } @@ -341,6 +434,7 @@ void Acb_ObjMarkTfo( Acb_Ntk_t * p, Vec_Int_t * vDivs, int Pivot, int nTfoLevMax int Acb_ObjLabelTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax ) { int iFanout, i, Diff, fHasNone = 0; +//printf( "Visiting %d\n", Vec_IntEntry(&p->vArray2, iObj) ); if ( (Diff = Acb_ObjTravIdDiff(p, iObj)) <= 2 ) return Diff; Acb_ObjSetTravIdDiff( p, iObj, 2 ); @@ -348,15 +442,15 @@ int Acb_ObjLabelTfo_rec( Acb_Ntk_t * p, int iObj, int nTfoLevMax, int nFanMax ) return 2; if ( Acb_ObjLevelD(p, iObj) == nTfoLevMax || Acb_ObjFanoutNum(p, iObj) >= nFanMax ) { - if ( Diff == 3 ) - Acb_ObjSetTravIdDiff( p, iObj, 1 ); // mark root + if ( Diff == 3 ) // belongs to TFO of TFI + Acb_ObjSetTravIdDiff( p, iObj, 1 ); // root return Acb_ObjTravIdDiff(p, iObj); } Acb_ObjForEachFanout( p, iObj, iFanout, i ) fHasNone |= 2 == Acb_ObjLabelTfo_rec( p, iFanout, nTfoLevMax, nFanMax ); - if ( fHasNone && Diff == 3 ) + if ( fHasNone && Diff == 3 ) // belongs to TFO of TFI Acb_ObjSetTravIdDiff( p, iObj, 1 ); // root - else + else if ( !fHasNone ) Acb_ObjSetTravIdDiff( p, iObj, 0 ); // inner return Acb_ObjTravIdDiff(p, iObj); } @@ -365,7 +459,7 @@ int Acb_ObjLabelTfo( Acb_Ntk_t * p, int Root, int nTfoLevMax, int nFanMax ) Acb_NtkIncTravId( p ); // none (2) marked (3) unmarked (4) Acb_NtkIncTravId( p ); // root (1) Acb_NtkIncTravId( p ); // inner (0) - assert( Acb_ObjTravIdDiff(p, Root) < 3 ); + assert( Acb_ObjTravIdDiff(p, Root) > 2 ); return Acb_ObjLabelTfo_rec( p, Root, nTfoLevMax, nFanMax ); } @@ -387,19 +481,20 @@ void Acb_ObjDeriveTfo_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfo, Vec_Int_t return; if ( Diff == 2 ) // root { - Vec_IntPush( vRoots, Diff ); + Vec_IntPush( vRoots, iObj ); + Vec_IntPush( vTfo, iObj ); return; } assert( Diff == 1 ); Acb_ObjForEachFanout( p, iObj, iFanout, i ) Acb_ObjDeriveTfo_rec( p, iFanout, vTfo, vRoots ); - Vec_IntPush( vTfo, Diff ); + Vec_IntPush( vTfo, iObj ); } void Acb_ObjDeriveTfo( Acb_Ntk_t * p, int Pivot, int nTfoLevMax, int nFanMax, Vec_Int_t ** pvTfo, Vec_Int_t ** pvRoots ) { int Res = Acb_ObjLabelTfo( p, Pivot, nTfoLevMax, nFanMax ); - Vec_Int_t * vTfo = *pvTfo = Vec_IntAlloc( 100 ); - Vec_Int_t * vRoots = *pvRoots = Vec_IntAlloc( 100 ); + Vec_Int_t * vTfo = *pvTfo = Vec_IntAlloc( 10 ); + Vec_Int_t * vRoots = *pvRoots = Vec_IntAlloc( 10 ); if ( Res ) // none or root return; Acb_NtkIncTravId( p ); // root (2) inner (1) visited (0) @@ -472,15 +567,18 @@ void Acb_NtkCollectNewTfi2_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vTfiNew ) Acb_NtkCollectNewTfi2_rec( p, iFanin, vTfiNew ); Vec_IntPush( vTfiNew, iObj ); } -Vec_Int_t * Acb_NtkCollectNewTfi( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vDivs, Vec_Int_t * vSide ) +Vec_Int_t * Acb_NtkCollectNewTfi( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vDivs, Vec_Int_t * vSide, int * pnDivs ) { Vec_Int_t * vTfiNew = Vec_IntAlloc( 100 ); int i, Node; Acb_NtkIncTravId( p ); +//Acb_NtkPrintVec( p, vDivs, "vDivs" ); Vec_IntForEachEntry( vDivs, Node, i ) Acb_NtkCollectNewTfi1_rec( p, Node, vTfiNew ); - assert( Vec_IntSize(vTfiNew) == Vec_IntSize(vDivs) ); + *pnDivs = Vec_IntSize(vTfiNew); +//Acb_NtkPrintVec( p, vTfiNew, "vTfiNew" ); Acb_NtkCollectNewTfi1_rec( p, Pivot, vTfiNew ); +//Acb_NtkPrintVec( p, vTfiNew, "vTfiNew" ); assert( Vec_IntEntryLast(vTfiNew) == Pivot ); Vec_IntPop( vTfiNew ); Vec_IntForEachEntry( vSide, Node, i ) @@ -505,95 +603,32 @@ Vec_Int_t * Acb_NtkCollectWindow( Acb_Ntk_t * p, int Pivot, Vec_Int_t * vTfi, Ve Vec_Int_t * vWin = Vec_IntAlloc( 100 ); int i, k, iObj, iFanin, * pFanins; assert( Vec_IntEntryLast(vTfi) == Pivot ); - // mark leaves + // mark nodes Acb_NtkIncTravId( p ); Vec_IntForEachEntry( vTfi, iObj, i ) Acb_ObjSetTravIdCur(p, iObj); - Acb_NtkIncTravId( p ); - Vec_IntForEachEntry( vTfi, iObj, i ) - if ( !Acb_ObjIsCi(p, iObj) ) - Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) - if ( !Acb_ObjIsTravIdCur(p, iFanin) ) - Acb_ObjSetTravIdCur(p, iObj); // add TFI Vec_IntForEachEntry( vTfi, iObj, i ) - Vec_IntPush( vWin, Abc_Var2Lit( iObj, Acb_ObjIsTravIdCur(p, iObj)) ); + { + int fIsTfiInput = 0; + Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) + if ( !Acb_ObjIsTravIdCur(p, iFanin) ) // fanin is not in TFI + fIsTfiInput = 1; // mark as leaf + Vec_IntPush( vWin, Abc_Var2Lit(iObj, Acb_ObjIsCi(p, iObj) || fIsTfiInput) ); + } // mark roots + Acb_NtkIncTravId( p ); Vec_IntForEachEntry( vRoots, iObj, i ) Acb_ObjSetTravIdCur(p, iObj); // add TFO Vec_IntForEachEntry( vTfo, iObj, i ) - Vec_IntPush( vWin, Abc_Var2Lit( iObj, Acb_ObjIsTravIdCur(p, iObj)) ); - return vWin; -} - - - -/**Function************************************************************* - - Synopsis [Collects divisors in a non-topo order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax ) -{ - Vec_Int_t * vDivs = Vec_IntAlloc( 100 ); - Vec_Int_t * vFront = Vec_IntAlloc( 100 ); - int i, k, iFanin, * pFanins; - // mark taboo nodes - Acb_NtkIncTravId( p ); - assert( !Acb_ObjIsCio(p, Pivot) ); - Acb_ObjSetTravIdCur( p, Pivot ); - for ( i = 0; i < nTaboo; i++ ) { - assert( !Acb_ObjIsCio(p, pTaboo[i]) ); - if ( Acb_ObjSetTravIdCur( p, pTaboo[i] ) ) - assert( 0 ); + assert( !Acb_ObjIsCo(p, iObj) ); + Vec_IntPush( vWin, Abc_Var2Lit(iObj, Acb_ObjIsTravIdCur(p, iObj)) ); } - // collect non-taboo fanins of pivot but do not use them as frontier - Acb_ObjForEachFaninFast( p, Pivot, pFanins, iFanin, k ) - if ( !Acb_ObjSetTravIdCur( p, iFanin ) ) - Vec_IntPush( vDivs, iFanin ); - // collect non-tabook fanins of taboo nodes and use them as frontier - for ( i = 0; i < nTaboo; i++ ) - Acb_ObjForEachFaninFast( p, pTaboo[i], pFanins, iFanin, k ) - if ( !Acb_ObjSetTravIdCur( p, iFanin ) ) - { - Vec_IntPush( vDivs, iFanin ); - if ( !Acb_ObjIsCio(p, iFanin) ) - Vec_IntPush( vFront, iFanin ); - } - // select divisors incrementally - while ( Vec_IntSize(vFront) > 0 && Vec_IntSize(vDivs) < nDivsMax ) - { - // select the topmost - int iObj, iObjMax = -1, LevelMax = -1; - Vec_IntForEachEntry( vFront, iObj, k ) - if ( LevelMax < Acb_ObjLevelD(p, iObj) ) - LevelMax = Acb_ObjLevelD(p, (iObjMax = iObj)); - assert( iObjMax > 0 ); - Vec_IntRemove( vFront, iObjMax ); - // expand the topmost - Acb_ObjForEachFaninFast( p, iObjMax, pFanins, iFanin, k ) - if ( !Acb_ObjSetTravIdCur( p, iFanin ) ) - { - Vec_IntPush( vDivs, iFanin ); - if ( !Acb_ObjIsCio(p, iFanin) ) - Vec_IntPush( vFront, iFanin ); - } - } - Vec_IntFree( vFront ); - // sort them by level - Vec_IntSelectSortCost( Vec_IntArray(vDivs), Vec_IntSize(vDivs), &p->vLevelD ); - return vDivs; + return vWin; } - /**Function************************************************************* Synopsis [] @@ -607,20 +642,26 @@ Vec_Int_t * Acb_NtkDivisors( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, ***********************************************************************/ Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, int nDivsMax, int nTfoLevs, int nFanMax, int * pnDivs ) { + int fVerbose = 0; int nTfoLevMax = Acb_ObjLevelD(p, Pivot) + nTfoLevs; Vec_Int_t * vWin, * vDivs, * vTfo, * vRoots, * vSide, * vTfi; // collect divisors by traversing limited TFI vDivs = Acb_NtkDivisors( p, Pivot, pTaboo, nTaboo, nDivsMax ); + if ( fVerbose ) Acb_NtkPrintVec( p, vDivs, "vDivs" ); // mark limited TFO of the divisors Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax ); // collect TFO and roots Acb_ObjDeriveTfo( p, Pivot, nTfoLevMax, nFanMax, &vTfo, &vRoots ); + if ( fVerbose ) Acb_NtkPrintVec( p, vTfo, "vTfo" ); + if ( fVerbose ) Acb_NtkPrintVec( p, vRoots, "vRoots" ); // collect side inputs of the TFO vSide = Acb_NtkCollectTfoSideInputs( p, Pivot, vTfo ); + if ( fVerbose ) Acb_NtkPrintVec( p, vSide, "vSide" ); // mark limited TFO of the divisors Acb_ObjMarkTfo( p, vDivs, Pivot, nTfoLevMax, nFanMax ); // collect new TFI - vTfi = Acb_NtkCollectNewTfi( p, Pivot, vDivs, vSide ); + vTfi = Acb_NtkCollectNewTfi( p, Pivot, vDivs, vSide, pnDivs ); + if ( fVerbose ) Acb_NtkPrintVec( p, vTfi, "vTfi" ); Vec_IntFree( vSide ); Vec_IntFree( vDivs ); // collect all nodes @@ -636,34 +677,6 @@ Vec_Int_t * Acb_NtkWindow( Acb_Ntk_t * p, int Pivot, int * pTaboo, int nTaboo, i /**Function************************************************************* - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Acb_NtkFindSupp( sat_solver * pSat, Acb_Ntk_t * p, Vec_Int_t * vWin, Vec_Int_t * vDivs, int nBTLimit ) -{ - int i, iObj, nDivsNew; - // reload divisors in terms of SAT variables - Vec_IntForEachEntry( vDivs, iObj, i ) - Vec_IntWriteEntry( vDivs, i, Acb_ObjCopy(p, iObj) ); - // try solving - nDivsNew = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vDivs), Vec_IntSize(vDivs), nBTLimit ); - Vec_IntShrink( vDivs, nDivsNew ); - // reload divisors in terms of network variables - Vec_IntForEachEntry( vDivs, iObj, i ) - Vec_IntWriteEntry( vDivs, i, Vec_IntEntry(vWin, iObj) ); - return Vec_IntSize(vDivs); -} - - - -/**Function************************************************************* - Synopsis [Computes function of the node] Description [] @@ -704,7 +717,6 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_ // compute cube and add clause nFinal = sat_solver_final( pSat, &pFinal ); Vec_IntFill( vTempLits, 1, Abc_LitNot(pLits[1]) ); // NOT(iNewLit) - uCube = ~(word)0; for ( i = 0; i < nFinal; i++ ) if ( pFinal[i] != pLits[0] ) Vec_IntPush( vTempLits, pFinal[i] ); @@ -716,7 +728,8 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_ Vec_IntForEachEntry( vDivVars, iVar, i ) Vec_IntPush( vTempLits, Abc_LitNot(sat_solver_var_literal(pSat, iVar)) ); } - Vec_IntForEachEntry( vTempLits, iLit, i ) + uCube = ~(word)0; + Vec_IntForEachEntryStart( vTempLits, iLit, i, 1 ) { iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(iLit) ); assert( iVar >= 0 ); uCube &= Abc_LitIsCompl(iLit) ? s_Truths6[iVar] : ~s_Truths6[iVar]; @@ -736,7 +749,7 @@ word Acb_ComputeFunction( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_ /**Function************************************************************* - Synopsis [Collects the taboo nodes.] + Synopsis [Collects the taboo nodes (nodes that cannot be divisors).] Description [] @@ -820,6 +833,12 @@ int Acb_NtkCollectTaboo( Acb_Ntk_t * p, int Pivot, int nTabooMax, int * pTaboo ) SeeAlso [] ***********************************************************************/ +static inline void Vec_IntVars2Vars( Vec_Int_t * p, int Shift ) +{ + int i; + for ( i = 0; i < p->nSize; i++ ) + p->pArray[i] += Shift; +} static inline void Vec_IntVars2Lits( Vec_Int_t * p, int Shift, int fCompl ) { int i; @@ -830,7 +849,7 @@ static inline void Vec_IntLits2Vars( Vec_Int_t * p, int Shift ) { int i; for ( i = 0; i < p->nSize; i++ ) - p->pArray[i] = Abc_Lit2Var( p->pArray[i] ) - Shift; + p->pArray[i] = Abc_Lit2Var( p->pArray[i] ) + Shift; } static inline void Vec_IntRemap( Vec_Int_t * p, Vec_Int_t * vMap ) { @@ -839,21 +858,53 @@ static inline void Vec_IntRemap( Vec_Int_t * p, Vec_Int_t * vMap ) p->pArray[i] = Vec_IntEntry(vMap, p->pArray[i]); } -void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int nTfoLevs, int nFanMax, int nLutSize ) +void Acb_WinPrint( Acb_Ntk_t * p, Vec_Int_t * vWin, int Pivot, int nDivs ) +{ + int i, Node; + printf( "Window for node %d with %d divisors:\n", Vec_IntEntry(&p->vArray2, Pivot), nDivs ); + Vec_IntForEachEntry( vWin, Node, i ) + { + if ( i == nDivs ) + printf( " | " ); + if ( Abc_Lit2Var(Node) == Pivot ) + printf( "(%d) ", Vec_IntEntry(&p->vArray2, Pivot) ); + else + printf( "%s%d ", Abc_LitIsCompl(Node) ? "*":"", Vec_IntEntry(&p->vArray2, Abc_Lit2Var(Node)) ); + } + printf( "\n" ); +} + +Vec_Int_t * Acb_NtkFindSupp( Acb_Ntk_t * p, sat_solver * pSat2, int nVars, int nDivs ) +{ + int nSuppNew; + Vec_Int_t * vSupp = Vec_IntStartNatural( nDivs ); + Vec_IntReverseOrder( vSupp ); + Vec_IntVars2Lits( vSupp, 2*nVars, 0 ); + nSuppNew = sat_solver_minimize_assumptions( pSat2, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 ); + Vec_IntShrink( vSupp, nSuppNew ); + Vec_IntLits2Vars( vSupp, -2*nVars ); + return vSupp; +} + +void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int nTfoLevs, int nFanMax, int nLutSize, int fVerbose ) { Cnf_Dat_t * pCnf; Vec_Int_t * vWin, * vSupp = NULL; sat_solver * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL; - int c, nSuppNew, PivotVar, nDivs = 0; + int c, PivotVar, nDivs = 0; word uTruth; int pTaboo[16], nTaboo = Acb_NtkCollectTaboo( p, Pivot, nTabooMax, pTaboo ); if ( nTaboo == 0 ) return; assert( nTabooMax == 0 || nTaboo <= nTabooMax ); assert( nTaboo <= 16 ); - // compute divisor and window for these nodes + // compute divisors and window for this target node with these taboo nodes vWin = Acb_NtkWindow( p, Pivot, pTaboo, nTaboo, nDivMax, nTfoLevs, nFanMax, &nDivs ); - PivotVar = Vec_IntFind(vWin, Abc_Var2Lit(Pivot, 0)); + PivotVar = Vec_IntFind( vWin, Abc_Var2Lit(Pivot, 0) ); + if ( fVerbose ) + printf( "Node %d: Window contains %d objects and %d divisors. ", Vec_IntEntry(&p->vArray2, Pivot), Vec_IntSize(vWin), nDivs ); +// Acb_WinPrint( p, vWin, Pivot, nDivs ); +// return; // derive CNF and SAT solvers pCnf = Acb_NtkWindow2Cnf( p, vWin, Pivot ); @@ -865,66 +916,84 @@ void Acb_NtkOptNode( Acb_Ntk_t * p, int Pivot, int nTabooMax, int nDivMax, int n int status = sat_solver_solve( pSat1, &Lit, &Lit + 1, 0, 0, 0, 0 ); if ( status == l_False ) { + if ( fVerbose ) + printf( "Found constant %d.\n", c ); Acb_NtkUpdateNode( p, Pivot, c ? ~(word)0 : 0, NULL ); goto cleanup; } assert( status == l_True ); } + // check for one-node implementation pSat2 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 2 ); - //pSat6 = Acb_NtkWindow2Solver( pCnf, PivotVar, nDivs, 6 ); - - // try solving the original support - vSupp = Vec_IntStartNatural( nDivs ); - Vec_IntVars2Lits( vSupp, 2*pCnf->nVars, 0 ); - nSuppNew = sat_solver_minimize_assumptions( pSat2, Vec_IntArray(vSupp), Vec_IntSize(vSupp), 0 ); - Vec_IntShrink( vSupp, nSuppNew ); - Vec_IntLits2Vars( vSupp, -2*pCnf->nVars ); - - if ( nSuppNew <= nLutSize ) + vSupp = Acb_NtkFindSupp( p, pSat2, pCnf->nVars, nDivs ); + if ( Vec_IntSize(vSupp) <= nLutSize ) { - int FreeVar = sat_solver_nvars( pSat1 ) - 1; - word uTruth; - - Vec_IntVars2Lits( vSupp, pCnf->nVars, 0 ); - uTruth = Acb_ComputeFunction( pSat1, PivotVar, FreeVar, vSupp ); - Vec_IntLits2Vars( vSupp, -pCnf->nVars ); + if ( fVerbose ) + printf( "Found %d inputs: ", Vec_IntSize(vSupp) ); + uTruth = Acb_ComputeFunction( pSat1, PivotVar, sat_solver_nvars(pSat1)-1, vSupp ); + if ( fVerbose ) + Extra_PrintHex( stdout, (unsigned *)&uTruth, Vec_IntSize(vSupp) ); + if ( fVerbose ) + printf( "\n" ); // create support in terms of nodes Vec_IntRemap( vSupp, vWin ); Vec_IntLits2Vars( vSupp, 0 ); - Acb_NtkUpdateNode( p, Pivot, uTruth, vSupp ); - goto cleanup; } + if ( fVerbose ) + printf( "\n" ); - // cleanup cleanup: if ( pSat1 ) sat_solver_delete( pSat1 ); if ( pSat2 ) sat_solver_delete( pSat2 ); if ( pSat3 ) sat_solver_delete( pSat3 ); Cnf_DataFree( pCnf ); Vec_IntFree( vWin ); - Vec_IntFree( vSupp ); + Vec_IntFreeP( &vSupp ); } +/**Function************************************************************* + + Synopsis [] + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Acb_NtkOpt( Acb_Ntk_t * p, Acb_Par_t * pPars ) { - int iObj; + if ( pPars->fVerbose ) + printf( "Performing %s-oriented optimization with DivMax = %d. TfoLev = %d. LutSize = %d.\n", + pPars->fArea ? "area" : "delay", pPars->nDivMax, pPars->nTfoLevMax, pPars->nLutSize ); + Acb_NtkCreateFanout( p ); // fanout data structure + Acb_NtkCleanObjFuncs( p ); // SAT variables + Acb_NtkCleanObjCnfs( p ); // CNF representations if ( pPars->fArea ) { + int iObj; + Acb_NtkUpdateLevelD( p, -1 ); // compute forward logic level Acb_NtkForEachNode( p, iObj ) - Acb_NtkOptNode( p, iObj, pPars->nTabooMax, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize ); + { + //if ( iObj != 433 ) + // continue; + Acb_NtkOptNode( p, iObj, pPars->nTabooMax, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize, pPars->fVerbose ); + } } else { - Acb_NtkUpdateTiming( p, -1 ); - while ( 1 ) + Acb_NtkUpdateTiming( p, -1 ); // compute delay information + while ( Vec_QueTopPriority(p->vQue) > 0 ) { - int iObj = 0; - Acb_NtkOptNode( p, iObj, 0, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize ); + int iObj = Vec_QuePop(p->vQue); + //if ( iObj != 28 ) + // continue; + Acb_NtkOptNode( p, iObj, 0, pPars->nDivMax, pPars->nTfoLevMax, pPars->nFanoutMax, pPars->nLutSize, pPars->fVerbose ); } } } diff --git a/src/base/acb/acbUtil.c b/src/base/acb/acbUtil.c index ab9bf44c..cc8b9f11 100644 --- a/src/base/acb/acbUtil.c +++ b/src/base/acb/acbUtil.c @@ -33,38 +33,7 @@ ABC_NAMESPACE_IMPL_START /**Function************************************************************* - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Acb_ObjAddFanout( Acb_Ntk_t * p, int iObj ) -{ - int k, iFanin, * pFanins; - Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) - Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj ); -} -void Acb_ObjRemoveFanout( Acb_Ntk_t * p, int iObj ) -{ - int k, iFanin, * pFanins; - Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) - Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj ); -} -void Acb_NtkCreateFanout( Acb_Ntk_t * p ) -{ - int iObj; - Vec_WecInit( &p->vFanouts, Acb_NtkObjNumMax(p) ); - Acb_NtkForEachObj( p, iObj ) - Acb_ObjAddFanout( p, iObj ); -} - -/**Function************************************************************* - - Synopsis [] + Synopsis [Collecting TFI and TFO.] Description [] @@ -86,9 +55,14 @@ void Acb_ObjCollectTfi_rec( Acb_Ntk_t * p, int iObj, int fTerm ) } Vec_Int_t * Acb_ObjCollectTfi( Acb_Ntk_t * p, int iObj, int fTerm ) { + int i; Vec_IntClear( &p->vArray0 ); Acb_NtkIncTravId( p ); - Acb_ObjCollectTfi_rec( p, iObj, fTerm ); + if ( iObj > 0 ) + Acb_ObjCollectTfi_rec( p, iObj, fTerm ); + else + Acb_NtkForEachCo( p, iObj, i ) + Acb_ObjCollectTfi_rec( p, iObj, fTerm ); return &p->vArray0; } @@ -105,16 +79,20 @@ void Acb_ObjCollectTfo_rec( Acb_Ntk_t * p, int iObj, int fTerm ) } Vec_Int_t * Acb_ObjCollectTfo( Acb_Ntk_t * p, int iObj, int fTerm ) { + int i; Vec_IntClear( &p->vArray1 ); Acb_NtkIncTravId( p ); - Acb_ObjCollectTfo_rec( p, iObj, fTerm ); + if ( iObj > 0 ) + Acb_ObjCollectTfo_rec( p, iObj, fTerm ); + else + Acb_NtkForEachCi( p, iObj, i ) + Acb_ObjCollectTfo_rec( p, iObj, fTerm ); return &p->vArray1; } - /**Function************************************************************* - Synopsis [] + Synopsis [Computing and updating direct and reverse logic level.] Description [] @@ -132,19 +110,12 @@ int Acb_ObjComputeLevelD( Acb_Ntk_t * p, int iObj ) } int Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo ) { + // it is assumed that vTfo contains CO nodes and level of new nodes was already updated int i, iObj, Level = 0; - if ( vTfo == NULL ) - { + if ( !Acb_NtkHasObjLevelD( p ) ) Acb_NtkCleanObjLevelD( p ); - Acb_NtkForEachObj( p, iObj ) - Acb_ObjComputeLevelD( p, iObj ); - } - else - { - // it is assumed that vTfo contains CO nodes and level of new nodes was already updated - Vec_IntForEachEntry( vTfo, iObj, i ) - Acb_ObjComputeLevelD( p, iObj ); - } + Vec_IntForEachEntryReverse( vTfo, iObj, i ) + Acb_ObjComputeLevelD( p, iObj ); Acb_NtkForEachCo( p, iObj, i ) Level = Abc_MaxInt( Level, Acb_ObjLevelD(p, iObj) ); p->LevelMax = Level; @@ -160,28 +131,27 @@ int Acb_ObjComputeLevelR( Acb_Ntk_t * p, int iObj ) } int Acb_NtkComputeLevelR( Acb_Ntk_t * p, Vec_Int_t * vTfi ) { + // it is assumed that vTfi contains CI nodes int i, iObj, Level = 0; - if ( vTfi == NULL ) - { - Acb_NtkCleanObjLevelR( p ); - Acb_NtkForEachObjReverse( p, iObj ) - Acb_ObjComputeLevelR( p, iObj ); - } - else - { - // it is assumed that vTfi contains CI nodes - Vec_IntForEachEntryReverse( vTfi, iObj, i ) - Acb_ObjComputeLevelR( p, iObj ); - } + if ( !Acb_NtkHasObjLevelD( p ) ) + Acb_NtkCleanObjLevelD( p ); + Vec_IntForEachEntryReverse( vTfi, iObj, i ) + Acb_ObjComputeLevelR( p, iObj ); Acb_NtkForEachCi( p, iObj, i ) Level = Abc_MaxInt( Level, Acb_ObjLevelR(p, iObj) ); assert( p->LevelMax == Level ); return Level; } +void Acb_NtkUpdateLevelD( Acb_Ntk_t * p, int Pivot ) +{ + Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, Pivot, 1 ); + Acb_NtkComputeLevelD( p, vTfo ); +} + /**Function************************************************************* - Synopsis [] + Synopsis [Computing and updating direct and reverse path count.] Description [] @@ -192,9 +162,11 @@ int Acb_NtkComputeLevelR( Acb_Ntk_t * p, Vec_Int_t * vTfi ) ***********************************************************************/ int Acb_ObjSlack( Acb_Ntk_t * p, int iObj ) { - assert( !Acb_ObjIsCio(p, iObj) + p->LevelMax >= Acb_ObjLevelD(p, iObj) + Acb_ObjLevelR(p, iObj) ); - return !Acb_ObjIsCio(p, iObj) + p->LevelMax - Acb_ObjLevelD(p, iObj) - Acb_ObjLevelR(p, iObj); + int LevelSum = Acb_ObjLevelD(p, iObj) + Acb_ObjLevelR(p, iObj); + assert( !Acb_ObjIsCio(p, iObj) + p->LevelMax >= LevelSum ); + return !Acb_ObjIsCio(p, iObj) + p->LevelMax - LevelSum; } + int Acb_ObjComputePathD( Acb_Ntk_t * p, int iObj ) { int * pFanins, iFanin, k, Path = 0; @@ -207,26 +179,13 @@ int Acb_ObjComputePathD( Acb_Ntk_t * p, int iObj ) int Acb_NtkComputePathsD( Acb_Ntk_t * p, Vec_Int_t * vTfo ) { int i, iObj, Path = 0; - if ( vTfo == NULL ) - { - Acb_NtkCleanObjPathD( p ); - Acb_NtkForEachCi( p, iObj, i ) - if ( Acb_ObjLevelR(p, iObj) == p->LevelMax ) - Acb_ObjSetPathD( p, iObj, 1 ); - Acb_NtkForEachObj( p, iObj ) - if ( !Acb_ObjIsCi(p, iObj) && !Acb_ObjSlack(p, iObj) ) - Acb_ObjComputePathD( p, iObj ); - } - else - { - // it is assumed that vTfo contains CO nodes - assert( Acb_ObjSlack(p, Vec_IntEntry(vTfo, 0)) ); - Vec_IntForEachEntry( vTfo, iObj, i ) - if ( !Acb_ObjSlack(p, iObj) ) - Acb_ObjComputePathD( p, iObj ); - else - Acb_ObjSetPathD( p, iObj, 0 ); - } + // it is assumed that vTfo contains CO nodes + //assert( Acb_ObjSlack(p, Vec_IntEntry(vTfo, 0)) ); + Vec_IntForEachEntryReverse( vTfo, iObj, i ) + if ( !Acb_ObjSlack(p, iObj) ) + Acb_ObjComputePathD( p, iObj ); + else + Acb_ObjSetPathD( p, iObj, 0 ); Acb_NtkForEachCo( p, iObj, i ) Path += Acb_ObjPathD(p, iObj); p->nPaths = Path; @@ -245,55 +204,39 @@ int Acb_ObjComputePathR( Acb_Ntk_t * p, int iObj ) int Acb_NtkComputePathsR( Acb_Ntk_t * p, Vec_Int_t * vTfi ) { int i, iObj, Path = 0; - if ( vTfi == NULL ) - { - Acb_NtkCleanObjPathR( p ); - Acb_NtkForEachCo( p, iObj, i ) - if ( Acb_ObjLevelD(p, iObj) == p->LevelMax ) - Acb_ObjSetPathR( p, iObj, 1 ); - Acb_NtkForEachObjReverse( p, iObj ) - if ( !Acb_ObjIsCo(p, iObj) && !Acb_ObjSlack(p, iObj) ) - Acb_ObjComputePathR( p, iObj ); - } - else - { - // it is assumed that vTfi contains CI nodes - assert( Acb_ObjSlack(p, Vec_IntEntry(vTfi, 0)) ); - Vec_IntForEachEntryReverse( vTfi, iObj, i ) - if ( !Acb_ObjSlack(p, iObj) ) - Acb_ObjComputePathR( p, iObj ); - else - Acb_ObjSetPathR( p, iObj, 0 ); - } + // it is assumed that vTfi contains CI nodes + //assert( Acb_ObjSlack(p, Vec_IntEntry(vTfi, 0)) ); + Vec_IntForEachEntryReverse( vTfi, iObj, i ) + if ( !Acb_ObjSlack(p, iObj) ) + Acb_ObjComputePathR( p, iObj ); + else + Acb_ObjSetPathR( p, iObj, 0 ); Acb_NtkForEachCi( p, iObj, i ) Path += Acb_ObjPathR(p, iObj); assert( p->nPaths == Path ); return Path; } - int Acb_NtkComputePaths( Acb_Ntk_t * p ) { - Acb_NtkComputeLevelD( p, NULL ); - Acb_NtkComputeLevelR( p, NULL ); - Acb_NtkComputePathsD( p, NULL ); - Acb_NtkComputePathsR( p, NULL ); + Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, -1, 1 ); + Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, -1, 1 ); + Acb_NtkComputeLevelD( p, vTfi ); + Acb_NtkComputeLevelR( p, vTfo ); + Acb_NtkComputePathsD( p, vTfi ); + Acb_NtkComputePathsR( p, vTfo ); return p->nPaths; } - void Abc_NtkComputePaths( Abc_Ntk_t * p ) { extern Acb_Ntk_t * Acb_NtkFromAbc( Abc_Ntk_t * p ); Acb_Ntk_t * pNtk = Acb_NtkFromAbc( p ); - Acb_NtkCreateFanout( pNtk ); printf( "Computed %d paths.\n", Acb_NtkComputePaths(pNtk) ); - Acb_ManFree( pNtk->pDesign ); } - /**Function************************************************************* Synopsis [] @@ -305,42 +248,47 @@ void Abc_NtkComputePaths( Abc_Ntk_t * p ) SeeAlso [] ***********************************************************************/ -int Acb_ObjPath( Acb_Ntk_t * p, int iObj ) -{ - return Acb_ObjPathD(p, iObj) + Acb_ObjPathR(p, iObj); -} -void Acb_ObjUpdateTiming( Acb_Ntk_t * p, int iObj ) -{ -} -void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj ) +void Acb_ObjUpdatePriority( Acb_Ntk_t * p, int iObj ) { - int i, Entry; - if ( iObj > 0 ) + int nPaths; + if ( p->vQue == NULL ) { - // assuming that level of the new nodes is up to date - Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, iObj, 1 ); - Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, iObj, 1 ); - Acb_NtkComputeLevelD( p, vTfo ); - Acb_NtkComputeLevelR( p, vTfi ); - Acb_NtkComputePathsD( p, vTfo ); - Acb_NtkComputePathsR( p, vTfi ); - Vec_IntForEachEntry( vTfi, Entry, i ) - Acb_ObjUpdateTiming( p, Entry ); - Vec_IntForEachEntry( vTfo, Entry, i ) - Acb_ObjUpdateTiming( p, Entry ); + Acb_NtkCleanObjCounts( p ); + p->vQue = Vec_QueAlloc( 1000 ); + Vec_QueSetPriority( p->vQue, Vec_FltArrayP(&p->vCounts) ); } + nPaths = Acb_ObjPathD(p, iObj) + Acb_ObjPathR(p, iObj); + if ( nPaths == 0 ) + return; + Acb_ObjSetCounts( p, iObj, (float)nPaths ); + if ( Vec_QueIsMember( p->vQue, iObj ) ) + Vec_QueUpdate( p->vQue, iObj ); else + Vec_QuePush( p->vQue, iObj ); +} +void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj ) +{ + int i, Entry, LevelMax = p->LevelMax; + // assuming that level of the new nodes is up to date + Vec_Int_t * vTfi = Acb_ObjCollectTfi( p, iObj, 1 ); + Vec_Int_t * vTfo = Acb_ObjCollectTfo( p, iObj, 1 ); + Acb_NtkComputeLevelD( p, vTfo ); + Acb_NtkComputeLevelR( p, vTfi ); + if ( iObj > 0 && LevelMax > p->LevelMax ) // reduced level { - Acb_NtkComputeLevelD( p, NULL ); - Acb_NtkComputeLevelR( p, NULL ); - Acb_NtkComputePathsD( p, NULL ); - Acb_NtkComputePathsR( p, NULL ); - Acb_NtkForEachNode( p, Entry ) - Acb_ObjUpdateTiming( p, Entry ); + vTfi = Acb_ObjCollectTfi( p, -1, 1 ); + vTfo = Acb_ObjCollectTfo( p, -1, 1 ); + Vec_QueClear( p->vQue ); + // add backup here } + Acb_NtkComputePathsD( p, vTfo ); + Acb_NtkComputePathsR( p, vTfi ); + Vec_IntForEachEntry( vTfi, Entry, i ) + Acb_ObjUpdatePriority( p, Entry ); + Vec_IntForEachEntry( vTfo, Entry, i ) + Acb_ObjUpdatePriority( p, Entry ); } - /**Function************************************************************* Synopsis [] @@ -352,20 +300,28 @@ void Acb_NtkUpdateTiming( Acb_Ntk_t * p, int iObj ) SeeAlso [] ***********************************************************************/ +void Acb_NtkCreateNode( Acb_Ntk_t * p, word uTruth, Vec_Int_t * vSupp ) +{ + int Pivot = Acb_ObjAlloc( p, ABC_OPER_LUT, Vec_IntSize(vSupp), 0 ); + Acb_ObjSetTruth( p, Pivot, uTruth ); + Acb_ObjAddFanins( p, Pivot, vSupp ); + Acb_ObjAddFaninFanout( p, Pivot ); + Acb_ObjComputeLevelD( p, Pivot ); +} void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp ) { - int i, iFanin; Vec_WrdSetEntry( &p->vObjTruth, Pivot, uTruth ); - Acb_ObjRemoveFanout( p, Pivot ); - Acb_ObjRemoveFanins( p, Pivot ); - Vec_IntForEachEntry( vSupp, iFanin, i ) - Acb_ObjAddFanin( p, Pivot, iFanin ); - Acb_ObjAddFanout( p, Pivot ); - Acb_NtkUpdateTiming( p, Pivot ); Vec_IntErase( Vec_WecEntry(&p->vCnfs, Pivot) ); + Acb_ObjRemoveFaninFanout( p, Pivot ); + Acb_ObjRemoveFanins( p, Pivot ); + Acb_ObjAddFanins( p, Pivot, vSupp ); + Acb_ObjAddFaninFanout( p, Pivot ); + if ( p->vQue == NULL ) + Acb_NtkUpdateLevelD( p, Pivot ); + else + Acb_NtkUpdateTiming( p, Pivot ); } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c index bf2a5b8a..d3a8aa9c 100644 --- a/src/sat/cnf/cnfMan.c +++ b/src/sat/cnf/cnfMan.c @@ -251,7 +251,7 @@ void Cnf_DataPrint( Cnf_Dat_t * p, int fReadable ) for ( i = 0; i < p->nClauses; i++ ) { for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ ) - fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) ); + fprintf( pFile, "%s%d ", Abc_LitIsCompl(*pLit) ? "-":"", fReadable? Abc_Lit2Var(*pLit) : Abc_Lit2Var(*pLit)+1 ); fprintf( pFile, "\n" ); } fprintf( pFile, "\n" ); |