diff options
Diffstat (limited to 'src/aig/gia')
42 files changed, 453 insertions, 508 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 14fd4d6e..a784ab92 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -18,8 +18,8 @@ ***********************************************************************/ -#ifndef __GIA_H__ -#define __GIA_H__ +#ifndef ABC__aig__gia__gia_h +#define ABC__aig__gia__gia_h //////////////////////////////////////////////////////////////////////// @@ -32,8 +32,8 @@ #include <assert.h> #include <time.h> -#include "vec.h" -#include "utilCex.h" +#include "src/misc/vec/vec.h" +#include "src/misc/util/utilCex.h" #include "giaAbs.h" //////////////////////////////////////////////////////////////////////// @@ -210,19 +210,6 @@ struct Gia_ParVta_t_ int iFrame; // the number of frames covered }; -static inline int Gia_IntAbs( int n ) { return (n < 0)? -n : n; } -static inline int Gia_Float2Int( float Val ) { union { int x; float y; } v; v.y = Val; return v.x; } -static inline float Gia_Int2Float( int Num ) { union { int x; float y; } v; v.x = Num; return v.y; } -static inline int Gia_Base2Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; } -static inline int Gia_Base10Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; } -static inline int Gia_Base16Log( unsigned n ) { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 16, r++ ); return r; } -static inline char * Gia_UtilStrsav( char * s ) { return s ? strcpy(ABC_ALLOC(char, strlen(s)+1), s) : NULL; } -static inline int Gia_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } -static inline int Gia_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } -static inline int Gia_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } -static inline void Gia_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } -static inline void Gia_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } -static inline unsigned Gia_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); } static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } static inline int Gia_WordHasOneBit( unsigned uWord ) { return (uWord & (uWord-1)) == 0; } static inline int Gia_WordHasOnePair( unsigned uWord ) { return Gia_WordHasOneBit(uWord & (uWord>>1) & 0x55555555); } @@ -246,7 +233,7 @@ static inline int Gia_WordFindFirstBit( unsigned uWord ) static inline int Gia_ManTruthIsConst0( unsigned * pIn, int nVars ) { int w; - for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) + for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- ) if ( pIn[w] ) return 0; return 1; @@ -254,7 +241,7 @@ static inline int Gia_ManTruthIsConst0( unsigned * pIn, int nVars ) static inline int Gia_ManTruthIsConst1( unsigned * pIn, int nVars ) { int w; - for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) + for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- ) if ( pIn[w] != ~(unsigned)0 ) return 0; return 1; @@ -262,35 +249,28 @@ static inline int Gia_ManTruthIsConst1( unsigned * pIn, int nVars ) static inline void Gia_ManTruthCopy( unsigned * pOut, unsigned * pIn, int nVars ) { int w; - for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) + for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- ) pOut[w] = pIn[w]; } static inline void Gia_ManTruthClear( unsigned * pOut, int nVars ) { int w; - for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) + for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- ) pOut[w] = 0; } static inline void Gia_ManTruthFill( unsigned * pOut, int nVars ) { int w; - for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) + for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- ) pOut[w] = ~(unsigned)0; } static inline void Gia_ManTruthNot( unsigned * pOut, unsigned * pIn, int nVars ) { int w; - for ( w = Gia_TruthWordNum(nVars)-1; w >= 0; w-- ) + for ( w = Abc_TruthWordNum(nVars)-1; w >= 0; w-- ) pOut[w] = ~pIn[w]; } -static inline int Gia_Var2Lit( int Var, int fCompl ) { return Var + Var + fCompl; } -static inline int Gia_Lit2Var( int Lit ) { return Lit >> 1; } -static inline int Gia_LitIsCompl( int Lit ) { return Lit & 1; } -static inline int Gia_LitNot( int Lit ) { return Lit ^ 1; } -static inline int Gia_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); } -static inline int Gia_LitRegular( int Lit ) { return Lit & ~01; } - static inline Gia_Obj_t * Gia_Regular( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); } static inline Gia_Obj_t * Gia_Not( Gia_Obj_t * p ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ 01); } static inline Gia_Obj_t * Gia_NotCond( Gia_Obj_t * p, int c ) { return (Gia_Obj_t *)((ABC_PTRUINT_T)(p) ^ (c)); } @@ -358,33 +338,33 @@ static inline int Gia_ObjFaninId0( Gia_Obj_t * pObj, int ObjId ) { static inline int Gia_ObjFaninId1( Gia_Obj_t * pObj, int ObjId ) { return ObjId - pObj->iDiff1; } static inline int Gia_ObjFaninId0p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId0( pObj, Gia_ObjId(p, pObj) ); } static inline int Gia_ObjFaninId1p( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjFaninId1( pObj, Gia_ObjId(p, pObj) ); } -static inline int Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId ) { return Gia_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); } -static inline int Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId ) { return Gia_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); } -static inline int Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) ); } -static inline int Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Gia_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) ); } +static inline int Gia_ObjFaninLit0( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId0(pObj, ObjId), Gia_ObjFaninC0(pObj) ); } +static inline int Gia_ObjFaninLit1( Gia_Obj_t * pObj, int ObjId ) { return Abc_Var2Lit( Gia_ObjFaninId1(pObj, ObjId), Gia_ObjFaninC1(pObj) ); } +static inline int Gia_ObjFaninLit0p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId0p(p, pObj), Gia_ObjFaninC0(pObj) ); } +static inline int Gia_ObjFaninLit1p( Gia_Man_t * p, Gia_Obj_t * pObj) { return Abc_Var2Lit( Gia_ObjFaninId1p(p, pObj), Gia_ObjFaninC1(pObj) ); } static inline void Gia_ObjFlipFaninC0( Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); pObj->fCompl0 ^= 1; } static inline int Gia_ObjWhatFanin( Gia_Obj_t * pObj, Gia_Obj_t * pFanin ) { return Gia_ObjFanin0(pObj) == pFanin ? 0 : (Gia_ObjFanin1(pObj) == pFanin ? 1 : -1); } -static inline Gia_Obj_t * Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ManObj( p, Gia_Lit2Var(pObj->Value) ); } +static inline Gia_Obj_t * Gia_ObjCopy( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ManObj( p, Abc_Lit2Var(pObj->Value) ); } -static inline int Gia_ObjFanin0Copy( Gia_Obj_t * pObj ) { return Gia_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); } -static inline int Gia_ObjFanin1Copy( Gia_Obj_t * pObj ) { return Gia_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); } +static inline int Gia_ObjFanin0Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); } +static inline int Gia_ObjFanin1Copy( Gia_Obj_t * pObj ) { return Abc_LitNotCond( Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); } static inline int Gia_ObjCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)]; } static inline void Gia_ObjSetCopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj, int iLit ) { p->pCopies[Gia_ManObjNum(p) * f + Gia_ObjId(p,pObj)] = iLit; } -static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } -static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } +static inline int Gia_ObjFanin0CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); } +static inline int Gia_ObjFanin1CopyF( Gia_Man_t * p, int f, Gia_Obj_t * pObj ) { return Abc_LitNotCond(Gia_ObjCopyF(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); } -static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Gia_Lit2Var(iLit)), Gia_LitIsCompl(iLit) ); } -static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); } +static inline Gia_Obj_t * Gia_ObjFromLit( Gia_Man_t * p, int iLit ) { return Gia_NotCond( Gia_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit) ); } +static inline int Gia_ObjToLit( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Abc_Var2Lit( Gia_ObjId(p, Gia_Regular(pObj)), Gia_IsComplement(pObj) ); } static inline int Gia_ObjPhaseRealLit( Gia_Man_t * p, int iLit ) { return Gia_ObjPhaseReal( Gia_ObjFromLit(p, iLit) ); } static inline int Gia_ObjLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Vec_IntGetEntry(p->vLevels, Gia_ObjId(p,pObj)); } static inline int Gia_ObjLevelId( Gia_Man_t * p, int Id ) { return Vec_IntGetEntry(p->vLevels, Id); } static inline void Gia_ObjSetLevel( Gia_Man_t * p, Gia_Obj_t * pObj, int l ) { Vec_IntSetEntry(p->vLevels, Gia_ObjId(p,pObj), l); } static inline void Gia_ObjSetCoLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsCo(pObj) ); Gia_ObjSetLevel( p, pObj, Gia_ObjLevel(p,Gia_ObjFanin0(pObj)) ); } -static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+ABC_MAX(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); } +static inline void Gia_ObjSetAndLevel( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjIsAnd(pObj) ); Gia_ObjSetLevel( p, pObj, 1+Abc_MaxInt(Gia_ObjLevel(p,Gia_ObjFanin0(pObj)),Gia_ObjLevel(p,Gia_ObjFanin1(pObj))) ); } static inline int Gia_ObjRefs( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( p->pRefs); return p->pRefs[Gia_ObjId(p, pObj)]; } static inline int Gia_ObjRefsId( Gia_Man_t * p, int Id ) { assert( p->pRefs); return p->pRefs[Id]; } @@ -457,17 +437,17 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 ) assert( iLit0 != iLit1 ); if ( iLit0 < iLit1 ) { - pObj->iDiff0 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0); - pObj->fCompl0 = Gia_LitIsCompl(iLit0); - pObj->iDiff1 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit1); - pObj->fCompl1 = Gia_LitIsCompl(iLit1); + pObj->iDiff0 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0); + pObj->fCompl0 = Abc_LitIsCompl(iLit0); + pObj->iDiff1 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1); + pObj->fCompl1 = Abc_LitIsCompl(iLit1); } else { - pObj->iDiff1 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0); - pObj->fCompl1 = Gia_LitIsCompl(iLit0); - pObj->iDiff0 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit1); - pObj->fCompl0 = Gia_LitIsCompl(iLit1); + pObj->iDiff1 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0); + pObj->fCompl1 = Abc_LitIsCompl(iLit0); + pObj->iDiff0 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit1); + pObj->fCompl0 = Abc_LitIsCompl(iLit1); } if ( p->pFanData ) { @@ -480,8 +460,8 @@ static inline int Gia_ManAppendCo( Gia_Man_t * p, int iLit0 ) { Gia_Obj_t * pObj = Gia_ManAppendObj( p ); pObj->fTerm = 1; - pObj->iDiff0 = Gia_ObjId(p, pObj) - Gia_Lit2Var(iLit0); - pObj->fCompl0 = Gia_LitIsCompl(iLit0); + pObj->iDiff0 = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0); + pObj->fCompl0 = Abc_LitIsCompl(iLit0); pObj->iDiff1 = Vec_IntSize( p->vCos ); Vec_IntPush( p->vCos, Gia_ObjId(p, pObj) ); if ( p->pFanData ) @@ -490,9 +470,9 @@ static inline int Gia_ManAppendCo( Gia_Man_t * p, int iLit0 ) } static inline int Gia_ManAppendMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 ) { - int iTemp0 = Gia_ManAppendAnd( p, Gia_LitNot(iCtrl), iData0 ); + int iTemp0 = Gia_ManAppendAnd( p, Abc_LitNot(iCtrl), iData0 ); int iTemp1 = Gia_ManAppendAnd( p, iCtrl, iData1 ); - return Gia_LitNotCond( Gia_ManAppendAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), 1 ); + return Abc_LitNotCond( Gia_ManAppendAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 ); } #define GIA_ZER 1 @@ -587,7 +567,7 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re #define Gia_ManForEachObjVec( vVec, p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Vec_IntEntry(vVec,i))); i++ ) #define Gia_ManForEachObjVecLit( vVec, p, pObj, fCompl, i ) \ - for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Gia_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Gia_LitIsCompl(Vec_IntEntry(vVec,i))),1); i++ ) + for ( i = 0; (i < Vec_IntSize(vVec)) && ((pObj) = Gia_ManObj(p, Abc_Lit2Var(Vec_IntEntry(vVec,i)))) && (((fCompl) = Abc_LitIsCompl(Vec_IntEntry(vVec,i))),1); i++ ) #define Gia_ManForEachObjReverse( p, pObj, i ) \ for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) #define Gia_ManForEachAnd( p, pObj, i ) \ @@ -817,7 +797,6 @@ extern Gia_Man_t * Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose ); /*=== giaUtil.c ===========================================================*/ extern unsigned Gia_ManRandom( int fReset ); extern void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int iWordStop ); -extern unsigned int Gia_PrimeCudd( unsigned int p ); extern char * Gia_TimeStamp(); extern char * Gia_FileNameGenericAppend( char * pBase, char * pSuffix ); extern void Gia_ManIncrementTravId( Gia_Man_t * p ); diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index e9861977..e25ff7fb 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -20,7 +20,7 @@ #include "gia.h" #include "giaAig.h" -#include "saig.h" +#include "src/aig/saig/saig.h" ABC_NAMESPACE_IMPL_START @@ -472,7 +472,7 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars, int fNewSolver ) // this obj was abstracted before assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsRo(pGia, pObj) ); // if corresponding AIG object is not abstracted, remove abstraction - if ( !Vec_IntEntry(vGateClasses, Gia_Lit2Var(pObj->Value)) ) + if ( !Vec_IntEntry(vGateClasses, Abc_Lit2Var(pObj->Value)) ) { Vec_IntWriteEntry( pGia->vGateClasses, i, 0 ); Counter++; diff --git a/src/aig/gia/giaAbs.h b/src/aig/gia/giaAbs.h index 090d5dca..366a4d8a 100644 --- a/src/aig/gia/giaAbs.h +++ b/src/aig/gia/giaAbs.h @@ -18,8 +18,8 @@ ***********************************************************************/ -#ifndef __GIA_ABS_H__ -#define __GIA_ABS_H__ +#ifndef ABC__aig__gia__giaAbs_h +#define ABC__aig__gia__giaAbs_h //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c index fe30d0f0..3e7f2a01 100644 --- a/src/aig/gia/giaAbsVta.c +++ b/src/aig/gia/giaAbsVta.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "gia.h" -#include "satSolver2.h" +#include "src/sat/bsat/satSolver2.h" ABC_NAMESPACE_IMPL_START @@ -210,7 +210,7 @@ Vec_Int_t * Gia_VtaConvertToGla( Gia_Man_t * p, Vec_Int_t * vAbs ) int i, Entry, nFrames = Vec_IntEntry( vAbs, 0 ); assert( Vec_IntEntry(vAbs, nFrames+1) == Vec_IntSize(vAbs) ); // get the bitmask - nObjMask = (1 << Gia_Base2Log(nObjs)) - 1; + nObjMask = (1 << Abc_Base2Log(nObjs)) - 1; assert( nObjs <= nObjMask ); // go through objects vPresent = Vec_IntStart( nObjs ); @@ -248,7 +248,7 @@ static inline int Vta_ManReadFrameStart( Vec_Int_t * p, int nWords ) pTotal[w] |= pThis[i]; } for ( i = nWords * 32 - 1; i >= 0; i-- ) - if ( Gia_InfoHasBit(pTotal, i) ) + if ( Abc_InfoHasBit(pTotal, i) ) { ABC_FREE( pTotal ); return i+1; @@ -716,7 +716,7 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p ) if ( Gia_ObjIsRo(p->pGia, pObj) ) assert( pThis->iFrame == 0 && pThis->Value == VTA_VAR0 ); else if ( Gia_ObjIsPi(p->pGia, pObj) && pThis->Value == VTA_VAR1 ) - Gia_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) ); + Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) ); } } // perform refinement @@ -776,7 +776,7 @@ Vta_Man_t * Vga_ManStart( Gia_Man_t * pGia, Gia_ParVta_t * pPars ) p->pBins = ABC_CALLOC( int, p->nBins ); p->vOrder = Vec_IntAlloc( 1013 ); // abstraction - p->nObjBits = Gia_Base2Log( Gia_ManObjNum(pGia) ); + p->nObjBits = Abc_Base2Log( Gia_ManObjNum(pGia) ); p->nObjMask = (1 << p->nObjBits) - 1; assert( Gia_ManObjNum(pGia) <= (int)p->nObjMask ); p->nWords = 1; @@ -922,7 +922,8 @@ Vec_Int_t * Vta_ManUnsatCore( int iLit, Vec_Int_t * vCla2Var, sat_solver2 * pSat ***********************************************************************/ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames ) { - unsigned * pInfo, * pCountAll, * pCountUni; + unsigned * pInfo; + int * pCountAll, * pCountUni; int i, k, iFrame, iObj, Entry; // print info about frames pCountAll = ABC_CALLOC( int, nFrames + 1 ); @@ -933,9 +934,9 @@ void Vta_ManAbsPrintFrame( Vta_Man_t * p, Vec_Int_t * vCore, int nFrames ) iFrame = (Entry >> p->nObjBits); assert( iFrame < nFrames ); pInfo = (unsigned *)Vec_IntEntryP( p->vSeens, p->nWords * iObj ); - if ( Gia_InfoHasBit(pInfo, iFrame) == 0 ) + if ( Abc_InfoHasBit(pInfo, iFrame) == 0 ) { - Gia_InfoSetBit( pInfo, iFrame ); + Abc_InfoSetBit( pInfo, iFrame ); pCountUni[iFrame+1]++; pCountUni[0]++; } @@ -1062,7 +1063,7 @@ static inline int Vga_ManGetOutLit( Vta_Man_t * p, int f ) Gia_Obj_t * pObj = Gia_ManPo(p->pGia, 0); Vta_Obj_t * pThis = Vga_ManFind( p, Gia_ObjFaninId0p(p->pGia, pObj), f ); assert( pThis != NULL && pThis->fAdded ); - return Gia_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) ); + return Abc_Var2Lit( Vta_ObjId(p, pThis), Gia_ObjFaninC0(pObj) ); } /**Function************************************************************* @@ -1105,7 +1106,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) if ( f < p->pPars->nFramesStart ) { // load this timeframe - Vga_ManLoadSlice( p, Vec_PtrEntry(p->vFrames, f), 0 ); + Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vFrames, f), 0 ); // run SAT solver vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, p->pPars->fVerbose, &Status ); assert( (vCore != NULL) == (Status == 1) ); @@ -1123,7 +1124,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) { pObj = Gia_ManObj( p->pGia, pThis->iObj ); if ( Gia_ObjIsPi(p->pGia, pObj) && sat_solver2_var_value(p->pSat, Vta_ObjId(p, pThis)) ) - Gia_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) ); + Abc_InfoSetBit( pCex->pData, pCex->nRegs + pThis->iFrame * pCex->nPis + Gia_ObjCioId(pObj) ); } } } @@ -1133,7 +1134,7 @@ int Gia_VtaPerform( Gia_Man_t * pAig, Gia_ParVta_t * pPars ) // load the time frame int Limit = Abc_MinInt(5, p->pPars->nFramesStart); for ( i = 1; i <= Limit; i++ ) - Vga_ManLoadSlice( p, Vec_PtrEntry(p->vCores, f-i), i ); + Vga_ManLoadSlice( p, (Vec_Int_t *)Vec_PtrEntry(p->vCores, f-i), i ); // iterate as long as there are counter-examples do { vCore = Vta_ManUnsatCore( Vga_ManGetOutLit(p, f), p->vCla2Var, p->pSat, pPars->nConfLimit, pPars->fVerbose, &Status ); diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 00148451..6da633e0 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -19,9 +19,9 @@ ***********************************************************************/ #include "giaAig.h" -#include "fra.h" -#include "dch.h" -#include "dar.h" +#include "src/proof/fra/fra.h" +#include "src/proof/dch/dch.h" +#include "src/opt/dar/dar.h" ABC_NAMESPACE_IMPL_START @@ -30,8 +30,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Gia_ObjChild0Copy( Aig_Obj_t * pObj ) { return Gia_LitNotCond( Aig_ObjFanin0(pObj)->iData, Aig_ObjFaninC0(pObj) ); } -static inline int Gia_ObjChild1Copy( Aig_Obj_t * pObj ) { return Gia_LitNotCond( Aig_ObjFanin1(pObj)->iData, Aig_ObjFaninC1(pObj) ); } +static inline int Gia_ObjChild0Copy( Aig_Obj_t * pObj ) { return Abc_LitNotCond( Aig_ObjFanin0(pObj)->iData, Aig_ObjFaninC0(pObj) ); } +static inline int Gia_ObjChild1Copy( Aig_Obj_t * pObj ) { return Abc_LitNotCond( Aig_ObjFanin1(pObj)->iData, Aig_ObjFaninC1(pObj) ); } static inline Aig_Obj_t * Gia_ObjChild0Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Aig_NotCond( ppNodes[Gia_ObjFaninId0(pObj, Id)], Gia_ObjFaninC0(pObj) ); } static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id ) { return Aig_NotCond( ppNodes[Gia_ObjFaninId1(pObj, Id)], Gia_ObjFaninC1(pObj) ); } @@ -64,8 +64,8 @@ void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) { int iObjNew, iNextNew; Gia_ManFromAig_rec( pNew, p, pNext ); - iObjNew = Gia_Lit2Var(pObj->iData); - iNextNew = Gia_Lit2Var(pNext->iData); + iObjNew = Abc_Lit2Var(pObj->iData); + iNextNew = Abc_Lit2Var(pNext->iData); if ( pNew->pNexts ) pNew->pNexts[iObjNew] = iNextNew; } @@ -89,7 +89,7 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ) int i; // create the new manager pNew = Gia_ManStart( Aig_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->nConstrs = p->nConstrs; // create room to store equivalences if ( p->pEquivs ) @@ -128,7 +128,7 @@ Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p ) int i; // create the new manager pNew = Gia_ManStart( Aig_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->nConstrs = p->nConstrs; // create the PIs Aig_ManCleanData( p ); @@ -167,7 +167,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ) int i; // create the new manager pNew = Gia_ManStart( Aig_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->nConstrs = p->nConstrs; // create the PIs Aig_ManCleanData( p ); @@ -246,9 +246,9 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ) assert( !fChoices || (p->pNexts && p->pReprs) ); // create the new manager pNew = Aig_ManStart( Gia_ManAndNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->nConstrs = p->nConstrs; -// pNew->pSpec = Gia_UtilStrsav( p->pName ); +// pNew->pSpec = Abc_UtilStrsav( p->pName ); // duplicate representation of choice nodes if ( fChoices ) pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) ); @@ -293,9 +293,9 @@ Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta ) assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 ); // create the new manager pNew = Aig_ManStart( Gia_ManAndNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->nConstrs = p->nConstrs; -// pNew->pSpec = Gia_UtilStrsav( p->pName ); +// pNew->pSpec = Abc_UtilStrsav( p->pName ); // create the PIs ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) ); ppNodes[0] = Aig_ManConst0(pNew); @@ -334,7 +334,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p ) ppNodes = ABC_FALLOC( Aig_Obj_t *, Gia_ManObjNum(p) ); // create the new manager pNew = Aig_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->nConstrs = p->nConstrs; // create the PIs Gia_ManForEachObj( p, pObj, i ) @@ -349,7 +349,7 @@ Aig_Man_t * Gia_ManToAigSimple( Gia_Man_t * p ) ppNodes[i] = Aig_ManConst0(pNew); else assert( 0 ); - pObj->Value = Gia_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) ); + pObj->Value = Abc_Var2Lit( Aig_ObjId(Aig_Regular(ppNodes[i])), Aig_IsComplement(ppNodes[i]) ); assert( i == 0 || Aig_ObjId(ppNodes[i]) == i ); } Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) ); @@ -402,8 +402,8 @@ void Gia_ManReprToAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ) // move pointers from AIG to GIA Aig_ManForEachObj( pAig, pObj, i ) { - assert( i == 0 || !Gia_LitIsCompl(pObj->iData) ); - pGiaObj = Gia_ManObj( pGia, Gia_Lit2Var(pObj->iData) ); + assert( i == 0 || !Abc_LitIsCompl(pObj->iData) ); + pGiaObj = Gia_ManObj( pGia, Abc_Lit2Var(pObj->iData) ); pGiaObj->Value = i; } // set the pointers to the nodes in AIG @@ -441,7 +441,7 @@ void Gia_ManReprToAigRepr2( Aig_Man_t * pAig, Gia_Man_t * pGia ) pGiaRepr = Gia_ObjReprObj( pGia, i ); if ( pGiaRepr == NULL ) continue; - Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Gia_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Gia_Lit2Var(pGiaObj->Value)) ); + Aig_ObjCreateRepr( pAig, Aig_ManObj(pAig, Abc_Lit2Var(pGiaRepr->Value)), Aig_ManObj(pAig, Abc_Lit2Var(pGiaObj->Value)) ); } } @@ -472,8 +472,8 @@ void Gia_ManReprFromAigRepr( Aig_Man_t * pAig, Gia_Man_t * pGia ) // Abc_Print( 1, "%d -> %d %d\n", i, Gia_ObjValue(pObjGia), Gia_ObjValue(pObjGia)/2 ); if ( Gia_ObjIsCo(pObjGia) ) continue; - assert( i == 0 || !Gia_LitIsCompl(Gia_ObjValue(pObjGia)) ); - pObjAig = Aig_ManObj( pAig, Gia_Lit2Var(Gia_ObjValue(pObjGia)) ); + assert( i == 0 || !Abc_LitIsCompl(Gia_ObjValue(pObjGia)) ); + pObjAig = Aig_ManObj( pAig, Abc_Lit2Var(Gia_ObjValue(pObjGia)) ); pObjAig->iData = i; } Aig_ManForEachObj( pAig, pObjAig, i ) diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h index 1c0a24d5..6522a5bc 100644 --- a/src/aig/gia/giaAig.h +++ b/src/aig/gia/giaAig.h @@ -18,15 +18,15 @@ ***********************************************************************/ -#ifndef __GIA_AIG_H__ -#define __GIA_AIG_H__ +#ifndef ABC__aig__gia__giaAig_h +#define ABC__aig__gia__giaAig_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -#include "aig.h" +#include "src/aig/aig/aig.h" #include "gia.h" ABC_NAMESPACE_HEADER_START diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index db194c69..2ae070d3 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -146,7 +146,7 @@ int Gia_FileSize( char * pFileName ) char * Gia_FileNameGeneric( char * FileName ) { char * pDot, * pRes; - pRes = Gia_UtilStrsav( FileName ); + pRes = Abc_UtilStrsav( FileName ); if ( (pDot = strrchr( pRes, '.' )) ) *pDot = 0; return pRes; @@ -445,8 +445,8 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) // allocate the empty AIG pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 ); pName = Gia_FileNameGeneric( pFileName ); - pNew->pName = Gia_UtilStrsav( pName ); -// pNew->pSpec = Gia_UtilStrsav( pFileName ); + pNew->pName = Abc_UtilStrsav( pName ); +// pNew->pSpec = Abc_UtilStrsav( pFileName ); ABC_FREE( pName ); pNew->nConstrs = nConstr; @@ -482,8 +482,8 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) uLit1 = uLit - Gia_ReadAigerDecode( &pCur ); uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur ); // assert( uLit1 > uLit0 ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); - iNode1 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 ); + iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); + iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 ); assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches ); // Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) ); Vec_IntPush( vNodes, Gia_ManAppendAnd(pNew, iNode0, iNode1) ); @@ -500,14 +500,14 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) for ( i = 0; i < nLatches; i++ ) { uLit0 = atoi( (char *)pCur ); while ( *pCur++ != '\n' ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); + iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); Vec_IntPush( vDrivers, iNode0 ); } // read the PO driver literals for ( i = 0; i < nOutputs; i++ ) { uLit0 = atoi( (char *)pCur ); while ( *pCur++ != '\n' ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); + iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); Vec_IntPush( vDrivers, iNode0 ); } @@ -518,14 +518,14 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) for ( i = 0; i < nLatches; i++ ) { uLit0 = Vec_IntEntry( vLits, i ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); + iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); Vec_IntPush( vDrivers, iNode0 ); } // read the PO driver literals for ( i = 0; i < nOutputs; i++ ) { uLit0 = Vec_IntEntry( vLits, i+nLatches ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); + iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); Vec_IntPush( vDrivers, iNode0 ); } Vec_IntFree( vLits ); @@ -604,7 +604,7 @@ Gia_Man_t * Gia_ReadAiger2( char * pFileName, int fCheck ) pCur++; // read model name ABC_FREE( pNew->pName ); - pNew->pName = Gia_UtilStrsav( (char *)pCur ); + pNew->pName = Abc_UtilStrsav( (char *)pCur ); } } Vec_IntFree( vNodes ); @@ -753,8 +753,8 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck uLit1 = uLit - Gia_ReadAigerDecode( &pCur ); uLit0 = uLit1 - Gia_ReadAigerDecode( &pCur ); // assert( uLit1 > uLit0 ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); - iNode1 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 ); + iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); + iNode1 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit1 >> 1), uLit1 & 1 ); assert( Vec_IntSize(vNodes) == i + 1 + nInputs + nLatches ); // Vec_IntPush( vNodes, Gia_And(pNew, iNode0, iNode1) ); Vec_IntPush( vNodes, Gia_ManHashAnd(pNew, iNode0, iNode1) ); @@ -772,14 +772,14 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck for ( i = 0; i < nLatches; i++ ) { uLit0 = atoi( (char *)pCur ); while ( *pCur++ != '\n' ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); + iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); Vec_IntPush( vDrivers, iNode0 ); } // read the PO driver literals for ( i = 0; i < nOutputs; i++ ) { uLit0 = atoi( (char *)pCur ); while ( *pCur++ != '\n' ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); + iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); Vec_IntPush( vDrivers, iNode0 ); } @@ -790,14 +790,14 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck for ( i = 0; i < nLatches; i++ ) { uLit0 = Vec_IntEntry( vLits, i ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); + iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); Vec_IntPush( vDrivers, iNode0 ); } // read the PO driver literals for ( i = 0; i < nOutputs; i++ ) { uLit0 = Vec_IntEntry( vLits, i+nLatches ); - iNode0 = Gia_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); + iNode0 = Abc_LitNotCond( Vec_IntEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ); Vec_IntPush( vDrivers, iNode0 ); } Vec_IntFree( vLits ); @@ -877,7 +877,7 @@ Gia_Man_t * Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck pCur++; // read model name ABC_FREE( pNew->pName ); - pNew->pName = Gia_UtilStrsav( (char *)pCur ); + pNew->pName = Abc_UtilStrsav( (char *)pCur ); } } @@ -1094,7 +1094,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck ) { ABC_FREE( pNew->pName ); pName = Gia_FileNameGeneric( pFileName ); - pNew->pName = Gia_UtilStrsav( pName ); + pNew->pName = Abc_UtilStrsav( pName ); // pNew->pSpec = Ioa_UtilStrsav( pFileName ); ABC_FREE( pName ); } @@ -1246,30 +1246,30 @@ unsigned char * Gia_WriteEquivClasses( Gia_Man_t * p, int * pEquivSize ) } pBuffer = ABC_ALLOC( unsigned char, sizeof(int) * (nItems + 1) ); // write constant class - iPos = Gia_WriteAigerEncode( pBuffer, 4, Gia_Var2Lit(0, 1) ); + iPos = Gia_WriteAigerEncode( pBuffer, 4, Abc_Var2Lit(0, 1) ); //printf( "\nRepr = %d ", 0 ); iPrevNode = 0; for ( iNode = 1; iNode < Gia_ManObjNum(p); iNode++ ) if ( Gia_ObjIsConst(p, iNode) ) { //printf( "Node = %d ", iNode ); - iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); + iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); iPrevNode = iNode; - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) ); + iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iLit, 0) ); } // write non-constant classes iPrevRepr = 0; Gia_ManForEachClass( p, iRepr ) { //printf( "\nRepr = %d ", iRepr ); - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iRepr - iPrevRepr, 1) ); + iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iRepr - iPrevRepr, 1) ); iPrevRepr = iPrevNode = iRepr; Gia_ClassForEachObj1( p, iRepr, iNode ) { //printf( "Node = %d ", iNode ); - iLit = Gia_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); + iLit = Abc_Var2Lit( iNode - iPrevNode, Gia_ObjProved(p, iNode) ); iPrevNode = iNode; - iPos = Gia_WriteAigerEncode( pBuffer, iPos, Gia_Var2Lit(iLit, 0) ); + iPos = Gia_WriteAigerEncode( pBuffer, iPos, Abc_Var2Lit(iLit, 0) ); } } Gia_WriteInt( pBuffer, iPos ); @@ -1291,8 +1291,8 @@ unsigned char * Gia_WriteEquivClasses( Gia_Man_t * p, int * pEquivSize ) int Gia_WriteDiffValue( unsigned char * pPos, int iPos, int iPrev, int iThis ) { if ( iPrev < iThis ) - return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iThis - iPrev, 1) ); - return Gia_WriteAigerEncode( pPos, iPos, Gia_Var2Lit(iPrev - iThis, 0) ); + return Gia_WriteAigerEncode( pPos, iPos, Abc_Var2Lit(iThis - iPrev, 1) ); + return Gia_WriteAigerEncode( pPos, iPos, Abc_Var2Lit(iPrev - iThis, 0) ); } /**Function************************************************************* @@ -1420,7 +1420,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int pBuffer = ABC_ALLOC( unsigned char, nBufferSize ); Gia_ManForEachAnd( p, pObj, i ) { - uLit = Gia_Var2Lit( i, 0 ); + uLit = Abc_Var2Lit( i, 0 ); uLit0 = Gia_ObjFaninLit0( pObj, i ); uLit1 = Gia_ObjFaninLit1( pObj, i ); assert( uLit0 < uLit1 ); diff --git a/src/aig/gia/giaBidec.c b/src/aig/gia/giaBidec.c index fc17b582..54f98afd 100644 --- a/src/aig/gia/giaBidec.c +++ b/src/aig/gia/giaBidec.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "gia.h" -#include "bdc.h" +#include "src/bool/bdc/bdc.h" ABC_NAMESPACE_IMPL_START @@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Bdc_FunObjCopy( Bdc_Fun_t * pObj ) { return Gia_LitNotCond( Bdc_FuncCopyInt(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) ); } +static inline int Bdc_FunObjCopy( Bdc_Fun_t * pObj ) { return Abc_LitNotCond( Bdc_FuncCopyInt(Bdc_Regular(pObj)), Bdc_IsComplement(pObj) ); } static inline int Bdc_FunFanin0Copy( Bdc_Fun_t * pObj ) { return Bdc_FunObjCopy( Bdc_FuncFanin0(pObj) ); } static inline int Bdc_FunFanin1Copy( Bdc_Fun_t * pObj ) { return Bdc_FunObjCopy( Bdc_FuncFanin1(pObj) ); } @@ -109,7 +109,7 @@ unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t int i, nWords, nVars; // get the number of variables and words nVars = Vec_IntSize( vLeaves ); - nWords = Gia_TruthWordNum( nVars ); + nWords = Abc_TruthWordNum( nVars ); // check the case of a constant if ( Gia_ObjIsConst0( Gia_Regular(pRoot) ) ) { @@ -263,7 +263,7 @@ Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose ) Gia_ManConst0(p)->Value = 0; // start the new manager pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); // Gia_ManCleanLevels( pNew, Gia_ManObjNum(p) ); pManDec = Bdc_ManAlloc( pPars ); diff --git a/src/aig/gia/giaCCof.c b/src/aig/gia/giaCCof.c index 38e5ccdf..b04d5953 100644 --- a/src/aig/gia/giaCCof.c +++ b/src/aig/gia/giaCCof.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "gia.h" -#include "satSolver.h" +#include "src/sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START @@ -134,10 +134,10 @@ void Gia_ManCofExtendSolver( Ccf_Man_t * p ) } static inline int Gia_Obj0Copy( Vec_Int_t * vCopies, int Fan0, int fCompl0 ) -{ return Gia_LitNotCond( Vec_IntEntry(vCopies, Fan0), fCompl0 ); } +{ return Abc_LitNotCond( Vec_IntEntry(vCopies, Fan0), fCompl0 ); } static inline int Gia_Obj1Copy( Vec_Int_t * vCopies, int Fan1, int fCompl1 ) -{ return Gia_LitNotCond( Vec_IntEntry(vCopies, Fan1), fCompl1 ); } +{ return Abc_LitNotCond( Vec_IntEntry(vCopies, Fan1), fCompl1 ); } /**Function************************************************************* @@ -173,7 +173,7 @@ void Gia_ManCofOneDerive_rec( Ccf_Man_t * p, int Id ) else if ( Gia_ObjCioId(pObj) >= Gia_ManRegNum(p->pGia) ) // PI Res = sat_solver_var_value( p->pSat, Id ); else - Res = Gia_Var2Lit( Id, 0 ); + Res = Abc_Var2Lit( Id, 0 ); Vec_IntWriteEntry( p->vCopies, Id, Res ); } @@ -193,15 +193,15 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp ) int LitOut; // derive the cofactor of the property node Vec_IntFill( p->vCopies, Gia_ManObjNum(p->pFrames), -1 ); - Gia_ManCofOneDerive_rec( p, Gia_Lit2Var(LitProp) ); - LitOut = Vec_IntEntry( p->vCopies, Gia_Lit2Var(LitProp) ); - LitOut = Gia_LitNotCond( LitOut, Gia_LitIsCompl(LitProp) ); + Gia_ManCofOneDerive_rec( p, Abc_Lit2Var(LitProp) ); + LitOut = Vec_IntEntry( p->vCopies, Abc_Lit2Var(LitProp) ); + LitOut = Abc_LitNotCond( LitOut, Abc_LitIsCompl(LitProp) ); // add new PO for the cofactor Gia_ManAppendCo( p->pFrames, LitOut ); // add SAT clauses Gia_ManCofExtendSolver( p ); // return negative literal of the cofactor - return Gia_LitNot(LitOut); + return Abc_LitNot(LitOut); } /**Function************************************************************* diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index 745b19ba..d83f79e9 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -238,8 +238,8 @@ static inline void Cbs_ManSaveModel( Cbs_Man_t * p, Vec_Int_t * vCex ) p->pProp.iHead = 0; Cbs_QueForEachEntry( p->pProp, pVar, i ) if ( Gia_ObjIsCi(pVar) ) -// Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) ); - Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) ); +// Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs_VarValue(pVar)) ); + Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Cbs_VarValue(pVar)) ); } /**Function************************************************************* @@ -377,7 +377,7 @@ static inline int Cbs_VarFaninFanoutMax( Cbs_Man_t * p, Gia_Obj_t * pObj ) assert( Gia_ObjIsAnd(pObj) ); Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) ); Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) ); - return ABC_MAX( Count0, Count1 ); + return Abc_MaxInt( Count0, Count1 ); } /**Function************************************************************* @@ -504,7 +504,7 @@ static inline void Cbs_ManAssign( Cbs_Man_t * p, Gia_Obj_t * pObj, int Level, Gi Vec_IntPush( p->vLevReas, pRes1 ? pRes1-pObjR : 0 ); assert( Vec_IntSize(p->vLevReas) == 3 * p->pProp.iTail ); // s_Counter++; -// s_Counter = Abc_MaxInt( s_Counter, Vec_IntSize(p->vLevReas)/3 ); +// s_Counter = Abc_MaxIntInt( s_Counter, Vec_IntSize(p->vLevReas)/3 ); } @@ -872,7 +872,7 @@ int Cbs_ManSolve_rec( Cbs_Man_t * p, int Level ) if ( Cbs_QueIsEmpty(&p->pJust) ) return 0; // quit using resource limits - p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead ); + p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead ); if ( Cbs_ManCheckLimits( p ) ) return 0; // remember the state before branching @@ -946,7 +946,7 @@ int Cbs_ManSolve( Cbs_Man_t * p, Gia_Obj_t * pObj ) p->pJust.iHead = p->pJust.iTail = 0; p->pClauses.iHead = p->pClauses.iTail = 1; p->Pars.nBTTotal += p->Pars.nBTThis; - p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis ); + p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis ); if ( Cbs_ManCheckLimits( p ) ) RetValue = -1; diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c index 983081f0..8198c17f 100644 --- a/src/aig/gia/giaCSatOld.c +++ b/src/aig/gia/giaCSatOld.c @@ -213,8 +213,8 @@ static inline void Cbs0_ManSaveModel( Cbs0_Man_t * p, Vec_Int_t * vCex ) p->pProp.iHead = 0; Cbs0_QueForEachEntry( p->pProp, pVar, i ) if ( Gia_ObjIsCi(pVar) ) -// Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs0_VarValue(pVar)) ); - Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Cbs0_VarValue(pVar)) ); +// Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Cbs0_VarValue(pVar)) ); + Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Cbs0_VarValue(pVar)) ); } /**Function************************************************************* @@ -332,7 +332,7 @@ static inline int Cbs0_VarFaninFanoutMax( Cbs0_Man_t * p, Gia_Obj_t * pObj ) assert( Gia_ObjIsAnd(pObj) ); Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) ); Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) ); - return ABC_MAX( Count0, Count1 ); + return Abc_MaxInt( Count0, Count1 ); } /**Function************************************************************* @@ -596,7 +596,7 @@ int Cbs0_ManSolve_rec( Cbs0_Man_t * p ) if ( Cbs0_QueIsEmpty(&p->pJust) ) return 0; // quit using resource limits - p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead ); + p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead ); if ( Cbs0_ManCheckLimits( p ) ) return 0; // remember the state before branching @@ -656,7 +656,7 @@ int Cbs0_ManSolve( Cbs0_Man_t * p, Gia_Obj_t * pObj ) Cbs0_ManCancelUntil( p, 0 ); p->pJust.iHead = p->pJust.iTail = 0; p->Pars.nBTTotal += p->Pars.nBTThis; - p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis ); + p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis ); if ( Cbs0_ManCheckLimits( p ) ) RetValue = -1; // printf( "Outcome = %2d. Confs = %6d. Decision level max = %3d.\n", diff --git a/src/aig/gia/giaCTas.c b/src/aig/gia/giaCTas.c index c6aa3fec..7cfdac74 100644 --- a/src/aig/gia/giaCTas.c +++ b/src/aig/gia/giaCTas.c @@ -122,8 +122,8 @@ static inline void Tas_VarSetValue( Gia_Obj_t * pVar, int v ) { assert(pVar->fM static inline int Tas_VarIsJust( Gia_Obj_t * pVar ) { return Gia_ObjIsAnd(pVar) && !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) && !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)); } static inline int Tas_VarFanin0Value( Gia_Obj_t * pVar ) { return !Tas_VarIsAssigned(Gia_ObjFanin0(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin0(pVar)) ^ Gia_ObjFaninC0(pVar)); } static inline int Tas_VarFanin1Value( Gia_Obj_t * pVar ) { return !Tas_VarIsAssigned(Gia_ObjFanin1(pVar)) ? 2 : (Tas_VarValue(Gia_ObjFanin1(pVar)) ^ Gia_ObjFaninC1(pVar)); } -static inline int Tas_VarToLit( Tas_Man_t * p, Gia_Obj_t * pObj ) { assert( Tas_VarIsAssigned(pObj) ); return Gia_Var2Lit( Gia_ObjId(p->pAig, pObj), !Tas_VarValue(pObj) ); } -static inline int Tas_LitIsTrue( Gia_Obj_t * pObj, int Lit ) { assert( Tas_VarIsAssigned(pObj) ); return Tas_VarValue(pObj) != Gia_LitIsCompl(Lit); } +static inline int Tas_VarToLit( Tas_Man_t * p, Gia_Obj_t * pObj ) { assert( Tas_VarIsAssigned(pObj) ); return Abc_Var2Lit( Gia_ObjId(p->pAig, pObj), !Tas_VarValue(pObj) ); } +static inline int Tas_LitIsTrue( Gia_Obj_t * pObj, int Lit ) { assert( Tas_VarIsAssigned(pObj) ); return Tas_VarValue(pObj) != Abc_LitIsCompl(Lit); } static inline int Tas_ClsHandle( Tas_Man_t * p, Tas_Cls_t * pClause ) { return ((int *)pClause) - p->pStore.pData; } static inline Tas_Cls_t * Tas_ClsFromHandle( Tas_Man_t * p, int h ) { return (Tas_Cls_t *)(p->pStore.pData + h); } @@ -292,8 +292,8 @@ static inline void Tas_ManSaveModel( Tas_Man_t * p, Vec_Int_t * vCex ) Tas_QueForEachEntry( p->pProp, pVar, i ) { if ( Gia_ObjIsCi(pVar) ) -// Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjId(p->pAig,pVar), !Tas_VarValue(pVar)) ); - Vec_IntPush( vCex, Gia_Var2Lit(Gia_ObjCioId(pVar), !Tas_VarValue(pVar)) ); +// Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjId(p->pAig,pVar), !Tas_VarValue(pVar)) ); + Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pVar), !Tas_VarValue(pVar)) ); /* printf( "%5d(%d) = ", Gia_ObjId(p->pAig, pVar), Tas_VarValue(pVar) ); if ( Gia_ObjIsCi(pVar) ) @@ -443,7 +443,7 @@ static inline int Tas_VarFaninFanoutMax( Tas_Man_t * p, Gia_Obj_t * pObj ) assert( Gia_ObjIsAnd(pObj) ); Count0 = Gia_ObjRefs( p->pAig, Gia_ObjFanin0(pObj) ); Count1 = Gia_ObjRefs( p->pAig, Gia_ObjFanin1(pObj) ); - return ABC_MAX( Count0, Count1 ); + return Abc_MaxInt( Count0, Count1 ); } @@ -793,11 +793,11 @@ static inline void Tas_ManDeriveReason( Tas_Man_t * p, int Level ) if ( Tas_VarHasReasonCls( p, pObj ) ) { Tas_Cls_t * pCls = Tas_VarReasonCls( p, pObj ); - pReason = Gia_ManObj( p->pAig, Gia_Lit2Var(pCls->pLits[0]) ); + pReason = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[0]) ); assert( pReason == pObj ); for ( j = 1; j < pCls->nLits; j++ ) { - pReason = Gia_ManObj( p->pAig, Gia_Lit2Var(pCls->pLits[j]) ); + pReason = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[j]) ); iLitLevel2 = Tas_VarDecLevel( p, pReason ); assert( Tas_VarIsAssigned( pReason ) ); assert( !Tas_LitIsTrue( pReason, pCls->pLits[j] ) ); @@ -953,16 +953,16 @@ static inline Tas_Cls_t * Tas_ManAllocCls( Tas_Man_t * p, int nSize ) ***********************************************************************/ static inline void Tas_ManWatchClause( Tas_Man_t * p, Tas_Cls_t * pClause, int Lit ) { - assert( Gia_Lit2Var(Lit) < Gia_ManObjNum(p->pAig) ); + assert( Abc_Lit2Var(Lit) < Gia_ManObjNum(p->pAig) ); assert( pClause->nLits >= 2 ); assert( pClause->pLits[0] == Lit || pClause->pLits[1] == Lit ); if ( pClause->pLits[0] == Lit ) - pClause->iNext[0] = p->pWatches[Gia_LitNot(Lit)]; + pClause->iNext[0] = p->pWatches[Abc_LitNot(Lit)]; else - pClause->iNext[1] = p->pWatches[Gia_LitNot(Lit)]; - if ( p->pWatches[Gia_LitNot(Lit)] == 0 ) - Vec_IntPush( p->vWatchLits, Gia_LitNot(Lit) ); - p->pWatches[Gia_LitNot(Lit)] = Tas_ClsHandle( p, pClause ); + pClause->iNext[1] = p->pWatches[Abc_LitNot(Lit)]; + if ( p->pWatches[Abc_LitNot(Lit)] == 0 ) + Vec_IntPush( p->vWatchLits, Abc_LitNot(Lit) ); + p->pWatches[Abc_LitNot(Lit)] = Tas_ClsHandle( p, pClause ); } /**Function************************************************************* @@ -994,7 +994,7 @@ static inline Tas_Cls_t * Tas_ManCreateCls( Tas_Man_t * p, int hClause ) for ( i = hClause; (pObj = pQue->pData[i]); i++ ) { assert( Tas_VarIsAssigned( pObj ) ); - pClause->pLits[i-hClause] = Gia_LitNot( Tas_VarToLit(p, pObj) ); + pClause->pLits[i-hClause] = Abc_LitNot( Tas_VarToLit(p, pObj) ); } // add the clause as watched one if ( nLits >= 2 ) @@ -1027,7 +1027,7 @@ static inline int Tas_ManCreateFromCls( Tas_Man_t * p, Tas_Cls_t * pCls, int Lev Tas_QuePush( pQue, NULL ); for ( i = 0; i < pCls->nLits; i++ ) { - pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCls->pLits[i]) ); + pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCls->pLits[i]) ); assert( Tas_VarIsAssigned(pObj) ); assert( !Tas_LitIsTrue( pObj, pCls->pLits[i] ) ); Tas_QuePush( pQue, pObj ); @@ -1052,7 +1052,7 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit ) Gia_Obj_t * pObj; Tas_Cls_t * pCur; int * piPrev, iCur, iTemp; - int i, LitF = Gia_LitNot(Lit); + int i, LitF = Abc_LitNot(Lit); // iterate through the clauses piPrev = p->pWatches + Lit; for ( iCur = p->pWatches[Lit]; iCur; iCur = *piPrev ) @@ -1070,8 +1070,8 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit ) assert( pCur->pLits[1] == LitF ); // if the first literal is true, the clause is satisfied -// if ( pCur->pLits[0] == p->pAssigns[Gia_Lit2Var(pCur->pLits[0])] ) - pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[0]) ); +// if ( pCur->pLits[0] == p->pAssigns[Abc_Lit2Var(pCur->pLits[0])] ) + pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[0]) ); if ( Tas_VarIsAssigned(pObj) && Tas_LitIsTrue( pObj, pCur->pLits[0] ) ) { piPrev = &pCur->iNext[1]; @@ -1082,8 +1082,8 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit ) for ( i = 2; i < (int)pCur->nLits; i++ ) { // skip the case when the literal is false -// if ( Gia_LitNot(pCur->pLits[i]) == p->pAssigns[Gia_Lit2Var(pCur->pLits[i])] ) - pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[i]) ); +// if ( Abc_LitNot(pCur->pLits[i]) == p->pAssigns[Abc_Lit2Var(pCur->pLits[i])] ) + pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[i]) ); if ( Tas_VarIsAssigned(pObj) && !Tas_LitIsTrue( pObj, pCur->pLits[i] ) ) continue; // the literal is either true or unassigned - watch it @@ -1099,7 +1099,7 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit ) continue; // clause is unit - enqueue new implication - pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[0]) ); + pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[0]) ); if ( !Tas_VarIsAssigned(pObj) ) { /* @@ -1107,7 +1107,7 @@ static inline int Tas_ManPropagateWatch( Tas_Man_t * p, int Level, int Lit ) int iLitLevel, iPlace; for ( i = 1; i < (int)pCur->nLits; i++ ) { - pObj = Gia_ManObj( p->pAig, Gia_Lit2Var(pCur->pLits[i]) ); + pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(pCur->pLits[i]) ); iLitLevel = Tas_VarDecLevel( p, pObj ); iPlace = pObj->Value; printf( "Lit = %d. Level = %d. Place = %d.\n", pCur->pLits[i], iLitLevel, iPlace ); @@ -1300,7 +1300,7 @@ int Tas_ManSolve_rec( Tas_Man_t * p, int Level ) if ( Tas_QueIsEmpty(&p->pJust) ) return 0; // quit using resource limits - p->Pars.nJustThis = ABC_MAX( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead ); + p->Pars.nJustThis = Abc_MaxInt( p->Pars.nJustThis, p->pJust.iTail - p->pJust.iHead ); if ( Tas_ManCheckLimits( p ) ) return 0; // remember the state before branching @@ -1401,7 +1401,7 @@ int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ) Vec_IntClear( p->vActiveVars ); // statistics p->Pars.nBTTotal += p->Pars.nBTThis; - p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis ); + p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis ); if ( Tas_ManCheckLimits( p ) ) RetValue = -1; return RetValue; @@ -1460,7 +1460,7 @@ int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs ) Vec_IntClear( p->vActiveVars ); // statistics p->Pars.nBTTotal += p->Pars.nBTThis; - p->Pars.nJustTotal = ABC_MAX( p->Pars.nJustTotal, p->Pars.nJustThis ); + p->Pars.nJustTotal = Abc_MaxInt( p->Pars.nJustTotal, p->Pars.nJustThis ); if ( Tas_ManCheckLimits( p ) ) RetValue = -1; @@ -1644,19 +1644,19 @@ int Tas_StorePatternTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * p int i; for ( i = 0; i < nLits; i++ ) { - pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - if ( Gia_InfoHasBit( pPres, iBit ) && - Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i])); + pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i])); + if ( Abc_InfoHasBit( pPres, iBit ) && + Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) ) return 0; } for ( i = 0; i < nLits; i++ ) { - pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - Gia_InfoSetBit( pPres, iBit ); - if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) - Gia_InfoXorBit( pInfo, iBit ); + pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i])); + pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i])); + Abc_InfoSetBit( pPres, iBit ); + if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) ) + Abc_InfoXorBit( pInfo, iBit ); } return 1; } diff --git a/src/aig/gia/giaCof.c b/src/aig/gia/giaCof.c index 5a04d9d3..60dcf3af 100644 --- a/src/aig/gia/giaCof.c +++ b/src/aig/gia/giaCof.c @@ -457,7 +457,7 @@ int Cof_ManCountRemoved( Cof_Man_t * p, Cof_Obj_t * pRoot, int fConst1 ) pRoot->iNext = 0; p->pLevels[LevelStart] = Cof_ObjHandle( p, pRoot ); // set the new literal - pRoot->iLit = Gia_Var2Lit( 0, fConst1 ); + pRoot->iLit = Abc_Var2Lit( 0, fConst1 ); // process nodes in the levelized order for ( i = LevelStart; i < p->nLevels; i++ ) { @@ -465,7 +465,7 @@ int Cof_ManCountRemoved( Cof_Man_t * p, Cof_Obj_t * pRoot, int fConst1 ) iHandle && (pTemp = Cof_ManObj(p, iHandle)); iHandle = pTemp->iNext ) { - assert( pTemp->Id != Gia_Lit2Var(pTemp->iLit) ); + assert( pTemp->Id != Abc_Lit2Var(pTemp->iLit) ); Cof_ObjForEachFanout( pTemp, pNext, k ) { if ( Cof_ObjIsCo(pNext) ) @@ -477,11 +477,11 @@ int Cof_ManCountRemoved( Cof_Man_t * p, Cof_Obj_t * pRoot, int fConst1 ) assert( pFanin0 == pTemp || pFanin1 == pTemp ); pNextGia = Gia_ManObj( p->pGia, pNext->Id ); if ( Cof_ObjIsTravIdCurrent(p, pFanin0) ) - iLit0 = Gia_LitNotCond( pFanin0->iLit, Gia_ObjFaninC0(pNextGia) ); + iLit0 = Abc_LitNotCond( pFanin0->iLit, Gia_ObjFaninC0(pNextGia) ); else iLit0 = Gia_ObjFaninLit0( pNextGia, pNext->Id ); if ( Cof_ObjIsTravIdCurrent(p, pFanin1) ) - iLit1 = Gia_LitNotCond( pFanin1->iLit, Gia_ObjFaninC1(pNextGia) ); + iLit1 = Abc_LitNotCond( pFanin1->iLit, Gia_ObjFaninC1(pNextGia) ); else iLit1 = Gia_ObjFaninLit1( pNextGia, pNext->Id ); iNextNew = Gia_ManHashAndTry( p->pGia, iLit0, iLit1 ); @@ -578,12 +578,12 @@ void Cof_ManPrintFanio( Cof_Man_t * p ) nFanouts = Cof_ObjFanoutNum(pNode); nFaninsAll += nFanins; nFanoutsAll += nFanouts; - nFaninsMax = ABC_MAX( nFaninsMax, nFanins ); - nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts ); + nFaninsMax = Abc_MaxInt( nFaninsMax, nFanins ); + nFanoutsMax = Abc_MaxInt( nFanoutsMax, nFanouts ); } // allocate storage for fanin/fanout numbers - nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) ); + nSizeMax = Abc_MaxInt( 10 * (Abc_Base10Log(nFaninsMax) + 1), 10 * (Abc_Base10Log(nFanoutsMax) + 1) ); vFanins = Vec_IntStart( nSizeMax ); vFanouts = Vec_IntStart( nSizeMax ); @@ -717,7 +717,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar ) return NULL; } pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; @@ -728,7 +728,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar ) if ( pObj == pPivot ) { iCofVar = pObj->Value; - pObj->Value = Gia_Var2Lit( 0, 0 ); + pObj->Value = Abc_Var2Lit( 0, 0 ); } } Gia_ManForEachAnd( p, pObj, i ) @@ -737,7 +737,7 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar ) if ( pObj == pPivot ) { iCofVar = pObj->Value; - pObj->Value = Gia_Var2Lit( 0, 0 ); + pObj->Value = Abc_Var2Lit( 0, 0 ); } } Gia_ManForEachCo( p, pObj, i ) @@ -745,15 +745,15 @@ Gia_Man_t * Gia_ManDupCofInt( Gia_Man_t * p, int iVar ) // compute the positive cofactor Gia_ManForEachCi( p, pObj, i ) { - pObj->Value = Gia_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 ); + pObj->Value = Abc_Var2Lit( Gia_ObjId(pNew, Gia_ManCi(pNew, i)), 0 ); if ( pObj == pPivot ) - pObj->Value = Gia_Var2Lit( 0, 1 ); + pObj->Value = Abc_Var2Lit( 0, 1 ); } Gia_ManForEachAnd( p, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); if ( pObj == pPivot ) - pObj->Value = Gia_Var2Lit( 0, 1 ); + pObj->Value = Abc_Var2Lit( 0, 1 ); } // create MUXes assert( iCofVar > 0 ); @@ -836,9 +836,9 @@ Vec_Int_t * Gia_ManTransfer( Gia_Man_t * pAig, Gia_Man_t * pCof, Gia_Man_t * pNe Gia_ManForEachObjVec( vSigs, pAig, pObj, i ) { assert( Gia_ObjIsCand(pObj) ); - pObjF = Gia_ManObj( pCof, Gia_Lit2Var(pObj->Value) ); + pObjF = Gia_ManObj( pCof, Abc_Lit2Var(pObj->Value) ); if ( pObjF->Value && ~pObjF->Value ) - Vec_IntPushUnique( vSigsNew, Gia_Lit2Var(pObjF->Value) ); + Vec_IntPushUnique( vSigsNew, Abc_Lit2Var(pObjF->Value) ); } return vSigsNew; } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 258687fe..b3c04acb 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -55,14 +55,14 @@ void Gia_ManDupRemapEquiv( Gia_Man_t * pNew, Gia_Man_t * p ) Gia_ObjSetRepr( pNew, i, GIA_VOID ); // iterate over constant candidates Gia_ManForEachConst( p, i ) - Gia_ObjSetRepr( pNew, Gia_Lit2Var(Gia_ManObj(p, i)->Value), 0 ); + Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 ); // iterate over class candidates vClass = Vec_IntAlloc( 100 ); Gia_ManForEachClass( p, i ) { Vec_IntClear( vClass ); Gia_ClassForEachObj( p, i, k ) - Vec_IntPushUnique( vClass, Gia_Lit2Var(Gia_ManObj(p, k)->Value) ); + Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) ); assert( Vec_IntSize( vClass ) > 1 ); Vec_IntSort( vClass, 0 ); iRepr = iPrev = Vec_IntEntry( vClass, 0 ); @@ -173,7 +173,7 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ) int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCo( p, pObj, i ) Gia_ManDupOrderDfs_rec( pNew, p, pObj ); @@ -205,7 +205,7 @@ Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop ) int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; for ( i = iOutStart; i < iOutStop; i++ ) { @@ -240,8 +240,8 @@ void Gia_ManDupOrderDfsChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); if ( pNext ) { - pNew->pNexts[Gia_Lit2Var(pObj->Value)] = Gia_Lit2Var( Gia_Lit2Var(pNext->Value) ); - assert( Gia_Lit2Var(pObj->Value) > Gia_Lit2Var(pNext->Value) ); + pNew->pNexts[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var( Abc_Lit2Var(pNext->Value) ); + assert( Abc_Lit2Var(pObj->Value) > Abc_Lit2Var(pNext->Value) ); } } @@ -264,7 +264,7 @@ Gia_Man_t * Gia_ManDupOrderDfsChoices( Gia_Man_t * p ) assert( p->pReprs && p->pNexts ); Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) @@ -297,7 +297,7 @@ Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ) int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCoReverse( p, pObj, i ) Gia_ManDupOrderDfs_rec( pNew, p, pObj ); @@ -329,7 +329,7 @@ Gia_Man_t * Gia_ManDupOrderAiger( Gia_Man_t * p ) Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -361,7 +361,7 @@ Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ) Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachObj1( p, pObj, i ) { @@ -371,13 +371,13 @@ Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ) { pObj->Value = Gia_ManAppendCi( pNew ); if ( Gia_ObjCioId(pObj) >= Gia_ManPiNum(p) ) - pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPiNum(p)) ); + pObj->Value = Abc_LitNotCond( pObj->Value, Abc_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPiNum(p)) ); } else if ( Gia_ObjIsCo(pObj) ) { pObj->Value = Gia_ObjFanin0Copy(pObj); if ( Gia_ObjCioId(pObj) >= Gia_ManPoNum(p) ) - pObj->Value = Gia_LitNotCond( pObj->Value, Gia_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPoNum(p)) ); + pObj->Value = Abc_LitNotCond( pObj->Value, Abc_InfoHasBit((unsigned *)pInitState, Gia_ObjCioId(pObj) - Gia_ManPoNum(p)) ); pObj->Value = Gia_ManAppendCo( pNew, pObj->Value ); } } @@ -403,7 +403,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p ) Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachObj1( p, pObj, i ) { @@ -437,7 +437,7 @@ Gia_Man_t * Gia_ManDupSelf( Gia_Man_t * p ) Gia_Obj_t * pObj; int i, iCtrl; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; @@ -477,7 +477,7 @@ Gia_Man_t * Gia_ManDupFlopClass( Gia_Man_t * p, int iClass ) int i, Counter1 = 0, Counter2 = 0; assert( p->vFlopClasses != NULL ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachPi( p, pObj, i ) @@ -522,7 +522,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ) Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->nConstrs = p->nConstrs; - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachObj1( p, pObj, i ) { @@ -561,8 +561,8 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ) // assert( ~pRepr->Value ); if ( !~pRepr->Value ) continue; - if ( Gia_Lit2Var(pObj->Value) != Gia_Lit2Var(pRepr->Value) ) - Gia_ObjSetRepr( pNew, Gia_Lit2Var(pObj->Value), Gia_Lit2Var(pRepr->Value) ); + if ( Abc_Lit2Var(pObj->Value) != Abc_Lit2Var(pRepr->Value) ) + Gia_ObjSetRepr( pNew, Abc_Lit2Var(pObj->Value), Abc_Lit2Var(pRepr->Value) ); } pNew->pNexts = Gia_ManDeriveNexts( pNew ); } @@ -588,7 +588,7 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes ) int i, t, Entry; assert( nTimes > 0 ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; vPis = Vec_IntAlloc( Gia_ManPiNum(p) * nTimes ); vPos = Vec_IntAlloc( Gia_ManPoNum(p) * nTimes ); @@ -604,17 +604,17 @@ Gia_Man_t * Gia_ManDupTimes( Gia_Man_t * p, int nTimes ) { pObj->Value = Gia_ManAppendCi( pNew ); if ( Gia_ObjIsPi(p, pObj) ) - Vec_IntPush( vPis, Gia_Lit2Var(pObj->Value) ); + Vec_IntPush( vPis, Abc_Lit2Var(pObj->Value) ); else - Vec_IntPush( vRos, Gia_Lit2Var(pObj->Value) ); + Vec_IntPush( vRos, Abc_Lit2Var(pObj->Value) ); } else if ( Gia_ObjIsCo(pObj) ) { pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); if ( Gia_ObjIsPo(p, pObj) ) - Vec_IntPush( vPos, Gia_Lit2Var(pObj->Value) ); + Vec_IntPush( vPos, Abc_Lit2Var(pObj->Value) ); else - Vec_IntPush( vRis, Gia_Lit2Var(pObj->Value) ); + Vec_IntPush( vRis, Abc_Lit2Var(pObj->Value) ); } } } @@ -667,7 +667,7 @@ int Gia_ManDupDfs2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) { Gia_Obj_t * pRepr = Gia_ManObj( p, p->pReprsOld[Gia_ObjId(p, pObj)] ); pRepr->Value = Gia_ManDupDfs2_rec( pNew, p, pRepr ); - return pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + return pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); } if ( Gia_ObjIsCi(pObj) ) return pObj->Value = Gia_ManAppendCi(pNew); @@ -698,7 +698,7 @@ Gia_Man_t * Gia_ManDupDfs2( Gia_Man_t * p ) int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCo( p, pObj, i ) Gia_ManDupDfs2_rec( pNew, p, pObj ); @@ -756,7 +756,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p ) Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) @@ -789,7 +789,7 @@ Gia_Man_t * Gia_ManDupDfsSkip( Gia_Man_t * p ) int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -819,7 +819,7 @@ Gia_Man_t * Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pRoot ) assert( Gia_ObjIsCo(pRoot) ); Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -847,14 +847,14 @@ Gia_Man_t * Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits ) int i, iLit, iLitRes; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); Vec_IntForEachEntry( vLits, iLit, i ) { - iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) ); - Gia_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) ); + iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Abc_Lit2Var(iLit)) ); + Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iLit)) ); } Gia_ManSetRegNum( pNew, 0 ); return pNew; @@ -877,7 +877,7 @@ Gia_Man_t * Gia_ManDupNormalized( Gia_Man_t * p ) Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -908,7 +908,7 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos ) int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManSetRefs( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) @@ -943,7 +943,7 @@ Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 ) assert( Gia_ManRegNum(p) == 0 ); assert( Gia_ManRegNum(p2) == 0 ); pNew = Gia_ManStart( Gia_ManObjNum(p)+Gia_ManObjNum(p2) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); // dup first AIG Gia_ManConst0(p)->Value = 0; @@ -1005,13 +1005,13 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits int i; Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) { pObj->Value = Gia_ManAppendCi(pNew); if ( ~pCi2Lit[i] ) - pObj->Value = Gia_LitNotCond( Gia_ManObj(p, Gia_Lit2Var(pCi2Lit[i]))->Value, Gia_LitIsCompl(pCi2Lit[i]) ); + pObj->Value = Abc_LitNotCond( Gia_ManObj(p, Abc_Lit2Var(pCi2Lit[i]))->Value, Abc_LitIsCompl(pCi2Lit[i]) ); } Gia_ManHashAlloc( pNew ); if ( vLits ) @@ -1019,8 +1019,8 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits int iLit, iLitRes; Vec_IntForEachEntry( vLits, iLit, i ) { - iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Gia_Lit2Var(iLit)) ); - Gia_ManAppendCo( pNew, Gia_LitNotCond( iLitRes, Gia_LitIsCompl(iLit)) ); + iLitRes = Gia_ManDupDfs2_rec( pNew, p, Gia_ManObj(p, Abc_Lit2Var(iLit)) ); + Gia_ManAppendCo( pNew, Abc_LitNotCond( iLitRes, Abc_LitIsCompl(iLit)) ); } } else @@ -1055,7 +1055,7 @@ Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p ) assert( p->pReprsOld != NULL ); Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -1112,7 +1112,7 @@ Gia_Man_t * Gia_ManDupTopAnd_iter( Gia_Man_t * p, int fVerbose ) { if ( Gia_ObjIsCi(pObj) ) { - Vec_IntPush( vLeaves, Gia_Var2Lit( Gia_ObjId(p, pObj), 0 ) ); + Vec_IntPush( vLeaves, Abc_Var2Lit( Gia_ObjId(p, pObj), 0 ) ); continue; } assert( Gia_ObjIsAnd(pObj) ); @@ -1132,16 +1132,16 @@ Gia_Man_t * Gia_ManDupTopAnd_iter( Gia_Man_t * p, int fVerbose ) pVar2Val = ABC_FALLOC( char, Gia_ManObjNum(p) ); Vec_IntForEachEntry( vLeaves, iLit, i ) { - iObjId = Gia_Lit2Var(iLit); + iObjId = Abc_Lit2Var(iLit); pObj = Gia_ManObj(p, iObjId); if ( Gia_ObjIsCi(pObj) ) { - pCi2Lit[Gia_ObjCioId(pObj)] = !Gia_LitIsCompl(iLit); + pCi2Lit[Gia_ObjCioId(pObj)] = !Abc_LitIsCompl(iLit); nCiLits++; } if ( pVar2Val[iObjId] != 0 && pVar2Val[iObjId] != 1 ) - pVar2Val[iObjId] = Gia_LitIsCompl(iLit); - else if ( pVar2Val[iObjId] != Gia_LitIsCompl(iLit) ) + pVar2Val[iObjId] = Abc_LitIsCompl(iLit); + else if ( pVar2Val[iObjId] != Abc_LitIsCompl(iLit) ) break; } if ( i < Vec_IntSize(vLeaves) ) @@ -1156,7 +1156,7 @@ Gia_Man_t * Gia_ManDupTopAnd_iter( Gia_Man_t * p, int fVerbose ) Vec_IntClear( vLeaves ); Gia_ManForEachObj( p, pObj, i ) if ( !Gia_ObjIsCi(pObj) && (pVar2Val[i] == 0 || pVar2Val[i] == 1) ) - Vec_IntPush( vLeaves, Gia_Var2Lit(i, pVar2Val[i]) ); + Vec_IntPush( vLeaves, Abc_Var2Lit(i, pVar2Val[i]) ); if ( fVerbose ) printf( "Detected %6d AND leaves and %6d CI leaves.\n", Vec_IntSize(vLeaves), nCiLits ); // create the input map @@ -1272,7 +1272,7 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int fDualOut, int fSeq } // start the manager pNew = Gia_ManStart( Gia_ManObjNum(p0) + Gia_ManObjNum(p1) ); - pNew->pName = Gia_UtilStrsav( "miter" ); + pNew->pName = Abc_UtilStrsav( "miter" ); // map combinational inputs Gia_ManFillValue( p0 ); Gia_ManFillValue( p1 ); @@ -1372,7 +1372,7 @@ Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ) int i, iLit; assert( (Gia_ManPoNum(p) & 1) == 0 ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManHashAlloc( pNew ); Gia_ManForEachCi( p, pObj, i ) @@ -1444,7 +1444,7 @@ Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ) } // start the new manager pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) ); - pNew->pName = Gia_UtilStrsav( pGia0->pName ); + pNew->pName = Abc_UtilStrsav( pGia0->pName ); // create new CIs and assign them to the old manager CIs for ( k = 0; k < Gia_ManCiNum(pGia0); k++ ) { @@ -1485,7 +1485,7 @@ Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ) Gia_Obj_t * pObj; int i, nConstr = 0; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -1546,7 +1546,7 @@ Gia_Man_t * Gia_ManDupAbsFlops( Gia_Man_t * p, Vec_Int_t * vFlopClasses ) Gia_ManFillValue( p ); // start the new manager pNew = Gia_ManStart( 5000 ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); // create PIs Gia_ManConst0(p)->Value = 0; Gia_ManForEachPi( p, pObj, i ) @@ -1647,7 +1647,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ) // start the new manager pNew = Gia_ManStart( 5000 ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); // create constant Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; @@ -1681,7 +1681,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ) { if ( !~pObj->Value ) continue; - assert( !Gia_LitIsCompl(pObj->Value) ); + assert( !Abc_LitIsCompl(pObj->Value) ); pCopy = Gia_ObjCopy( pTemp, pObj ); if ( !~pCopy->Value ) { @@ -1689,7 +1689,7 @@ Gia_Man_t * Gia_ManDupAbsGates( Gia_Man_t * p, Vec_Int_t * vGateClasses ) pObj->Value = ~0; continue; } - assert( !Gia_LitIsCompl(pCopy->Value) ); + assert( !Abc_LitIsCompl(pCopy->Value) ); pObj->Value = pCopy->Value; } } diff --git a/src/aig/gia/giaEmbed.c b/src/aig/gia/giaEmbed.c index 5c7092a3..1daf52a1 100644 --- a/src/aig/gia/giaEmbed.c +++ b/src/aig/gia/giaEmbed.c @@ -20,7 +20,7 @@ #include <math.h> #include "gia.h" -#include "ioa.h" +#include "src/aig/ioa/ioa.h" ABC_NAMESPACE_IMPL_START @@ -690,12 +690,12 @@ void Emb_ManPrintFanio( Emb_Man_t * p ) nFanouts = Emb_ObjFanoutNum(pNode); nFaninsAll += nFanins; nFanoutsAll += nFanouts; - nFaninsMax = ABC_MAX( nFaninsMax, nFanins ); - nFanoutsMax = ABC_MAX( nFanoutsMax, nFanouts ); + nFaninsMax = Abc_MaxInt( nFaninsMax, nFanins ); + nFanoutsMax = Abc_MaxInt( nFanoutsMax, nFanouts ); } // allocate storage for fanin/fanout numbers - nSizeMax = ABC_MAX( 10 * (Gia_Base10Log(nFaninsMax) + 1), 10 * (Gia_Base10Log(nFanoutsMax) + 1) ); + nSizeMax = Abc_MaxInt( 10 * (Abc_Base10Log(nFaninsMax) + 1), 10 * (Abc_Base10Log(nFanoutsMax) + 1) ); vFanins = Vec_IntStart( nSizeMax ); vFanouts = Vec_IntStart( nSizeMax ); @@ -1436,8 +1436,8 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols ) pY0 = Emb_ManSol( p, 0 ); for ( k = 0; k < p->nObjs; k++ ) { - Min0 = ABC_MIN( Min0, pY0[k] ); - Max0 = ABC_MAX( Max0, pY0[k] ); + Min0 = Abc_MinInt( Min0, pY0[k] ); + Max0 = Abc_MaxInt( Max0, pY0[k] ); } Str0 = 1.0*GIA_PLACE_SIZE/(Max0 - Min0); // update the coordinates @@ -1450,8 +1450,8 @@ void Emb_ManDerivePlacement( Emb_Man_t * p, int nSols ) pY1 = Emb_ManSol( p, 1 ); for ( k = 0; k < p->nObjs; k++ ) { - Min1 = ABC_MIN( Min1, pY1[k] ); - Max1 = ABC_MAX( Max1, pY1[k] ); + Min1 = Abc_MinInt( Min1, pY1[k] ); + Max1 = Abc_MaxInt( Max1, pY1[k] ); } Str1 = 1.0*GIA_PLACE_SIZE/(Max1 - Min1); // update the coordinates @@ -1498,10 +1498,10 @@ double Emb_ManComputeHPWL( Emb_Man_t * p ) iMinY = iMaxY = p->pPlacement[2*pThis->Value+1]; Emb_ObjForEachFanout( pThis, pNext, k ) { - iMinX = ABC_MIN( iMinX, p->pPlacement[2*pNext->Value+0] ); - iMaxX = ABC_MAX( iMaxX, p->pPlacement[2*pNext->Value+0] ); - iMinY = ABC_MIN( iMinY, p->pPlacement[2*pNext->Value+1] ); - iMaxY = ABC_MAX( iMaxY, p->pPlacement[2*pNext->Value+1] ); + iMinX = Abc_MinInt( iMinX, p->pPlacement[2*pNext->Value+0] ); + iMaxX = Abc_MaxInt( iMaxX, p->pPlacement[2*pNext->Value+0] ); + iMinY = Abc_MinInt( iMinY, p->pPlacement[2*pNext->Value+1] ); + iMaxY = Abc_MaxInt( iMaxY, p->pPlacement[2*pNext->Value+1] ); } Result += (iMaxX - iMinX) + (iMaxY - iMinY); } @@ -1548,10 +1548,10 @@ void Emb_ManPlacementRefine( Emb_Man_t * p, int nIters, int fVerbose ) iMinY = iMaxY = p->pPlacement[2*pThis->Value+1]; Emb_ObjForEachFanout( pThis, pNext, k ) { - iMinX = ABC_MIN( iMinX, p->pPlacement[2*pNext->Value+0] ); - iMaxX = ABC_MAX( iMaxX, p->pPlacement[2*pNext->Value+0] ); - iMinY = ABC_MIN( iMinY, p->pPlacement[2*pNext->Value+1] ); - iMaxY = ABC_MAX( iMaxY, p->pPlacement[2*pNext->Value+1] ); + iMinX = Abc_MinInt( iMinX, p->pPlacement[2*pNext->Value+0] ); + iMaxX = Abc_MaxInt( iMaxX, p->pPlacement[2*pNext->Value+0] ); + iMinY = Abc_MinInt( iMinY, p->pPlacement[2*pNext->Value+1] ); + iMaxY = Abc_MaxInt( iMaxY, p->pPlacement[2*pNext->Value+1] ); } pEdgeX[pThis->Value] = 0.5 * (iMaxX + iMinX); pEdgeY[pThis->Value] = 0.5 * (iMaxY + iMinY); diff --git a/src/aig/gia/giaEnable.c b/src/aig/gia/giaEnable.c index 37f0c94f..d23c0c3d 100644 --- a/src/aig/gia/giaEnable.c +++ b/src/aig/gia/giaEnable.c @@ -338,9 +338,9 @@ Vec_Int_t * Gia_ManTransferFrames( Gia_Man_t * pAig, Gia_Man_t * pFrames, int nF assert( Gia_ObjIsCand(pObj) ); for ( f = 0; f < nFrames; f++ ) { - pObjF = Gia_ManObj( pFrames, Gia_Lit2Var(Gia_ObjCopyF( pAig, f, pObj )) ); + pObjF = Gia_ManObj( pFrames, Abc_Lit2Var(Gia_ObjCopyF( pAig, f, pObj )) ); if ( pObjF->Value && ~pObjF->Value ) - Vec_IntPushUnique( vSigsNew, Gia_Lit2Var(pObjF->Value) ); + Vec_IntPushUnique( vSigsNew, Abc_Lit2Var(pObjF->Value) ); } } return vSigsNew; @@ -365,7 +365,7 @@ Gia_Man_t * Gia_ManUnrollInit( Gia_Man_t * p, int nFrames ) ABC_FREE( p->pCopies ); p->pCopies = ABC_FALLOC( int, nFrames * Gia_ManObjNum(p) ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManForEachRo( p, pObj, i ) Gia_ObjSetCopyF( p, 0, pObj, 0 ); @@ -440,7 +440,7 @@ Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p ) Gia_Obj_t * pThis, * pNode; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; @@ -481,13 +481,13 @@ Gia_Man_t * Gia_ManRemoveEnables2( Gia_Man_t * p ) { // printf( "FlopIn compl = %d. FlopOut is d0. Complement = %d.\n", // Gia_ObjFaninC0(pFlopIn), Gia_IsComplement(pObj0) ); - pFlopIn->Value = Gia_LitNotCond(Gia_Regular(pObj1)->Value, !Gia_IsComplement(pObj1)); + pFlopIn->Value = Abc_LitNotCond(Gia_Regular(pObj1)->Value, !Gia_IsComplement(pObj1)); } else if ( Gia_Regular(pObj1) == pFlopOut ) { // printf( "FlopIn compl = %d. FlopOut is d1. Complement = %d.\n", // Gia_ObjFaninC0(pFlopIn), Gia_IsComplement(pObj1) ); - pFlopIn->Value = Gia_LitNotCond(Gia_Regular(pObj0)->Value, !Gia_IsComplement(pObj0)); + pFlopIn->Value = Abc_LitNotCond(Gia_Regular(pObj0)->Value, !Gia_IsComplement(pObj0)); } } Gia_ManForEachCo( p, pThis, i ) @@ -610,7 +610,7 @@ Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p ) pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachObj1( p, pObj, i ) { @@ -627,7 +627,7 @@ Gia_Man_t * Gia_ManRemoveEnables( Gia_Man_t * p ) if ( pData == NULL ) pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); else - pObj->Value = Gia_ManAppendCo( pNew, Gia_LitNotCond(Gia_Regular(pData)->Value, Gia_IsComplement(pData)) ); + pObj->Value = Gia_ManAppendCo( pNew, Abc_LitNotCond(Gia_Regular(pData)->Value, Gia_IsComplement(pData)) ); } Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); Vec_PtrFree( vDatas ); diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index c93da86e..43724871 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "gia.h" -#include "cec.h" +#include "src/proof/cec/cec.h" ABC_NAMESPACE_IMPL_START @@ -417,7 +417,7 @@ void Gia_ManEquivReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, if ( (pRepr = Gia_ManEquivRepr(p, pObj, fUseAll, fDualOut)) ) { Gia_ManEquivReduce_rec( pNew, p, pRepr, fUseAll, fDualOut ); - pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } if ( ~pObj->Value ) @@ -474,7 +474,7 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV if ( fDualOut ) Gia_ManEquivSetColors( p, fVerbose ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) @@ -536,7 +536,7 @@ void Gia_ManEquivUpdatePointers( Gia_Man_t * p, Gia_Man_t * pNew ) { if ( !~pObj->Value ) continue; - pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) ); + pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) ); if ( pObjNew->fMark0 ) pObj->Value = ~0; } @@ -568,10 +568,10 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina pObj = Gia_ManObj( p, i ); if ( !~pObj->Value ) continue; - pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) ); - if ( Gia_Lit2Var(pObjNew->Value) == 0 ) + pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) ); + if ( Abc_Lit2Var(pObjNew->Value) == 0 ) continue; - Gia_ObjSetRepr( pFinal, Gia_Lit2Var(pObjNew->Value), 0 ); + Gia_ObjSetRepr( pFinal, Abc_Lit2Var(pObjNew->Value), 0 ); } // iterate over class candidates vClass = Vec_IntAlloc( 100 ); @@ -583,8 +583,8 @@ void Gia_ManEquivDeriveReprs( Gia_Man_t * p, Gia_Man_t * pNew, Gia_Man_t * pFina pObj = Gia_ManObj( p, k ); if ( !~pObj->Value ) continue; - pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) ); - Vec_IntPushUnique( vClass, Gia_Lit2Var(pObjNew->Value) ); + pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) ); + Vec_IntPushUnique( vClass, Abc_Lit2Var(pObjNew->Value) ); } if ( Vec_IntSize( vClass ) < 2 ) continue; @@ -624,14 +624,14 @@ Gia_Man_t * Gia_ManEquivRemapDfs( Gia_Man_t * p ) Gia_ObjSetRepr( pNew, i, GIA_VOID ); // iterate over constant candidates Gia_ManForEachConst( p, i ) - Gia_ObjSetRepr( pNew, Gia_Lit2Var(Gia_ManObj(p, i)->Value), 0 ); + Gia_ObjSetRepr( pNew, Abc_Lit2Var(Gia_ManObj(p, i)->Value), 0 ); // iterate over class candidates vClass = Vec_IntAlloc( 100 ); Gia_ManForEachClass( p, i ) { Vec_IntClear( vClass ); Gia_ClassForEachObj( p, i, k ) - Vec_IntPushUnique( vClass, Gia_Lit2Var(Gia_ManObj(p, k)->Value) ); + Vec_IntPushUnique( vClass, Abc_Lit2Var(Gia_ManObj(p, k)->Value) ); assert( Vec_IntSize( vClass ) > 1 ); Vec_IntSort( vClass, 0 ); iRepr = iPrev = Vec_IntEntry( vClass, 0 ); @@ -758,7 +758,7 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) ) if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) ) return; - iLitNew = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + iLitNew = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); if ( pObj->Value != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) { if ( vTrace ) @@ -847,7 +847,7 @@ Gia_Man_t * Gia_ManSpecReduceTrace( Gia_Man_t * p, Vec_Int_t * vTrace ) Gia_ManSetPhase( p ); Gia_ManFillValue( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) @@ -917,7 +917,7 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fSynthesis, int if ( fDualOut ) Gia_ManEquivSetColors( p, fVerbose ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) @@ -983,7 +983,7 @@ void Gia_ManSpecBuildInit( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Ve // if ( fDualOut && !Gia_ObjDiffColors( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) ) if ( fDualOut && !Gia_ObjDiffColors2( p, Gia_ObjId(p, pObj), Gia_ObjId(p, pRepr) ) ) return; - iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + iLitNew = Abc_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); if ( Gia_ObjCopyF(p, f, pObj) != iLitNew && !Gia_ObjProved(p, Gia_ObjId(p,pObj)) ) Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, Gia_ObjCopyF(p, f, pObj), iLitNew) ); Gia_ObjSetCopyF( p, f, pObj, iLitNew ); @@ -1063,10 +1063,10 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Abc_Cex_t * pInit, int nFrames if ( fDualOut ) Gia_ManEquivSetColors( p, 0 ); pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManForEachRo( p, pObj, i ) - Gia_ObjSetCopyF( p, 0, pObj, Gia_InfoHasBit(pInit->pData, i) ); + Gia_ObjSetCopyF( p, 0, pObj, Abc_InfoHasBit(pInit->pData, i) ); for ( f = 0; f < nFrames; f++ ) { Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 ); @@ -1463,7 +1463,7 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb { if ( Gia_ObjIsConst0(pRepr) ) { - pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } Gia_ManEquivToChoices_rec( pNew, p, pRepr ); @@ -1471,22 +1471,22 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - if ( Gia_LitRegular(pObj->Value) == Gia_LitRegular(pRepr->Value) ) + if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) ) { - assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) ); + assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) ); return; } if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit return; assert( pRepr->Value < pObj->Value ); - pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) ); - pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) ); + pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) ); + pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) ); if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) ) { // assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew ); if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) != pReprNew ) return; - pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) ) @@ -1495,7 +1495,7 @@ void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) ); Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew ); } - pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } assert( Gia_ObjIsAnd(pObj) ); @@ -1573,7 +1573,7 @@ Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots ) assert( (Gia_ManCoNum(p) % nSnapshots) == 0 ); Gia_ManSetPhase( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) ); for ( i = 0; i < Gia_ManObjNum(p); i++ ) @@ -1654,9 +1654,9 @@ int Gia_ManCountChoices( Gia_Man_t * p ) ABC_NAMESPACE_IMPL_END -#include "aig.h" -#include "saig.h" -#include "cec.h" +#include "src/aig/aig/aig.h" +#include "src/aig/saig/saig.h" +#include "src/proof/cec/cec.h" #include "giaAig.h" ABC_NAMESPACE_IMPL_START @@ -1826,7 +1826,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p { if ( pObj1->Value == ~0 ) continue; - pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj1->Value) ); + pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) ); pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) ); pObj->fMark0 = 1; } @@ -1835,7 +1835,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p { if ( pObj2->Value == ~0 ) continue; - pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj2->Value) ); + pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) ); pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) ); pObj->fMark1 = 1; } @@ -1965,7 +1965,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName { if ( pObj1->Value == ~0 ) continue; - pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj1->Value) ); + pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj1->Value) ); pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) ); pObj->fMark0 = 1; } @@ -1974,7 +1974,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName { if ( pObj2->Value == ~0 ) continue; - pObjM = Gia_ManObj( pMiter, Gia_Lit2Var(pObj2->Value) ); + pObjM = Gia_ManObj( pMiter, Abc_Lit2Var(pObj2->Value) ); pObj = Gia_ManObj( pGia, Gia_ObjId(pMiter, pObjM) ); pObj->fMark1 = 1; } diff --git a/src/aig/gia/giaEra.c b/src/aig/gia/giaEra.c index ec3e1b1b..672149bc 100644 --- a/src/aig/gia/giaEra.c +++ b/src/aig/gia/giaEra.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "gia.h" -#include "mem.h" +#include "src/misc/mem/mem.h" ABC_NAMESPACE_IMPL_START @@ -45,7 +45,7 @@ struct Gia_ManEra_t_ { Gia_Man_t * pAig; // user's AIG manager int nWordsSim; // 2^(PInum) - int nWordsDat; // Gia_BitWordNum + int nWordsDat; // Abc_BitWordNum unsigned * pDataSim; // simulation data Mem_Fixed_t * pMemory; // memory manager Vec_Ptr_t * vStates; // reached states @@ -83,12 +83,12 @@ Gia_ManEra_t * Gia_ManEraCreate( Gia_Man_t * pAig ) int i; p = ABC_CALLOC( Gia_ManEra_t, 1 ); p->pAig = pAig; - p->nWordsSim = Gia_TruthWordNum( Gia_ManPiNum(pAig) ); - p->nWordsDat = Gia_BitWordNum( Gia_ManRegNum(pAig) ); + p->nWordsSim = Abc_TruthWordNum( Gia_ManPiNum(pAig) ); + p->nWordsDat = Abc_BitWordNum( Gia_ManRegNum(pAig) ); p->pDataSim = ABC_ALLOC( unsigned, p->nWordsSim*Gia_ManObjNum(pAig) ); p->pMemory = Mem_FixedStart( sizeof(Gia_ObjEra_t) + sizeof(unsigned) * p->nWordsDat ); p->vStates = Vec_PtrAlloc( 100000 ); - p->nBins = Gia_PrimeCudd( 100000 ); + p->nBins = Abc_PrimeCudd( 100000 ); p->pBins = ABC_CALLOC( unsigned, p->nBins ); Vec_PtrPush( p->vStates, NULL ); // assign primary input values @@ -226,7 +226,7 @@ void Gia_ManEraHashResize( Gia_ManEra_t * p ) // replace the table pBinsOld = p->pBins; nBinsOld = p->nBins; - p->nBins = Gia_PrimeCudd( 3 * p->nBins ); + p->nBins = Abc_PrimeCudd( 3 * p->nBins ); p->pBins = ABC_CALLOC( unsigned, p->nBins ); // rehash the entries from the old table Counter = 0; @@ -266,7 +266,7 @@ void Gia_ManInsertState( Gia_ManEra_t * p, Gia_ObjEra_t * pState ) Gia_ManForEachRo( p->pAig, pObj, i ) { pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) ); - if ( Gia_InfoHasBit(pState->pData, i) ) + if ( Abc_InfoHasBit(pState->pData, i) ) memset( pSimInfo, 0xff, sizeof(unsigned) * p->nWordsSim ); else memset( pSimInfo, 0, sizeof(unsigned) * p->nWordsSim ); @@ -465,8 +465,8 @@ int Gia_ManAnalyzeResult( Gia_ManEra_t * p, Gia_ObjEra_t * pState, int fMiter ) Gia_ManForEachRi( p->pAig, pObj, i ) { pSimInfo = Gia_ManEraData( p, Gia_ObjId(p->pAig, pObj) ); - if ( Gia_InfoHasBit(p->pStateNew->pData, i) != Gia_InfoHasBit(pSimInfo, k) ) - Gia_InfoXorBit( p->pStateNew->pData, i ); + if ( Abc_InfoHasBit(p->pStateNew->pData, i) != Abc_InfoHasBit(pSimInfo, k) ) + Abc_InfoXorBit( p->pStateNew->pData, i ); } piPlace = Gia_ManEraHashFind( p, p->pStateNew ); if ( piPlace == NULL ) diff --git a/src/aig/gia/giaEra2.c b/src/aig/gia/giaEra2.c index b3e516eb..265335e2 100644 --- a/src/aig/gia/giaEra2.c +++ b/src/aig/gia/giaEra2.c @@ -136,11 +136,11 @@ static inline Gia_ObjAre_t * Gia_ObjNextObj0( Gia_ManAre_t * p, Gia_ObjAre_t * static inline Gia_ObjAre_t * Gia_ObjNextObj1( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[1] ); } static inline Gia_ObjAre_t * Gia_ObjNextObj2( Gia_ManAre_t * p, Gia_ObjAre_t * q ) { return Gia_ManAreObj( p, q->F[2] ); } -static inline int Gia_StaHasValue0( Gia_StaAre_t * p, int iReg ) { return Gia_InfoHasBit( p->pData, iReg << 1 ); } -static inline int Gia_StaHasValue1( Gia_StaAre_t * p, int iReg ) { return Gia_InfoHasBit( p->pData, (iReg << 1) + 1 ); } +static inline int Gia_StaHasValue0( Gia_StaAre_t * p, int iReg ) { return Abc_InfoHasBit( p->pData, iReg << 1 ); } +static inline int Gia_StaHasValue1( Gia_StaAre_t * p, int iReg ) { return Abc_InfoHasBit( p->pData, (iReg << 1) + 1 ); } -static inline void Gia_StaSetValue0( Gia_StaAre_t * p, int iReg ) { Gia_InfoSetBit( p->pData, iReg << 1 ); } -static inline void Gia_StaSetValue1( Gia_StaAre_t * p, int iReg ) { Gia_InfoSetBit( p->pData, (iReg << 1) + 1 ); } +static inline void Gia_StaSetValue0( Gia_StaAre_t * p, int iReg ) { Abc_InfoSetBit( p->pData, iReg << 1 ); } +static inline void Gia_StaSetValue1( Gia_StaAre_t * p, int iReg ) { Abc_InfoSetBit( p->pData, (iReg << 1) + 1 ); } static inline Gia_StaAre_t * Gia_StaPrev( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return Gia_ManAreSta(p, pS->iPrev); } static inline Gia_StaAre_t * Gia_StaNext( Gia_ManAre_t * p, Gia_StaAre_t * pS ) { return Gia_ManAreSta(p, pS->iNext); } @@ -198,7 +198,7 @@ void Gia_ManCountMintermsInCube( Gia_StaAre_t * pCube, int nVars, unsigned * pSt for ( i = 0; i < nVars; i++ ) if ( m & (1 << i) ) Mint |= (1 << Dashes[i]); - Gia_InfoSetBit( pStore, Mint ); + Abc_InfoSetBit( pStore, Mint ); } } @@ -220,7 +220,7 @@ int Gia_ManCountMinterms( Gia_ManAre_t * p ) int i, nMemSize, Counter = 0; if ( Gia_ManRegNum(p->pAig) > 30 ) return -1; - nMemSize = Gia_BitWordNum( 1 << Gia_ManRegNum(p->pAig) ); + nMemSize = Abc_BitWordNum( 1 << Gia_ManRegNum(p->pAig) ); pMemory = ABC_CALLOC( unsigned, nMemSize ); Gia_ManAreForEachCubeStore( p, pCube, i ) if ( Gia_StaIsUsed(pCube) ) @@ -477,7 +477,7 @@ Gia_ManAre_t * Gia_ManAreCreate( Gia_Man_t * pAig ) assert( sizeof(Gia_ObjAre_t) == 16 ); p = ABC_CALLOC( Gia_ManAre_t, 1 ); p->pAig = pAig; - p->nWords = Gia_BitWordNum( 2 * Gia_ManRegNum(pAig) ); + p->nWords = Abc_BitWordNum( 2 * Gia_ManRegNum(pAig) ); p->nSize = sizeof(Gia_StaAre_t)/4 + p->nWords; p->ppObjs = ABC_CALLOC( unsigned *, MAX_PAGE_NUM ); p->ppStas = ABC_CALLOC( unsigned *, MAX_PAGE_NUM ); @@ -1421,7 +1421,7 @@ static inline Gia_Obj_t * Gia_ManAreMostUsedPi( Gia_ManAre_t * p ) if ( pObj->Value <= 1 ) continue; Gia_ManIncrementTravId( p->pNew ); - Gia_ManAreMostUsedPi_rec( p->pNew, Gia_ManObj(p->pNew, Gia_Lit2Var(pObj->Value)) ); + Gia_ManAreMostUsedPi_rec( p->pNew, Gia_ManObj(p->pNew, Abc_Lit2Var(pObj->Value)) ); } // check the CI counters Gia_ManForEachCi( p->pNew, pObj, i ) @@ -1471,7 +1471,7 @@ static inline int Gia_ManCheckPOs( Gia_ManAre_t * p ) int i, CountCur, CountMax = 0; Gia_ManForEachPo( p->pAig, pObj, i ) { - pObjNew = Gia_ManObj( p->pNew, Gia_Lit2Var(pObj->Value) ); + pObjNew = Gia_ManObj( p->pNew, Abc_Lit2Var(pObj->Value) ); if ( Gia_ObjIsConst0(pObjNew) ) CountCur = 0; else @@ -1479,7 +1479,7 @@ static inline int Gia_ManCheckPOs( Gia_ManAre_t * p ) Gia_ManIncrementTravId( p->pNew ); CountCur = Gia_ManCheckPOs_rec( p->pNew, pObjNew ); } - CountMax = ABC_MAX( CountMax, CountCur ); + CountMax = Abc_MaxInt( CountMax, CountCur ); } return CountMax; } @@ -1501,10 +1501,10 @@ static inline int Gia_ManCheckPOstatus( Gia_ManAre_t * p ) int i; Gia_ManForEachPo( p->pAig, pObj, i ) { - pObjNew = Gia_ManObj( p->pNew, Gia_Lit2Var(pObj->Value) ); + pObjNew = Gia_ManObj( p->pNew, Abc_Lit2Var(pObj->Value) ); if ( Gia_ObjIsConst0(pObjNew) ) { - if ( Gia_LitIsCompl(pObj->Value) ) + if ( Abc_LitIsCompl(pObj->Value) ) { p->iOutFail = i; return 1; @@ -1638,7 +1638,7 @@ int Gia_ManAreDeriveNexts( Gia_ManAre_t * p, Gia_PtrAre_t Sta ) else if ( Gia_StaHasValue1( pSta, i ) ) pObj->Value = 1; else // don't-care literal - pObj->Value = Gia_Var2Lit( Gia_ObjId( p->pNew, Gia_ManCi(p->pNew, Gia_ObjCioId(pObj)) ), 0 ); + pObj->Value = Abc_Var2Lit( Gia_ObjId( p->pNew, Gia_ManCi(p->pNew, Gia_ObjCioId(pObj)) ), 0 ); } Gia_ManForEachAnd( p->pAig, pObj, i ) pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); @@ -1770,8 +1770,8 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos ABC_NAMESPACE_IMPL_END #include "giaAig.h" -#include "cnf.h" -#include "satSolver.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START @@ -1848,22 +1848,22 @@ void Gia_ManAreDeriveCexSat( Gia_ManAre_t * p, Gia_StaAre_t * pCur, Gia_StaAre_t for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) { if ( Gia_StaHasValue0(pCur, i) ) - Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 1 ) ); + Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 1 ) ); else if ( Gia_StaHasValue1(pCur, i) ) - Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 0 ) ); + Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCis, Gia_ManPiNum(p->pAig)+i), 0 ) ); } if ( pNext ) for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) { if ( Gia_StaHasValue0(pNext, i) ) - Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 1 ) ); + Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 1 ) ); else if ( Gia_StaHasValue1(pNext, i) ) - Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 0 ) ); + Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, Gia_ManPoNum(p->pAig)+i), 0 ) ); } if ( iOutFailed >= 0 ) { assert( iOutFailed < Gia_ManPoNum(p->pAig) ); - Vec_IntPush( p->vAssumps, Gia_Var2Lit( Vec_IntEntry(p->vSatNumCos, iOutFailed), 0 ) ); + Vec_IntPush( p->vAssumps, Abc_Var2Lit( Vec_IntEntry(p->vSatNumCos, iOutFailed), 0 ) ); } // solve SAT status = sat_solver_solve( (sat_solver *)p->pSat, (int *)Vec_IntArray(p->vAssumps), (int *)Vec_IntArray(p->vAssumps) + Vec_IntSize(p->vAssumps), @@ -1935,7 +1935,7 @@ Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast ) Vec_IntForEachEntry( p->vCofVars, Var, v ) { assert( Var < Gia_ManPiNum(p->pAig) ); - Gia_InfoSetBit( pCex->pData, Gia_ManRegNum(p->pAig) + (Vec_PtrSize(vStates)-1-i) * Gia_ManPiNum(p->pAig) + Var ); + Abc_InfoSetBit( pCex->pData, Gia_ManRegNum(p->pAig) + (Vec_PtrSize(vStates)-1-i) * Gia_ManPiNum(p->pAig) + Var ); } } // free temporary things diff --git a/src/aig/gia/giaFanout.c b/src/aig/gia/giaFanout.c index c3e39405..412594ad 100644 --- a/src/aig/gia/giaFanout.c +++ b/src/aig/gia/giaFanout.c @@ -120,7 +120,7 @@ void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ) assert( Gia_ObjId(p, pFanout) > 0 ); if ( Gia_ObjId(p, pObj) >= p->nFansAlloc || Gia_ObjId(p, pFanout) >= p->nFansAlloc ) { - int nFansAlloc = 2 * ABC_MAX( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) ); + int nFansAlloc = 2 * Abc_MaxInt( Gia_ObjId(p, pObj), Gia_ObjId(p, pFanout) ); p->pFanData = ABC_REALLOC( int, p->pFanData, 5 * nFansAlloc ); memset( p->pFanData + 5 * p->nFansAlloc, 0, sizeof(int) * 5 * (nFansAlloc - p->nFansAlloc) ); p->nFansAlloc = nFansAlloc; diff --git a/src/aig/gia/giaForce.c b/src/aig/gia/giaForce.c index b9135404..6927266b 100644 --- a/src/aig/gia/giaForce.c +++ b/src/aig/gia/giaForce.c @@ -609,7 +609,7 @@ int Frc_ManCrossCut_rec( Frc_Man_t * p, Frc_Obj_t * pObj ) Frc_Obj_t * pFanin; int i; p->nCutCur++; - p->nCutMax = ABC_MAX( p->nCutMax, p->nCutCur ); + p->nCutMax = Abc_MaxInt( p->nCutMax, p->nCutCur ); if ( !Frc_ObjIsCi(pObj) ) Frc_ObjForEachFanin( pObj, pFanin, i ) p->nCutCur -= Frc_ManCrossCut_rec( p, pFanin ); @@ -636,7 +636,7 @@ int Frc_ManCrossCut2_rec( Frc_Man_t * p, Frc_Obj_t * pObj ) Frc_Obj_t * pFanin; int i; p->nCutCur++; - p->nCutMax = ABC_MAX( p->nCutMax, p->nCutCur ); + p->nCutMax = Abc_MaxInt( p->nCutMax, p->nCutCur ); if ( !Frc_ObjIsCi(pObj) ) Frc_ObjForEachFaninReverse( pObj, pFanin, i ) p->nCutCur -= Frc_ManCrossCut2_rec( p, pFanin ); @@ -912,8 +912,8 @@ void Frc_ManPlacementRefine( Frc_Man_t * p, int nIters, int fVerbose ) iMinX = iMaxX = pThis->pPlace; Frc_ObjForEachFanout( pThis, pNext, k ) { - iMinX = ABC_MIN( iMinX, pNext->pPlace ); - iMaxX = ABC_MAX( iMaxX, pNext->pPlace ); + iMinX = Abc_MinInt( iMinX, pNext->pPlace ); + iMaxX = Abc_MaxInt( iMaxX, pNext->pPlace ); } pThis->fEdgeCenter = 0.5 * (iMaxX + iMinX); CostThis += (iMaxX - iMinX); diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c index 480326bd..237e6c5c 100644 --- a/src/aig/gia/giaFrames.c +++ b/src/aig/gia/giaFrames.c @@ -90,7 +90,7 @@ void Gia_ManUnrollDup_rec( Gia_Man_t * pNew, Gia_Obj_t * pObj, int Id ) pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } else assert( 0 ); - Gia_ManObj(pNew, Gia_Lit2Var(pObj->Value))->Value = Id; + Gia_ManObj(pNew, Abc_Lit2Var(pObj->Value))->Value = Id; } /**Function************************************************************* @@ -111,7 +111,7 @@ Gia_Man_t * Gia_ManUnrollDup( Gia_Man_t * p, Vec_Int_t * vLimit ) int i; assert( Vec_IntSize(vLimit) == 0 ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); // save constant class Gia_ManFillValue( p ); @@ -161,7 +161,7 @@ Vec_Ptr_t * Gia_ManUnrollAbs( Gia_Man_t * p, int nFrames ) int nObjBits, nObjMask; int f, fMax, k, Entry, Prev, iStart, iStop, Size; // get the bitmasks - nObjBits = Gia_Base2Log( Gia_ManObjNum(p) ); + nObjBits = Abc_Base2Log( Gia_ManObjNum(p) ); nObjMask = (1 << nObjBits) - 1; assert( Gia_ManObjNum(p) <= nObjMask ); // derive the tents @@ -349,12 +349,12 @@ static inline int Gia_ObjUnrRead( Gia_ManUnr_t * p, int Id, int Degree ) static inline int Gia_ObjUnrReadCopy0( Gia_ManUnr_t * p, Gia_Obj_t * pObj, int Id ) { int Lit = Gia_ObjUnrRead(p, Gia_ObjFaninId0(pObj, Id), Vec_IntEntry(p->vDegDiff, 2*Id)); - return Gia_LitNotCond( Lit, Gia_ObjFaninC0(pObj) ); + return Abc_LitNotCond( Lit, Gia_ObjFaninC0(pObj) ); } static inline int Gia_ObjUnrReadCopy1( Gia_ManUnr_t * p, Gia_Obj_t * pObj, int Id ) { int Lit = Gia_ObjUnrRead(p, Gia_ObjFaninId1(pObj, Id), Vec_IntEntry(p->vDegDiff, 2*Id+1)); - return Gia_LitNotCond( Lit, Gia_ObjFaninC1(pObj) ); + return Abc_LitNotCond( Lit, Gia_ObjFaninC1(pObj) ); } static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t * pNew ) { @@ -367,7 +367,7 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t * pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) ); else pObj = Gia_ManPi( pNew, Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) ); - return Gia_Var2Lit( Gia_ObjId(pNew, pObj), 0 ); + return Abc_Var2Lit( Gia_ObjId(pNew, pObj), 0 ); } if ( f == 0 ) // initialize! { @@ -378,9 +378,9 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t * pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * p->pPars->nFrames + Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) ); else pObj = Gia_ManPi( pNew, Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) ); - return Gia_Var2Lit( Gia_ObjId(pNew, pObj), 0 ); + return Abc_Var2Lit( Gia_ObjId(pNew, pObj), 0 ); } - pObj = Gia_ManObj( p->pOrder, Gia_Lit2Var(Gia_ObjRoToRi(p->pAig, pObjReal)->Value) ); + pObj = Gia_ManObj( p->pOrder, Abc_Lit2Var(Gia_ObjRoToRi(p->pAig, pObjReal)->Value) ); assert( Gia_ObjIsCo(pObj) ); return Gia_ObjUnrRead( p, Gia_ObjId(p->pOrder, pObj), 0 ); } @@ -405,7 +405,7 @@ void * Gia_ManUnrollStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) // start timeframes assert( p->pNew == NULL ); p->pNew = Gia_ManStart( 10000 ); - p->pNew->pName = Gia_UtilStrsav( p->pAig->pName ); + p->pNew->pName = Abc_UtilStrsav( p->pAig->pName ); Gia_ManHashAlloc( p->pNew ); // create combinational inputs if ( !p->pPars->fSaveLastLit ) // only in the case when unrolling depth is known @@ -541,7 +541,7 @@ Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p ) int fMax, f, i, Lit, Beg, End; // start timeframes pNew = Gia_ManStart( 10000 ); - pNew->pName = Gia_UtilStrsav( p->pAig->pName ); + pNew->pName = Abc_UtilStrsav( p->pAig->pName ); Gia_ManHashAlloc( pNew ); // create combinational inputs for ( f = 0; f < p->pPars->nFrames; f++ ) @@ -754,7 +754,7 @@ Gia_Man_t * Gia_ManFramesInit( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) Gia_ManFraSupports( p ); pFrames = Gia_ManStart( Vec_VecSizeSize((Vec_Vec_t*)p->vIns)+ Vec_VecSizeSize((Vec_Vec_t*)p->vAnds)+Vec_VecSizeSize((Vec_Vec_t*)p->vOuts) ); - pFrames->pName = Gia_UtilStrsav( pAig->pName ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); Gia_ManHashAlloc( pFrames ); Gia_ManConst0(pAig)->Value = 0; for ( f = 0; f < pPars->nFrames; f++ ) @@ -864,7 +864,7 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) if ( pPars->fInit ) return Gia_ManFramesInit( pAig, pPars ); pFrames = Gia_ManStart( pPars->nFrames * Gia_ManObjNum(pAig) ); - pFrames->pName = Gia_UtilStrsav( pAig->pName ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); Gia_ManHashAlloc( pFrames ); Gia_ManConst0(pAig)->Value = 0; for ( f = 0; f < pPars->nFrames; f++ ) diff --git a/src/aig/gia/giaFront.c b/src/aig/gia/giaFront.c index 6eb20635..903a66e7 100644 --- a/src/aig/gia/giaFront.c +++ b/src/aig/gia/giaFront.c @@ -115,7 +115,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p ) Gia_ManSetRefs( p ); // start the new manager pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->nFront = 1 + (int)((float)1.1 * nCrossCutMaxInit); // start the frontier pFront = ABC_CALLOC( char, pNew->nFront ); @@ -134,7 +134,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p ) nCrossCutMax = nCrossCut; // create new node iLit = Gia_ManAppendCi( pNew ); - pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(iLit) ); + pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) ); assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) ); pObjNew->Value = iFront = Gia_ManFrontFindNext( pFront, pNew->nFront, iFront ); // handle CIs without fanout @@ -147,7 +147,7 @@ Gia_Man_t * Gia_ManFront( Gia_Man_t * p ) assert( Gia_ObjValue(pObj) == 0 ); // create new node iLit = Gia_ManAppendCo( pNew, 0 ); - pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(iLit) ); + pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(iLit) ); assert( Gia_ObjId(pNew, pObjNew) == Gia_ObjId(p, pObj) ); // get the fanin pFanin0New = Gia_ManObj( pNew, Gia_ObjFaninId0(pObj, i) ); diff --git a/src/aig/gia/giaGiarf.c b/src/aig/gia/giaGiarf.c index 501f9bb3..2f18c16d 100644 --- a/src/aig/gia/giaGiarf.c +++ b/src/aig/gia/giaGiarf.c @@ -301,7 +301,7 @@ int Hcd_ManHashKey( unsigned * pSim, int nWords, int nTableSize ) void Hcd_ManClassesRehash( Hcd_Man_t * p, Vec_Int_t * vRefined ) { int * pTable, nTableSize, Key, i, k; - nTableSize = Gia_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 ); + nTableSize = Abc_PrimeCudd( 100 + Vec_IntSize(vRefined) / 5 ); pTable = ABC_CALLOC( int, nTableSize ); Vec_IntForEachEntry( vRefined, i, k ) { @@ -538,7 +538,7 @@ Gia_Man_t * Gia_GenerateReducedLevel( Gia_Man_t * p, int Level, Vec_Ptr_t ** pvR vRoots = Vec_PtrAlloc( 100 ); // copy unmarked nodes pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); @@ -553,7 +553,7 @@ Gia_Man_t * Gia_GenerateReducedLevel( Gia_Man_t * p, int Level, Vec_Ptr_t ** pvR { // printf( "Substituting %d <--- %d\n", Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj) ); assert( pRepr < pObj ); - pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); + pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) ); continue; } pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); @@ -644,19 +644,19 @@ int Gia_GiarfStorePatternTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, in int i; for ( i = 0; i < nLits; i++ ) { - pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - if ( Gia_InfoHasBit( pPres, iBit ) && - Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) + pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i])); + pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i])); + if ( Abc_InfoHasBit( pPres, iBit ) && + Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) ) return 0; } for ( i = 0; i < nLits; i++ ) { - pInfo = (unsigned *)Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i])); - pPres = (unsigned *)Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i])); - Gia_InfoSetBit( pPres, iBit ); - if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) ) - Gia_InfoXorBit( pInfo, iBit ); + pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i])); + pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i])); + Abc_InfoSetBit( pPres, iBit ); + if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) ) + Abc_InfoXorBit( pInfo, iBit ); } return 1; } @@ -699,10 +699,10 @@ void Gia_GiarfInsertPattern( Hcd_Man_t * p, Vec_Int_t * vCex, int k ) int Lit, i; Vec_IntForEachEntry( vCex, Lit, i ) { - pObj = Gia_ManCi( p->pGia, Gia_Lit2Var(Lit) ); + pObj = Gia_ManCi( p->pGia, Abc_Lit2Var(Lit) ); pInfo = Hcd_ObjSimP( p, Gia_ObjId( p->pGia, pObj ) ); - if ( Gia_InfoHasBit( pInfo, k ) == Gia_LitIsCompl(Lit) ) - Gia_InfoXorBit( pInfo, k ); + if ( Abc_InfoHasBit( pInfo, k ) == Abc_LitIsCompl(Lit) ) + Abc_InfoXorBit( pInfo, k ); } } @@ -737,7 +737,7 @@ void Gia_GiarfPrintClasses( Gia_Man_t * pGia ) ABC_NAMESPACE_IMPL_END -#include "cecInt.h" +#include "src/proof/cec/cecInt.h" ABC_NAMESPACE_IMPL_START @@ -785,7 +785,7 @@ int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t iRoot = Gia_ObjId( p->pGia, pRoot ); if ( !Gia_ObjIsConst( p->pGia, iRoot ) ) continue; - iRootNew = Gia_LitNotCond( pRoot->Value, pRoot->fPhase ); + iRootNew = Abc_LitNotCond( pRoot->Value, pRoot->fPhase ); assert( iRootNew != 1 ); if ( fUse2Solver ) { @@ -880,8 +880,8 @@ int Gia_ComputeEquivalencesLevel( Hcd_Man_t * p, Gia_Man_t * pGiaLev, Vec_Ptr_t pMemberPrev = (Gia_Obj_t *)Vec_PtrEntryLast( vMembers ); Vec_PtrForEachEntry( Gia_Obj_t *, vMembers, pMember, k ) { - iMemberPrev = Gia_LitNotCond( pMemberPrev->Value, pMemberPrev->fPhase ); - iMember = Gia_LitNotCond( pMember->Value, !pMember->fPhase ); + iMemberPrev = Abc_LitNotCond( pMemberPrev->Value, pMemberPrev->fPhase ); + iMember = Abc_LitNotCond( pMember->Value, !pMember->fPhase ); assert( iMemberPrev != iMember ); if ( fUse2Solver ) { diff --git a/src/aig/gia/giaGlitch.c b/src/aig/gia/giaGlitch.c index a6e5315a..35d076e5 100644 --- a/src/aig/gia/giaGlitch.c +++ b/src/aig/gia/giaGlitch.c @@ -333,7 +333,7 @@ static inline int Gli_NodeComputeValue( Gli_Obj_t * pNode ) int i, Phase = 0; for ( i = 0; i < (int)pNode->nFanins; i++ ) Phase |= (Gli_ObjFanin(pNode, i)->fPhase << i); - return Gia_InfoHasBit( pNode->uTruth, Phase ); + return Abc_InfoHasBit( pNode->uTruth, Phase ); } /**Function************************************************************* @@ -352,7 +352,7 @@ static inline int Gli_NodeComputeValue2( Gli_Obj_t * pNode ) int i, Phase = 0; for ( i = 0; i < (int)pNode->nFanins; i++ ) Phase |= (Gli_ObjFanin(pNode, i)->fPhase2 << i); - return Gia_InfoHasBit( pNode->uTruth, Phase ); + return Abc_InfoHasBit( pNode->uTruth, Phase ); } /**Function************************************************************* @@ -593,7 +593,7 @@ unsigned Gli_ManSimulateSeqNode( Gli_Man_t * p, Gli_Obj_t * pNode ) for ( k = 0; k < nFanins; k++ ) if ( (pSimInfos[k] >> i) & 1 ) Phase |= (1 << k); - if ( Gia_InfoHasBit( pNode->uTruth, Phase ) ) + if ( Abc_InfoHasBit( pNode->uTruth, Phase ) ) Result |= (1 << i); } return Result; @@ -755,7 +755,7 @@ void Gli_ManSwitchesAndGlitches( Gli_Man_t * p, int nPatterns, float PiTransProb } else { - int nIters = Gia_BitWordNum(nPatterns); + int nIters = Abc_BitWordNum(nPatterns); Gli_ManSimulateSeqPref( p, 16 ); for ( i = 0; i < 32; i++ ) { diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index f346a310..41092cc7 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -46,10 +46,10 @@ static inline int Gia_ManHashOne( int iLit0, int iLit1, int TableSize ) { unsigned Key = 0; assert( iLit0 < iLit1 ); - Key ^= Gia_Lit2Var(iLit0) * 7937; - Key ^= Gia_Lit2Var(iLit1) * 2971; - Key ^= Gia_LitIsCompl(iLit0) * 911; - Key ^= Gia_LitIsCompl(iLit1) * 353; + Key ^= Abc_Lit2Var(iLit0) * 7937; + Key ^= Abc_Lit2Var(iLit1) * 2971; + Key ^= Abc_LitIsCompl(iLit0) * 911; + Key ^= Abc_LitIsCompl(iLit1) * 353; return (int)(Key % TableSize); } @@ -68,8 +68,8 @@ static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1 ) { Gia_Obj_t * pThis; int * pPlace = p->pHTable + Gia_ManHashOne( iLit0, iLit1, p->nHTable ); - for ( pThis = (*pPlace)? Gia_ManObj(p, Gia_Lit2Var(*pPlace)) : NULL; pThis; - pPlace = (int *)&pThis->Value, pThis = (*pPlace)? Gia_ManObj(p, Gia_Lit2Var(*pPlace)) : NULL ) + for ( pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL; pThis; + pPlace = (int *)&pThis->Value, pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL ) if ( Gia_ObjFaninLit0p(p, pThis) == iLit0 && Gia_ObjFaninLit1p(p, pThis) == iLit1 ) break; return pPlace; @@ -109,7 +109,7 @@ int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 ) void Gia_ManHashAlloc( Gia_Man_t * p ) { assert( p->pHTable == NULL ); - p->nHTable = Gia_PrimeCudd( p->nObjsAlloc ); + p->nHTable = Abc_PrimeCudd( p->nObjsAlloc ); p->pHTable = ABC_CALLOC( int, p->nHTable ); } @@ -134,7 +134,7 @@ void Gia_ManHashStart( Gia_Man_t * p ) { pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) ); assert( *pPlace == 0 ); - *pPlace = Gia_Var2Lit( i, 0 ); + *pPlace = Abc_Var2Lit( i, 0 ); } } @@ -175,20 +175,20 @@ void Gia_ManHashResize( Gia_Man_t * p ) // replace the table pHTableOld = p->pHTable; nHTableOld = p->nHTable; - p->nHTable = Gia_PrimeCudd( 2 * Gia_ManAndNum(p) ); + p->nHTable = Abc_PrimeCudd( 2 * Gia_ManAndNum(p) ); p->pHTable = ABC_CALLOC( int, p->nHTable ); // rehash the entries from the old table Counter = 0; for ( i = 0; i < nHTableOld; i++ ) - for ( pThis = (pHTableOld[i]? Gia_ManObj(p, Gia_Lit2Var(pHTableOld[i])) : NULL), + for ( pThis = (pHTableOld[i]? Gia_ManObj(p, Abc_Lit2Var(pHTableOld[i])) : NULL), iNext = (pThis? pThis->Value : 0); - pThis; pThis = (iNext? Gia_ManObj(p, Gia_Lit2Var(iNext)) : NULL), + pThis; pThis = (iNext? Gia_ManObj(p, Abc_Lit2Var(iNext)) : NULL), iNext = (pThis? pThis->Value : 0) ) { pThis->Value = 0; pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0p(p, pThis), Gia_ObjFaninLit1p(p, pThis) ); assert( *pPlace == 0 ); // should not be there - *pPlace = Gia_Var2Lit( Gia_ObjId(p, pThis), 0 ); + *pPlace = Abc_Var2Lit( Gia_ObjId(p, pThis), 0 ); assert( *pPlace != 0 ); Counter++; } @@ -220,9 +220,9 @@ void Gia_ManHashProfile( Gia_Man_t * p ) for ( i = 0; i < Limit; i++ ) { Counter = 0; - for ( pEntry = (p->pHTable[i]? Gia_ManObj(p, Gia_Lit2Var(p->pHTable[i])) : NULL); + for ( pEntry = (p->pHTable[i]? Gia_ManObj(p, Abc_Lit2Var(p->pHTable[i])) : NULL); pEntry; - pEntry = (pEntry->Value? Gia_ManObj(p, Gia_Lit2Var(pEntry->Value)) : NULL) ) + pEntry = (pEntry->Value? Gia_ManObj(p, Abc_Lit2Var(pEntry->Value)) : NULL) ) Counter++; if ( Counter ) printf( "%d ", Counter ); @@ -480,7 +480,7 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 ) return iLit1 ? iLit0 : 0; if ( iLit0 == iLit1 ) return iLit1; - if ( iLit0 == Gia_LitNot(iLit1) ) + if ( iLit0 == Abc_LitNot(iLit1) ) return 0; if ( (p->nObjs & 0xFF) == 0 && 2 * p->nHTable < Gia_ManAndNum(p) ) Gia_ManHashResize( p ); @@ -531,7 +531,7 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 ) return iLit1 ? iLit0 : 0; if ( iLit0 == iLit1 ) return iLit1; - if ( iLit0 == Gia_LitNot(iLit1) ) + if ( iLit0 == Abc_LitNot(iLit1) ) return 0; if ( iLit0 > iLit1 ) iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1; @@ -556,10 +556,10 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 ) ***********************************************************************/ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 ) { - int fCompl = Gia_LitIsCompl(iLit0) ^ Gia_LitIsCompl(iLit1); - int iTemp0 = Gia_ManHashAnd( p, Gia_LitRegular(iLit0), Gia_LitNot(Gia_LitRegular(iLit1)) ); - int iTemp1 = Gia_ManHashAnd( p, Gia_LitRegular(iLit1), Gia_LitNot(Gia_LitRegular(iLit0)) ); - return Gia_LitNotCond( Gia_ManHashAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), !fCompl ); + int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1); + int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) ); + int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) ); + return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl ); } /**Function************************************************************* @@ -575,9 +575,9 @@ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 ) ***********************************************************************/ int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 ) { - int iTemp0 = Gia_ManHashAnd( p, Gia_LitNot(iCtrl), iData0 ); + int iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 ); int iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 ); - return Gia_LitNotCond( Gia_ManHashAnd( p, Gia_LitNot(iTemp0), Gia_LitNot(iTemp1) ), 1 ); + return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 ); } /**Function************************************************************* @@ -597,7 +597,7 @@ Gia_Man_t * Gia_ManRehash( Gia_Man_t * p, int fAddStrash ) Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->fAddStrash = fAddStrash; Gia_ManHashAlloc( pNew ); Gia_ManConst0(p)->Value = 0; diff --git a/src/aig/gia/giaHcd.c b/src/aig/gia/giaHcd.c index 454785b9..3f37e724 100644 --- a/src/aig/gia/giaHcd.c +++ b/src/aig/gia/giaHcd.c @@ -20,8 +20,8 @@ #include "gia.h" #include "giaAig.h" -#include "aig.h" -#include "dar.h" +#include "src/aig/aig/aig.h" +#include "src/opt/dar/dar.h" ABC_NAMESPACE_IMPL_START @@ -332,7 +332,7 @@ Gia_Man_t * Hcd_ManChoiceMiter( Vec_Ptr_t * vGias ) } // start the new manager pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) ); - pNew->pName = Gia_UtilStrsav( pGia0->pName ); + pNew->pName = Abc_UtilStrsav( pGia0->pName ); // create new CIs and assign them to the old manager CIs for ( k = 0; k < Gia_ManCiNum(pGia0); k++ ) { @@ -457,7 +457,7 @@ void Hcd_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb { if ( Gia_ObjIsConst0(pRepr) ) { - pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } Hcd_ManEquivToChoices_rec( pNew, p, pRepr ); @@ -465,20 +465,20 @@ void Hcd_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); Hcd_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) ); pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - if ( Gia_LitRegular(pObj->Value) == Gia_LitRegular(pRepr->Value) ) + if ( Abc_LitRegular(pObj->Value) == Abc_LitRegular(pRepr->Value) ) { - assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) ); + assert( (int)pObj->Value == Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) ); return; } if ( pRepr->Value > pObj->Value ) // should never happen with high resource limit return; assert( pRepr->Value < pObj->Value ); - pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) ); - pObjNew = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) ); + pReprNew = Gia_ManObj( pNew, Abc_Lit2Var(pRepr->Value) ); + pObjNew = Gia_ManObj( pNew, Abc_Lit2Var(pObj->Value) ); if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) ) { assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew ); - pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } if ( !Hcd_ObjCheckTfi( pNew, pReprNew, pObjNew ) ) @@ -487,7 +487,7 @@ void Hcd_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) ); Hcd_ManAddNextEntry_rec( pNew, pReprNew, pObjNew ); } - pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); + pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ); return; } assert( Gia_ObjIsAnd(pObj) ); @@ -563,7 +563,7 @@ Gia_Man_t * Hcd_ManEquivToChoices( Gia_Man_t * p, int nSnapshots ) assert( (Gia_ManCoNum(p) % nSnapshots) == 0 ); Gia_ManSetPhase( p ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) ); for ( i = 0; i < Gia_ManObjNum(p); i++ ) diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 787aa090..e03439d0 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -19,9 +19,9 @@ ***********************************************************************/ #include "gia.h" -#include "aig.h" -#include "if.h" -#include "dar.h" +#include "src/aig/aig/aig.h" +#include "src/map/if/if.h" +#include "src/opt/dar/dar.h" ABC_NAMESPACE_IMPL_START @@ -306,11 +306,11 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p ) { nLuts++; nFanins += Gia_ObjLutSize(p, i); - nLutSize = ABC_MAX( nLutSize, Gia_ObjLutSize(p, i) ); + nLutSize = Abc_MaxInt( nLutSize, Gia_ObjLutSize(p, i) ); Gia_LutForEachFanin( p, i, iFan, k ) - pLevels[i] = ABC_MAX( pLevels[i], pLevels[iFan] ); + pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[iFan] ); pLevels[i]++; - LevelMax = ABC_MAX( LevelMax, pLevels[i] ); + LevelMax = Abc_MaxInt( LevelMax, pLevels[i] ); } ABC_FREE( pLevels ); Abc_Print( 1, "mapping (K=%d) : ", nLutSize ); @@ -355,7 +355,7 @@ int Gia_ManLutSizeMax( Gia_Man_t * p ) { int i, nSizeMax = -1; Gia_ManForEachLut( p, i ) - nSizeMax = ABC_MAX( nSizeMax, Gia_ObjLutSize(p, i) ); + nSizeMax = Abc_MaxInt( nSizeMax, Gia_ObjLutSize(p, i) ); return nSizeMax; } diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 39b0059d..972958bb 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "gia.h" -#include "tim.h" +#include "src/misc/tim/tim.h" ABC_NAMESPACE_IMPL_START @@ -262,7 +262,8 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p ) Vec_Int_t * vAbs = p->vObjClasses; int i, k, Entry, iStart, iStop, nFrames; int nObjBits, nObjMask, iObj, iFrame, nWords; - unsigned * pInfo, * pCountAll, * pCountUni; + unsigned * pInfo; + int * pCountAll, * pCountUni; if ( vAbs == NULL ) return; nFrames = Vec_IntEntry( vAbs, 0 ); @@ -270,10 +271,10 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p ) pCountAll = ABC_ALLOC( int, nFrames + 1 ); pCountUni = ABC_ALLOC( int, nFrames + 1 ); // start storage for seen objects - nWords = Gia_BitWordNum( nFrames ); + nWords = Abc_BitWordNum( nFrames ); vSeens = Vec_IntStart( Gia_ManObjNum(p) * nWords ); // get the bitmasks - nObjBits = Gia_Base2Log( Gia_ManObjNum(p) ); + nObjBits = Abc_Base2Log( Gia_ManObjNum(p) ); nObjMask = (1 << nObjBits) - 1; assert( Gia_ManObjNum(p) <= nObjMask ); // print info about frames @@ -289,16 +290,16 @@ void Gia_ManPrintObjClasses( Gia_Man_t * p ) iObj = (Entry & nObjMask); iFrame = (Entry >> nObjBits); pInfo = (unsigned *)Vec_IntEntryP( vSeens, nWords * iObj ); - if ( Gia_InfoHasBit(pInfo, iFrame) == 0 ) + if ( Abc_InfoHasBit(pInfo, iFrame) == 0 ) { - Gia_InfoSetBit( pInfo, iFrame ); + Abc_InfoSetBit( pInfo, iFrame ); pCountUni[iFrame+1]++; pCountUni[0]++; } pCountAll[iFrame+1]++; pCountAll[0]++; } - assert( pCountAll[0] == (unsigned)(iStop - iStart) ); + assert( pCountAll[0] == (iStop - iStart) ); // printf( "%5d%5d ", pCountAll[0], pCountUni[0] ); printf( "%3d :", i ); printf( "%6d", pCountAll[0] ); diff --git a/src/aig/gia/giaPat.c b/src/aig/gia/giaPat.c index 643ae6b7..124f5e0b 100644 --- a/src/aig/gia/giaPat.c +++ b/src/aig/gia/giaPat.c @@ -100,8 +100,8 @@ void Gia_SatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vCex, V Gia_SatCollectCone( p, Gia_ObjFanin0(pRoot), vVisit ); // set binary values to nodes in the counter-example Vec_IntForEachEntry( vCex, Entry, i ) -// Sat_ObjSetXValue( Gia_ManObj(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? GIA_ZER : GIA_ONE ); - Sat_ObjSetXValue( Gia_ManCi(p, Gia_Lit2Var(Entry)), Gia_LitIsCompl(Entry)? GIA_ZER : GIA_ONE ); +// Sat_ObjSetXValue( Gia_ManObj(p, Abc_Lit2Var(Entry)), Abc_LitIsCompl(Entry)? GIA_ZER : GIA_ONE ); + Sat_ObjSetXValue( Gia_ManCi(p, Abc_Lit2Var(Entry)), Abc_LitIsCompl(Entry)? GIA_ZER : GIA_ONE ); // simulate Gia_ManForEachObjVec( vVisit, p, pObj, i ) { diff --git a/src/aig/gia/giaReparam.c b/src/aig/gia/giaReparam.c index 5210f998..10294671 100644 --- a/src/aig/gia/giaReparam.c +++ b/src/aig/gia/giaReparam.c @@ -20,7 +20,7 @@ #include "gia.h" #include "giaAig.h" -#include "saig.h" +#include "src/aig/saig/saig.h" ABC_NAMESPACE_IMPL_START @@ -52,7 +52,7 @@ Gia_Man_t * Gia_ManDupIn2Ff( Gia_Man_t * p ) int i; vPiOuts = Vec_IntAlloc( Gia_ManPiNum(p) ); pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 * Gia_ManPiNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachPi( p, pObj, i ) @@ -112,7 +112,7 @@ Gia_Man_t * Gia_ManDupFf2In( Gia_Man_t * p, int nFlopsOld ) Gia_Obj_t * pObj; int i; pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachRo( p, pObj, i ) diff --git a/src/aig/gia/giaRetime.c b/src/aig/gia/giaRetime.c index 58029b66..0b9a6bfb 100644 --- a/src/aig/gia/giaRetime.c +++ b/src/aig/gia/giaRetime.c @@ -125,7 +125,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut ) int i; // create the new manager pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); // create the true PIs Gia_ManFillValue( p ); @@ -135,7 +135,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut ) pObj->Value = Gia_ManAppendCi( pNew ); // create the registers Vec_PtrForEachEntry( Gia_Obj_t *, vCut, pObj, i ) - pObj->Value = Gia_LitNotCond( Gia_ManAppendCi(pNew), pObj->fPhase ); + pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), pObj->fPhase ); // duplicate logic above the cut Gia_ManForEachCo( p, pObj, i ) Gia_ManRetimeDup_rec( pNew, Gia_ObjFanin0(pObj) ); @@ -156,7 +156,7 @@ Gia_Man_t * Gia_ManRetimeDupForward( Gia_Man_t * p, Vec_Ptr_t * vCut ) Vec_PtrForEachEntry( Gia_Obj_t *, vCut, pObj, i ) { Gia_ManRetimeDup_rec( pNew, pObj ); - Gia_ManAppendCo( pNew, Gia_LitNotCond( pObj->Value, pObj->fPhase ) ); + Gia_ManAppendCo( pNew, Abc_LitNotCond( pObj->Value, pObj->fPhase ) ); } Gia_ManHashStop( pNew ); Gia_ManSetRegNum( pNew, Vec_PtrSize(vCut) ); diff --git a/src/aig/gia/giaSat.c b/src/aig/gia/giaSat.c index c2d70795..cb410dd7 100644 --- a/src/aig/gia/giaSat.c +++ b/src/aig/gia/giaSat.c @@ -265,7 +265,7 @@ int Gia_ManSatPartCount( Gia_Man_t * p, Gia_Obj_t * pObj, int * pnLeaves, int * (*pnLeaves)++; else Level1 = Gia_ManSatPartCount(p, pFanin, pnLeaves, pnNodes) + Gia_ObjFaninC1(pObj); - return ABC_MAX( Level0, Level1 ); + return Abc_MaxInt( Level0, Level1 ); } /**Function************************************************************* diff --git a/src/aig/gia/giaScl.c b/src/aig/gia/giaScl.c index a482d024..0ec67c93 100644 --- a/src/aig/gia/giaScl.c +++ b/src/aig/gia/giaScl.c @@ -199,7 +199,7 @@ Gia_Man_t * Gia_ManReduceEquiv( Gia_Man_t * p, int fVerbose ) else if ( ~pMaps[iLit] ) // in this case, ID(pObj) > ID(pRepr) pCi2Lit[Gia_ManPiNum(p)+i] = pMaps[iLit], Counter++; else - pMaps[iLit] = Gia_Var2Lit( Gia_ObjId(p, pObjRo), 0 ); + pMaps[iLit] = Abc_Var2Lit( Gia_ObjId(p, pObjRo), 0 ); } /* Gia_ManForEachCi( p, pObjRo, i ) diff --git a/src/aig/gia/giaShrink.c b/src/aig/gia/giaShrink.c index fc9e80d6..07119daf 100644 --- a/src/aig/gia/giaShrink.c +++ b/src/aig/gia/giaShrink.c @@ -19,8 +19,8 @@ ***********************************************************************/ #include "gia.h" -#include "aig.h" -#include "dar.h" +#include "src/aig/aig/aig.h" +#include "src/opt/dar/dar.h" ABC_NAMESPACE_IMPL_START @@ -75,7 +75,7 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose Gia_ManConst0(p)->Value = 0; // start the new manager pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Gia_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManHashAlloc( pNew ); Gia_ManCleanLevels( pNew, Gia_ManObjNum(p) ); Gia_ManForEachObj1( p, pObj, i ) @@ -114,7 +114,7 @@ Gia_Man_t * Gia_ManPerformMapShrink( Gia_Man_t * p, int fKeepLevel, int fVerbose else { pObj->Value = Dar_LibEvalBuild( pNew, vLeaves, 0xffff & *pTruth, fKeepLevel, vLeavesBest ); - pObj->Value = Gia_LitNotCond( pObj->Value, Gia_ObjPhaseRealLit(pNew, pObj->Value) ^ pObj->fPhase ); + pObj->Value = Abc_LitNotCond( pObj->Value, Gia_ObjPhaseRealLit(pNew, pObj->Value) ^ pObj->fPhase ); } } } diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c index 4be740cd..817fc2e2 100644 --- a/src/aig/gia/giaSim.c +++ b/src/aig/gia/giaSim.c @@ -133,18 +133,18 @@ Vec_Int_t * Gia_ManSimDeriveResets( Gia_Man_t * pGia ) { if ( Count < nImpLimit ) continue; - pObj = Gia_ManObj( pGia, Gia_Lit2Var(Lit) ); - if ( Gia_LitIsCompl(Lit) ) // const 0 + pObj = Gia_ManObj( pGia, Abc_Lit2Var(Lit) ); + if ( Abc_LitIsCompl(Lit) ) // const 0 { // Ssm_ObjSetLogic0( pObj ); - Vec_IntWriteEntry( vResult, Gia_Lit2Var(Lit), 0 ); + Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 0 ); CounterPi0 += Gia_ObjIsPi(pGia, pObj); Counter0++; } else { // Ssm_ObjSetLogic1( pObj ); - Vec_IntWriteEntry( vResult, Gia_Lit2Var(Lit), 1 ); + Vec_IntWriteEntry( vResult, Abc_Lit2Var(Lit), 1 ); CounterPi1 += Gia_ObjIsPi(pGia, pObj); Counter1++; } @@ -568,8 +568,8 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int continue; for ( w = nWords-1; w >= 0; w-- ) pData[w] = Gia_ManRandom( 0 ); - if ( Gia_InfoHasBit( pData, iPat ) ) - Gia_InfoSetBit( p->pData, Counter + iPioId ); + if ( Abc_InfoHasBit( pData, iPat ) ) + Abc_InfoSetBit( p->pData, Counter + iPioId ); } ABC_FREE( pData ); return p; diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c index 27945704..74a34d1b 100644 --- a/src/aig/gia/giaSim2.c +++ b/src/aig/gia/giaSim2.c @@ -471,7 +471,7 @@ void Gia_Sim2ProcessRefined( Gia_Sim2_t * p, Vec_Int_t * vRefined ) int * pTable, nTableSize, i, k, Key; if ( Vec_IntSize(vRefined) == 0 ) return; - nTableSize = Gia_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 ); + nTableSize = Abc_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 ); pTable = ABC_CALLOC( int, nTableSize ); Vec_IntForEachEntry( vRefined, i, k ) { @@ -617,8 +617,8 @@ Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int { for ( w = nWords-1; w >= 0; w-- ) pData[w] = Gia_ManRandom( 0 ); - if ( Gia_InfoHasBit( pData, iPat ) ) - Gia_InfoSetBit( p->pData, Counter + i ); + if ( Abc_InfoHasBit( pData, iPat ) ) + Abc_InfoSetBit( p->pData, Counter + i ); } ABC_FREE( pData ); return p; diff --git a/src/aig/gia/giaSpeedup.c b/src/aig/gia/giaSpeedup.c index cce0b68d..d20fe1a4 100644 --- a/src/aig/gia/giaSpeedup.c +++ b/src/aig/gia/giaSpeedup.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "gia.h" -#include "if.h" +#include "src/map/if/if.h" ABC_NAMESPACE_IMPL_START @@ -597,7 +597,7 @@ void Gia_ManSpeedupObj( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_I for ( i = 0; i < nCofs; i++ ) { Gia_ManForEachObjVec( vLeaves, p, pTemp, k ) - pTemp->Value = Gia_Var2Lit( Gia_ObjId(p, pTemp), 0 ); + pTemp->Value = Abc_Var2Lit( Gia_ObjId(p, pTemp), 0 ); Gia_ManForEachObjVec( vTimes, p, pTemp, k ) pTemp->Value = ((i & (1<<k)) != 0); Gia_ManForEachObjVec( vNodes, p, pTemp, k ) @@ -611,7 +611,7 @@ void Gia_ManSpeedupObj( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_I pCofs[i] = Gia_ManHashMux( pNew, Gia_ObjToLit(p,pTemp), pCofs[i+nSkip], pCofs[i] ); // create choice node (pObj is repr and ppCofs[0] is new) iObj = Gia_ObjId( p, pObj ); - iResult = Gia_Lit2Var( pCofs[0] ); + iResult = Abc_Lit2Var( pCofs[0] ); if ( iResult <= iObj ) return; Gia_ObjSetRepr( pNew, iResult, iObj ); diff --git a/src/aig/gia/giaSupMin.c b/src/aig/gia/giaSupMin.c index 4abaab0f..90c30c71 100644 --- a/src/aig/gia/giaSupMin.c +++ b/src/aig/gia/giaSupMin.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "gia.h" -#include "kit.h" +#include "src/bool/kit/kit.h" ABC_NAMESPACE_IMPL_START diff --git a/src/aig/gia/giaSwitch.c b/src/aig/gia/giaSwitch.c index bc2f0f67..848bd646 100644 --- a/src/aig/gia/giaSwitch.c +++ b/src/aig/gia/giaSwitch.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "giaAig.h" -#include "main.h" +#include "src/base/main/main.h" ABC_NAMESPACE_IMPL_START @@ -569,7 +569,7 @@ Vec_Int_t * Gia_ManSwiSimulate( Gia_Man_t * pAig, Gia_ParSwi_t * pPars ) { printf( "Obj = %8d (%8d). F = %6d. ", pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront, - 4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20) ); + 4.0*Abc_BitWordNum(2 * p->pAig->nFront)/(1<<20) ); printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ", 12.0*Gia_ManObjNum(p->pAig)/(1<<20), 4.0*p->nWords*p->pAig->nFront/(1<<20), @@ -691,8 +691,8 @@ Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * pAig, int nFrames, int nPref Aig_ManForEachObj( pAig, pObj, i ) { // if ( Aig_ObjIsPo(pObj) ) -// printf( "%d=%f\n", i, Aig_Int2Float( Vec_IntEntry(vSwitching, Gia_Lit2Var(pObj->iData)) ) ); - Vec_IntWriteEntry( vResult, i, Vec_IntEntry(vSwitching, Gia_Lit2Var(pObj->iData)) ); +// printf( "%d=%f\n", i, Abc_Int2Float( Vec_IntEntry(vSwitching, Abc_Lit2Var(pObj->iData)) ) ); + Vec_IntWriteEntry( vResult, i, Vec_IntEntry(vSwitching, Abc_Lit2Var(pObj->iData)) ); } // delete intermediate results Vec_IntFree( vSwitching ); diff --git a/src/aig/gia/giaTsim.c b/src/aig/gia/giaTsim.c index e829ff5b..c4fb7f26 100644 --- a/src/aig/gia/giaTsim.c +++ b/src/aig/gia/giaTsim.c @@ -84,15 +84,15 @@ Gia_ManTer_t * Gia_ManTerCreate( Gia_Man_t * pAig ) p = ABC_CALLOC( Gia_ManTer_t, 1 ); p->pAig = Gia_ManFront( pAig ); p->nIters = 300; - p->pDataSim = ABC_ALLOC( unsigned, Gia_BitWordNum(2*p->pAig->nFront) ); - p->pDataSimCis = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCiNum(p->pAig)) ); - p->pDataSimCos = ABC_ALLOC( unsigned, Gia_BitWordNum(2*Gia_ManCoNum(p->pAig)) ); + p->pDataSim = ABC_ALLOC( unsigned, Abc_BitWordNum(2*p->pAig->nFront) ); + p->pDataSimCis = ABC_ALLOC( unsigned, Abc_BitWordNum(2*Gia_ManCiNum(p->pAig)) ); + p->pDataSimCos = ABC_ALLOC( unsigned, Abc_BitWordNum(2*Gia_ManCoNum(p->pAig)) ); // allocate storage for terminary states - p->nStateWords = Gia_BitWordNum( 2*Gia_ManRegNum(pAig) ); + p->nStateWords = Abc_BitWordNum( 2*Gia_ManRegNum(pAig) ); p->vStates = Vec_PtrAlloc( 1000 ); p->pCount0 = ABC_CALLOC( int, Gia_ManRegNum(pAig) ); p->pCountX = ABC_CALLOC( int, Gia_ManRegNum(pAig) ); - p->nBins = Gia_PrimeCudd( 500 ); + p->nBins = Abc_PrimeCudd( 500 ); p->pBins = ABC_CALLOC( unsigned *, p->nBins ); p->vRetired = Vec_IntAlloc( 100 ); p->pRetired = ABC_CALLOC( char, Gia_ManRegNum(pAig) ); @@ -511,7 +511,7 @@ void Gia_ManTerAnalyze2( Vec_Ptr_t * vStates, int nRegs ) unsigned * pTemp, * pStates = (unsigned *)Vec_PtrPop( vStates ); int i, w, nZeros, nConsts, nStateWords; // detect constant zero registers - nStateWords = Gia_BitWordNum( 2*nRegs ); + nStateWords = Abc_BitWordNum( 2*nRegs ); memset( pStates, 0, sizeof(int) * nStateWords ); Vec_PtrForEachEntry( unsigned *, vStates, pTemp, i ) for ( w = 0; w < nStateWords; w++ ) @@ -579,7 +579,7 @@ Vec_Ptr_t * Gia_ManTerTranspose( Gia_ManTer_t * p ) unsigned * pState, * pFlop; int i, k, nFlopWords; vFlops = Vec_PtrAlloc( 100 ); - nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) ); + nFlopWords = Abc_BitWordNum( 2*Vec_PtrSize(p->vStates) ); for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ ) { if ( p->pCount0[i] == Vec_PtrSize(p->vStates) ) @@ -634,7 +634,7 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p, int fVerbose ) Gia_Obj_t * pObj; Vec_Int_t * vMapKtoI; int i, iRepr, nFlopWords, Counter0 = 0, CounterE = 0; - nFlopWords = Gia_BitWordNum( 2*Vec_PtrSize(p->vStates) ); + nFlopWords = Abc_BitWordNum( 2*Vec_PtrSize(p->vStates) ); p->vFlops = Gia_ManTerTranspose( p ); pCi2Lit = ABC_FALLOC( int, Gia_ManCiNum(p->pAig) ); vMapKtoI = Vec_IntAlloc( 100 ); @@ -648,7 +648,7 @@ int * Gia_ManTerCreateMap( Gia_ManTer_t * p, int fVerbose ) if ( iRepr < 0 ) continue; pObj = Gia_ManCi( p->pAig, Gia_ManPiNum(p->pAig)+Vec_IntEntry(vMapKtoI, iRepr) ); - pCi2Lit[Gia_ManPiNum(p->pAig)+i] = Gia_Var2Lit( Gia_ObjId( p->pAig, pObj ), 0 ); + pCi2Lit[Gia_ManPiNum(p->pAig)+i] = Abc_Var2Lit( Gia_ObjId( p->pAig, pObj ), 0 ); CounterE++; } Vec_IntFree( vMapKtoI ); @@ -684,8 +684,8 @@ Gia_ManTer_t * Gia_ManTerSimulate( Gia_Man_t * pAig, int fVerbose ) pAig->nObjs, Gia_ManCiNum(pAig) + Gia_ManAndNum(pAig), p->pAig->nFront ); printf( "AIG = %7.2f Mb. F-mem = %7.2f Mb. Other = %7.2f Mb. ", 12.0*Gia_ManObjNum(p->pAig)/(1<<20), - 4.0*Gia_BitWordNum(2 * p->pAig->nFront)/(1<<20), - 4.0*Gia_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) ); + 4.0*Abc_BitWordNum(2 * p->pAig->nFront)/(1<<20), + 4.0*Abc_BitWordNum(2 * (Gia_ManCiNum(pAig) + Gia_ManCoNum(pAig)))/(1<<20) ); ABC_PRT( "Time", clock() - clk ); } // perform simulation diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index f19f0602..e56f6ea9 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -80,42 +80,6 @@ void Gia_ManRandomInfo( Vec_Ptr_t * vInfo, int iInputStart, int iWordStart, int pInfo[w] = Gia_ManRandom(0); } -/**Function******************************************************************** - - Synopsis [Returns the next prime >= p.] - - Description [Copied from CUDD, for stand-aloneness.] - - SideEffects [None] - - SeeAlso [] - -******************************************************************************/ -unsigned int Gia_PrimeCudd( unsigned int p ) -{ - int i,pn; - - p--; - do { - p++; - if (p&1) { - pn = 1; - i = 3; - while ((unsigned) (i * i) <= p) { - if (p % i == 0) { - pn = 0; - break; - } - i += 2; - } - } else { - pn = 0; - } - } while (!pn); - return(p); - -} /* end of Cudd_Prime */ - /**Function************************************************************* @@ -483,7 +447,7 @@ int Gia_ManLevelNum( Gia_Man_t * p ) else if ( Gia_ObjIsCo(pObj) ) { Gia_ObjSetCoLevel( p, pObj ); - p->nLevels = ABC_MAX( p->nLevels, Gia_ObjLevel(p, pObj) ); + p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) ); } else Gia_ObjSetLevel( p, pObj, 0 ); @@ -1150,11 +1114,11 @@ int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut ) int RetValue, i, k, iBit = 0; Gia_ManCleanMark0(pAig); Gia_ManForEachRo( pAig, pObj, i ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); for ( i = 0; i <= p->iFrame; i++ ) { Gia_ManForEachPi( pAig, pObj, k ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); Gia_ManForEachAnd( pAig, pObj, k ) pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); @@ -1194,12 +1158,12 @@ int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p, int nOutputs ) assert( Gia_ManPiNum(pAig) == p->nPis ); Gia_ManCleanMark0(pAig); // Gia_ManForEachRo( pAig, pObj, i ) -// pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); +// pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); iBit = p->nRegs; for ( i = 0; i <= p->iFrame; i++ ) { Gia_ManForEachPi( pAig, pObj, k ) - pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++); + pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++); Gia_ManForEachAnd( pAig, pObj, k ) pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)); |