diff options
Diffstat (limited to 'src/aig/saig')
35 files changed, 236 insertions, 236 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 64bb3b02..b22821ab 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -18,16 +18,16 @@ ***********************************************************************/ -#ifndef __SAIG_H__ -#define __SAIG_H__ +#ifndef ABC__aig__saig__saig_h +#define ABC__aig__saig__saig_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -#include "aig.h" -#include "giaAbs.h" +#include "src/aig/aig/aig.h" +#include "src/aig/gia/giaAbs.h" ABC_NAMESPACE_HEADER_START diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index 01b1e6a6..ffb17db8 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -105,8 +105,8 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA { if ( i == Saig_ManPiNum(p) ) break; - if ( Aig_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) ) - Aig_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i ); + if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) ) + Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i ); } } // verify the counter example diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c index f3e55c72..e8b68a6f 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/aig/saig/saigAbsCba.c @@ -19,8 +19,8 @@ ***********************************************************************/ #include "saig.h" -#include "giaAig.h" -#include "ioa.h" +#include "src/aig/gia/giaAig.h" +#include "src/aig/ioa/ioa.h" ABC_NAMESPACE_IMPL_START @@ -89,7 +89,7 @@ Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_I // override the flop values according to the cex iBit = pAbsCex->nRegs + f * pAbsCex->nPis + Saig_ManPiNum(pAig); Vec_IntForEachEntry( vMapEntries, Entry, k ) - Saig_ManLo(pAig, Entry)->fMarkB = Aig_InfoHasBit(pAbsCex->pData, iBit + k); + Saig_ManLo(pAig, Entry)->fMarkB = Abc_InfoHasBit(pAbsCex->pData, iBit + k); // simulate Aig_ManForEachNode( pAig, pObj, k ) pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & @@ -102,7 +102,7 @@ Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_I // compare iBit = pAbsCex->nRegs + (f + 1) * pAbsCex->nPis + Saig_ManPiNum(pAig); Vec_IntForEachEntry( vMapEntries, Entry, k ) - if ( Saig_ManLi(pAig, Entry)->fMarkB != (unsigned)Aig_InfoHasBit(pAbsCex->pData, iBit + k) ) + if ( Saig_ManLi(pAig, Entry)->fMarkB != (unsigned)Abc_InfoHasBit(pAbsCex->pData, iBit + k) ) Vec_IntAddToEntry( vFlopCosts, k, 1 ); } // Vec_IntForEachEntry( vFlopCosts, Entry, i ) @@ -153,7 +153,7 @@ Aig_Man_t * Saig_ManDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value ) assert( pAig->nConstrs == 0 ); // start the new manager pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pAigNew->pName = Abc_UtilStrsav( pAig->pName ); // map the constant node Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); // create variables for PIs @@ -168,8 +168,8 @@ Aig_Man_t * Saig_ManDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value ) pMiter = Aig_ManConst1( pAigNew ); Vec_IntForEachEntry( vLevel, Lit, k ) { - pObj = Saig_ManLi( pAig, Aig_Lit2Var(Lit) ); - pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Aig_LitIsCompl(Lit)) ); + pObj = Saig_ManLi( pAig, Abc_Lit2Var(Lit) ); + pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Abc_LitIsCompl(Lit)) ); } Aig_ObjCreatePo( pAigNew, pMiter ); } @@ -227,20 +227,20 @@ Abc_Cex_t * Saig_ManCbaReason2Cex( Saig_ManCba_t * p, Vec_Int_t * vReasons ) Abc_Cex_t * pCare; int i, Entry, iInput, iFrame; pCare = Abc_CexDup( p->pCex, p->pCex->nRegs ); - memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) ); + memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); Vec_IntForEachEntry( vReasons, Entry, i ) { assert( Entry >= 0 && Entry < Aig_ManPiNum(p->pFrames) ); iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 ); - Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); + Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); } /* for ( iFrame = 0; iFrame <= pCare->iFrame; iFrame++ ) { int Count = 0; for ( i = 0; i < pCare->nPis; i++ ) - Count += Aig_InfoHasBit(pCare->pData, pCare->nRegs + pCare->nPis * iFrame + i); + Count += Abc_InfoHasBit(pCare->pData, pCare->nRegs + pCare->nPis * iFrame + i); printf( "%d ", Count ); } printf( "\n" ); @@ -322,7 +322,7 @@ Vec_Int_t * Saig_ManCbaFindReason( Saig_ManCba_t * p ) { int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); - pObj->fPhase = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); + pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i ); } @@ -434,11 +434,11 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI // derive unrolled timeframes pFrames = Aig_ManStart( 10000 ); - pFrames->pName = Aig_UtilStrsav( pAig->pName ); - pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); + pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); // initialize the flops Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Aig_InfoHasBit(pCex->pData, i) ); + pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, i) ); // iterate through the frames for ( f = 0; f <= pCex->iFrame; f++ ) { @@ -457,7 +457,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI if ( Aig_ObjPioNum(pObj) < nInputs ) { int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj); - pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Aig_InfoHasBit(pCex->pData, iBit) ); + pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) ); } else { @@ -558,12 +558,12 @@ void Saig_ManCbaShrink( Saig_ManCba_t * p ) { Vec_IntForEachEntryDouble( vLevel, ObjId, Lit, k ) { - pObjFrame = Aig_ManObj( p->pFrames, Aig_Lit2Var(Lit) ); + pObjFrame = Aig_ManObj( p->pFrames, Abc_Lit2Var(Lit) ); if ( pObjFrame == NULL || (!Aig_ObjIsConst1(pObjFrame) && !Aig_ObjIsTravIdCurrent(p->pFrames, pObjFrame)) ) continue; pObjLi = Aig_ManObj( p->pAig, ObjId ); assert( Saig_ObjIsLi(p->pAig, pObjLi) ); - Vec_VecPushInt( p->vReg2Value, f, Aig_Var2Lit( Aig_ObjPioNum(pObjLi) - Saig_ManPoNum(p->pAig), Aig_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) ); + Vec_VecPushInt( p->vReg2Value, f, Abc_Var2Lit( Aig_ObjPioNum(pObjLi) - Saig_ManPoNum(p->pAig), Abc_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) ); } } // print statistics diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c index a42515f3..3c9de875 100644 --- a/src/aig/saig/saigAbsPba.c +++ b/src/aig/saig/saigAbsPba.c @@ -19,9 +19,9 @@ ***********************************************************************/ #include "saig.h" -#include "cnf.h" -#include "satSolver.h" -#include "giaAig.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver.h" +#include "src/aig/gia/giaAig.h" ABC_NAMESPACE_IMPL_START @@ -99,8 +99,8 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec } // derive unrolled timeframes pFrames = Aig_ManStart( 10000 ); - pFrames->pName = Aig_UtilStrsav( pAig->pName ); - pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); + pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); // create activation variables Saig_ManForEachLo( pAig, pObj, i ) Aig_ObjCreatePi( pFrames ); @@ -186,19 +186,19 @@ Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t { int iSatVar = pCnf->pVarNums[ Aig_ObjId(Aig_ManPi(pCnf->pMan, Entry)) ]; if ( sat_solver_var_value( pSat, iSatVar ) ) - Aig_InfoSetBit( pCex->pData, Aig_ManRegNum(pAig) + i ); + Abc_InfoSetBit( pCex->pData, Aig_ManRegNum(pAig) + i ); } } // check what frame has failed Aig_ManCleanMarkB(pAig); Aig_ManConst1(pAig)->fMarkB = 1; Saig_ManForEachLo( pAig, pObj, i ) - pObj->fMarkB = Aig_InfoHasBit(pCex->pData, iBit++); + pObj->fMarkB = Abc_InfoHasBit(pCex->pData, iBit++); for ( f = 0; f < nFrames; f++ ) { // compute new state Saig_ManForEachPi( pAig, pObj, i ) - pObj->fMarkB = Aig_InfoHasBit(pCex->pData, iBit++); + pObj->fMarkB = Abc_InfoHasBit(pCex->pData, iBit++); Aig_ManForEachNode( pAig, pObj, i ) pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c index 71ef98d5..a5ec7dac 100644 --- a/src/aig/saig/saigAbsStart.c +++ b/src/aig/saig/saigAbsStart.c @@ -19,10 +19,10 @@ ***********************************************************************/ #include "saig.h" -#include "ssw.h" -#include "fra.h" -#include "bbr.h" -#include "pdr.h" +#include "src/proof/ssw/ssw.h" +#include "src/proof/fra/fra.h" +#include "src/proof/bbr/bbr.h" +#include "src/proof/pdr/pdr.h" ABC_NAMESPACE_IMPL_START diff --git a/src/aig/saig/saigAbsVfa.c b/src/aig/saig/saigAbsVfa.c index 4226ba51..c3243b0e 100644 --- a/src/aig/saig/saigAbsVfa.c +++ b/src/aig/saig/saigAbsVfa.c @@ -19,8 +19,8 @@ ***********************************************************************/ #include "saig.h" -#include "cnf.h" -#include "satSolver.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index 011a746e..814c445f 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -19,9 +19,9 @@ ***********************************************************************/ #include "saig.h" -#include "fra.h" -#include "cnf.h" -#include "satStore.h" +#include "src/proof/fra/fra.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satStore.h" ABC_NAMESPACE_IMPL_START @@ -167,7 +167,7 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax ABC_NAMESPACE_IMPL_END -#include "utilMem.h" +#include "src/misc/util/utilMem.h" ABC_NAMESPACE_IMPL_START diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index 169b9404..2586a457 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -19,9 +19,9 @@ ***********************************************************************/ #include "saig.h" -#include "cnf.h" -#include "satStore.h" -#include "ssw.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satStore.h" +#include "src/proof/ssw/ssw.h" ABC_NAMESPACE_IMPL_START @@ -180,8 +180,8 @@ Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose assert( Aig_ManRegNum(p) > 0 ); // the maximum number of frames will be determined to use at most 200Mb of RAM nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p); - nFramesLimit = ABC_MIN( nFramesLimit, nFramesMax ); - nFrameWords = Aig_BitWordNum( 2 * Aig_ManObjNum(p) ); + nFramesLimit = Abc_MinInt( nFramesLimit, nFramesMax ); + nFrameWords = Abc_BitWordNum( 2 * Aig_ManObjNum(p) ); // allocate simulation info vSimInfo = Vec_PtrAlloc( nFramesLimit ); for ( f = 0; f < nFramesLimit; f++ ) @@ -652,7 +652,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p ) if ( iVarNum == 0 ) continue; if ( sat_solver_var_value( p->pSat, iVarNum ) ) - Aig_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i ); + Abc_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i ); } } // verify the counter example diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 2035ac72..27393f32 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -19,9 +19,9 @@ ***********************************************************************/ #include "saig.h" -#include "fra.h" -#include "cnf.h" -#include "satStore.h" +#include "src/proof/fra/fra.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satStore.h" ABC_NAMESPACE_IMPL_START @@ -130,7 +130,7 @@ unsigned * Saig_ManBmcTerSimOne( Aig_Man_t * p, unsigned * pPrev ) Aig_Obj_t * pObj, * pObjLi; unsigned * pInfo; int i, Val0, Val1; - pInfo = ABC_CALLOC( unsigned, Aig_BitWordNum(2 * Aig_ManObjNumMax(p)) ); + pInfo = ABC_CALLOC( unsigned, Abc_BitWordNum(2 * Aig_ManObjNumMax(p)) ); Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(p), SAIG_TER_ONE ); Saig_ManForEachPi( p, pObj, i ) Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND ); @@ -1105,7 +1105,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) Gia_ManBmc_t * p; Aig_Obj_t * pObj; int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0; - int nOutDigits = Aig_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); + int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock(); int nTimeToStop = time(NULL) + pPars->nTimeOut; if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 ) diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c index 824f9eb3..f1826f50 100644 --- a/src/aig/saig/saigCexMin.c +++ b/src/aig/saig/saigCexMin.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "saig.h" -#include "ioa.h" +#include "src/aig/ioa/ioa.h" ABC_NAMESPACE_IMPL_START @@ -151,18 +151,18 @@ void Saig_ManCexMinDerivePhasePriority_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj ) Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin1(pObj) ); assert( Aig_ObjFanin0(pObj)->iData >= 0 ); assert( Aig_ObjFanin1(pObj)->iData >= 0 ); - fPhase0 = Aig_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj); - fPhase1 = Aig_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj); - iPrio0 = Aig_Lit2Var( Aig_ObjFanin0(pObj)->iData ); - iPrio1 = Aig_Lit2Var( Aig_ObjFanin1(pObj)->iData ); + fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj); + fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj); + iPrio0 = Abc_Lit2Var( Aig_ObjFanin0(pObj)->iData ); + iPrio1 = Abc_Lit2Var( Aig_ObjFanin1(pObj)->iData ); if ( fPhase0 && fPhase1 ) // both are one - pObj->iData = Aig_Var2Lit( Abc_MinInt(iPrio0, iPrio1), 1 ); + pObj->iData = Abc_Var2Lit( Abc_MinInt(iPrio0, iPrio1), 1 ); else if ( !fPhase0 && fPhase1 ) - pObj->iData = Aig_Var2Lit( iPrio0, 0 ); + pObj->iData = Abc_Var2Lit( iPrio0, 0 ); else if ( fPhase0 && !fPhase1 ) - pObj->iData = Aig_Var2Lit( iPrio1, 0 ); + pObj->iData = Abc_Var2Lit( iPrio1, 0 ); else // both are zero - pObj->iData = Aig_Var2Lit( Abc_MaxInt(iPrio0, iPrio1), 0 ); + pObj->iData = Abc_Var2Lit( Abc_MaxInt(iPrio0, iPrio1), 0 ); } } @@ -183,7 +183,7 @@ void Saig_ManCexMinVerifyPhase( Aig_Man_t * pAig, Abc_Cex_t * pCex, int f ) int i; Aig_ManConst1(pAig)->fPhase = 1; Saig_ManForEachPi( pAig, pObj, i ) - pObj->fPhase = Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + i); + pObj->fPhase = Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + i); if ( f == 0 ) { Saig_ManForEachLo( pAig, pObj, i ) @@ -266,7 +266,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * p // set the constant node to higher priority than the flops vFramePPs = Vec_VecStart( pCex->iFrame+1 ); nPrioOffset = (pCex->iFrame + 1) * pCex->nPis; - Aig_ManConst1(pAig)->iData = Aig_Var2Lit( nPrioOffset + pCex->nRegs, 1 ); + Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + pCex->nRegs, 1 ); vRoots = Vec_IntAlloc( 1000 ); //printf( "Const1 = %d Offset = %d\n", Aig_ManConst1(pAig)->iData, nPrioOffset ); for ( f = 0; f <= pCex->iFrame; f++ ) @@ -280,9 +280,9 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * p { assert( Aig_ObjIsPi(pObj) ); if ( Saig_ObjIsPi(pAig, pObj) ) - Vec_IntPush( vFramePPsOne, Aig_Var2Lit( (f+1) * pCex->nPis - nPiCount++, Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) ); + Vec_IntPush( vFramePPsOne, Abc_Var2Lit( (f+1) * pCex->nPis - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) ); else if ( f == 0 ) - Vec_IntPush( vFramePPsOne, Aig_Var2Lit( nPrioOffset + Saig_ObjRegId(pAig, pObj), 0 ) ); + Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + Saig_ObjRegId(pAig, pObj), 0 ) ); else { Aig_Obj_t * pObj0 = Saig_ObjLoToLi(pAig, pObj); @@ -298,7 +298,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * p Vec_IntFree( vRoots ); // check the output pObj = Aig_ManPo( pAig, pCex->iPo ); - assert( Aig_LitIsCompl(pObj->iData) ); + assert( Abc_LitIsCompl(pObj->iData) ); return vFramePPs; } @@ -327,7 +327,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC // set the constant node to higher priority than the flops vFramePPs = Vec_VecStart( pCex->iFrame+1 ); nPrioOffset = pCex->nRegs; - Aig_ManConst1(pAig)->iData = Aig_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 ); + Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 ); vRoots = Vec_IntAlloc( 1000 ); //printf( "Const1 = %d Offset = %d\n", Aig_ManConst1(pAig)->iData, nPrioOffset ); for ( f = 0; f <= pCex->iFrame; f++ ) @@ -341,9 +341,9 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC { assert( Aig_ObjIsPi(pObj) ); if ( Saig_ObjIsPi(pAig, pObj) ) - Vec_IntPush( vFramePPsOne, Aig_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) ); + Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) ); else if ( f == 0 ) - Vec_IntPush( vFramePPsOne, Aig_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) ); + Vec_IntPush( vFramePPsOne, Abc_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) ); else { Aig_Obj_t * pObj0 = Saig_ObjLoToLi(pAig, pObj); @@ -359,7 +359,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC Vec_IntFree( vRoots ); // check the output pObj = Aig_ManPo( pAig, pCex->iPo ); - assert( Aig_LitIsCompl(pObj->iData) ); + assert( Abc_LitIsCompl(pObj->iData) ); return vFramePPs; } @@ -383,9 +383,9 @@ void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t if ( Aig_ObjIsPi(pObj) ) { if ( fPiReason && Saig_ObjIsPi(p, pObj) ) - Vec_IntPush( vReason, Aig_Var2Lit( Aig_ObjPioNum(pObj), !Aig_LitIsCompl(pObj->iData) ) ); + Vec_IntPush( vReason, Abc_Var2Lit( Aig_ObjPioNum(pObj), !Abc_LitIsCompl(pObj->iData) ) ); else if ( !fPiReason && Saig_ObjIsLo(p, pObj) ) - Vec_IntPush( vReason, Aig_Var2Lit( Saig_ObjRegId(p, pObj), !Aig_LitIsCompl(pObj->iData) ) ); + Vec_IntPush( vReason, Abc_Var2Lit( Saig_ObjRegId(p, pObj), !Abc_LitIsCompl(pObj->iData) ) ); return; } if ( Aig_ObjIsPo(pObj) ) @@ -396,18 +396,18 @@ void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t if ( Aig_ObjIsConst1(pObj) ) return; assert( Aig_ObjIsNode(pObj) ); - if ( Aig_LitIsCompl(pObj->iData) ) // value 1 + if ( Abc_LitIsCompl(pObj->iData) ) // value 1 { - int fPhase0 = Aig_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj); - int fPhase1 = Aig_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj); + int fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj); + int fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj); assert( fPhase0 && fPhase1 ); Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason ); Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason ); } else { - int fPhase0 = Aig_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj); - int fPhase1 = Aig_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj); + int fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj); + int fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj); assert( !fPhase0 || !fPhase1 ); if ( !fPhase0 && fPhase1 ) Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason ); @@ -415,8 +415,8 @@ void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason ); else { - int iPrio0 = Aig_Lit2Var( Aig_ObjFanin0(pObj)->iData ); - int iPrio1 = Aig_Lit2Var( Aig_ObjFanin1(pObj)->iData ); + int iPrio0 = Abc_Lit2Var( Aig_ObjFanin0(pObj)->iData ); + int iPrio1 = Abc_Lit2Var( Aig_ObjFanin1(pObj)->iData ); if ( iPrio0 >= iPrio1 ) Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason ); else @@ -514,7 +514,7 @@ Aig_Man_t * Saig_ManCexMinDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value assert( pAig->nConstrs == 0 ); // start the new manager pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) + Vec_VecSize(vReg2Value) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pAigNew->pName = Abc_UtilStrsav( pAig->pName ); // map the constant node Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); // create variables for PIs @@ -532,8 +532,8 @@ Aig_Man_t * Saig_ManCexMinDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value Vec_IntForEachEntry( vLevel, Lit, k ) { assert( Lit >= 0 && Lit < 2 * Aig_ManRegNum(pAig) ); - pObj = Saig_ManLi( pAig, Aig_Lit2Var(Lit) ); - pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Aig_LitIsCompl(Lit)) ); + pObj = Saig_ManLi( pAig, Abc_Lit2Var(Lit) ); + pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Abc_LitIsCompl(Lit)) ); } Aig_ObjCreatePo( pAigNew, pMiter ); } diff --git a/src/aig/saig/saigConstr.c b/src/aig/saig/saigConstr.c index d58074e3..91bdf46f 100644 --- a/src/aig/saig/saigConstr.c +++ b/src/aig/saig/saigConstr.c @@ -19,10 +19,10 @@ ***********************************************************************/ #include "saig.h" -#include "cnf.h" -#include "satSolver.h" -#include "kit.h" -#include "ioa.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver.h" +#include "src/bool/kit/kit.h" +#include "src/aig/ioa/ioa.h" ABC_NAMESPACE_IMPL_START @@ -64,7 +64,7 @@ Aig_Man_t * Saig_ManDupUnfoldConstrs( Aig_Man_t * pAig ) } // start the new manager pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pAigNew->pName = Abc_UtilStrsav( pAig->pName ); // map the constant node Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); // create variables for PIs @@ -113,7 +113,7 @@ Aig_Man_t * Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * vConstrs ) assert( Saig_ManRegNum(pAig) > 0 ); // start the new manager pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pAigNew->pName = Abc_UtilStrsav( pAig->pName ); // map the constant node Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); // create variables for PIs diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c index 7f2eab6a..e60d1b82 100644 --- a/src/aig/saig/saigConstr2.c +++ b/src/aig/saig/saigConstr2.c @@ -19,10 +19,10 @@ ***********************************************************************/ #include "saig.h" -#include "cnf.h" -#include "satSolver.h" -#include "kit.h" -#include "bar.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver.h" +#include "src/bool/kit/kit.h" +#include "src/misc/bar/bar.h" ABC_NAMESPACE_IMPL_START @@ -244,8 +244,8 @@ Aig_Man_t * Saig_ManCreateIndMiter( Aig_Man_t * pAig, Vec_Vec_t * vCands ) // start the fraig package pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames ); - pFrames->pName = Aig_UtilStrsav( pAig->pName ); - pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); + pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); // map constant nodes for ( f = 0; f < nFrames; f++ ) Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) ); @@ -437,8 +437,8 @@ Aig_Man_t * Saig_ManUnrollCOI( Aig_Man_t * pAig, int nFrames ) pObjMap = ABC_CALLOC( Aig_Obj_t *, nFrames * Aig_ManObjNumMax(pAig) ); // start the fraig package pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames ); - pFrames->pName = Aig_UtilStrsav( pAig->pName ); - pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); + pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); // map constant nodes for ( f = 0; f < nFrames; f++ ) Aig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) ); @@ -504,8 +504,8 @@ void Saig_CollectSatValues( sat_solver * pSat, Cnf_Dat_t * pCnf, Vec_Ptr_t * vIn continue; assert( pCnf->pVarNums[i] > 0 ); pInfo = (unsigned *)Vec_PtrEntry( vInfo, i ); - if ( Aig_InfoHasBit(pInfo, *piPat) != sat_solver_var_value(pSat, pCnf->pVarNums[i]) ) - Aig_InfoXorBit(pInfo, *piPat); + if ( Abc_InfoHasBit(pInfo, *piPat) != sat_solver_var_value(pSat, pCnf->pVarNums[i]) ) + Abc_InfoXorBit(pInfo, *piPat); } } @@ -949,8 +949,8 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo assert( Aig_ManConstrNum(pAig) < Saig_ManPoNum(pAig) ); // start the new manager pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); - pAigNew->pSpec = Aig_UtilStrsav( pAig->pSpec ); + pAigNew->pName = Abc_UtilStrsav( pAig->pName ); + pAigNew->pSpec = Abc_UtilStrsav( pAig->pSpec ); // map the constant node Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); // create variables for PIs diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index ca06398c..fa915f52 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -54,7 +54,7 @@ Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * pAig ) } // start the new manager pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pAigNew->pName = Abc_UtilStrsav( pAig->pName ); pAigNew->nConstrs = pAig->nConstrs; // map the constant node Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); @@ -100,7 +100,7 @@ Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ) } // start the new manager pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pAigNew->pName = Abc_UtilStrsav( pAig->pName ); pAigNew->nConstrs = pAig->nConstrs; // map the constant node Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); @@ -150,7 +150,7 @@ Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p ) fAllPisHaveNoRefs = 0; // start the new manager pNew = Aig_ManStart( Aig_ManObjNum(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); pNew->nConstrs = p->nConstrs; // start mapping of the CI numbers pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManPiNum(p) ); @@ -210,7 +210,7 @@ Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops ) Aig_ManCleanData( p ); // start the new manager pNew = Aig_ManStart( 5000 ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); // map the constant node Aig_ManConst1(p)->pData = Aig_ManConst1( pNew ); // label included flops @@ -283,11 +283,11 @@ int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ) Aig_ManCleanMarkB(pAig); Aig_ManConst1(pAig)->fMarkB = 1; Saig_ManForEachLo( pAig, pObj, i ) - pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++); for ( i = 0; i <= p->iFrame; i++ ) { Saig_ManForEachPi( pAig, pObj, k ) - pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++); Aig_ManForEachNode( pAig, pObj, k ) pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); @@ -328,15 +328,15 @@ Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p ) Aig_ManCleanMarkB(pAig); Aig_ManConst1(pAig)->fMarkB = 1; Saig_ManForEachLo( pAig, pObj, i ) - pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++); for ( i = 0; i <= p->iFrame; i++ ) { Saig_ManForEachPi( pAig, pObj, k ) - pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++); ///////// write PI+LO values //////////// Aig_ManForEachPi( pAig, pObj, k ) if ( pObj->fMarkB ) - Aig_InfoSetBit(pNew->pData, Aig_ManPiNum(pAig)*i + k); + Abc_InfoSetBit(pNew->pData, Aig_ManPiNum(pAig)*i + k); ///////////////////////////////////////// Aig_ManForEachNode( pAig, pObj, k ) pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & @@ -374,11 +374,11 @@ int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p ) Aig_ManCleanMarkB(pAig); Aig_ManConst1(pAig)->fMarkB = 1; Saig_ManForEachLo( pAig, pObj, i ) - pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++); for ( i = 0; i <= p->iFrame; i++ ) { Saig_ManForEachPi( pAig, pObj, k ) - pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++); + pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++); Aig_ManForEachNode( pAig, pObj, k ) pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); @@ -421,7 +421,7 @@ Aig_Man_t * Saig_ManDupWithPhase( Aig_Man_t * pAig, Vec_Int_t * vInit ) assert( Aig_ManRegNum(pAig) <= Vec_IntSize(vInit) ); // start the new manager pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pAigNew->pName = Abc_UtilStrsav( pAig->pName ); pAigNew->nConstrs = pAig->nConstrs; // map the constant node Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c index d5a94acb..d6af6e47 100644 --- a/src/aig/saig/saigGlaCba.c +++ b/src/aig/saig/saigGlaCba.c @@ -19,8 +19,8 @@ ***********************************************************************/ #include "saig.h" -#include "satSolver.h" -#include "cnf.h" +#include "src/sat/bsat/satSolver.h" +#include "src/sat/cnf/cnf.h" ABC_NAMESPACE_IMPL_START @@ -250,7 +250,7 @@ Aig_Man_t * Aig_Gla1DeriveAbs( Aig_Gla1Man_t * p ) assert( Saig_ManPoNum(p->pAig) == 1 ); // start the new manager pNew = Aig_ManStart( 5000 ); - pNew->pName = Aig_UtilStrsav( p->pAig->pName ); + pNew->pName = Abc_UtilStrsav( p->pAig->pName ); // create constant Aig_ManCleanData( p->pAig ); Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew); @@ -596,7 +596,7 @@ Abc_Cex_t * Aig_Gla1DeriveCex( Aig_Gla1Man_t * p, int iFrame ) continue; assert( iSatId > 0 ); if ( sat_solver_var_value(p->pSat, iSatId) ) - Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + i ); + Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + i ); } } Aig_ManForEachObjVec( p->vPPis, p->pAig, pObj, i ) @@ -610,7 +610,7 @@ Abc_Cex_t * Aig_Gla1DeriveCex( Aig_Gla1Man_t * p, int iFrame ) continue; assert( iSatId > 0 ); if ( sat_solver_var_value(p->pSat, iSatId) ) - Aig_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Vec_IntSize(p->vPis) + i ); + Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Vec_IntSize(p->vPis) + i ); } } return pCex; diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c index cdbc05c7..c22cf415 100644 --- a/src/aig/saig/saigGlaPba.c +++ b/src/aig/saig/saigGlaPba.c @@ -19,8 +19,8 @@ ***********************************************************************/ #include "saig.h" -#include "satSolver.h" -#include "satStore.h" +#include "src/sat/bsat/satSolver.h" +#include "src/sat/bsat/satStore.h" ABC_NAMESPACE_IMPL_START diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c index 1daea5d9..8bc2b982 100644 --- a/src/aig/saig/saigGlaPba2.c +++ b/src/aig/saig/saigGlaPba2.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "saig.h" -#include "satSolver2.h" +#include "src/sat/bsat/satSolver2.h" ABC_NAMESPACE_IMPL_START diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c index 3ea0a2c6..ee058a3c 100644 --- a/src/aig/saig/saigHaig.c +++ b/src/aig/saig/saigHaig.c @@ -19,8 +19,8 @@ ***********************************************************************/ #include "saig.h" -#include "satSolver.h" -#include "cnf.h" +#include "src/sat/bsat/satSolver.h" +#include "src/sat/cnf/cnf.h" ABC_NAMESPACE_IMPL_START @@ -101,8 +101,8 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames ) assert( nFrames == 1 || Saig_ManRegNum(pHaig) > 0 ); // start AIG manager for timeframes pFrames = Aig_ManStart( Aig_ManNodeNum(pHaig) * nFrames ); - pFrames->pName = Aig_UtilStrsav( pHaig->pName ); - pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec ); + pFrames->pName = Abc_UtilStrsav( pHaig->pName ); + pFrames->pSpec = Abc_UtilStrsav( pHaig->pSpec ); // map the constant node Aig_ManConst1(pHaig)->pData = Aig_ManConst1( pFrames ); // create variables for register outputs diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c index 190d8d25..c9043ba2 100644 --- a/src/aig/saig/saigInd.c +++ b/src/aig/saig/saigInd.c @@ -19,8 +19,8 @@ ***********************************************************************/ #include "saig.h" -#include "cnf.h" -#include "satSolver.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START @@ -324,7 +324,7 @@ nextrun: Vec_IntForEachEntryStart( vTopVarIds, VarNum, i, 1 ) { if ( VarNum >= 0 && sat_solver_var_value( pSat, VarNum ) ) - Aig_InfoSetBit( pCex->pData, iBit ); + Abc_InfoSetBit( pCex->pData, iBit ); iBit++; } assert( iBit == pCex->nBits ); diff --git a/src/aig/saig/saigIoa.c b/src/aig/saig/saigIoa.c index c84c37f3..bdd187d9 100644 --- a/src/aig/saig/saigIoa.c +++ b/src/aig/saig/saigIoa.c @@ -47,15 +47,15 @@ char * Saig_ObjName( Aig_Man_t * p, Aig_Obj_t * pObj ) { static char Buffer[16]; if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) ) - sprintf( Buffer, "n%0*d", Aig_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) ); + sprintf( Buffer, "n%0*d", Abc_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) ); else if ( Saig_ObjIsPi(p, pObj) ) - sprintf( Buffer, "pi%0*d", Aig_Base10Log(Saig_ManPiNum(p)), Aig_ObjPioNum(pObj) ); + sprintf( Buffer, "pi%0*d", Abc_Base10Log(Saig_ManPiNum(p)), Aig_ObjPioNum(pObj) ); else if ( Saig_ObjIsPo(p, pObj) ) - sprintf( Buffer, "po%0*d", Aig_Base10Log(Saig_ManPoNum(p)), Aig_ObjPioNum(pObj) ); + sprintf( Buffer, "po%0*d", Abc_Base10Log(Saig_ManPoNum(p)), Aig_ObjPioNum(pObj) ); else if ( Saig_ObjIsLo(p, pObj) ) - sprintf( Buffer, "lo%0*d", Aig_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPiNum(p) ); + sprintf( Buffer, "lo%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPiNum(p) ); else if ( Saig_ObjIsLi(p, pObj) ) - sprintf( Buffer, "li%0*d", Aig_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPoNum(p) ); + sprintf( Buffer, "li%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPoNum(p) ); else assert( 0 ); return Buffer; @@ -268,8 +268,8 @@ Aig_Man_t * Saig_ManReadBlif( char * pFileName ) { printf( "Saig_ManReadBlif(): Error 2.\n" ); return NULL; } // start the package p = Aig_ManStart( 10000 ); - p->pName = Aig_UtilStrsav( pToken ); - p->pSpec = Aig_UtilStrsav( pFileName ); + p->pName = Abc_UtilStrsav( pToken ); + p->pSpec = Abc_UtilStrsav( pFileName ); // count PIs pToken = Saig_ManReadToken( pFile ); if ( pToken == NULL || strcmp( pToken, ".inputs" ) ) diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index c50eaac5..20dbeec7 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "saig.h" -#include "fra.h" +#include "src/proof/fra/fra.h" ABC_NAMESPACE_IMPL_START @@ -106,7 +106,7 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) ); assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) ); pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) ); - pNew->pName = Aig_UtilStrsav( "miter" ); + pNew->pName = Abc_UtilStrsav( "miter" ); Aig_ManCleanData( p0 ); Aig_ManCleanData( p1 ); // map constant nodes @@ -168,7 +168,7 @@ Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) assert( Aig_ManPiNum(p0) == Aig_ManPiNum(p1) ); assert( Aig_ManPoNum(p0) == Aig_ManPoNum(p1) ); pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) ); - pNew->pName = Aig_UtilStrsav( "miter" ); + pNew->pName = Abc_UtilStrsav( "miter" ); // map constant nodes Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew); Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew); @@ -246,8 +246,8 @@ Aig_Man_t * Saig_ManDualRail( Aig_Man_t * p, int fMiter ) Aig_ManCleanNext( p ); // create the new manager pNew = Aig_ManStart( 4*Aig_ManObjNumMax(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); - pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); // create the PIs Aig_ManConst1(p)->pData = Aig_ManConst0(pNew); Aig_ManConst1(p)->pNext = Aig_ManConst1(pNew); @@ -331,8 +331,8 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames ) assert( Saig_ManRegNum(pBot) == Saig_ManRegNum(pTop) ); assert( Saig_ManRegNum(pBot) > 0 || Saig_ManRegNum(pTop) > 0 ); // start timeframes - p = Aig_ManStart( nFrames * ABC_MAX(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) ); - p->pName = Aig_UtilStrsav( "frames" ); + p = Aig_ManStart( nFrames * Abc_MaxInt(Aig_ManObjNumMax(pBot), Aig_ManObjNumMax(pTop)) ); + p->pName = Abc_UtilStrsav( "frames" ); // create variables for register outputs pAig = pBot; Saig_ManForEachLo( pAig, pObj, i ) @@ -392,7 +392,7 @@ Aig_Man_t * Aig_ManDupNodesAll( Aig_Man_t * p, Vec_Ptr_t * vSet ) Aig_Obj_t * pObj; int i; pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Aig_ManForEachPi( p, pObj, i ) pObj->pData = Aig_ObjCreatePi( pNew ); @@ -430,7 +430,7 @@ Aig_Man_t * Aig_ManDupNodesHalf( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart ) int i; Aig_ManCleanData( p ); pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Saig_ManForEachPi( p, pObj, i ) pObj->pData = Aig_ObjCreatePi( pNew ); @@ -534,13 +534,13 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi { *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); ABC_FREE( (*ppAig0)->pName ); - (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); + (*ppAig0)->pName = Abc_UtilStrsav( "part0" ); } if ( ppAig1 ) { *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); ABC_FREE( (*ppAig1)->pName ); - (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); + (*ppAig1)->pName = Abc_UtilStrsav( "part1" ); } Vec_PtrFree( vSet0 ); Vec_PtrFree( vSet1 ); @@ -682,11 +682,11 @@ int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** // create new AIG *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); ABC_FREE( (*ppAig0)->pName ); - (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); + (*ppAig0)->pName = Abc_UtilStrsav( "part0" ); // create new AIGs *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); ABC_FREE( (*ppAig1)->pName ); - (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); + (*ppAig1)->pName = Abc_UtilStrsav( "part1" ); // cleanup Vec_PtrFree( vSet0 ); Vec_PtrFree( vSet1 ); @@ -812,13 +812,13 @@ int Saig_ManDemiterSimpleDiff_old( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t { *ppAig0 = Aig_ManDupNodesAll( p, vSet0 ); ABC_FREE( (*ppAig0)->pName ); - (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); + (*ppAig0)->pName = Abc_UtilStrsav( "part0" ); } if ( ppAig1 ) { *ppAig1 = Aig_ManDupNodesAll( p, vSet1 ); ABC_FREE( (*ppAig1)->pName ); - (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); + (*ppAig1)->pName = Abc_UtilStrsav( "part1" ); } Vec_PtrFree( vSet0 ); Vec_PtrFree( vSet1 ); @@ -984,14 +984,14 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) assert( 0 ); *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); // not ready ABC_FREE( (*ppAig0)->pName ); - (*ppAig0)->pName = Aig_UtilStrsav( "part0" ); + (*ppAig0)->pName = Abc_UtilStrsav( "part0" ); } if ( ppAig1 ) { assert( 0 ); *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); // not ready ABC_FREE( (*ppAig1)->pName ); - (*ppAig1)->pName = Aig_UtilStrsav( "part1" ); + (*ppAig1)->pName = Abc_UtilStrsav( "part1" ); } Vec_PtrFree( vSet0 ); Vec_PtrFree( vSet1 ); diff --git a/src/aig/saig/saigOutDec.c b/src/aig/saig/saigOutDec.c index d8cc591e..e72ea132 100644 --- a/src/aig/saig/saigOutDec.c +++ b/src/aig/saig/saigOutDec.c @@ -19,8 +19,8 @@ ***********************************************************************/ #include "saig.h" -#include "cnf.h" -#include "satSolver.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START @@ -160,7 +160,7 @@ Aig_Man_t * Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits, int fVerbose // start the new manager pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pAigNew->pName = Abc_UtilStrsav( pAig->pName ); pAigNew->nConstrs = pAig->nConstrs; // map the constant node Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); @@ -180,7 +180,7 @@ Aig_Man_t * Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits, int fVerbose pMiter = Aig_ManConst1( pAigNew ); Vec_IntForEachEntry( vCube, Lit, i ) { - pObj = Aig_NotCond( Aig_ObjCopy(Aig_ManObj(pAig, Aig_Lit2Var(Lit))), Aig_LitIsCompl(Lit) ); + pObj = Aig_NotCond( Aig_ObjCopy(Aig_ManObj(pAig, Abc_Lit2Var(Lit))), Abc_LitIsCompl(Lit) ); pMiter = Aig_And( pAigNew, pMiter, pObj ); } Aig_ObjCreatePo( pAigNew, pMiter ); diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c index bd7176fa..4107c5a2 100644 --- a/src/aig/saig/saigPhase.c +++ b/src/aig/saig/saigPhase.c @@ -145,10 +145,10 @@ Saig_Tsim_t * Saig_TsiStart( Aig_Man_t * pAig ) p = (Saig_Tsim_t *)ABC_ALLOC( char, sizeof(Saig_Tsim_t) ); memset( p, 0, sizeof(Saig_Tsim_t) ); p->pAig = pAig; - p->nWords = Aig_BitWordNum( 2*Aig_ManRegNum(pAig) ); + p->nWords = Abc_BitWordNum( 2*Aig_ManRegNum(pAig) ); p->vStates = Vec_PtrAlloc( 1000 ); p->pMem = Aig_MmFixedStart( sizeof(unsigned) * p->nWords + sizeof(unsigned *), 10000 ); - p->nBins = Aig_PrimeCudd(TSIM_MAX_ROUNDS/2); + p->nBins = Abc_PrimeCudd(TSIM_MAX_ROUNDS/2); p->pBins = ABC_ALLOC( unsigned *, p->nBins ); memset( p->pBins, 0, sizeof(unsigned *) * p->nBins ); return p; @@ -233,7 +233,7 @@ int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nPref ) { Vec_PtrForEachEntryStart( unsigned *, p->vStates, pState, k, nPref ) { - Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i ); assert( Value != 0 ); if ( Value == SAIG_XVSX ) break; @@ -266,7 +266,7 @@ Vec_Int_t * Saig_TsiComputeTransient( Saig_Tsim_t * p, int nPref ) { Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k ) { - ValueThis = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + ValueThis = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i ); //printf( "%s", (ValueThis == 1)? "0" : ((ValueThis == 2)? "1" : "x") ); assert( ValueThis != 0 ); if ( ValuePrev != ValueThis ) @@ -320,7 +320,7 @@ void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix, int nLoop ) /* Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k ) { - Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i ); if ( Value == SAIG_XVSX ) break; } @@ -335,7 +335,7 @@ void Saig_TsiPrintTraces( Saig_Tsim_t * p, int nWords, int nPrefix, int nLoop ) printf( "%5d : ", Counter++ ); Vec_PtrForEachEntryStop( unsigned *, p->vStates, pState, k, Vec_PtrSize(p->vStates)-1 ) { - Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i ); if ( Value == SAIG_XVS0 ) printf( "0" ); else if ( Value == SAIG_XVS1 ) @@ -458,7 +458,7 @@ void Saig_TsiStatePrint( Saig_Tsim_t * p, unsigned * pState ) int i, Value, nZeros = 0, nOnes = 0, nDcs = 0; for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) { - Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i ); if ( Value == SAIG_XVS0 ) printf( "0" ), nZeros++; else if ( Value == SAIG_XVS1 ) @@ -488,7 +488,7 @@ int Saig_TsiStateCount( Saig_Tsim_t * p, unsigned * pState ) int i, Value, nCounter = 0; Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i ) { - Value = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i ); + Value = (Abc_InfoHasBit( pState, 2 * i + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * i ); nCounter += (Value == SAIG_XVS0 || Value == SAIG_XVS1); } return nCounter; @@ -559,9 +559,9 @@ Saig_Tsim_t * Saig_ManReachableTernary( Aig_Man_t * p, Vec_Int_t * vInits, int f { Value = Saig_ObjGetXsim(pObjLo); if ( Value & 1 ) - Aig_InfoSetBit( pState, 2 * i ); + Abc_InfoSetBit( pState, 2 * i ); if ( Value & 2 ) - Aig_InfoSetBit( pState, 2 * i + 1 ); + Abc_InfoSetBit( pState, 2 * i + 1 ); } // printf( "%d ", Saig_TsiStateCount(pTsi, pState) ); // Saig_TsiStatePrint( pTsi, pState ); @@ -679,7 +679,7 @@ int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVe pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, k ); else pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, k - pTsi->nCycle ); - Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg ); + Value = (Abc_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * Reg ); assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 ); if ( k < nFrames || (fIgnore && k == nFrames) ) Values[k % nFrames] = Value; @@ -761,8 +761,8 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe // start the fraig package pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames ); - pFrames->pName = Aig_UtilStrsav( pAig->pName ); - pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); + pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); // map constant nodes for ( f = 0; f < nFrames; f++ ) Saig_ObjSetFrames( pObjMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pFrames) ); @@ -782,7 +782,7 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe { pObj = Saig_ManLo( pAig, Reg ); pState = (unsigned *)Vec_PtrEntry( pTsi->vStates, f ); - Value = (Aig_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * Reg ); + Value = (Abc_InfoHasBit( pState, 2 * Reg + 1 ) << 1) | Abc_InfoHasBit( pState, 2 * Reg ); assert( Value == SAIG_XVS0 || Value == SAIG_XVS1 ); pObjNew = (Value == SAIG_XVS1)? Aig_ManConst1(pFrames) : Aig_ManConst0(pFrames); Saig_ObjSetFrames( pObjMap, nFrames, pObj, f, pObjNew ); @@ -922,7 +922,7 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame // derive information pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords ); pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix; - pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, ABC_MIN(pTsi->nPrefix,nPref)); + pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, Abc_MinInt(pTsi->nPrefix,nPref)); // print statistics if ( fVerbose ) { @@ -1066,8 +1066,8 @@ Abc_Cex_t * Saig_PhaseTranslateCex( Aig_Man_t * p, Abc_Cex_t * pCex ) pNew->iPo = pCex->iPo % Saig_ManPoNum(p); // copy the bit data for ( i = pCex->nRegs, k = pNew->nRegs; k < pNew->nBits; k++, i++ ) - if ( Aig_InfoHasBit( pCex->pData, i ) ) - Aig_InfoSetBit( pNew->pData, k ); + if ( Abc_InfoHasBit( pCex->pData, i ) ) + Abc_InfoSetBit( pNew->pData, k ); assert( i <= pCex->nBits ); return pNew; } diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c index b2ea80a6..1f862c1a 100644 --- a/src/aig/saig/saigRefSat.c +++ b/src/aig/saig/saigRefSat.c @@ -19,8 +19,8 @@ ***********************************************************************/ #include "saig.h" -#include "cnf.h" -#include "satSolver.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START @@ -95,13 +95,13 @@ Abc_Cex_t * Saig_RefManReason2Cex( Saig_RefMan_t * p, Vec_Int_t * vReasons ) Abc_Cex_t * pCare; int i, Entry, iInput, iFrame; pCare = Abc_CexDup( p->pCex, p->pCex->nRegs ); - memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) ); + memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); Vec_IntForEachEntry( vReasons, Entry, i ) { assert( Entry >= 0 && Entry < Aig_ManPiNum(p->pFrames) ); iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 ); - Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); + Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); } return pCare; } @@ -181,7 +181,7 @@ Vec_Int_t * Saig_RefManFindReason( Saig_RefMan_t * p ) { int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); - pObj->fPhase = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); + pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); // assign priority if ( Vec_IntEntry(vPi2Prio, iInput) == ~0 ) Vec_IntWriteEntry( vPi2Prio, iInput, CountPrios++ ); @@ -295,11 +295,11 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu // derive unrolled timeframes pFrames = Aig_ManStart( 10000 ); - pFrames->pName = Aig_UtilStrsav( pAig->pName ); - pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); + pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec ); // initialize the flops Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Aig_InfoHasBit(pCex->pData, i) ); + pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, i) ); // iterate through the frames for ( f = 0; f <= pCex->iFrame; f++ ) { @@ -318,7 +318,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu if ( Aig_ObjPioNum(pObj) < nInputs ) { int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj); - pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Aig_InfoHasBit(pCex->pData, iBit) ); + pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) ); } else { @@ -409,9 +409,9 @@ int Saig_RefManSetPhases( Saig_RefMan_t * p, Abc_Cex_t * pCare, int fValue1 ) { iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); - pObj->fPhase = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); + pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); // update value if it is a don't-care - if ( pCare && !Aig_InfoHasBit( pCare->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ) ) + if ( pCare && !Abc_InfoHasBit( pCare->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ) ) pObj->fPhase = fValue1; } Aig_ManForEachNode( p->pFrames, pObj, i ) @@ -448,7 +448,7 @@ Vec_Vec_t * Saig_RefManOrderLiterals( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) ); iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum ); iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 ); -// Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); +// Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); if ( Vec_IntEntry( vVar2New, iInput ) == ~0 ) Vec_IntWriteEntry( vVar2New, iInput, Vec_VecSize(vLits) ); Vec_VecPushInt( vLits, Vec_IntEntry( vVar2New, iInput ), Entry ); @@ -475,14 +475,14 @@ Abc_Cex_t * Saig_RefManCreateCex( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, Vec_ int i, Entry, iInput, iFrame; // create counter-example pCare = Abc_CexDup( p->pCex, p->pCex->nRegs ); - memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) ); + memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); Vec_IntForEachEntry( vAssumps, Entry, i ) { int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) ); assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) ); iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum ); iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 ); - Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); + Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); } return pCare; } @@ -540,7 +540,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder ) printf( "The problem is trivially UNSAT. The CEX is real.\n" ); // create counter-example pCare = Abc_CexDup( p->pCex, p->pCex->nRegs ); - memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) ); + memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); return pCare; } // the problem is SAT - it is expected @@ -552,7 +552,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder ) { int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); -// RetValue = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); +// RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); // Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) ); Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) ); Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i ); @@ -740,7 +740,7 @@ Vec_Int_t * Saig_RefManRefineWithSat( Saig_RefMan_t * p, Vec_Int_t * vAigPis ) int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 ); if ( Vec_IntEntry(vVisited, iInput) == 0 ) continue; - RetValue = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); + RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) ); // Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) ); Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i ); diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c index cce7dcc6..3f06177c 100644 --- a/src/aig/saig/saigRetMin.c +++ b/src/aig/saig/saigRetMin.c @@ -20,10 +20,10 @@ #include "saig.h" -#include "nwk.h" -#include "cnf.h" -#include "satSolver.h" -#include "satStore.h" +#include "src/opt/nwk/nwk.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver.h" +#include "src/sat/bsat/satStore.h" ABC_NAMESPACE_IMPL_START @@ -287,8 +287,8 @@ Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut ) // assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) ); // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); - pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); pNew->nRegs = Vec_PtrSize(vCut); pNew->nTruePis = p->nTruePis; pNew->nTruePos = p->nTruePos; @@ -346,8 +346,8 @@ Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Int_ // assert( Vec_PtrSize(vCut) == Saig_ManRetimeCountCut(p, vCut) ); // create the new manager pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); - pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); pNew->nRegs = Vec_PtrSize(vCut); pNew->nTruePis = p->nTruePis; pNew->nTruePos = p->nTruePos; diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c index ac0fa697..021481b9 100644 --- a/src/aig/saig/saigSimExt.c +++ b/src/aig/saig/saigSimExt.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "saig.h" -#include "ssw.h" +#include "src/proof/ssw/ssw.h" ABC_NAMESPACE_IMPL_START @@ -111,12 +111,12 @@ int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i, f, Entry, iBit = 0; Saig_ManForEachLo( p, pObj, i ) - Saig_ManSimInfoSet( vSimInfo, pObj, 0, Aig_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER ); + Saig_ManSimInfoSet( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER ); for ( f = 0; f <= pCex->iFrame; f++ ) { Saig_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE ); Saig_ManForEachPi( p, pObj, i ) - Saig_ManSimInfoSet( vSimInfo, pObj, f, Aig_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER ); + Saig_ManSimInfoSet( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER ); if ( vRes ) Vec_IntForEachEntry( vRes, Entry, i ) Saig_ManSimInfoSet( vSimInfo, Aig_ManPi(p, Entry), f, SAIG_UND ); @@ -251,7 +251,7 @@ Vec_Int_t * Saig_ManExtendCounterExample0( Aig_Man_t * p, int iFirstFlopPi, Abc_ Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; int i, f, Value; // assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); + assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) ); // start simulation data Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); assert( Value == SAIG_ONE ); @@ -301,7 +301,7 @@ Vec_Int_t * Saig_ManExtendCounterExample1( Aig_Man_t * p, int iFirstFlopPi, Abc_ Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; int i, f, Value; // assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); + assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) ); // start simulation data Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); assert( Value == SAIG_ONE ); @@ -351,7 +351,7 @@ Vec_Int_t * Saig_ManExtendCounterExample2( Aig_Man_t * p, int iFirstFlopPi, Abc_ Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; int i, f, Value; // assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); + assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) ); // start simulation data Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); assert( Value == SAIG_ONE ); @@ -419,7 +419,7 @@ Vec_Int_t * Saig_ManExtendCounterExample3( Aig_Man_t * p, int iFirstFlopPi, Abc_ Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; int i, f, Value; // assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); + assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) ); // start simulation data Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); assert( Value == SAIG_ONE ); @@ -529,8 +529,8 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, A return NULL; } Aig_ManFanoutStart( p ); - vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) ); - Vec_PtrCleanSimInfo( vSimInfo, 0, Aig_BitWordNum(2*(pCex->iFrame+1)) ); + vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) ); + Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) ); clk = clock(); if ( fTryFour ) diff --git a/src/aig/saig/saigSimExt2.c b/src/aig/saig/saigSimExt2.c index 3d9cc88a..858c2b3b 100644 --- a/src/aig/saig/saigSimExt2.c +++ b/src/aig/saig/saigSimExt2.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "saig.h" -#include "ssw.h" +#include "src/proof/ssw/ssw.h" ABC_NAMESPACE_IMPL_START @@ -139,12 +139,12 @@ int Saig_ManSimDataInit2( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i, f, iBit = 0; Saig_ManForEachLo( p, pObj, i ) - Saig_ManSimInfo2Set( vSimInfo, pObj, 0, Aig_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW ); + Saig_ManSimInfo2Set( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW ); for ( f = 0; f <= pCex->iFrame; f++ ) { Saig_ManSimInfo2Set( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE_NEW ); Saig_ManForEachPi( p, pObj, i ) - Saig_ManSimInfo2Set( vSimInfo, pObj, f, Aig_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW ); + Saig_ManSimInfo2Set( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW ); Aig_ManForEachNode( p, pObj, i ) Saig_ManExtendOneEval2( vSimInfo, pObj, f ); Aig_ManForEachPo( p, pObj, i ) @@ -284,7 +284,7 @@ Vec_Int_t * Saig_ManProcessCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCe Vec_Int_t * vRes, * vResInv; int i, f, Value; // assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); + assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) ); // start simulation data Value = Saig_ManSimDataInit2( p, pCex, vSimInfo ); assert( Value == SAIG_ONE_NEW ); @@ -345,8 +345,8 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstFlopPi, return NULL; } Aig_ManFanoutStart( p ); - vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) ); - Vec_PtrCleanSimInfo( vSimInfo, 0, Aig_BitWordNum(2*(pCex->iFrame+1)) ); + vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) ); + Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) ); clk = clock(); vRes = Saig_ManProcessCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); @@ -382,7 +382,7 @@ Abc_Cex_t * Saig_ManDeriveCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex Vec_Int_t * vRes, * vResInv; int i, f, Value; // assert( Aig_ManRegNum(p) > 0 ); - assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); + assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) ); // start simulation data Value = Saig_ManSimDataInit2( p, pCex, vSimInfo ); assert( Value == SAIG_ONE_NEW ); @@ -400,7 +400,7 @@ Abc_Cex_t * Saig_ManDeriveCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex // create CEX pCare = Abc_CexDup( pCex, pCex->nRegs ); - memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) ); + memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); // select the result vRes = Vec_IntAlloc( 1000 ); @@ -414,7 +414,7 @@ Abc_Cex_t * Saig_ManDeriveCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex if ( Saig_ManSimInfo2IsOld( Value ) ) { fFound = 1; - Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * f + i ); + Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * f + i ); } } if ( fFound ) @@ -454,8 +454,8 @@ Abc_Cex_t * Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int i return NULL; } Aig_ManFanoutStart( p ); - vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) ); - Vec_PtrCleanSimInfo( vSimInfo, 0, Aig_BitWordNum(2*(pCex->iFrame+1)) ); + vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) ); + Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) ); clk = clock(); pCare = Saig_ManDeriveCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); diff --git a/src/aig/saig/saigSimFast.c b/src/aig/saig/saigSimFast.c index 1840eaa7..b8eed19e 100644 --- a/src/aig/saig/saigSimFast.c +++ b/src/aig/saig/saigSimFast.c @@ -20,7 +20,7 @@ #include "saig.h" -#include "main.h" +#include "src/base/main/main.h" ABC_NAMESPACE_IMPL_START diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c index 7076d07b..6579c37b 100644 --- a/src/aig/saig/saigSimMv.c +++ b/src/aig/saig/saigSimMv.c @@ -184,7 +184,7 @@ static inline int Saig_MvCreateObj( Saig_MvMan_t * p, int iFan0, int iFan1 ) pNode->iFan1 = iFan1; pNode->iNext = 0; if ( iFan0 || iFan1 ) - p->pLevels[p->nObjs] = 1 + ABC_MAX( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) ); + p->pLevels[p->nObjs] = 1 + Abc_MaxInt( Saig_MvLev(p, iFan0), Saig_MvLev(p, iFan1) ); else p->pLevels[p->nObjs] = 0, p->nPis++; return p->nObjs++; @@ -216,7 +216,7 @@ Saig_MvMan_t * Saig_MvManStart( Aig_Man_t * pAig, int nFramesSatur ) p->nFlops = Aig_ManRegNum(pAig); // compacted AIG p->pAigOld = Saig_ManCreateReducedAig( pAig, &p->vFlops ); - p->nTStatesSize = Aig_PrimeCudd( p->nStatesMax ); + p->nTStatesSize = Abc_PrimeCudd( p->nStatesMax ); p->pTStates = ABC_CALLOC( unsigned, p->nTStatesSize ); p->pMemStates = Aig_MmFixedStart( sizeof(int) * (p->nFlops+1), p->nStatesMax ); p->vStates = Vec_PtrAlloc( p->nStatesMax ); @@ -231,7 +231,7 @@ Saig_MvMan_t * Saig_MvManStart( Aig_Man_t * pAig, int nFramesSatur ) // internal AIG p->nObjsAlloc = 1000000; p->pAigNew = ABC_ALLOC( Saig_MvAnd_t, p->nObjsAlloc ); - p->nTNodesSize = Aig_PrimeCudd( p->nObjsAlloc / 3 ); + p->nTNodesSize = Abc_PrimeCudd( p->nObjsAlloc / 3 ); p->pTNodes = ABC_CALLOC( int, p->nTNodesSize ); p->pLevels = ABC_ALLOC( unsigned char, p->nObjsAlloc ); Saig_MvCreateObj( p, 0, 0 ); diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c index cc5a9e05..538afef0 100644 --- a/src/aig/saig/saigSimSeq.c +++ b/src/aig/saig/saigSimSeq.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "saig.h" -#include "ssw.h" +#include "src/proof/ssw/ssw.h" ABC_NAMESPACE_IMPL_START @@ -433,8 +433,8 @@ Abc_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int continue; for ( w = 0; w < nWords; w++ ) pData[w] = Aig_ManRandom( 0 ); - if ( Aig_InfoHasBit( pData, iPat ) ) - Aig_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/saig/saigStrSim.c b/src/aig/saig/saigStrSim.c index 1d69630f..cdf177d0 100644 --- a/src/aig/saig/saigStrSim.c +++ b/src/aig/saig/saigStrSim.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "saig.h" -#include "ssw.h" +#include "src/proof/ssw/ssw.h" ABC_NAMESPACE_IMPL_START @@ -398,7 +398,7 @@ int Saig_StrSimDetectUnique( Aig_Man_t * p0, Aig_Man_t * p1 ) int i, nTableSize, Counter; // allocate the hash table hashing simulation info into nodes - nTableSize = Aig_PrimeCudd( Aig_ManObjNum(p0)/2 ); + nTableSize = Abc_PrimeCudd( Aig_ManObjNum(p0)/2 ); ppTable = ABC_CALLOC( Aig_Obj_t *, nTableSize ); ppNexts = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) ); ppCands = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p0) ); diff --git a/src/aig/saig/saigSwitch.c b/src/aig/saig/saigSwitch.c index bbad9be4..01411c05 100644 --- a/src/aig/saig/saigSwitch.c +++ b/src/aig/saig/saigSwitch.c @@ -20,7 +20,7 @@ #include "saig.h" -#include "main.h" +#include "src/base/main/main.h" ABC_NAMESPACE_IMPL_START diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c index 00f7517e..08a10b66 100644 --- a/src/aig/saig/saigSynch.c +++ b/src/aig/saig/saigSynch.c @@ -471,7 +471,7 @@ Aig_Man_t * Saig_ManDupInitZero( Aig_Man_t * p ) Aig_Obj_t * pObj; int i; pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pName = Abc_UtilStrsav( p->pName ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Saig_ManForEachPi( p, pObj, i ) pObj->pData = Aig_ObjCreatePi( pNew ); @@ -619,7 +619,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords, return NULL; } clk = clock(); - vSimInfo = Vec_PtrAllocSimInfo( ABC_MAX( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 ); + vSimInfo = Vec_PtrAllocSimInfo( Abc_MaxInt( Aig_ManObjNumMax(pAig1), Aig_ManObjNumMax(pAig2) ), 1 ); // process Design 1 RetValue = Saig_SynchSequenceRun( pAig1, vSimInfo, vSeq1, 1 ); diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c index fc57c1f5..1a6f1919 100644 --- a/src/aig/saig/saigTempor.c +++ b/src/aig/saig/saigTempor.c @@ -50,7 +50,7 @@ Aig_Man_t * Saig_ManTemporFrames( Aig_Man_t * pAig, int nFrames ) // start the frames package Aig_ManCleanData( pAig ); pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * nFrames ); - pFrames->pName = Aig_UtilStrsav( pAig->pName ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); // initiliaze the flops Saig_ManForEachLo( pAig, pObj, i ) pObj->pData = Aig_ManConst0(pFrames); @@ -103,7 +103,7 @@ Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames ) // start the new manager Aig_ManCleanData( pAig ); pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pAigNew->pName = Abc_UtilStrsav( pAig->pName ); // map the constant node and primary inputs Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); Saig_ManForEachPi( pAig, pObj, i ) diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c index 09639e27..11e775e5 100644 --- a/src/aig/saig/saigTrans.c +++ b/src/aig/saig/saigTrans.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "saig.h" -#include "fra.h" +#include "src/proof/fra/fra.h" ABC_NAMESPACE_IMPL_START diff --git a/src/aig/saig/saigWnd.c b/src/aig/saig/saigWnd.c index c11798ea..6753370f 100644 --- a/src/aig/saig/saigWnd.c +++ b/src/aig/saig/saigWnd.c @@ -232,7 +232,7 @@ Aig_Man_t * Saig_ManWindowExtractNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes ) Aig_ManCleanData( p ); // create the new manager pNew = Aig_ManStart( Vec_PtrSize(vNodes) ); - pNew->pName = Aig_UtilStrsav( "wnd" ); + pNew->pName = Abc_UtilStrsav( "wnd" ); pNew->pSpec = NULL; // map constant nodes pObj = Aig_ManConst1( p ); @@ -375,8 +375,8 @@ Aig_Man_t * Saig_ManWindowInsertNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes, Aig_Ma Aig_ManCleanData( p ); Aig_ManCleanData( pWnd ); pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); - pNew->pName = Aig_UtilStrsav( p->pName ); - pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); // map constant nodes pObj = Aig_ManConst1( p ); pObj->pData = Aig_ManConst1( pNew ); @@ -745,7 +745,7 @@ Aig_Man_t * Saig_ManWindowExtractMiter( Aig_Man_t * p0, Aig_Man_t * p1 ) vNodes1 = Saig_ManCollectedDiffNodes( p1, p0 ); // create the new manager pNew = Aig_ManStart( Vec_PtrSize(vNodes0) + Vec_PtrSize(vNodes1) ); - pNew->pName = Aig_UtilStrsav( "wnd" ); + pNew->pName = Abc_UtilStrsav( "wnd" ); pNew->pSpec = NULL; // map constant nodes pObj0 = Aig_ManConst1( p0 ); |