From 0f22046bcb71ba096fedfc6a75b6bc7fd4090e70 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 27 Jan 2015 09:54:35 -0800 Subject: New assertions and bug fix in DSD balancing. --- src/map/if/ifDelay.c | 6 +++--- src/map/if/ifDsd.c | 13 ++++++++----- src/misc/util/abc_global.h | 27 +++++++++++++++++++-------- src/misc/vec/vecFlt.h | 10 ++++++++++ src/misc/vec/vecInt.h | 10 ++++++++++ src/misc/vec/vecPtr.h | 10 ++++++++++ src/misc/vec/vecStr.h | 10 ++++++++++ src/misc/vec/vecWec.h | 10 ++++++++++ src/misc/vec/vecWrd.h | 10 ++++++++++ 9 files changed, 90 insertions(+), 16 deletions(-) (limited to 'src') diff --git a/src/map/if/ifDelay.c b/src/map/if/ifDelay.c index 5afb77eb..cb25e767 100644 --- a/src/map/if/ifDelay.c +++ b/src/map/if/ifDelay.c @@ -204,9 +204,9 @@ int If_CutSopBalanceEvalInt( Vec_Int_t * vCover, int * pTimes, int * pFaninLits, { Literal = 3 & (Entry >> (k << 1)); if ( Literal == 1 ) // neg literal - nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], Abc_LitNot(pFaninLits[k]), vAig, nSuppAll, 0, 0 ); + nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], vAig ? Abc_LitNot(pFaninLits[k]) : -1, vAig, nSuppAll, 0, 0 ); else if ( Literal == 2 ) // pos literal - nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], pFaninLits[k], vAig, nSuppAll, 0, 0 ); + nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], vAig ? pFaninLits[k] : -1, vAig, nSuppAll, 0, 0 ); else if ( Literal != 0 ) assert( 0 ); } @@ -216,7 +216,7 @@ int If_CutSopBalanceEvalInt( Vec_Int_t * vCover, int * pTimes, int * pFaninLits, iRes = If_LogCreateAndXorMulti( vAig, pFaninLitsAnd, nCounterAnd, nSuppAll, 0 ); else *pArea += nLits == 1 ? 0 : nLits - 1; - Delay = If_LogCounterAddAig( pCounterOr, &nCounterOr, pFaninLitsOr, Delay, Abc_LitNot(iRes), vAig, nSuppAll, 0, 0 ); + Delay = If_LogCounterAddAig( pCounterOr, &nCounterOr, pFaninLitsOr, Delay, vAig ? Abc_LitNot(iRes) : -1, vAig, nSuppAll, 0, 0 ); } assert( nCounterOr > 0 ); if ( vAig ) diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index d97cd9be..9b09ce95 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -2211,7 +2211,7 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup if ( If_DsdObjType(pObj) == IF_DSD_VAR ) { int iCutVar = Abc_Lit2Var( pPermLits[*pnSupp] ); - if ( vAig ) + if ( vAig ) *piLit = Abc_Var2Lit( iCutVar, Abc_LitIsCompl(pPermLits[*pnSupp]) ); (*pnSupp)++; return pTimes[iCutVar]; @@ -2224,7 +2224,8 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits ); if ( Delays[i] == -1 ) return -1; - pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); + if ( vAig ) + pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); } if ( vAig ) *piLit = If_LogCreateMux( vAig, pFaninLits[0], pFaninLits[1], pFaninLits[2], nSuppAll ); @@ -2243,7 +2244,8 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits ); if ( Delays[i] == -1 ) return -1; - pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); + if ( vAig ) + pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); } return If_CutSopBalanceEvalInt( vCover, Delays, pFaninLits, vAig, piLit, nSuppAll, pArea ); } @@ -2258,8 +2260,9 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup Delay = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits ); if ( Delay == -1 ) return -1; - pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); - Result = If_LogCounterAddAig( pCounter, &nCounter, pFaninLits, Delay, pFaninLits[i], vAig, nSuppAll, fXor, fXorFunc ); + if ( vAig ) + pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); + Result = If_LogCounterAddAig( pCounter, &nCounter, pFaninLits, Delay, vAig ? pFaninLits[i] : -1, vAig, nSuppAll, fXor, fXorFunc ); } assert( nCounter > 0 ); if ( fXor ) diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index b798961e..6e112bb8 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -80,6 +80,7 @@ #include #include #include +#include //////////////////////////////////////////////////////////////////////// /// NAMESPACES /// @@ -260,20 +261,30 @@ static inline void Abc_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1< static inline void Abc_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } static inline unsigned Abc_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); } -static inline int Abc_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } -static inline int Abc_Lit2Var( int Lit ) { return Lit >> 1; } -static inline int Abc_LitIsCompl( int Lit ) { return Lit & 1; } -static inline int Abc_LitNot( int Lit ) { return Lit ^ 1; } -static inline int Abc_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); } -static inline int Abc_LitRegular( int Lit ) { return Lit & ~01; } -static inline int Abc_Lit2LitV( int * pMap, int Lit ) { return Abc_Var2Lit( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) ); } -static inline int Abc_Lit2LitL( int * pMap, int Lit ) { return Abc_LitNotCond( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) ); } +static inline int Abc_Var2Lit( int Var, int c ) { assert(Var >= 0 && !(c >> 1)); return Var + Var + c; } +static inline int Abc_Lit2Var( int Lit ) { assert(Lit >= 0); return Lit >> 1; } +static inline int Abc_LitIsCompl( int Lit ) { assert(Lit >= 0); return Lit & 1; } +static inline int Abc_LitNot( int Lit ) { assert(Lit >= 0); return Lit ^ 1; } +static inline int Abc_LitNotCond( int Lit, int c ) { assert(Lit >= 0); return Lit ^ (int)(c > 0); } +static inline int Abc_LitRegular( int Lit ) { assert(Lit >= 0); return Lit & ~01; } +static inline int Abc_Lit2LitV( int * pMap, int Lit ) { assert(Lit >= 0); return Abc_Var2Lit( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) ); } +static inline int Abc_Lit2LitL( int * pMap, int Lit ) { assert(Lit >= 0); return Abc_LitNotCond( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) ); } static inline int Abc_Ptr2Int( void * p ) { return (int)(ABC_PTRINT_T)p; } static inline void * Abc_Int2Ptr( int i ) { return (void *)(ABC_PTRINT_T)i; } static inline word Abc_Ptr2Wrd( void * p ) { return (word)(ABC_PTRUINT_T)p; } static inline void * Abc_Wrd2Ptr( word i ) { return (void *)(ABC_PTRUINT_T)i; } +static inline int Abc_Var2Lit2( int Var, int Att ) { assert(!(Att >> 2)); return (Var << 2) + Att; } +static inline int Abc_Lit2Var2( int Lit ) { assert(Lit >= 0); return Lit >> 2; } +static inline int Abc_Lit2Att2( int Lit ) { assert(Lit >= 0); return Lit & 3; } +static inline int Abc_Var2Lit3( int Var, int Att ) { assert(!(Att >> 3)); return (Var << 3) + Att; } +static inline int Abc_Lit2Var3( int Lit ) { assert(Lit >= 0); return Lit >> 3; } +static inline int Abc_Lit2Att3( int Lit ) { assert(Lit >= 0); return Lit & 7; } +static inline int Abc_Var2Lit4( int Var, int Att ) { assert(!(Att >> 4)); return (Var << 4) + Att; } +static inline int Abc_Lit2Var4( int Lit ) { assert(Lit >= 0); return Lit >> 4; } +static inline int Abc_Lit2Att4( int Lit ) { assert(Lit >= 0); return Lit & 15; } + // time counting typedef ABC_INT64_T abctime; static inline abctime Abc_Clock() diff --git a/src/misc/vec/vecFlt.h b/src/misc/vec/vecFlt.h index 8f3005a4..482973f7 100644 --- a/src/misc/vec/vecFlt.h +++ b/src/misc/vec/vecFlt.h @@ -86,6 +86,16 @@ static inline Vec_Flt_t * Vec_FltAlloc( int nCap ) p->pArray = p->nCap? ABC_ALLOC( float, p->nCap ) : NULL; return p; } +static inline Vec_Flt_t * Vec_FltAllocExact( int nCap ) +{ + Vec_Flt_t * p; + assert( nCap >= 0 ); + p = ABC_ALLOC( Vec_Flt_t, 1 ); + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_ALLOC( float, p->nCap ) : NULL; + return p; +} /**Function************************************************************* diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index 3e195bd3..e37743c5 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -96,6 +96,16 @@ static inline Vec_Int_t * Vec_IntAlloc( int nCap ) p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; return p; } +static inline Vec_Int_t * Vec_IntAllocExact( int nCap ) +{ + Vec_Int_t * p; + assert( nCap >= 0 ); + p = ABC_ALLOC( Vec_Int_t, 1 ); + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL; + return p; +} /**Function************************************************************* diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h index 516429ff..5fa40112 100644 --- a/src/misc/vec/vecPtr.h +++ b/src/misc/vec/vecPtr.h @@ -91,6 +91,16 @@ static inline Vec_Ptr_t * Vec_PtrAlloc( int nCap ) p->pArray = p->nCap? ABC_ALLOC( void *, p->nCap ) : NULL; return p; } +static inline Vec_Ptr_t * Vec_PtrAllocExact( int nCap ) +{ + Vec_Ptr_t * p; + assert( nCap >= 0 ); + p = ABC_ALLOC( Vec_Ptr_t, 1 ); + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_ALLOC( void *, p->nCap ) : NULL; + return p; +} /**Function************************************************************* diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h index 5f04615c..4198ac82 100644 --- a/src/misc/vec/vecStr.h +++ b/src/misc/vec/vecStr.h @@ -80,6 +80,16 @@ static inline Vec_Str_t * Vec_StrAlloc( int nCap ) p->pArray = p->nCap? ABC_ALLOC( char, p->nCap ) : NULL; return p; } +static inline Vec_Str_t * Vec_StrAllocExact( int nCap ) +{ + Vec_Str_t * p; + assert( nCap >= 0 ); + p = ABC_ALLOC( Vec_Str_t, 1 ); + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_ALLOC( char, p->nCap ) : NULL; + return p; +} /**Function************************************************************* diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h index f2fe3216..b09852ff 100644 --- a/src/misc/vec/vecWec.h +++ b/src/misc/vec/vecWec.h @@ -95,6 +95,16 @@ static inline Vec_Wec_t * Vec_WecAlloc( int nCap ) p->pArray = p->nCap? ABC_CALLOC( Vec_Int_t, p->nCap ) : NULL; return p; } +static inline Vec_Wec_t * Vec_WecAllocExact( int nCap ) +{ + Vec_Wec_t * p; + assert( nCap >= 0 ); + p = ABC_ALLOC( Vec_Wec_t, 1 ); + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_CALLOC( Vec_Int_t, p->nCap ) : NULL; + return p; +} static inline Vec_Wec_t * Vec_WecStart( int nSize ) { Vec_Wec_t * p; diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h index 5688d7b2..5227fec5 100644 --- a/src/misc/vec/vecWrd.h +++ b/src/misc/vec/vecWrd.h @@ -88,6 +88,16 @@ static inline Vec_Wrd_t * Vec_WrdAlloc( int nCap ) p->pArray = p->nCap? ABC_ALLOC( word, p->nCap ) : NULL; return p; } +static inline Vec_Wrd_t * Vec_WrdAllocExact( int nCap ) +{ + Vec_Wrd_t * p; + assert( nCap >= 0 ); + p = ABC_ALLOC( Vec_Wrd_t, 1 ); + p->nSize = 0; + p->nCap = nCap; + p->pArray = p->nCap? ABC_ALLOC( word, p->nCap ) : NULL; + return p; +} /**Function************************************************************* -- cgit v1.2.3