diff options
Diffstat (limited to 'src/aig/saig')
39 files changed, 291 insertions, 291 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 8fde2ef6..0f2234b7 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -101,27 +101,27 @@ static inline int Saig_ManCiNum( Aig_Man_t * p ) { static inline int Saig_ManCoNum( Aig_Man_t * p ) { return p->nTruePos + p->nRegs; } static inline int Saig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; } static inline int Saig_ManConstrNum( Aig_Man_t * p ) { return p->nConstrs; } -static inline Aig_Obj_t * Saig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+i); } -static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+i); } - -static inline int Saig_ObjIsPi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPi(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPiNum(p); } -static inline int Saig_ObjIsPo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPoNum(p); } -static inline int Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPi(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPiNum(p); } -static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsPo(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPoNum(p); } -static inline Aig_Obj_t * Saig_ObjLoToLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLo(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPiNum(p)); } -static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLi(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPoNum(p)); } +static inline Aig_Obj_t * Saig_ManLo( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, Saig_ManPiNum(p)+i); } +static inline Aig_Obj_t * Saig_ManLi( Aig_Man_t * p, int i ) { return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, Saig_ManPoNum(p)+i); } + +static inline int Saig_ObjIsPi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCi(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPiNum(p); } +static inline int Saig_ObjIsPo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCo(pObj) && Aig_ObjPioNum(pObj) < Saig_ManPoNum(p); } +static inline int Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCi(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPiNum(p); } +static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCo(pObj) && Aig_ObjPioNum(pObj) >= Saig_ManPoNum(p); } +static inline Aig_Obj_t * Saig_ObjLoToLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLo(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vCos, Saig_ManPoNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPiNum(p)); } +static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(Saig_ObjIsLi(p, pObj)); return (Aig_Obj_t *)Vec_PtrEntry(p->vCis, Saig_ManPiNum(p)+Aig_ObjPioNum(pObj)-Saig_ManPoNum(p)); } static inline int Saig_ObjRegId( Aig_Man_t * p, Aig_Obj_t * pObj ) { if ( Saig_ObjIsLo(p, pObj) ) return Aig_ObjPioNum(pObj)-Saig_ManPiNum(p); if ( Saig_ObjIsLi(p, pObj) ) return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p); else assert(0); return -1; } // iterator over the primary inputs/outputs #define Saig_ManForEachPi( p, pObj, i ) \ - Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vPis, pObj, i, Saig_ManPiNum(p) ) + Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCis, pObj, i, Saig_ManPiNum(p) ) #define Saig_ManForEachPo( p, pObj, i ) \ - Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vPos, pObj, i, Saig_ManPoNum(p) ) + Vec_PtrForEachEntryStop( Aig_Obj_t *, p->vCos, pObj, i, Saig_ManPoNum(p) ) // iterator over the latch inputs/outputs #define Saig_ManForEachLo( p, pObj, i ) \ - for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vPis, i+Saig_ManPiNum(p))), 1); i++ ) + for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vCis, i+Saig_ManPiNum(p))), 1); i++ ) #define Saig_ManForEachLi( p, pObj, i ) \ - for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vPos, i+Saig_ManPoNum(p))), 1); i++ ) + for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObj) = (Aig_Obj_t *)Vec_PtrEntry(p->vCos, i+Saig_ManPoNum(p))), 1); i++ ) // iterator over the latch input and outputs #define Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) \ for ( i = 0; (i < Saig_ManRegNum(p)) && (((pObjLi) = Saig_ManLi(p, i)), 1) \ @@ -185,7 +185,7 @@ extern Aig_Man_t * Saig_ManReadBlif( char * pFileName ); /*=== saigIso.c ==========================================================*/ extern Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose ); extern Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose ); -extern Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fVerbose ); +extern Aig_Man_t * Saig_ManIsoReduce( Aig_Man_t * pAig, Vec_Ptr_t ** pvCosEquivs, int fVerbose ); /*=== saigIsoFast.c ==========================================================*/ extern Vec_Vec_t * Saig_IsoDetectFast( Aig_Man_t * pAig ); /*=== saigMiter.c ==========================================================*/ diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c index c68143d4..d7975d92 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/aig/saig/saigAbsCba.c @@ -202,7 +202,7 @@ Vec_Int_t * Saig_ManCbaReason2Inputs( Saig_ManCba_t * p, Vec_Int_t * vReasons ) Vec_IntForEachEntry( vReasons, Entry, i ) { int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); - assert( iInput >= p->nInputs && iInput < Aig_ManPiNum(p->pAig) ); + assert( iInput >= p->nInputs && iInput < Aig_ManCiNum(p->pAig) ); if ( Vec_IntEntry(vVisited, iInput) == 0 ) Vec_IntPush( vOriginal, iInput - p->nInputs ); Vec_IntAddToEntry( vVisited, iInput, 1 ); @@ -230,7 +230,7 @@ Abc_Cex_t * Saig_ManCbaReason2Cex( Saig_ManCba_t * p, Vec_Int_t * vReasons ) memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); Vec_IntForEachEntry( vReasons, Entry, i ) { - assert( Entry >= 0 && Entry < Aig_ManPiNum(p->pFrames) ); + assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pFrames) ); iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 ); Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); @@ -266,7 +266,7 @@ void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr Aig_ObjSetTravIdCurrent(p, pObj); if ( Aig_ObjIsConst1(pObj) ) return; - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) ); return; @@ -344,7 +344,7 @@ Vec_Int_t * Saig_ManCbaFindReason( Saig_ManCba_t * p ) Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) ); } // check the property output - pObj = Aig_ManPo( p->pFrames, 0 ); + pObj = Aig_ManCo( p->pFrames, 0 ); pObj->fPhase = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase; assert( !pObj->fPhase ); @@ -374,7 +374,7 @@ void Saig_ManCbaUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) return; Aig_ObjSetTravIdCurrent(pAig, pObj); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); else if ( Aig_ObjIsNode(pObj) ) { @@ -417,7 +417,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI vFrameCos = Vec_VecStart( pCex->iFrame+1 ); vFrameObjs = Vec_VecStart( pCex->iFrame+1 ); // initialized the topmost frame - pObj = Aig_ManPo( pAig, pCex->iPo ); + pObj = Aig_ManCo( pAig, pCex->iPo ); Vec_VecPushInt( vFrameCos, pCex->iFrame, Aig_ObjId(pObj) ); for ( f = pCex->iFrame; f >= 0; f-- ) { @@ -454,7 +454,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI { if ( Aig_ObjIsNode(pObj) ) pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) pObj->pData = Aig_ObjChild0Copy(pObj); else if ( Aig_ObjIsConst1(pObj) ) pObj->pData = Aig_ManConst1(pFrames); @@ -488,7 +488,7 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI } } // create output - pObj = Aig_ManPo( pAig, pCex->iPo ); + pObj = Aig_ManCo( pAig, pCex->iPo ); Aig_ObjCreateCo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) ); Aig_ManSetRegNum( pFrames, 0 ); // cleanup @@ -611,7 +611,7 @@ static inline void Saig_ObjCexMinSim( Aig_Obj_t * pObj ) else Saig_ObjCexMinSetX( pObj ); } - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) { if ( Saig_ObjCexMinGet0Fanin0(pObj) ) Saig_ObjCexMinSet0( pObj ); @@ -700,7 +700,7 @@ int Saig_ManCexVerifyUsingTernary( Aig_Man_t * pAig, Abc_Cex_t * pCex, Abc_Cex_t pObjRo->fMarkB = pObjRi->fMarkB; } assert( iBit == pCex->nBits ); - return Saig_ObjCexMinGet1( Aig_ManPo( pAig, pCex->iPo ) ); + return Saig_ObjCexMinGet1( Aig_ManCo( pAig, pCex->iPo ) ); } /**Function************************************************************* @@ -741,7 +741,7 @@ Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int { Vec_Int_t * vRes = Saig_ManCbaReason2Inputs( p, vReasons ); printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", - Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), + Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); Vec_IntFree( vRes ); ABC_PRT( "Time", clock() - clk ); @@ -789,7 +789,7 @@ Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex if ( Saig_ManPiNum(pAig) != pCex->nPis ) { printf( "Saig_ManCbaFilterInputs(): The PI count of AIG (%d) does not match that of cex (%d).\n", - Aig_ManPiNum(pAig), pCex->nPis ); + Aig_ManCiNum(pAig), pCex->nPis ); return NULL; } @@ -801,7 +801,7 @@ clk = clock(); if ( fVerbose ) { printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", - Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), + Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); ABC_PRT( "Time", clock() - clk ); } diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c index 736cd699..b735f3c0 100644 --- a/src/aig/saig/saigAbsPba.c +++ b/src/aig/saig/saigAbsPba.c @@ -49,7 +49,7 @@ void Saig_ManUnrollForPba_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * v if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) return; Aig_ObjSetTravIdCurrent(pAig, pObj); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); else if ( Aig_ObjIsNode(pObj) ) { @@ -106,7 +106,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec Aig_ObjCreateCi( pFrames ); // initialize the flops Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_Mux( pFrames, Aig_ManPi(pFrames,i), Aig_ObjCreateCi(pFrames), Aig_ManConst0(pFrames) ); + pObj->pData = Aig_Mux( pFrames, Aig_ManCi(pFrames,i), Aig_ObjCreateCi(pFrames), Aig_ManConst0(pFrames) ); // iterate through the frames *pvPiVarMap = Vec_IntStartFull( nFrames * Saig_ManPiNum(pAig) ); pObjNew = Aig_ManConst0(pFrames); @@ -118,11 +118,11 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec { if ( Aig_ObjIsNode(pObj) ) pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) pObj->pData = Aig_ObjChild0Copy(pObj); else if ( Saig_ObjIsPi(pAig, pObj) ) { - Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjPioNum(pObj), Aig_ManPiNum(pFrames) ); + Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjPioNum(pObj), Aig_ManCiNum(pFrames) ); pObj->pData = Aig_ObjCreateCi( pFrames ); } else if ( Aig_ObjIsConst1(pObj) ) @@ -146,7 +146,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec { int iFlopNum = Aig_ObjPioNum(pObj) - Saig_ManPoNum(pAig); assert( iFlopNum >= 0 && iFlopNum < Aig_ManRegNum(pAig) ); - Saig_ObjLiToLo(pAig, pObj)->pData = Aig_Mux( pFrames, Aig_ManPi(pFrames,iFlopNum), Aig_ObjCreateCi(pFrames), (Aig_Obj_t *)pObj->pData ); + Saig_ObjLiToLo(pAig, pObj)->pData = Aig_Mux( pFrames, Aig_ManCi(pFrames,iFlopNum), Aig_ObjCreateCi(pFrames), (Aig_Obj_t *)pObj->pData ); } } } @@ -184,7 +184,7 @@ Abc_Cex_t * Saig_ManPbaDeriveCex( Aig_Man_t * pAig, sat_solver * pSat, Cnf_Dat_t { if ( Entry >= 0 ) { - int iSatVar = pCnf->pVarNums[ Aig_ObjId(Aig_ManPi(pCnf->pMan, Entry)) ]; + int iSatVar = pCnf->pVarNums[ Aig_ObjId(Aig_ManCi(pCnf->pMan, Entry)) ]; if ( sat_solver_var_value( pSat, iSatVar ) ) Abc_InfoSetBit( pCex->pData, Aig_ManRegNum(pAig) + i ); } diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c index eb02eba9..d6583862 100644 --- a/src/aig/saig/saigAbsStart.c +++ b/src/aig/saig/saigAbsStart.c @@ -145,7 +145,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo { Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry); assert( Entry >= Saig_ManPiNum(p) ); - assert( Entry < Aig_ManPiNum(p) ); + assert( Entry < Aig_ManCiNum(p) ); Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) ); } Vec_IntFree( vFlopsNew ); @@ -187,7 +187,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopC if ( Vec_IntSize(vFlopsNew) == 0 ) { printf( "Refinement did not happen. Discovered a true counter-example.\n" ); - printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManPiNum(pAbs), Aig_ManPiNum(p) ); + printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManCiNum(pAbs), Aig_ManCiNum(p) ); p->pSeqModel = Saig_ManCexRemap( p, pAbs, pCex ); Vec_IntFree( vFlopsNew ); Aig_ManStop( pAbs ); @@ -222,7 +222,7 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vFlopC { Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry); assert( Entry >= Saig_ManPiNum(p) ); - assert( Entry < Aig_ManPiNum(p) ); + assert( Entry < Aig_ManCiNum(p) ); Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) ); } Vec_IntFree( vFlopsNew ); diff --git a/src/aig/saig/saigAbsVfa.c b/src/aig/saig/saigAbsVfa.c index c3243b0e..897c1638 100644 --- a/src/aig/saig/saigAbsVfa.c +++ b/src/aig/saig/saigAbsVfa.c @@ -183,11 +183,11 @@ int Abs_VfaManCreateFrame_rec( Abs_VfaMan_t * p, Aig_Obj_t * pObj, int f ) if ( Aig_ObjIsConst1(pObj) ) return -1; SatVar = Abs_VfaManAddVar( p, pObj, f, &fNew ); - if ( (SatVar > 0 && !fNew) || Saig_ObjIsPi(p->pAig, pObj) || (Aig_ObjIsPi(pObj) && f==0) ) + if ( (SatVar > 0 && !fNew) || Saig_ObjIsPi(p->pAig, pObj) || (Aig_ObjIsCi(pObj) && f==0) ) return SatVar; - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) return Abs_VfaManCreateFrame_rec( p, Aig_ObjFanin0(pObj), f ); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) return Abs_VfaManCreateFrame_rec( p, Saig_ObjLoToLi(p->pAig, pObj), f-1 ); assert( Aig_ObjIsAnd(pObj) ); Abs_VfaManCreateFrame_rec( p, Aig_ObjFanin0(pObj), f ); diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index b0ae1750..60f406ad 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -203,7 +203,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim else if ( nSizeMax > 0 ) { pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax ); - nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0); + nFrames = Aig_ManCoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManCoNum(pFrames) % Saig_ManPoNum(pAig)) > 0); } else pFrames = Saig_ManFramesBmc( pAig, nFrames ); @@ -215,7 +215,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ", - nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), + nFrames, Aig_ManCiNum(pFrames), Aig_ManCoNum(pFrames), Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) ); ABC_PRT( "Time", clock() - clk ); fflush( stdout ); @@ -237,7 +237,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } // create the SAT solver clk = clock(); - pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) ); + pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) ); //if ( s_fInterrupt ) //return -1; pSat = sat_solver_new(); @@ -303,7 +303,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim { Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames ); int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); - pModel[Aig_ManPiNum(pFrames)] = pObj->Id; + pModel[Aig_ManCiNum(pFrames)] = pObj->Id; pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel ); ABC_FREE( pModel ); Vec_IntFree( vCiIds ); diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index a3e3ea71..ca6049ef 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -129,7 +129,7 @@ int Abs_ManExtendOneEval_rec( Vec_Ptr_t * vSimInfo, Aig_Man_t * p, Aig_Obj_t * p Value = Abs_ManSimInfoGet( vSimInfo, pObj, iFrame ); if ( Value ) return Value; - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { assert( Saig_ObjIsLo(p, pObj) ); Value = Abs_ManExtendOneEval_rec( vSimInfo, p, Saig_ObjLoToLi(p, pObj), iFrame-1 ); @@ -139,7 +139,7 @@ int Abs_ManExtendOneEval_rec( Vec_Ptr_t * vSimInfo, Aig_Man_t * p, Aig_Obj_t * p Value0 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin0(pObj), iFrame ); if ( Aig_ObjFaninC0(pObj) ) Value0 = Abs_ManSimInfoNot( Value0 ); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 ); return Value0; @@ -358,7 +358,7 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i pRes = AIG_VISITED; else if ( Saig_ObjIsLo( p->pAig, pObj ) ) pRes = Saig_BmcIntervalExplore_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 ); - else if ( Aig_ObjIsPo( pObj ) ) + else if ( Aig_ObjIsCo( pObj ) ) { pRes = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i ); if ( pRes != AIG_VISITED ) @@ -410,7 +410,7 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int pRes = Aig_ObjCreateCi(p->pFrm); else if ( Saig_ObjIsLo( p->pAig, pObj ) ) pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1, vVisited ); - else if ( Aig_ObjIsPo( pObj ) ) + else if ( Aig_ObjIsCo( pObj ) ) { Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited ); pRes = Saig_BmcObjChild0( p, pObj, i ); @@ -462,9 +462,9 @@ void Saig_BmcInterval( Saig_Bmc_t * p ) { if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax ) return; -// Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast ); +// Saig_BmcIntervalExplore_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast ); Vec_PtrClear( p->vVisited ); - pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited ); + pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited ); Vec_PtrPush( p->vTargets, pTarget ); Aig_ObjCreateCo( p->pFrm, pTarget ); Aig_ManCleanup( p->pFrm ); @@ -501,9 +501,9 @@ Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj if ( pObj->pData ) return (Aig_Obj_t *)pObj->pData; Vec_PtrPush( p->vVisited, pObj ); - if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsPi(pObj) ) + if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsCi(pObj) ) { - p->nStitchVars += !Aig_ObjIsPi(pObj); + p->nStitchVars += !Aig_ObjIsCi(pObj); return (Aig_Obj_t *)(pObj->pData = Aig_ObjCreateCi(pNew)); } Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) ); @@ -784,7 +784,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax pNew = Saig_BmcIntervalToAig( p ); //printf( "StitchVars = %d.\n", p->nStitchVars ); // derive CNF for the new AIG - pCnf = Cnf_Derive( pNew, Aig_ManPoNum(pNew) ); + pCnf = Cnf_Derive( pNew, Aig_ManCoNum(pNew) ); Cnf_DataLift( pCnf, p->nSatVars ); p->nSatVars += pCnf->nVars; // add this CNF to the solver diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 19753c3c..e96d0039 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -352,7 +352,7 @@ void Saig_ManBmcSectionsTest( Aig_Man_t * p ) void Saig_ManBmcSupergate_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper ) { // if the new node is complemented or a PI, another gate begins - if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) ) // || (Aig_ObjRefs(pObj) > 1) ) + if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ) // || (Aig_ObjRefs(pObj) > 1) ) { Vec_PtrPushUnique( vSuper, Aig_Regular(pObj) ); return; @@ -378,7 +378,7 @@ Vec_Ptr_t * Saig_ManBmcSupergate( Aig_Man_t * p, int iPo ) Vec_Ptr_t * vSuper; Aig_Obj_t * pObj; vSuper = Vec_PtrAlloc( 10 ); - pObj = Aig_ManPo( p, iPo ); + pObj = Aig_ManCo( p, iPo ); pObj = Aig_ObjChild0( pObj ); if ( !Aig_IsComplement(pObj) ) { @@ -905,7 +905,7 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in if ( iLit != ~0 ) return iLit; assert( iFrame >= 0 ); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { if ( Saig_ObjIsPi(p->pAig, pObj) ) iLit = fAddClauses ? toLit( p->nSatVars++ ) : ABC_INFINITY; @@ -913,7 +913,7 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in iLit = Saig_ManBmcCreateCnf_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame-1, fAddClauses ); return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit ); } - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { iLit = Saig_ManBmcCreateCnf_rec( p, Aig_ObjFanin0(pObj), iFrame, fAddClauses ); if ( Aig_ObjFaninC0(pObj) ) diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c index 2fb5cd54..466159e6 100644 --- a/src/aig/saig/saigCexMin.c +++ b/src/aig/saig/saigCexMin.c @@ -50,7 +50,7 @@ void Saig_ManCexMinGetCos( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Int_t * vLeav Vec_IntClear( vRoots ); if ( vLeaves == NULL ) { - pObj = Aig_ManPo( pAig, pCex->iPo ); + pObj = Aig_ManCo( pAig, pCex->iPo ); Vec_IntPush( vRoots, Aig_ObjId(pObj) ); return; } @@ -75,14 +75,14 @@ void Saig_ManCexMinCollectFrameTerms_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Ve if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) return; Aig_ObjSetTravIdCurrent(pAig, pObj); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFrameCisOne ); else if ( Aig_ObjIsNode(pObj) ) { Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFrameCisOne ); Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin1(pObj), vFrameCisOne ); } - else if ( Aig_ObjIsPi(pObj) ) + else if ( Aig_ObjIsCi(pObj) ) Vec_IntPush( vFrameCisOne, Aig_ObjId(pObj) ); } @@ -138,7 +138,7 @@ void Saig_ManCexMinDerivePhasePriority_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj ) if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) return; Aig_ObjSetTravIdCurrent(pAig, pObj); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin0(pObj) ); assert( Aig_ObjFanin0(pObj)->iData >= 0 ); @@ -277,7 +277,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * p assert( Vec_IntSize(vFramePPsOne) == 0 ); Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i ) { - assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsCi(pObj) ); if ( Saig_ObjIsPi(pAig, 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 ) @@ -290,7 +290,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 ); + pObj = Aig_ManCo( pAig, pCex->iPo ); assert( Abc_LitIsCompl(pObj->iData) ); return vFramePPs; } @@ -331,7 +331,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC assert( Vec_IntSize(vFramePPsOne) == 0 ); Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i ) { - assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsCi(pObj) ); if ( Saig_ObjIsPi(pAig, 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 ) @@ -344,7 +344,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 ); + pObj = Aig_ManCo( pAig, pCex->iPo ); assert( Abc_LitIsCompl(pObj->iData) ); return vFramePPs; } @@ -366,7 +366,7 @@ void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t if ( Aig_ObjIsTravIdCurrent(p, pObj) ) return; Aig_ObjSetTravIdCurrent(p, pObj); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { if ( fPiReason && Saig_ObjIsPi(p, pObj) ) Vec_IntPush( vReason, Abc_Var2Lit( Aig_ObjPioNum(pObj), !Abc_LitIsCompl(pObj->iData) ) ); @@ -374,7 +374,7 @@ void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t Vec_IntPush( vReason, Abc_Var2Lit( Saig_ObjRegId(p, pObj), !Abc_LitIsCompl(pObj->iData) ) ); return; } - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason ); return; diff --git a/src/aig/saig/saigCone.c b/src/aig/saig/saigCone.c index 2b0da5c9..a6b0d864 100644 --- a/src/aig/saig/saigCone.c +++ b/src/aig/saig/saigCone.c @@ -49,7 +49,7 @@ void Saig_ManSupport_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp ) Aig_ObjSetTravIdCurrent(p, pObj); if ( Aig_ObjIsConst1(pObj) ) return; - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { if ( Saig_ObjIsLo(p,pObj) ) { @@ -83,7 +83,7 @@ Vec_Ptr_t * Saig_ManSupport( Aig_Man_t * p, Vec_Ptr_t * vNodes ) Aig_ManIncrementTravId( p ); Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) { - assert( Aig_ObjIsPo(pObj) ); + assert( Aig_ObjIsCo(pObj) ); Saig_ManSupport_rec( p, Aig_ObjFanin0(pObj), vSupp ); } return vSupp; diff --git a/src/aig/saig/saigConstr.c b/src/aig/saig/saigConstr.c index 7f45b844..6b90f2c1 100644 --- a/src/aig/saig/saigConstr.c +++ b/src/aig/saig/saigConstr.c @@ -128,7 +128,7 @@ Aig_Man_t * Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * vConstrs ) Vec_IntForEachEntry( vConstrs, Entry, i ) { assert( Entry > 0 && Entry < Saig_ManPoNum(pAig) ); - pObj = Aig_ManPo( pAig, Entry ); + pObj = Aig_ManCo( pAig, Entry ); pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) ); } // create additional flop @@ -283,7 +283,7 @@ int Saig_ManDetectConstr( Aig_Man_t * p, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvCon printf( "The number of POs is other than 1.\n" ); return 0; } - pObj = Aig_ObjChild0( Aig_ManPo(p, 0) ); + pObj = Aig_ObjChild0( Aig_ManCo(p, 0) ); if ( Aig_IsComplement(pObj) || !Aig_ObjIsNode(pObj) ) { printf( "The output is not an AND.\n" ); diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c index 3532ac3f..f54f2dbe 100644 --- a/src/aig/saig/saigConstr2.c +++ b/src/aig/saig/saigConstr2.c @@ -312,7 +312,7 @@ int Saig_ManFilterUsingIndOne_new( Aig_Man_t * p, Aig_Man_t * pFrame, sat_solver { Aig_Obj_t * pObj; int Lit, status; - pObj = Aig_ManPo( pFrame, Counter ); + pObj = Aig_ManCo( pFrame, Counter ); Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 0 ); status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 ); if ( status == l_False ) @@ -354,9 +354,9 @@ void Saig_ManFilterUsingInd( Aig_Man_t * p, Vec_Vec_t * vCands, int nConfs, int // create timeframes // pFrames = Saig_ManUnrollInd( p ); pFrames = Saig_ManCreateIndMiter( p, vCands ); - assert( Aig_ManPoNum(pFrames) == Vec_VecSizeSize(vCands) ); + assert( Aig_ManCoNum(pFrames) == Vec_VecSizeSize(vCands) ); // start the SAT solver - pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) ); + pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); // check candidates if ( fVerbose ) @@ -500,7 +500,7 @@ void Saig_CollectSatValues( sat_solver * pSat, Cnf_Dat_t * pCnf, Vec_Ptr_t * vIn int i; Aig_ManForEachObj( pCnf->pMan, pObj, i ) { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; assert( pCnf->pVarNums[i] > 0 ); pInfo = (unsigned *)Vec_PtrEntry( vInfo, i ); @@ -522,7 +522,7 @@ void Saig_CollectSatValues( sat_solver * pSat, Cnf_Dat_t * pCnf, Vec_Ptr_t * vIn ***********************************************************************/ int Saig_DetectTryPolarity( sat_solver * pSat, int nConfs, int nProps, Cnf_Dat_t * pCnf, Aig_Obj_t * pObj, int iPol, Vec_Ptr_t * vInfo, int * piPat, int fVerbose ) { - Aig_Obj_t * pOut = Aig_ManPo( pCnf->pMan, 0 ); + Aig_Obj_t * pOut = Aig_ManCo( pCnf->pMan, 0 ); int status, Lits[2]; // ABC_INT64_T nOldConfs = pSat->stats.conflicts; // ABC_INT64_T nOldImps = pSat->stats.propagations; @@ -576,7 +576,7 @@ Vec_Vec_t * Ssw_ManFindDirectImplications( Aig_Man_t * p, int nFrames, int nConf // perform unrolling pFrames = Saig_ManUnrollCOI( p, nFrames ); - assert( Aig_ManPoNum(pFrames) == 1 ); + assert( Aig_ManCoNum(pFrames) == 1 ); // start the SAT solver pCnf = Cnf_DeriveSimple( pFrames, 0 ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); @@ -679,7 +679,7 @@ Vec_Vec_t * Saig_ManDetectConstrFunc( Aig_Man_t * p, int nFrames, int nConfs, in // perform unrolling pFrames = Saig_ManUnrollCOI( p, nFrames ); - assert( Aig_ManPoNum(pFrames) == 1 ); + assert( Aig_ManCoNum(pFrames) == 1 ); if ( fVerbose ) { printf( "Detecting constraints with %d frames, %d conflicts, and %d propagations.\n", nFrames, nConfs, nProps ); @@ -689,12 +689,12 @@ Vec_Vec_t * Saig_ManDetectConstrFunc( Aig_Man_t * p, int nFrames, int nConfs, in // Aig_ManShow( pFrames, 0, NULL ); // start the SAT solver - pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) ); + pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); //printf( "Implications = %d.\n", pSat->qhead ); // solve the original problem - Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(Aig_ManPo(pFrames,0))], 0 ); + Lit = toLitCond( pCnf->pVarNums[Aig_ObjId(Aig_ManCo(pFrames,0))], 0 ); status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfs, 0, 0, 0 ); if ( status == l_False ) { @@ -732,7 +732,7 @@ Vec_Vec_t * Saig_ManDetectConstrFunc( Aig_Man_t * p, int nFrames, int nConfs, in Aig_ManCleanMarkAB( pFrames ); Aig_ManForEachObj( pFrames, pObj, i ) { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; Bar_ProgressUpdate( pProgress, i, NULL ); // check if the node is available in both polarities @@ -774,7 +774,7 @@ Vec_Vec_t * Saig_ManDetectConstrFunc( Aig_Man_t * p, int nFrames, int nConfs, in { Aig_ManForEachObj( p, pObj, i ) { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; pRepr = p->pObjCopies[nFrames*i + nFrames-1-k]; // pRepr = p->pObjCopies[nFrames*i + k]; diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index 7e1499b4..cd978717 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -153,7 +153,7 @@ Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p ) pNew->pName = Abc_UtilStrsav( p->pName ); pNew->nConstrs = p->nConstrs; // start mapping of the CI numbers - pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManPiNum(p) ); + pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) ); // map const and primary inputs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); @@ -225,7 +225,7 @@ Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops ) } // create variables for PIs assert( p->vCiNumsOrig == NULL ); - pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManPiNum(p) ); + pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) ); Aig_ManForEachCi( p, pObj, i ) if ( !pObj->fMarkA ) { @@ -299,7 +299,7 @@ int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ) pObjRo->fMarkB = pObjRi->fMarkB; } assert( iBit == p->nBits ); - RetValue = Aig_ManPo(pAig, p->iPo)->fMarkB; + RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB; Aig_ManCleanMarkB(pAig); return RetValue; } @@ -321,7 +321,7 @@ Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p ) Aig_Obj_t * pObj, * pObjRi, * pObjRo; int RetValue, i, k, iBit = 0; // create new counter-example - pNew = Abc_CexAlloc( 0, Aig_ManPiNum(pAig), p->iFrame + 1 ); + pNew = Abc_CexAlloc( 0, Aig_ManCiNum(pAig), p->iFrame + 1 ); pNew->iPo = p->iPo; pNew->iFrame = p->iFrame; // simulate the AIG @@ -336,7 +336,7 @@ Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p ) ///////// write PI+LO values //////////// Aig_ManForEachCi( pAig, pObj, k ) if ( pObj->fMarkB ) - Abc_InfoSetBit(pNew->pData, Aig_ManPiNum(pAig)*i + k); + Abc_InfoSetBit(pNew->pData, Aig_ManCiNum(pAig)*i + k); ///////////////////////////////////////// Aig_ManForEachNode( pAig, pObj, k ) pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & @@ -349,7 +349,7 @@ Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p ) pObjRo->fMarkB = pObjRi->fMarkB; } assert( iBit == p->nBits ); - RetValue = Aig_ManPo(pAig, p->iPo)->fMarkB; + RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB; Aig_ManCleanMarkB(pAig); if ( RetValue == 0 ) printf( "Saig_ManExtendCex(): The counter-example is invalid!!!\n" ); @@ -468,7 +468,7 @@ void Saig_ManDupCones_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vLeaves, Saig_ManDupCones_rec( p, Aig_ObjFanin1(pObj), vLeaves, vNodes, vRoots ); Vec_PtrPush( vNodes, pObj ); } - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots ); else if ( Saig_ObjIsLo(p, pObj) ) Vec_PtrPush( vRoots, Saig_ObjLoToLi(p, pObj) ); @@ -488,7 +488,7 @@ Aig_Man_t * Saig_ManDupCones( Aig_Man_t * pAig, int * pPos, int nPos ) vNodes = Vec_PtrAlloc( 100 ); vRoots = Vec_PtrAlloc( 100 ); for ( i = 0; i < nPos; i++ ) - Vec_PtrPush( vRoots, Aig_ManPo(pAig, pPos[i]) ); + Vec_PtrPush( vRoots, Aig_ManCo(pAig, pPos[i]) ); // mark internal nodes Aig_ManIncrementTravId( pAig ); diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c index f3bfc695..459d8ede 100644 --- a/src/aig/saig/saigGlaCba.c +++ b/src/aig/saig/saigGlaCba.c @@ -730,7 +730,7 @@ Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, i continue; // create output literal to represent property failure - pObj = Aig_ManPo( pAig, 0 ); + pObj = Aig_ManCo( pAig, 0 ); iSatVar = Aig_Gla1FetchVar( p, Aig_ObjFanin0(pObj), f ); Lit = toLitCond( iSatVar, Aig_ObjFaninC0(pObj) ); diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c index cdc91759..6f461995 100644 --- a/src/aig/saig/saigGlaPba.c +++ b/src/aig/saig/saigGlaPba.c @@ -229,7 +229,7 @@ void Aig_Gla2AssignVars_rec( Aig_Gla2Man_t * p, Aig_Obj_t * pObj, int f ) Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0(pObj), f ); return; } - if ( Aig_ObjIsPi( pObj ) ) + if ( Aig_ObjIsCi( pObj ) ) { if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 ) Aig_Gla2AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 ); @@ -260,7 +260,7 @@ int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p ) // assign variables for ( f = p->nFramesMax - 1; f >= 0; f-- ) // for ( f = 0; f < p->nFramesMax; f++ ) - Aig_Gla2AssignVars_rec( p, Aig_ManPo(p->pAig, 0), f ); + Aig_Gla2AssignVars_rec( p, Aig_ManCo(p->pAig, 0), f ); // create SAT solver p->pSat = sat_solver_new(); @@ -334,7 +334,7 @@ int Aig_Gla2CreateSatSolver( Aig_Gla2Man_t * p ) // add output clause vPoLits = Vec_IntAlloc( p->nFramesMax ); for ( f = p->nStart; f < p->nFramesMax; f++ ) - Vec_IntPush( vPoLits, 2 * Aig_Gla2FetchVar(p, Aig_ManPo(p->pAig, 0), f) ); + Vec_IntPush( vPoLits, 2 * Aig_Gla2FetchVar(p, Aig_ManCo(p->pAig, 0), f) ); RetValue &= sat_solver_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ); Vec_IntFree( vPoLits ); Vec_IntPush( p->vCla2Obj, 0 ); diff --git a/src/aig/saig/saigGlaPba2.c b/src/aig/saig/saigGlaPba2.c index 8417cbf5..a7122d01 100644 --- a/src/aig/saig/saigGlaPba2.c +++ b/src/aig/saig/saigGlaPba2.c @@ -198,7 +198,7 @@ void Aig_Gla3AssignVars_rec( Aig_Gla3Man_t * p, Aig_Obj_t * pObj, int f ) Aig_Gla3AssignVars_rec( p, Aig_ObjFanin0(pObj), f ); return; } - if ( Aig_ObjIsPi( pObj ) ) + if ( Aig_ObjIsCi( pObj ) ) { if ( Saig_ObjIsLo(p->pAig, pObj) && f > 0 ) Aig_Gla3AssignVars_rec( p, Aig_ObjFanin0( Saig_ObjLoToLi(p->pAig, pObj) ), f-1 ); @@ -228,7 +228,7 @@ int Aig_Gla3CreateSatSolver( Aig_Gla3Man_t * p ) // assign variables for ( f = p->nFramesMax - 1; f >= 0; f-- ) - Aig_Gla3AssignVars_rec( p, Aig_ManPo(p->pAig, 0), f ); + Aig_Gla3AssignVars_rec( p, Aig_ManCo(p->pAig, 0), f ); // create SAT solver p->pSat = sat_solver2_new(); @@ -301,7 +301,7 @@ int Aig_Gla3CreateSatSolver( Aig_Gla3Man_t * p ) // add output clause vPoLits = Vec_IntAlloc( p->nFramesMax ); for ( f = p->nStart; f < p->nFramesMax; f++ ) - Vec_IntPush( vPoLits, 2 * Aig_Gla3FetchVar(p, Aig_ManPo(p->pAig, 0), f) ); + Vec_IntPush( vPoLits, 2 * Aig_Gla3FetchVar(p, Aig_ManCo(p->pAig, 0), f) ); sat_solver2_addclause( p->pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ); Vec_IntFree( vPoLits ); Vec_IntPush( p->vCla2Obj, 0 ); diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c index ef90734a..d3539abb 100644 --- a/src/aig/saig/saigHaig.c +++ b/src/aig/saig/saigHaig.c @@ -122,7 +122,7 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames ) Aig_ManHaigSpeculate( pFrames, pObj ); } if ( f == nFrames - 2 ) - nAssumptions = Aig_ManPoNum(pFrames); + nAssumptions = Aig_ManCoNum(pFrames); if ( f == nFrames - 1 ) break; // save register inputs @@ -133,7 +133,7 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames ) pObjLo->pData = pObjLi->pData; } Aig_ManCleanup( pFrames ); - pFrames->nAsserts = Aig_ManPoNum(pFrames) - nAssumptions; + pFrames->nAsserts = Aig_ManCoNum(pFrames) - nAssumptions; Aig_ManSetRegNum( pFrames, 0 ); return pFrames; } @@ -161,13 +161,13 @@ int Aig_ManMapHaigNodes( Aig_Man_t * pHaig ) pObj1 = Aig_ManObj( pHaig, Id1 ); pObj2 = Aig_ManObj( pHaig, Id2 ); assert( pObj1 != pObj2 ); - assert( !Aig_ObjIsPi(pObj1) || !Aig_ObjIsPi(pObj2) ); - if ( Aig_ObjIsPi(pObj1) ) + assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) ); + if ( Aig_ObjIsCi(pObj1) ) { Counter += (int)(pObj2->pHaig != NULL); pObj2->pHaig = pObj1; } - else if ( Aig_ObjIsPi(pObj2) ) + else if ( Aig_ObjIsCi(pObj2) ) { Counter += (int)(pObj1->pHaig != NULL); pObj1->pHaig = pObj2; @@ -225,13 +225,13 @@ clk = clock(); Aig_ManPrintStats( pFrames ); printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n", - Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers ); -// pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) ); - pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) ); + Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers ); +// pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) ); + pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) ); -// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts ); +// pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) - pFrames->nAsserts ); //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); // Saig_ManDumpBlif( pHaig, "haig_temp.blif" ); // Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" ); @@ -248,10 +248,10 @@ clk = clock(); // add clauses for the first frame Aig_ManForEachCo( pFrames, pObj1, i ) { - if ( i >= Aig_ManPoNum(pFrames) - pFrames->nAsserts ) + if ( i >= Aig_ManCoNum(pFrames) - pFrames->nAsserts ) break; - pObj2 = Aig_ManPo( pFrames, ++i ); + pObj2 = Aig_ManCo( pFrames, ++i ); assert( pObj1->fPhase == pObj2->fPhase ); Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 ); @@ -285,10 +285,10 @@ clk = clock(); printf( "Started solving ...\r" ); Aig_ManForEachCo( pFrames, pObj1, i ) { - if ( i < Aig_ManPoNum(pFrames) - pFrames->nAsserts ) + if ( i < Aig_ManCoNum(pFrames) - pFrames->nAsserts ) continue; - pObj2 = Aig_ManPo( pFrames, ++i ); + pObj2 = Aig_ManCo( pFrames, ++i ); assert( pObj1->fPhase == pObj2->fPhase ); Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 ); @@ -320,7 +320,7 @@ clk = clock(); if ( i % 50 == 1 ) printf( "Solving assertion %6d out of %6d.\r", - (i - (Aig_ManPoNum(pFrames) - pFrames->nAsserts))/2, + (i - (Aig_ManCoNum(pFrames) - pFrames->nAsserts))/2, pFrames->nAsserts/2 ); // if ( nClasses == 1000 ) // break; @@ -376,7 +376,7 @@ clkVerif = clock() - clk; fprintf( pTable, "%d ", pCnf->nClauses ); fprintf( pTable, "%d ", pCnf->nLiterals ); - fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 ); + fprintf( pTable, "%d ", Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2 ); fprintf( pTable, "%d ", pFrames->nAsserts/2 ); fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 ); @@ -419,7 +419,7 @@ int Aig_ManHaigVerify2( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int assert( nFrames == 1 || nFrames == 2 ); clk = clock(); - pCnf = Cnf_DeriveSimple( pHaig, Aig_ManPoNum(pHaig) ); + pCnf = Cnf_DeriveSimple( pHaig, Aig_ManCoNum(pHaig) ); // Aig_ManForEachObj( pHaig, pObj, i ) // printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] ); // printf( "\n" ); @@ -572,8 +572,8 @@ Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig ) Vec_PtrPush( vTemp, pObj ); } } - Vec_PtrShrink( pHaig->vPos, 0 ); - pHaig->nObjs[AIG_OBJ_PO] = Vec_PtrSize( vTemp ); + Vec_PtrShrink( pHaig->vCos, 0 ); + pHaig->nObjs[AIG_OBJ_CO] = Vec_PtrSize( vTemp ); // add new POs Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i ) { @@ -581,7 +581,7 @@ Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig ) pObj1 = Aig_ManObj( pHaig, Id1 ); pObj2 = Aig_ManObj( pHaig, Id2 ); assert( pObj1 != pObj2 ); - assert( !Aig_ObjIsPi(pObj1) || !Aig_ObjIsPi(pObj2) ); + assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) ); pMiter = Aig_Exor( pHaig, pObj1, pObj2 ); pMiter = Aig_NotCond( pMiter, Aig_ObjPhaseReal(pMiter) ); assert( Aig_ObjPhaseReal(pMiter) == 0 ); @@ -590,9 +590,9 @@ Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig ) printf( "Added %d property outputs.\n", Vec_IntSize(pHaig->vEquPairs)/2 ); // add the registers Vec_PtrForEachEntry( Aig_Obj_t *, vTemp, pObj, i ) - Vec_PtrPush( pHaig->vPos, pObj ); + Vec_PtrPush( pHaig->vCos, pObj ); Vec_PtrFree( vTemp ); - assert( pHaig->nObjs[AIG_OBJ_PO] == Vec_PtrSize(pHaig->vPos) ); + assert( pHaig->nObjs[AIG_OBJ_CO] == Vec_PtrSize(pHaig->vCos) ); Aig_ManCleanup( pHaig ); Aig_ManSetRegNum( pHaig, pHaig->nRegs ); // return pHaig; diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c index 0dd1e7d2..18aebc74 100644 --- a/src/aig/saig/saigInd.c +++ b/src/aig/saig/saigInd.c @@ -160,7 +160,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, vBot = Vec_PtrAlloc( 100 ); vTop = Vec_PtrAlloc( 100 ); vState = Vec_IntAlloc( 1000 ); - Vec_PtrPush( vTop, Aig_ManPo(p, 0) ); + Vec_PtrPush( vTop, Aig_ManCo(p, 0) ); // start the array of CNF variables vTopVarNums = Vec_IntAlloc( 100 ); // start the solver @@ -185,7 +185,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, // derive AIG for the part between top and bottom pAigPart = Aig_ManDupSimpleDfsPart( p, vBot, vTop ); // convert it into CNF - pCnfPart = Cnf_Derive( pAigPart, Aig_ManPoNum(pAigPart) ); + pCnfPart = Cnf_Derive( pAigPart, Aig_ManCoNum(pAigPart) ); Cnf_DataLift( pCnfPart, nSatVarNum ); nSatVarNum += pCnfPart->nVars; nClauses += pCnfPart->nClauses; @@ -193,13 +193,13 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, // remember top frame var IDs if ( fGetCex && vTopVarIds == NULL ) { - vTopVarIds = Vec_IntStartFull( Aig_ManPiNum(p) ); + vTopVarIds = Vec_IntStartFull( Aig_ManCiNum(p) ); Aig_ManForEachCi( p, pObjPi, i ) { if ( pObjPi->pData == NULL ) continue; pObjPiCopy = (Aig_Obj_t *)pObjPi->pData; - assert( Aig_ObjIsPi(pObjPiCopy) ); + assert( Aig_ObjIsCi(pObjPiCopy) ); if ( Saig_ObjIsPi(p, pObjPi) ) Vec_IntWriteEntry( vTopVarIds, Aig_ObjPioNum(pObjPi) + Saig_ManRegNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] ); else if ( Saig_ObjIsLo(p, pObjPi) ) @@ -209,7 +209,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, } // stitch variables of top and bot - assert( Aig_ManPoNum(pAigPart)-1 == Vec_IntSize(vTopVarNums) ); + assert( Aig_ManCoNum(pAigPart)-1 == Vec_IntSize(vTopVarNums) ); Aig_ManForEachCo( pAigPart, pObjPo, i ) { if ( i == 0 ) @@ -247,13 +247,13 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, // create new set of POs to derive new top Vec_PtrClear( vTop ); - Vec_PtrPush( vTop, Aig_ManPo(p, 0) ); + Vec_PtrPush( vTop, Aig_ManCo(p, 0) ); Vec_IntClear( vTopVarNums ); nOldSize = Vec_IntSize(vState); Vec_IntFillExtra( vState, nOldSize + Aig_ManRegNum(p), -1 ); Vec_PtrForEachEntry( Aig_Obj_t *, vBot, pObjPi, i ) { - assert( Aig_ObjIsPi(pObjPi) ); + assert( Aig_ObjIsCi(pObjPi) ); if ( Saig_ObjIsLo(p, pObjPi) ) { pObjPiCopy = (Aig_Obj_t *)pObjPi->pData; @@ -286,7 +286,7 @@ nextrun: if ( fVerbose ) { printf( "%4d : PI =%5d. PO =%5d. AIG =%5d. Var =%7d. Clau =%7d. Conf =%7d. ", - f, Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), Aig_ManNodeNum(pAigPart), + f, Aig_ManCiNum(pAigPart), Aig_ManCoNum(pAigPart), Aig_ManNodeNum(pAigPart), nSatVarNum, nClauses, (int)pSat->stats.conflicts-nConfPrev ); ABC_PRT( "Time", clock() - clk ); } diff --git a/src/aig/saig/saigIoa.c b/src/aig/saig/saigIoa.c index 82d6c9af..9eba652d 100644 --- a/src/aig/saig/saigIoa.c +++ b/src/aig/saig/saigIoa.c @@ -77,7 +77,7 @@ void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) FILE * pFile; Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i; - if ( Aig_ManPoNum(p) == 0 ) + if ( Aig_ManCoNum(p) == 0 ) { printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" ); return; @@ -208,7 +208,7 @@ Aig_Obj_t * Saig_ManReadNode( Aig_Man_t * p, int * pNum2Id, char * pToken ) if ( pToken[0] == 'i' ) { Num = atoi( pToken + 1 ); - return Aig_ManPi( p, Num ); + return Aig_ManCi( p, Num ); } if ( pToken[0] == 'o' ) return NULL; @@ -382,7 +382,7 @@ Aig_Man_t * Saig_ManReadBlif( char * pFileName ) } if ( pToken == NULL || strcmp( pToken, ".end" ) ) { printf( "Saig_ManReadBlif(): Error 19.\n" ); Aig_ManStop(p); return NULL; } - if ( nPos + nRegs != Aig_ManPoNum(p) ) + if ( nPos + nRegs != Aig_ManCoNum(p) ) { printf( "Saig_ManReadBlif(): Error 20.\n" ); Aig_ManStop(p); return NULL; } // add non-node objects to the mapping Aig_ManForEachCi( p, pNode, i ) diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c index dac8e273..d68819f3 100644 --- a/src/aig/saig/saigIso.c +++ b/src/aig/saig/saigIso.c @@ -49,8 +49,8 @@ Vec_Int_t * Saig_ManFindIsoPermCos( Aig_Man_t * pAig, Vec_Int_t * vPermCis ) Vec_Int_t * vPermCos; Aig_Obj_t * pObj, * pFanin; int i, Entry, Diff; - assert( Vec_IntSize(vPermCis) == Aig_ManPiNum(pAig) ); - vPermCos = Vec_IntAlloc( Aig_ManPoNum(pAig) ); + assert( Vec_IntSize(vPermCis) == Aig_ManCiNum(pAig) ); + vPermCos = Vec_IntAlloc( Aig_ManCoNum(pAig) ); if ( Saig_ManPoNum(pAig) == 1 ) Vec_IntPush( vPermCos, 0 ); else @@ -145,20 +145,20 @@ Aig_Man_t * Saig_ManDupIsoCanonical( Aig_Man_t * pAig, int fVerbose ) // create PIs Vec_IntForEachEntry( vPerm, Entry, i ) { - pObj = Aig_ManPi(pAig, Entry); + pObj = Aig_ManCi(pAig, Entry); pObj->pData = Aig_ObjCreateCi(pNew); Aig_ObjSetTravIdCurrent( pAig, pObj ); } // traverse from the POs Vec_IntForEachEntry( vPermCo, Entry, i ) { - pObj = Aig_ManPo(pAig, Entry); + pObj = Aig_ManCo(pAig, Entry); Saig_ManDupIsoCanonical_rec( pNew, pAig, Aig_ObjFanin0(pObj) ); } // create POs Vec_IntForEachEntry( vPermCo, Entry, i ) { - pObj = Aig_ManPo(pAig, Entry); + pObj = Aig_ManCo(pAig, Entry); Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); } Aig_ManSetRegNum( pNew, Aig_ManRegNum(pAig) ); @@ -187,15 +187,15 @@ int Iso_ManCheckMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vMap2 { Aig_Obj_t * pObj, * pFanin0, * pFanin1; int i; - assert( Aig_ManPiNum(pAig1) == Aig_ManPiNum(pAig2) ); - assert( Aig_ManPoNum(pAig1) == Aig_ManPoNum(pAig2) ); + assert( Aig_ManCiNum(pAig1) == Aig_ManCiNum(pAig2) ); + assert( Aig_ManCoNum(pAig1) == Aig_ManCoNum(pAig2) ); assert( Aig_ManRegNum(pAig1) == Aig_ManRegNum(pAig2) ); assert( Aig_ManNodeNum(pAig1) == Aig_ManNodeNum(pAig2) ); Aig_ManCleanData( pAig1 ); // map const and PI nodes Aig_ManConst1(pAig2)->pData = Aig_ManConst1(pAig1); Aig_ManForEachCi( pAig2, pObj, i ) - pObj->pData = Aig_ManPi( pAig1, Vec_IntEntry(vMap2to1, i) ); + pObj->pData = Aig_ManCi( pAig1, Vec_IntEntry(vMap2to1, i) ); // try internal nodes Aig_ManForEachNode( pAig2, pObj, i ) { @@ -210,7 +210,7 @@ int Iso_ManCheckMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vMap2 } } // make sure the first PO points to the same node - if ( Aig_ManPoNum(pAig1)-Aig_ManRegNum(pAig1) == 1 && Aig_ObjChild0Copy(Aig_ManPo(pAig2, 0)) != Aig_ObjChild0(Aig_ManPo(pAig1, 0)) ) + if ( Aig_ManCoNum(pAig1)-Aig_ManRegNum(pAig1) == 1 && Aig_ObjChild0Copy(Aig_ManCo(pAig2, 0)) != Aig_ObjChild0(Aig_ManCo(pAig1, 0)) ) { if ( fVerbose ) printf( "Structural equivalence failed at primary output 0.\n" ); @@ -244,7 +244,7 @@ int Iso_ManNegEdgeNum( Aig_Man_t * pAig ) Counter += Aig_ObjFaninC0(pObj); Counter += Aig_ObjFaninC1(pObj); } - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) Counter += Aig_ObjFaninC0(pObj); return (pAig->nComplEdges = Counter); } @@ -265,9 +265,9 @@ Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t { Vec_Int_t * vPerm1, * vPerm2, * vInvPerm2; int i, Entry; - if ( Aig_ManPiNum(pAig1) != Aig_ManPiNum(pAig2) ) + if ( Aig_ManCiNum(pAig1) != Aig_ManCiNum(pAig2) ) return NULL; - if ( Aig_ManPoNum(pAig1) != Aig_ManPoNum(pAig2) ) + if ( Aig_ManCoNum(pAig1) != Aig_ManCoNum(pAig2) ) return NULL; if ( Aig_ManRegNum(pAig1) != Aig_ManRegNum(pAig2) ) return NULL; @@ -286,15 +286,15 @@ Vec_Int_t * Iso_ManFindMapping( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t printf( "AIG1:\n" ); vPerm2 = vPerm2_ ? vPerm2_ : Saig_ManFindIsoPerm( pAig2, fVerbose ); if ( vPerm1_ ) - assert( Vec_IntSize(vPerm1_) == Aig_ManPiNum(pAig1) ); + assert( Vec_IntSize(vPerm1_) == Aig_ManCiNum(pAig1) ); if ( vPerm2_ ) - assert( Vec_IntSize(vPerm2_) == Aig_ManPiNum(pAig2) ); + assert( Vec_IntSize(vPerm2_) == Aig_ManCiNum(pAig2) ); // find canonical permutation // vPerm1/vPerm2 give canonical order of CIs of AIG1/AIG2 vInvPerm2 = Vec_IntInvert( vPerm2, -1 ); Vec_IntForEachEntry( vInvPerm2, Entry, i ) { - assert( Entry >= 0 && Entry < Aig_ManPiNum(pAig1) ); + assert( Entry >= 0 && Entry < Aig_ManCiNum(pAig1) ); Vec_IntWriteEntry( vInvPerm2, i, Vec_IntEntry(vPerm1, Entry) ); } if ( vPerm1_ == NULL ) @@ -328,7 +328,7 @@ Aig_Man_t * Iso_ManFilterPos_old( Aig_Man_t * pAig, int fVerbose ) int i, k, nPos; // derive AIG for each PO - nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig); + nPos = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig); vParts = Vec_PtrAlloc( nPos ); vPerms = Vec_PtrAlloc( nPos ); for ( i = 0; i < nPos; i++ ) @@ -431,7 +431,7 @@ Aig_Man_t * Iso_ManFilterPos( Aig_Man_t * pAig, Vec_Ptr_t ** pvPosEquivs, int fV *pvPosEquivs = NULL; // derive AIG for each PO - nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig); + nPos = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig); vBuffers = Vec_PtrAlloc( nPos ); for ( i = 0; i < nPos; i++ ) { diff --git a/src/aig/saig/saigIsoFast.c b/src/aig/saig/saigIsoFast.c index befbf934..a7cc942c 100644 --- a/src/aig/saig/saigIsoFast.c +++ b/src/aig/saig/saigIsoFast.c @@ -111,7 +111,7 @@ void Iso_StoStop( Iso_Sto_t * p ) void Iso_StoCollectInfo_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fCompl, Vec_Int_t * vVisited, Iso_Dat_t * pData, Vec_Ptr_t * vRoots ) { Iso_Dat_t * pThis = pData + Aig_ObjId(pObj); - assert( Aig_ObjIsPi(pObj) || Aig_ObjIsNode(pObj) ); + assert( Aig_ObjIsCi(pObj) || Aig_ObjIsNode(pObj) ); if ( pThis->fVisit ) { if ( fCompl ) @@ -183,7 +183,7 @@ Vec_Int_t * Iso_StoCollectInfo( Iso_Sto_t * p, Aig_Obj_t * pPo ) int i, Value, Entry, * pPerm; // int clk = clock(); - assert( Aig_ObjIsPo(pPo) ); + assert( Aig_ObjIsCo(pPo) ); // collect initial POs Vec_IntClear( p->vVisited ); diff --git a/src/aig/saig/saigIsoSlow.c b/src/aig/saig/saigIsoSlow.c index eabf7c1b..e4c1dc47 100644 --- a/src/aig/saig/saigIsoSlow.c +++ b/src/aig/saig/saigIsoSlow.c @@ -393,7 +393,7 @@ void Iso_FindNumbers() ***********************************************************************/ void Iso_ManObjCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int * pnNodes, int * pnEdges ) { - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) return; if ( Aig_ObjIsTravIdCurrent(p, pObj) ) return; @@ -490,8 +490,8 @@ int Iso_ObjCompareByData( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) { Aig_Obj_t * pIso1 = *pp1; Aig_Obj_t * pIso2 = *pp2; - assert( Aig_ObjIsPi(pIso1) || Aig_ObjIsPo(pIso1) ); - assert( Aig_ObjIsPi(pIso2) || Aig_ObjIsPo(pIso2) ); + assert( Aig_ObjIsCi(pIso1) || Aig_ObjIsCo(pIso1) ); + assert( Aig_ObjIsCi(pIso2) || Aig_ObjIsCo(pIso2) ); return pIso1->iData - pIso2->iData; } @@ -605,7 +605,7 @@ Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig ) // create TFI signatures Aig_ManForEachObj( pAig, pObj, i ) { - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) continue; pIso = p->pObjs + i; pIso->Level = pObj->Level; @@ -644,7 +644,7 @@ Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig ) // create TFO signatures Aig_ManForEachObjReverse( pAig, pObj, i ) { - if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) ) + if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) ) continue; pIso = p->pObjs + i; if ( fUseXor ) @@ -659,7 +659,7 @@ Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig ) pIsoF->FanoutSig ^= pIso->FanoutSig; pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC1(pObj)) & ISO_MASK]; } - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) { pIsoF = p->pObjs + Aig_ObjFaninId0(pObj); pIsoF->FanoutSig ^= pIso->FanoutSig; @@ -678,7 +678,7 @@ Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig ) pIsoF->FanoutSig += pIso->FanoutSig; pIsoF->FanoutSig += pIso->Level * s_1kPrimes[Abc_Var2Lit(pIso->Level, Aig_ObjFaninC1(pObj)) & ISO_MASK]; } - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) { pIsoF = p->pObjs + Aig_ObjFaninId0(pObj); pIsoF->FanoutSig += pIso->FanoutSig; @@ -713,7 +713,7 @@ Iso_Man_t * Iso_ManCreate( Aig_Man_t * pAig ) // add to the hash table Aig_ManForEachObj( pAig, pObj, i ) { - if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) ) + if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) ) continue; pIso = p->pObjs + i; Iso_ObjHashAdd( p, pIso ); @@ -748,7 +748,7 @@ void Iso_ManAssignAdjacency( Iso_Man_t * p ) pIso->FaninSig = 0; pIso->FanoutSig = 0; - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) continue; if ( fUseXor ) { @@ -784,10 +784,10 @@ void Iso_ManAssignAdjacency( Iso_Man_t * p ) // create TFO signatures Aig_ManForEachObjReverse( p->pAig, pObj, i ) { - if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) ) + if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) ) continue; pIso = p->pObjs + i; - assert( !Aig_ObjIsPo(pObj) || pIso->Id == 0 ); + assert( !Aig_ObjIsCo(pObj) || pIso->Id == 0 ); if ( fUseXor ) { if ( Aig_ObjIsNode(pObj) ) @@ -802,7 +802,7 @@ void Iso_ManAssignAdjacency( Iso_Man_t * p ) if ( pIso->Id ) pIsoF->FanoutSig ^= s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC1(pObj)) & ISO_MASK]; } - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) { pIsoF = p->pObjs + Aig_ObjFaninId0(pObj); pIsoF->FanoutSig ^= pIso->FanoutSig; @@ -824,7 +824,7 @@ void Iso_ManAssignAdjacency( Iso_Man_t * p ) if ( pIso->Id ) pIsoF->FanoutSig += pIso->Id * s_1kPrimes[Abc_Var2Lit(pIso->Id, Aig_ObjFaninC1(pObj)) & ISO_MASK]; } - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) { pIsoF = p->pObjs + Aig_ObjFaninId0(pObj); pIsoF->FanoutSig += pIso->FanoutSig; @@ -1093,7 +1093,7 @@ Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p ) // set canonical numbers Aig_ManForEachObj( p->pAig, pObj, i ) { - if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) ) + if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) ) { pObj->iData = -1; continue; @@ -1108,7 +1108,7 @@ Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p ) Aig_ManForEachCi( p->pAig, pObj, i ) { assert( pObj->iData > 0 ); - if ( Aig_ObjPioNum(pObj) >= Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig) ) // flop + if ( Aig_ObjPioNum(pObj) >= Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig) ) // flop Vec_PtrPush( p->vTemp2, pObj ); else // PI Vec_PtrPush( p->vTemp1, pObj ); @@ -1117,7 +1117,7 @@ Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p ) Vec_PtrSort( p->vTemp1, (int (*)(void))Iso_ObjCompareByData ); Vec_PtrSort( p->vTemp2, (int (*)(void))Iso_ObjCompareByData ); // create the result - vRes = Vec_IntAlloc( Aig_ManPiNum(p->pAig) ); + vRes = Vec_IntAlloc( Aig_ManCiNum(p->pAig) ); Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp1, pObj, i ) Vec_IntPush( vRes, Aig_ObjPioNum(pObj) ); Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp2, pObj, i ) @@ -1205,8 +1205,8 @@ Vec_Int_t * Saig_ManFindIsoPerm( Aig_Man_t * pAig, int fVerbose ) } } p->timeTotal = clock() - clk2; -// printf( "IDs assigned = %d. Objects = %d.\n", p->nObjIds, 1+Aig_ManPiNum(p->pAig)+Aig_ManNodeNum(p->pAig) ); - assert( p->nObjIds == 1+Aig_ManPiNum(p->pAig)+Aig_ManNodeNum(p->pAig) ); +// printf( "IDs assigned = %d. Objects = %d.\n", p->nObjIds, 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) ); + assert( p->nObjIds == 1+Aig_ManCiNum(p->pAig)+Aig_ManNodeNum(p->pAig) ); // if ( p->nClasses ) // Iso_ManDumpOneClass( p ); vRes = Iso_ManFinalize( p ); diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 9f8328b1..4c0e9bdf 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -116,7 +116,7 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) Saig_ManForEachPi( p0, pObj, i ) pObj->pData = Aig_ObjCreateCi( pNew ); Saig_ManForEachPi( p1, pObj, i ) - pObj->pData = Aig_ManPi( pNew, i ); + pObj->pData = Aig_ManCi( pNew, i ); // map register outputs Saig_ManForEachLo( p0, pObj, i ) pObj->pData = Aig_ObjCreateCi( pNew ); @@ -131,9 +131,9 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) Saig_ManForEachPo( p0, pObj, i ) { if ( Oper == 0 ) // XOR - pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManPo(p1,i)) ); + pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) ); else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1) ... complement is PO(p0) & !PO(p1) - pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManPo(p1,i))) ); + pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) ); else assert( 0 ); Aig_ObjCreateCo( pNew, pObj ); @@ -165,8 +165,8 @@ Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) Aig_Man_t * pNew; Aig_Obj_t * pObj; int i; - assert( Aig_ManPiNum(p0) == Aig_ManPiNum(p1) ); - assert( Aig_ManPoNum(p0) == Aig_ManPoNum(p1) ); + assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) ); + assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) ); pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) ); pNew->pName = Abc_UtilStrsav( "miter" ); // map constant nodes @@ -176,7 +176,7 @@ Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) Aig_ManForEachCi( p0, pObj, i ) pObj->pData = Aig_ObjCreateCi( pNew ); Aig_ManForEachCi( p1, pObj, i ) - pObj->pData = Aig_ManPi( pNew, i ); + pObj->pData = Aig_ManCi( pNew, i ); // map internal nodes Aig_ManForEachNode( p0, pObj, i ) pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); @@ -186,9 +186,9 @@ Aig_Man_t * Saig_ManCreateMiterComb( Aig_Man_t * p0, Aig_Man_t * p1, int Oper ) Aig_ManForEachCo( p0, pObj, i ) { if ( Oper == 0 ) // XOR - pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManPo(p1,i)) ); + pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManCo(p1,i)) ); else if ( Oper == 1 ) // implication is PO(p0) -> PO(p1) ... complement is PO(p0) & !PO(p1) - pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManPo(p1,i))) ); + pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManCo(p1,i))) ); else assert( 0 ); Aig_ObjCreateCo( pNew, pObj ); @@ -721,11 +721,11 @@ int Saig_ManDemiterDual( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 if ( i & 1 ) Aig_ObjDeletePo( pTemp, pObj ); else - Vec_PtrWriteEntry( pTemp->vPos, k++, pObj ); + Vec_PtrWriteEntry( pTemp->vCos, k++, pObj ); } Saig_ManForEachLi( pTemp, pObj, i ) - Vec_PtrWriteEntry( pTemp->vPos, k++, pObj ); - Vec_PtrShrink( pTemp->vPos, k ); + Vec_PtrWriteEntry( pTemp->vCos, k++, pObj ); + Vec_PtrShrink( pTemp->vCos, k ); pTemp->nTruePos = k - Saig_ManRegNum(pTemp); Aig_ManSeqCleanup( pTemp ); *ppAig0 = Aig_ManDupSimple( pTemp ); @@ -736,13 +736,13 @@ int Saig_ManDemiterDual( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 Saig_ManForEachPo( pTemp, pObj, i ) { if ( i & 1 ) - Vec_PtrWriteEntry( pTemp->vPos, k++, pObj ); + Vec_PtrWriteEntry( pTemp->vCos, k++, pObj ); else Aig_ObjDeletePo( pTemp, pObj ); } Saig_ManForEachLi( pTemp, pObj, i ) - Vec_PtrWriteEntry( pTemp->vPos, k++, pObj ); - Vec_PtrShrink( pTemp->vPos, k ); + Vec_PtrWriteEntry( pTemp->vCos, k++, pObj ); + Vec_PtrShrink( pTemp->vCos, k ); pTemp->nTruePos = k - Saig_ManRegNum(pTemp); Aig_ManSeqCleanup( pTemp ); *ppAig1 = Aig_ManDupSimple( pTemp ); diff --git a/src/aig/saig/saigOutDec.c b/src/aig/saig/saigOutDec.c index 4e7e955f..d059a935 100644 --- a/src/aig/saig/saigOutDec.c +++ b/src/aig/saig/saigOutDec.c @@ -57,11 +57,11 @@ Vec_Ptr_t * Saig_ManFindPrimes( Aig_Man_t * pAig, int nLits, int fVerbose ) assert( nLits < 10 ); // create SAT solver - pCnf = Cnf_DeriveSimple( pAig, Aig_ManPoNum(pAig) ); + pCnf = Cnf_DeriveSimple( pAig, Aig_ManCoNum(pAig) ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); // collect nodes in the property output cone - pMiter = Aig_ManPo( pAig, 0 ); + pMiter = Aig_ManCo( pAig, 0 ); pRoot = Aig_ObjFanin0( pMiter ); vNodes = Aig_ManDfsNodes( pAig, &pRoot, 1 ); // sort nodes by level and remove the last few diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c index f0bf3281..e7a586fe 100644 --- a/src/aig/saig/saigPhase.c +++ b/src/aig/saig/saigPhase.c @@ -810,8 +810,8 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe } } pFrames->nRegs = pAig->nRegs; - pFrames->nTruePis = Aig_ManPiNum(pFrames) - Aig_ManRegNum(pFrames); - pFrames->nTruePos = Aig_ManPoNum(pFrames) - Aig_ManRegNum(pFrames); + pFrames->nTruePis = Aig_ManCiNum(pFrames) - Aig_ManRegNum(pFrames); + pFrames->nTruePos = Aig_ManCoNum(pFrames) - Aig_ManRegNum(pFrames); Aig_ManForEachLiSeq( pAig, pObj, i ) { pObjNew = Aig_ObjCreateCo( pFrames, Saig_ObjChild0Frames(pObjMap,nFrames,pObj,nFrames-1) ); @@ -820,7 +820,7 @@ Aig_Man_t * Saig_ManPerformAbstraction( Saig_Tsim_t * pTsi, int nFrames, int fVe //Aig_ManPrintStats( pFrames ); Aig_ManSeqCleanup( pFrames ); //Aig_ManPrintStats( pFrames ); -// Aig_ManPiCleanup( pFrames ); +// Aig_ManCiCleanup( pFrames ); //Aig_ManPrintStats( pFrames ); ABC_FREE( pObjMap ); return pFrames; @@ -1021,7 +1021,7 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ) Saig_TsiStop( pTsi ); if ( pNew == NULL ) pNew = Aig_ManDupSimple( p ); - if ( Aig_ManPiNum(pNew) == Aig_ManRegNum(pNew) ) + if ( Aig_ManCiNum(pNew) == Aig_ManRegNum(pNew) ) { Aig_ManStop( pNew); pNew = Aig_ManDupSimple( p ); diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c index 09a0c69b..f195f36c 100644 --- a/src/aig/saig/saigRefSat.c +++ b/src/aig/saig/saigRefSat.c @@ -70,7 +70,7 @@ Vec_Int_t * Saig_RefManReason2Inputs( Saig_RefMan_t * p, Vec_Int_t * vReasons ) Vec_IntForEachEntry( vReasons, Entry, i ) { int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); - assert( iInput >= 0 && iInput < Aig_ManPiNum(p->pAig) ); + assert( iInput >= 0 && iInput < Aig_ManCiNum(p->pAig) ); if ( Vec_IntEntry(vVisited, iInput) == 0 ) Vec_IntPush( vOriginal, iInput ); Vec_IntAddToEntry( vVisited, iInput, 1 ); @@ -98,7 +98,7 @@ Abc_Cex_t * Saig_RefManReason2Cex( Saig_RefMan_t * p, Vec_Int_t * vReasons ) memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) ); Vec_IntForEachEntry( vReasons, Entry, i ) { - assert( Entry >= 0 && Entry < Aig_ManPiNum(p->pFrames) ); + assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pFrames) ); iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry ); iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 ); Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); @@ -122,7 +122,7 @@ void Saig_RefManFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr if ( Aig_ObjIsTravIdCurrent(p, pObj) ) return; Aig_ObjSetTravIdCurrent(p, pObj); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) ); return; @@ -209,7 +209,7 @@ Vec_Int_t * Saig_RefManFindReason( Saig_RefMan_t * p ) Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) ); } // check the property output - pObj = Aig_ManPo( p->pFrames, 0 ); + pObj = Aig_ManCo( p->pFrames, 0 ); assert( (int)Aig_ObjFanin0(pObj)->fPhase == Aig_ObjFaninC0(pObj) ); // select the reason @@ -238,7 +238,7 @@ void Saig_ManUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) return; Aig_ObjSetTravIdCurrent(pAig, pObj); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) Saig_ManUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots ); else if ( Aig_ObjIsNode(pObj) ) { @@ -281,7 +281,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu vFrameCos = Vec_VecStart( pCex->iFrame+1 ); vFrameObjs = Vec_VecStart( pCex->iFrame+1 ); // initialized the topmost frame - pObj = Aig_ManPo( pAig, pCex->iPo ); + pObj = Aig_ManCo( pAig, pCex->iPo ); Vec_VecPushInt( vFrameCos, pCex->iFrame, Aig_ObjId(pObj) ); for ( f = pCex->iFrame; f >= 0; f-- ) { @@ -310,7 +310,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu { if ( Aig_ObjIsNode(pObj) ) pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) pObj->pData = Aig_ObjChild0Copy(pObj); else if ( Aig_ObjIsConst1(pObj) ) pObj->pData = Aig_ManConst1(pFrames); @@ -337,7 +337,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData; } // create output - pObj = Aig_ManPo( pAig, pCex->iPo ); + pObj = Aig_ManCo( pAig, pCex->iPo ); Aig_ObjCreateCo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) ); Aig_ManSetRegNum( pFrames, 0 ); // cleanup @@ -420,7 +420,7 @@ int Saig_RefManSetPhases( Saig_RefMan_t * p, Abc_Cex_t * pCare, int fValue1 ) & ( Aig_ObjFanin1(pObj)->fPhase ^ Aig_ObjFaninC1(pObj) ); Aig_ManForEachCo( p->pFrames, pObj, i ) pObj->fPhase = ( Aig_ObjFanin0(pObj)->fPhase ^ Aig_ObjFaninC0(pObj) ); - pObj = Aig_ManPo( p->pFrames, 0 ); + pObj = Aig_ManCo( p->pFrames, 0 ); return pObj->fPhase; } @@ -446,7 +446,7 @@ Vec_Vec_t * Saig_RefManOrderLiterals( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, Vec_IntForEachEntry( vAssumps, Entry, i ) { int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) ); - assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) ); + assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) ); iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum ); iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 ); // Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); @@ -480,7 +480,7 @@ Abc_Cex_t * Saig_RefManCreateCex( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, Vec_ Vec_IntForEachEntry( vAssumps, Entry, i ) { int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) ); - assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) ); + assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) ); iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum ); iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 ); Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput ); @@ -548,7 +548,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder ) } // create assumptions vVar2PiId = Vec_IntStartFull( pCnf->nVars ); - vAssumps = Vec_IntAlloc( Aig_ManPiNum(p->pFrames) ); + vAssumps = Vec_IntAlloc( Aig_ManCiNum(p->pFrames) ); Aig_ManForEachCi( p->pFrames, pObj, i ) { // RetValue = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ); @@ -726,13 +726,13 @@ Vec_Int_t * Saig_RefManRefineWithSat( Saig_RefMan_t * p, Vec_Int_t * vAigPis ) vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) ); Vec_IntForEachEntry( vAigPis, Entry, i ) { - assert( Entry >= 0 && Entry < Aig_ManPiNum(p->pAig) ); + assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pAig) ); Vec_IntWriteEntry( vVisited, Entry, 1 ); } // create assumptions vVar2PiId = Vec_IntStartFull( pCnf->nVars ); - vAssumps = Vec_IntAlloc( Aig_ManPiNum(p->pFrames) ); + vAssumps = Vec_IntAlloc( Aig_ManCiNum(p->pFrames) ); Aig_ManForEachCi( p->pFrames, pObj, i ) { int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i ); @@ -836,7 +836,7 @@ Vec_Int_t * Saig_RefManRefineWithSat( Saig_RefMan_t * p, Vec_Int_t * vAigPis ) Vec_IntForEachEntry( vAssumps, Entry, i ) { int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) ); - assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) ); + assert( iPiNum >= 0 && iPiNum < Aig_ManCiNum(p->pFrames) ); Vec_IntPush( vReasons, iPiNum ); } @@ -881,7 +881,7 @@ Aig_ManPrintStats( p->pFrames ); { Vec_Int_t * vRes = Saig_RefManReason2Inputs( p, vReasons ); printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", - Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), + Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); ABC_PRT( "Time", clock() - clk ); @@ -896,7 +896,7 @@ ABC_PRT( "Time", clock() - clk ); Vec_IntFree( vRes ); vRes = Saig_RefManReason2Inputs( p, vReasons ); printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", - Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), + Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); Vec_IntFree( vRes ); @@ -935,7 +935,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopP if ( Saig_ManPiNum(pAig) != pCex->nPis ) { printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n", - Aig_ManPiNum(pAig), pCex->nPis ); + Aig_ManCiNum(pAig), pCex->nPis ); return NULL; } @@ -948,7 +948,7 @@ clk = clock(); // if ( fVerbose ) { printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", - Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), + Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); ABC_PRT( "Time", clock() - clk ); } @@ -965,7 +965,7 @@ ABC_PRT( "Time", clock() - clk ); // if ( fVerbose ) { printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ", - Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), + Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons), Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) ); ABC_PRT( "Time", clock() - clk ); } diff --git a/src/aig/saig/saigRetFwd.c b/src/aig/saig/saigRetFwd.c index 94d08aaf..bbd7f397 100644 --- a/src/aig/saig/saigRetFwd.c +++ b/src/aig/saig/saigRetFwd.c @@ -53,7 +53,7 @@ Aig_Obj_t ** Aig_ManStaticFanoutStart( Aig_Man_t * p ) Aig_Obj_t ** ppFanouts, * pObj; int i, nFanouts, nFanoutsAlloc; // allocate fanouts - nFanoutsAlloc = 2 * Aig_ManObjNumMax(p) - Aig_ManPiNum(p) - Aig_ManPoNum(p); + nFanoutsAlloc = 2 * Aig_ManObjNumMax(p) - Aig_ManCiNum(p) - Aig_ManCoNum(p); ppFanouts = ABC_ALLOC( Aig_Obj_t *, nFanoutsAlloc ); // mark up storage nFanouts = 0; diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c index d4caff3f..161fce0a 100644 --- a/src/aig/saig/saigRetMin.c +++ b/src/aig/saig/saigRetMin.c @@ -69,12 +69,12 @@ Vec_Int_t * Saig_ManRetimeInitState( Aig_Man_t * p ) if ( RetValue == l_True ) { // accumulate SAT variables of the CIs - vCiIds = Vec_IntAlloc( Aig_ManPiNum(p) ); + vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) ); Aig_ManForEachCi( p, pObj, i ) Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] ); // create the model pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); - vInit = Vec_IntAllocArray( pModel, Aig_ManPiNum(p) ); + vInit = Vec_IntAllocArray( pModel, Aig_ManCiNum(p) ); Vec_IntFree( vCiIds ); } sat_solver_delete( pSat ); @@ -376,7 +376,7 @@ Aig_Man_t * Saig_ManRetimeDupBackward( Aig_Man_t * p, Vec_Ptr_t * vCut, Vec_Int_ pObj = Aig_ManConst1(p); pObj->pData = Aig_ManConst1(pNew); Saig_ManForEachPi( p, pObj, i ) - pObj->pData = Aig_ManPi( pNew, i ); + pObj->pData = Aig_ManCi( pNew, i ); // duplicate logic below the cut Saig_ManForEachPo( p, pObj, i ) { @@ -499,10 +499,10 @@ int Saig_ManHideBadRegs( Aig_Man_t * p, Vec_Ptr_t * vBadRegs ) Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) pObjLi->pData = pObjLo; // reorder them by putting bad registers first - vPisNew = Vec_PtrDup( p->vPis ); - vPosNew = Vec_PtrDup( p->vPos ); - nTruePi = Aig_ManPiNum(p) - Aig_ManRegNum(p); - nTruePo = Aig_ManPoNum(p) - Aig_ManRegNum(p); + vPisNew = Vec_PtrDup( p->vCis ); + vPosNew = Vec_PtrDup( p->vCos ); + nTruePi = Aig_ManCiNum(p) - Aig_ManRegNum(p); + nTruePo = Aig_ManCoNum(p) - Aig_ManRegNum(p); assert( nTruePi == p->nTruePis ); assert( nTruePo == p->nTruePos ); Vec_PtrForEachEntry( Aig_Obj_t *, vBadRegs, pObjLi, i ) @@ -522,11 +522,11 @@ int Saig_ManHideBadRegs( Aig_Man_t * p, Vec_Ptr_t * vBadRegs ) Vec_PtrWriteEntry( vPosNew, nTruePo++, pObjLi ); } // check the sizes - assert( nTruePi == Aig_ManPiNum(p) ); - assert( nTruePo == Aig_ManPoNum(p) ); + assert( nTruePi == Aig_ManCiNum(p) ); + assert( nTruePo == Aig_ManCoNum(p) ); // transfer the arrays - Vec_PtrFree( p->vPis ); p->vPis = vPisNew; - Vec_PtrFree( p->vPos ); p->vPos = vPosNew; + Vec_PtrFree( p->vCis ); p->vCis = vPisNew; + Vec_PtrFree( p->vCos ); p->vCos = vPosNew; // update the PIs nBadRegs = Vec_PtrSize(vBadRegs); p->nRegs -= nBadRegs; @@ -604,7 +604,7 @@ Aig_Man_t * Saig_ManRetimeMinAreaBackward( Aig_Man_t * pNew, int fVerbose ) printf( "Excluding register %d.\n", iBadReg ); // prepare to remove this output vBadRegs = Vec_PtrAlloc( 1 ); - Vec_PtrPush( vBadRegs, Aig_ManPo( pNew, Saig_ManPoNum(pNew) + iBadReg ) ); + Vec_PtrPush( vBadRegs, Aig_ManCo( pNew, Saig_ManPoNum(pNew) + iBadReg ) ); } return NULL; } diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c index 543c7e24..e43923f8 100644 --- a/src/aig/saig/saigRetStep.c +++ b/src/aig/saig/saigRetStep.c @@ -56,7 +56,7 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug pFanin0 = Aig_ObjFanin0(pObj); pFanin1 = Aig_ObjFanin1(pObj); // skip of they are not primary inputs - if ( !Aig_ObjIsPi(pFanin0) || !Aig_ObjIsPi(pFanin1) ) + if ( !Aig_ObjIsCi(pFanin0) || !Aig_ObjIsCi(pFanin1) ) return NULL; // skip of they are not register outputs @@ -90,11 +90,11 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug // create new register input pObjLi = Aig_ObjCreateCo( p, Aig_NotCond(pObjNew, fCompl) ); - pObjLi->PioNum = Aig_ManPoNum(p) - 1; + pObjLi->PioNum = Aig_ManCoNum(p) - 1; // create new register output pObjLo = Aig_ObjCreateCi( p ); - pObjLo->PioNum = Aig_ManPiNum(p) - 1; + pObjLo->PioNum = Aig_ManCiNum(p) - 1; p->nRegs++; // make sure the register is retimable. @@ -148,15 +148,15 @@ Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo ) // create latch inputs pLi0New = Aig_ObjCreateCo( p, Aig_NotCond(pFanin0, fCompl0) ); - pLi0New->PioNum = Aig_ManPoNum(p) - 1; + pLi0New->PioNum = Aig_ManCoNum(p) - 1; pLi1New = Aig_ObjCreateCo( p, Aig_NotCond(pFanin1, fCompl1) ); - pLi1New->PioNum = Aig_ManPoNum(p) - 1; + pLi1New->PioNum = Aig_ManCoNum(p) - 1; // create latch outputs pLo0New = Aig_ObjCreateCi(p); - pLo0New->PioNum = Aig_ManPiNum(p) - 1; + pLo0New->PioNum = Aig_ManCiNum(p) - 1; pLo1New = Aig_ObjCreateCi(p); - pLo1New->PioNum = Aig_ManPiNum(p) - 1; + pLo1New->PioNum = Aig_ManCiNum(p) - 1; pLo0New = Aig_NotCond( pLo0New, fCompl0 ); pLo1New = Aig_NotCond( pLo1New, fCompl1 ); p->nRegs += 2; diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c index d4b87e92..c83a7a64 100644 --- a/src/aig/saig/saigSimExt.c +++ b/src/aig/saig/saigSimExt.c @@ -81,7 +81,7 @@ int Saig_ManExtendOneEval( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) Value0 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin0(pObj), iFrame ); if ( Aig_ObjFaninC0(pObj) ) Value0 = Saig_ManSimInfoNot( Value0 ); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 ); return Value0; @@ -119,7 +119,7 @@ int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, 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 ); + Saig_ManSimInfoSet( vSimInfo, Aig_ManCi(p, Entry), f, SAIG_UND ); Aig_ManForEachNode( p, pObj, i ) Saig_ManExtendOneEval( vSimInfo, pObj, f ); Aig_ManForEachCo( p, pObj, i ) @@ -130,7 +130,7 @@ int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Saig_ManSimInfoSet( vSimInfo, pObjLo, f+1, Saig_ManSimInfoGet(vSimInfo, pObjLi, f) ); } // make sure the output of the property failed - pObj = Aig_ManPo( p, pCex->iPo ); + pObj = Aig_ManCo( p, pCex->iPo ); return Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame ); } @@ -148,7 +148,7 @@ int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int Saig_ManExtendOne( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int iPi, int iFrame, Vec_Int_t * vUndo, Vec_Int_t * vVis, Vec_Int_t * vVis2 ) { - Aig_Obj_t * pFanout, * pObj = Aig_ManPi(p, iPi); + Aig_Obj_t * pFanout, * pObj = Aig_ManCi(p, iPi); int i, k, f, iFanout = -1, Value, Value2, Entry; // save original value Value = Saig_ManSimInfoGet( vSimInfo, pObj, iFrame ); @@ -204,7 +204,7 @@ int Saig_ManExtendOne( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, } } // check the output - pObj = Aig_ManPo( p, pCex->iPo ); + pObj = Aig_ManCo( p, pCex->iPo ); Value = Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame ); assert( Value == SAIG_ONE || Value == SAIG_UND ); return (int)(Value == SAIG_ONE); @@ -525,7 +525,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, A if ( Saig_ManPiNum(p) != pCex->nPis ) { printf( "Saig_ManExtendCounterExampleTest(): The PI count of AIG (%d) does not match that of cex (%d).\n", - Aig_ManPiNum(p), pCex->nPis ); + Aig_ManCiNum(p), pCex->nPis ); return NULL; } Aig_ManFanoutStart( p ); diff --git a/src/aig/saig/saigSimExt2.c b/src/aig/saig/saigSimExt2.c index 6a0f514e..70a8892e 100644 --- a/src/aig/saig/saigSimExt2.c +++ b/src/aig/saig/saigSimExt2.c @@ -109,7 +109,7 @@ int Saig_ManExtendOneEval2( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) Value0 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin0(pObj), iFrame ); if ( Aig_ObjFaninC0(pObj) ) Value0 = Saig_ManSimInfo2Not( Value0 ); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { Saig_ManSimInfo2Set( vSimInfo, pObj, iFrame, Value0 ); return Value0; @@ -155,7 +155,7 @@ int Saig_ManSimDataInit2( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo Saig_ManSimInfo2Set( vSimInfo, pObjLo, f+1, Saig_ManSimInfo2Get(vSimInfo, pObjLi, f) ); } // make sure the output of the property failed - pObj = Aig_ManPo( p, pCex->iPo ); + pObj = Aig_ManCo( p, pCex->iPo ); return Saig_ManSimInfo2Get( vSimInfo, pObj, pCex->iFrame ); } @@ -177,7 +177,7 @@ void Saig_ManSetAndDriveImplications_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f int Value = Saig_ManSimInfo2Get( vSimInfo, pObj, f ); assert( !Saig_ManSimInfo2IsOld( Value ) ); Saig_ManSimInfo2Set( vSimInfo, pObj, f, Saig_ManSimInfo2SetOld(Value) ); - if ( (Aig_ObjIsPo(pObj) && f == fMax) || Saig_ObjIsPo(p, pObj) ) + if ( (Aig_ObjIsCo(pObj) && f == fMax) || Saig_ObjIsPo(p, pObj) ) return; if ( Saig_ObjIsLi( p, pObj ) ) { @@ -188,13 +188,13 @@ void Saig_ManSetAndDriveImplications_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f Saig_ManSetAndDriveImplications_rec( p, pFanout, f+1, fMax, vSimInfo ); return; } - assert( Aig_ObjIsPi(pObj) || Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) ); + assert( Aig_ObjIsCi(pObj) || Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) ); Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, k ) { Value = Saig_ManSimInfo2Get( vSimInfo, pFanout, f ); if ( Saig_ManSimInfo2IsOld( Value ) ) continue; - if ( Aig_ObjIsPo(pFanout) ) + if ( Aig_ObjIsCo(pFanout) ) { Saig_ManSetAndDriveImplications_rec( p, pFanout, f, fMax, vSimInfo ); continue; @@ -238,7 +238,7 @@ void Saig_ManExplorePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax, int i, iPiNum = Aig_ObjPioNum(pObj); for ( i = fMax; i >= 0; i-- ) if ( i != f ) - Saig_ManSetAndDriveImplications_rec( p, Aig_ManPi(p, iPiNum), i, fMax, vSimInfo ); + Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, iPiNum), i, fMax, vSimInfo ); return; } if ( Saig_ObjIsLo( p, pObj ) ) @@ -247,7 +247,7 @@ void Saig_ManExplorePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax, Saig_ManExplorePaths_rec( p, Saig_ObjLoToLi(p, pObj), f-1, fMax, vSimInfo ); return; } - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, fMax, vSimInfo ); return; @@ -295,10 +295,10 @@ Vec_Int_t * Saig_ManProcessCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCe { Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo ); for ( i = 0; i < iFirstFlopPi; i++ ) - Saig_ManSetAndDriveImplications_rec( p, Aig_ManPi(p, i), f, pCex->iFrame, vSimInfo ); + Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, i), f, pCex->iFrame, vSimInfo ); } // recursively compute justification - Saig_ManExplorePaths_rec( p, Aig_ManPo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo ); + Saig_ManExplorePaths_rec( p, Aig_ManCo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo ); // select the result vRes = Vec_IntAlloc( 1000 ); vResInv = Vec_IntAlloc( 1000 ); @@ -306,7 +306,7 @@ Vec_Int_t * Saig_ManProcessCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCe { for ( f = pCex->iFrame; f >= 0; f-- ) { - Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManPi(p, i), f ); + Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManCi(p, i), f ); if ( Saig_ManSimInfo2IsOld( Value ) ) break; } @@ -341,7 +341,7 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstFlopPi, if ( Saig_ManPiNum(p) != pCex->nPis ) { printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", - Aig_ManPiNum(p), pCex->nPis ); + Aig_ManCiNum(p), pCex->nPis ); return NULL; } Aig_ManFanoutStart( p ); @@ -393,10 +393,10 @@ Abc_Cex_t * Saig_ManDeriveCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex { Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo ); for ( i = 0; i < iFirstFlopPi; i++ ) - Saig_ManSetAndDriveImplications_rec( p, Aig_ManPi(p, i), f, pCex->iFrame, vSimInfo ); + Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, i), f, pCex->iFrame, vSimInfo ); } // recursively compute justification - Saig_ManExplorePaths_rec( p, Aig_ManPo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo ); + Saig_ManExplorePaths_rec( p, Aig_ManCo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo ); // create CEX pCare = Abc_CexDup( pCex, pCex->nRegs ); @@ -410,7 +410,7 @@ Abc_Cex_t * Saig_ManDeriveCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex int fFound = 0; for ( f = pCex->iFrame; f >= 0; f-- ) { - Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManPi(p, i), f ); + Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManCi(p, i), f ); if ( Saig_ManSimInfo2IsOld( Value ) ) { fFound = 1; @@ -450,7 +450,7 @@ Abc_Cex_t * Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int i if ( Saig_ManPiNum(p) != pCex->nPis ) { printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", - Aig_ManPiNum(p), pCex->nPis ); + Aig_ManCiNum(p), pCex->nPis ); return NULL; } Aig_ManFanoutStart( p ); diff --git a/src/aig/saig/saigSimFast.c b/src/aig/saig/saigSimFast.c index 2c0f3974..27855bfd 100644 --- a/src/aig/saig/saigSimFast.c +++ b/src/aig/saig/saigSimFast.c @@ -93,7 +93,7 @@ static inline int Faig_ObjFanin( int iFan ) { return iFan >> 1 int Faig_ManIsCorrect( Aig_Man_t * pAig ) { return Aig_ManObjNumMax(pAig) == - 1 + Aig_ManPiNum(pAig) + Aig_ManNodeNum(pAig) + Aig_ManPoNum(pAig); + 1 + Aig_ManCiNum(pAig) + Aig_ManNodeNum(pAig) + Aig_ManCoNum(pAig); } /**Function************************************************************* @@ -112,14 +112,14 @@ Faig_Man_t * Faig_ManAlloc( Aig_Man_t * pAig ) Faig_Man_t * p; int nWords; // assert( Faig_ManIsCorrect(pAig) ); - nWords = 2 * Aig_ManNodeNum(pAig) + Aig_ManPoNum(pAig); + nWords = 2 * Aig_ManNodeNum(pAig) + Aig_ManCoNum(pAig); p = (Faig_Man_t *)ABC_ALLOC( char, sizeof(Faig_Man_t) + sizeof(int) * nWords ); //printf( "Allocating %7.2f Mb.\n", 1.0 * (sizeof(Faig_Man_t) + sizeof(int) * nWords)/(1<<20) ); memset( p, 0, sizeof(Faig_Man_t) ); - p->nPis = Aig_ManPiNum(pAig) - Aig_ManRegNum(pAig); - p->nPos = Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig); - p->nCis = Aig_ManPiNum(pAig); - p->nCos = Aig_ManPoNum(pAig); + p->nPis = Aig_ManCiNum(pAig) - Aig_ManRegNum(pAig); + p->nPos = Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig); + p->nCis = Aig_ManCiNum(pAig); + p->nCos = Aig_ManCoNum(pAig); p->nFfs = Aig_ManRegNum(pAig); p->nNos = Aig_ManNodeNum(pAig); // offsets diff --git a/src/aig/saig/saigSimMv.c b/src/aig/saig/saigSimMv.c index 2a1cea40..11bd088c 100644 --- a/src/aig/saig/saigSimMv.c +++ b/src/aig/saig/saigSimMv.c @@ -138,7 +138,7 @@ Saig_MvObj_t * Saig_ManCreateReducedAig( Aig_Man_t * p, Vec_Ptr_t ** pvFlops ) { pEntry = pAig + i; pEntry->Type = pObj->Type; - if ( Aig_ObjIsPi(pObj) || i == 0 ) + if ( Aig_ObjIsCi(pObj) || i == 0 ) { if ( Saig_ObjIsLo(p, pObj) ) { @@ -149,7 +149,7 @@ Saig_MvObj_t * Saig_ManCreateReducedAig( Aig_Man_t * p, Vec_Ptr_t ** pvFlops ) continue; } pEntry->iFan0 = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) continue; assert( Aig_ObjIsNode(pObj) ); pEntry->iFan1 = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj); @@ -442,9 +442,9 @@ void Saig_MvSimulateFrame( Saig_MvMan_t * p, int fFirst, int fVerbose ) Saig_MvSimulateValue0(p->pAigOld, pEntry), Saig_MvSimulateValue1(p->pAigOld, pEntry), fFirst ); } - else if ( pEntry->Type == AIG_OBJ_PO ) + else if ( pEntry->Type == AIG_OBJ_CO ) pEntry->Value = Saig_MvSimulateValue0(p->pAigOld, pEntry); - else if ( pEntry->Type == AIG_OBJ_PI ) + else if ( pEntry->Type == AIG_OBJ_CI ) { if ( pEntry->iFan1 == 0 ) // true PI { @@ -827,7 +827,7 @@ Vec_Ptr_t * Saig_MvManDeriveMap( Saig_MvMan_t * p, int fVerbose ) int i, k, j, FlopK, FlopJ; int Counter1 = 0, Counter2 = 0; // prepare CI map - vMap = Vec_PtrAlloc( Aig_ManPiNum(p->pAig) ); + vMap = Vec_PtrAlloc( Aig_ManCiNum(p->pAig) ); Aig_ManForEachCi( p->pAig, pObj, i ) Vec_PtrPush( vMap, pObj ); // detect constant flops diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c index 89dd2b5d..a134b412 100644 --- a/src/aig/saig/saigSimSeq.c +++ b/src/aig/saig/saigSimSeq.c @@ -115,7 +115,7 @@ int Raig_ManCreate_rec( Raig_Man_t * p, Aig_Obj_t * pObj ) iFan1 = Raig_ManCreate_rec( p, Aig_ObjFanin1(pObj) ); iFan1 = (iFan1 << 1) | Aig_ObjFaninC1(pObj); } - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) { iFan0 = Raig_ManCreate_rec( p, Aig_ObjFanin0(pObj) ); iFan0 = (iFan0 << 1) | Aig_ObjFaninC0(pObj); @@ -154,15 +154,15 @@ Raig_Man_t * Raig_ManCreate( Aig_Man_t * pAig ) p->pAig = pAig; p->nPis = Saig_ManPiNum(pAig); p->nPos = Saig_ManPoNum(pAig); - p->nCis = Aig_ManPiNum(pAig); - p->nCos = Aig_ManPoNum(pAig); + p->nCis = Aig_ManCiNum(pAig); + p->nCos = Aig_ManCoNum(pAig); p->nNodes = Aig_ManNodeNum(pAig); nObjs = p->nCis + p->nCos + p->nNodes + 2; p->pFans0 = ABC_ALLOC( int, nObjs ); p->pFans1 = ABC_ALLOC( int, nObjs ); p->pRefs = ABC_ALLOC( int, nObjs ); p->pSims = ABC_CALLOC( unsigned, nObjs ); - p->vCis2Ids = Vec_IntAlloc( Aig_ManPiNum(pAig) ); + p->vCis2Ids = Vec_IntAlloc( Aig_ManCiNum(pAig) ); // add objects (0=unused; 1=const1) p->nObjs = 2; pObj = Aig_ManConst1( pAig ); @@ -172,7 +172,7 @@ Raig_Man_t * Raig_ManCreate( Aig_Man_t * pAig ) Raig_ManCreate_rec( p, pObj ); Aig_ManForEachCo( pAig, pObj, i ) Raig_ManCreate_rec( p, pObj ); - assert( Vec_IntSize(p->vCis2Ids) == Aig_ManPiNum(pAig) ); + assert( Vec_IntSize(p->vCis2Ids) == Aig_ManCiNum(pAig) ); assert( p->nObjs == nObjs ); // collect flop outputs p->vLos = Vec_IntAlloc( Aig_ManRegNum(pAig) ); @@ -426,7 +426,7 @@ Abc_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int Counter = p->nRegs; pData = ABC_ALLOC( unsigned, nWords ); for ( f = 0; f <= iFrame; f++, Counter += p->nPis ) - for ( i = 0; i < Aig_ManPiNum(pAig); i++ ) + for ( i = 0; i < Aig_ManCiNum(pAig); i++ ) { iPioId = Vec_IntEntry( vCis2Ids, i ); if ( iPioId >= p->nPis ) diff --git a/src/aig/saig/saigStrSim.c b/src/aig/saig/saigStrSim.c index 06890c7a..5d33595f 100644 --- a/src/aig/saig/saigStrSim.c +++ b/src/aig/saig/saigStrSim.c @@ -298,7 +298,7 @@ void Saig_StrSimulateRound( Aig_Man_t * p0, Aig_Man_t * p1 ) // simulate the nodes Aig_ManForEachObj( p0, pObj0, i ) { - if ( !Aig_ObjIsPi(pObj0) && !Aig_ObjIsNode(pObj0) ) + if ( !Aig_ObjIsCi(pObj0) && !Aig_ObjIsNode(pObj0) ) continue; pObj1 = Aig_ObjRepr(p0, pObj0); if ( pObj1 == NULL ) @@ -406,7 +406,7 @@ int Saig_StrSimDetectUnique( Aig_Man_t * p0, Aig_Man_t * p1 ) // hash nodes of the first AIG Aig_ManForEachObj( p0, pObj, i ) { - if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) ) + if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) ) continue; if ( Aig_ObjRepr(p0, pObj) ) continue; @@ -423,7 +423,7 @@ int Saig_StrSimDetectUnique( Aig_Man_t * p0, Aig_Man_t * p1 ) // hash nodes from the second AIG Aig_ManForEachObj( p1, pObj, i ) { - if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) ) + if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) ) continue; if ( Aig_ObjRepr(p1, pObj) ) continue; @@ -551,7 +551,7 @@ void Saig_StrSimSetInitMatching( Aig_Man_t * p0, Aig_Man_t * p1 ) Aig_ObjSetRepr( p1, pObj1, pObj0 ); Saig_ManForEachPi( p0, pObj0, i ) { - pObj1 = Aig_ManPi( p1, i ); + pObj1 = Aig_ManCi( p1, i ); Aig_ObjSetRepr( p0, pObj0, pObj1 ); Aig_ObjSetRepr( p1, pObj1, pObj0 ); } @@ -650,14 +650,14 @@ void Saig_StrSimSetContiguousMatching_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) Saig_StrSimSetContiguousMatching_rec( p, Saig_ObjLiToLo(p, pObj) ); return; } - assert( Aig_ObjIsPi(pObj) || Aig_ObjIsNode(pObj) ); + assert( Aig_ObjIsCi(pObj) || Aig_ObjIsNode(pObj) ); if ( Aig_ObjRepr(p, pObj) == NULL ) return; // go through the fanouts Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, i ) Saig_StrSimSetContiguousMatching_rec( p, pFanout ); // go through the fanins - if ( !Aig_ObjIsPi( pObj ) ) + if ( !Aig_ObjIsCi( pObj ) ) { Saig_StrSimSetContiguousMatching_rec( p, Aig_ObjFanin0(pObj) ); Saig_StrSimSetContiguousMatching_rec( p, Aig_ObjFanin1(pObj) ); @@ -724,7 +724,7 @@ void Ssw_StrSimMatchingExtendOne( Aig_Man_t * p, Vec_Ptr_t * vNodes ) Aig_ManIncrementTravId( p ); Aig_ManForEachObj( p, pObj, i ) { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; if ( Aig_ObjRepr( p, pObj ) != NULL ) continue; @@ -785,7 +785,7 @@ int Ssw_StrSimMatchingCountUnmached( Aig_Man_t * p ) int i, Counter = 0; Aig_ManForEachObj( p, pObj, i ) { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; if ( Aig_ObjRepr( p, pObj ) != NULL ) continue; @@ -817,8 +817,8 @@ void Ssw_StrSimMatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fV int nUnmached = Ssw_StrSimMatchingCountUnmached(p0); printf( "Extending islands by %d steps:\n", nDist ); printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n", - 0, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0), - nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) ); + 0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), + nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) ); } for ( d = 0; d < nDist; d++ ) { @@ -850,8 +850,8 @@ void Ssw_StrSimMatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fV { int nUnmached = Ssw_StrSimMatchingCountUnmached(p0); printf( "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n", - d+1, Aig_ManPiNum(p0) + Aig_ManNodeNum(p0), - nUnmached, 100.0 * nUnmached/(Aig_ManPiNum(p0) + Aig_ManNodeNum(p0)) ); + d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0), + nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) ); } } Vec_PtrFree( vNodes0 ); diff --git a/src/aig/saig/saigSwitch.c b/src/aig/saig/saigSwitch.c index 37270b52..4c54e3ad 100644 --- a/src/aig/saig/saigSwitch.c +++ b/src/aig/saig/saigSwitch.c @@ -74,7 +74,7 @@ Saig_SimObj_t * Saig_ManCreateMan( Aig_Man_t * p ) { pEntry = pAig + i; pEntry->Type = pObj->Type; - if ( Aig_ObjIsPi(pObj) || i == 0 ) + if ( Aig_ObjIsCi(pObj) || i == 0 ) { if ( Saig_ObjIsLo(p, pObj) ) { @@ -84,7 +84,7 @@ Saig_SimObj_t * Saig_ManCreateMan( Aig_Man_t * p ) continue; } pEntry->iFan0 = (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) continue; assert( Aig_ObjIsNode(pObj) ); pEntry->iFan1 = (Aig_ObjFaninId1(pObj) << 1) | Aig_ObjFaninC1(pObj); @@ -179,9 +179,9 @@ void Saig_ManSimulateFrames( Saig_SimObj_t * pAig, int nFrames, int nPref ) { if ( pEntry->Type == AIG_OBJ_AND ) Saig_ManSimulateNode( pAig, pEntry ); - else if ( pEntry->Type == AIG_OBJ_PO ) + else if ( pEntry->Type == AIG_OBJ_CO ) Saig_ManSimulateOneInput( pAig, pEntry ); - else if ( pEntry->Type == AIG_OBJ_PI ) + else if ( pEntry->Type == AIG_OBJ_CI ) { if ( pEntry->iFan0 == 0 ) // true PI pEntry->pData[0] = Aig_ManRandom( 0 ); @@ -548,7 +548,7 @@ Aig_CMan_t * Aig_CManCreate( Aig_Man_t * p ) Aig_CMan_t * pCMan; Aig_Obj_t * pObj; int i; - pCMan = Aig_CManStart( Aig_ManPiNum(p), Aig_ManNodeNum(p), Aig_ManPoNum(p) ); + pCMan = Aig_CManStart( Aig_ManCiNum(p), Aig_ManNodeNum(p), Aig_ManCoNum(p) ); Aig_ManForEachNode( p, pObj, i ) Aig_CManAddNode( pCMan, (Aig_ObjFaninId0(pObj) << 1) | Aig_ObjFaninC0(pObj), diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c index 3b11c55c..c8c33680 100644 --- a/src/aig/saig/saigTempor.c +++ b/src/aig/saig/saigTempor.c @@ -98,7 +98,7 @@ Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames ) } // create initialized timeframes pFrames = Saig_ManTemporFrames( pAig, nFrames ); - assert( Aig_ManPoNum(pFrames) == Aig_ManRegNum(pAig) ); + assert( Aig_ManCoNum(pFrames) == Aig_ManRegNum(pAig) ); // start the new manager Aig_ManCleanData( pAig ); @@ -123,7 +123,7 @@ Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames ) // create flop output values Saig_ManForEachLo( pAig, pObj, i ) - pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreateCi(pAigNew), (Aig_Obj_t *)Aig_ManPo(pFrames, i)->pData ); + pObj->pData = Aig_Mux( pAigNew, pReset, Aig_ObjCreateCi(pAigNew), (Aig_Obj_t *)Aig_ManCo(pFrames, i)->pData ); Aig_ManStop( pFrames ); // add internal nodes of this frame diff --git a/src/aig/saig/saigTrans.c b/src/aig/saig/saigTrans.c index 552ec8f3..9be84e31 100644 --- a/src/aig/saig/saigTrans.c +++ b/src/aig/saig/saigTrans.c @@ -299,7 +299,7 @@ Aig_Man_t * Saig_ManFramesInitialMapped( Aig_Man_t * pAig, int nFrames, int nFra if ( fInit ) pObj->pData = Aig_ObjCreateCi( pFrames ); else - pObj->pData = Aig_ManPi( pFrames, f * Saig_ManPiNum(pAig) + i ); + pObj->pData = Aig_ManCi( pFrames, f * Saig_ManPiNum(pAig) + i ); Saig_ManSetMap1( pAig, pObj, f, Aig_Regular((Aig_Obj_t *)pObj->pData) ); } // add internal nodes of this frame diff --git a/src/aig/saig/saigWnd.c b/src/aig/saig/saigWnd.c index fc1f9191..ce70e7b4 100644 --- a/src/aig/saig/saigWnd.c +++ b/src/aig/saig/saigWnd.c @@ -359,7 +359,7 @@ Aig_Man_t * Saig_ManWindowInsertNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes, Aig_Ma vSmallPi2BigNode = Vec_PtrStart( Aig_ManObjNumMax(pWnd) ); vNodesPi = Saig_ManWindowCollectPis( p, vNodes ); Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPi, pObj, i ) - Vec_PtrWriteEntry( vSmallPi2BigNode, Aig_ManPi(pWnd, i)->Id, pObj ); + Vec_PtrWriteEntry( vSmallPi2BigNode, Aig_ManCi(pWnd, i)->Id, pObj ); assert( i == Saig_ManPiNum(pWnd) ); Vec_PtrFree( vNodesPi ); @@ -367,7 +367,7 @@ Aig_Man_t * Saig_ManWindowInsertNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes, Aig_Ma vBigNode2SmallPo = Vec_PtrStart( Aig_ManObjNumMax(p) ); vNodesPo = Saig_ManWindowCollectPos( p, vNodes, NULL ); Vec_PtrForEachEntry( Aig_Obj_t *, vNodesPo, pObj, i ) - Vec_PtrWriteEntry( vBigNode2SmallPo, pObj->Id, Aig_ManPo(pWnd, i) ); + Vec_PtrWriteEntry( vBigNode2SmallPo, pObj->Id, Aig_ManCo(pWnd, i) ); assert( i == Saig_ManPoNum(pWnd) ); Vec_PtrFree( vNodesPo ); @@ -407,8 +407,8 @@ Aig_Man_t * Saig_ManWindowInsertNodes( Aig_Man_t * p, Vec_Ptr_t * vNodes, Aig_Ma Vec_PtrFree( vBigNode2SmallPo ); Vec_PtrFree( vSmallPi2BigNode ); // set the new number of registers - assert( Aig_ManPiNum(pNew) - Aig_ManPiNum(p) == Aig_ManPoNum(pNew) - Aig_ManPoNum(p) ); - Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) + (Aig_ManPiNum(pNew) - Aig_ManPiNum(p)) ); + assert( Aig_ManCiNum(pNew) - Aig_ManCiNum(p) == Aig_ManCoNum(pNew) - Aig_ManCoNum(p) ); + Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) + (Aig_ManCiNum(pNew) - Aig_ManCiNum(p)) ); Aig_ManCleanup( pNew ); return pNew; } @@ -567,7 +567,7 @@ Vec_Ptr_t * Saig_ManCollectedDiffNodes( Aig_Man_t * p0, Aig_Man_t * p1 ) } // mark and collect unmatched objects Aig_ObjSetTravIdCurrent( p0, pObj0 ); - if ( Aig_ObjIsNode(pObj0) || Aig_ObjIsPi(pObj0) ) + if ( Aig_ObjIsNode(pObj0) || Aig_ObjIsCi(pObj0) ) Vec_PtrPush( vNodes, pObj0 ); } // make sure LI/LO are labeled/unlabeled mutually @@ -658,11 +658,11 @@ void Saig_ManWindowCreatePos( Aig_Man_t * pNew, Aig_Man_t * p0, Aig_Man_t * p1 ) continue; if ( Aig_ObjIsConst1(pObj0) ) continue; - if ( Aig_ObjIsPi(pObj0) ) + if ( Aig_ObjIsCi(pObj0) ) continue; pObj1 = Aig_ObjRepr( p0, pObj0 ); assert( pObj0 == Aig_ObjRepr( p1, pObj1 ) ); - if ( Aig_ObjIsPo(pObj0) ) + if ( Aig_ObjIsCo(pObj0) ) { pFanin0 = Aig_ObjFanin0(pObj0); pFanin1 = Aig_ObjFanin0(pObj1); @@ -722,7 +722,7 @@ Aig_Man_t * Saig_ManWindowExtractMiter( Aig_Man_t * p0, Aig_Man_t * p1 ) // add matching of POs and LIs Saig_ManForEachPo( p0, pObj0, i ) { - pObj1 = Aig_ManPo( p1, i ); + pObj1 = Aig_ManCo( p1, i ); Aig_ObjSetRepr( p0, pObj0, pObj1 ); Aig_ObjSetRepr( p1, pObj1, pObj0 ); } |