diff options
45 files changed, 146 insertions, 146 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 4c437b8c..3c390a37 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -71,7 +71,7 @@ struct Aig_Obj_t_ // 9 words { union { Aig_Obj_t * pNext; // strashing table - int PioNum; // the number of PI/PO + int CioId; // 0-based number of CI/CO }; Aig_Obj_t * pFanin0; // fanin Aig_Obj_t * pFanin1; // fanin @@ -268,7 +268,6 @@ static inline Aig_Obj_t * Aig_ManLi( Aig_Man_t * p, int i ) { return (Aig_ static inline Aig_Obj_t * Aig_ManObj( Aig_Man_t * p, int i ) { return p->vObjs ? (Aig_Obj_t *)Vec_PtrEntry(p->vObjs, i) : NULL; } static inline Aig_Type_t Aig_ObjType( Aig_Obj_t * pObj ) { return (Aig_Type_t)pObj->Type; } -static inline int Aig_ObjId( Aig_Obj_t * pObj ) { return pObj->Id; } static inline int Aig_ObjIsNone( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_NONE; } static inline int Aig_ObjIsConst1( Aig_Obj_t * pObj ) { assert(!Aig_IsComplement(pObj)); return pObj->Type == AIG_OBJ_CONST1; } static inline int Aig_ObjIsCi( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_CI; } @@ -281,6 +280,8 @@ static inline int Aig_ObjIsTerm( Aig_Obj_t * pObj ) { return pObj- static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; } static inline int Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0; } static inline int Aig_ObjIsCand( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_CI || pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; } +static inline int Aig_ObjCioId( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return pObj->CioId; } +static inline int Aig_ObjId( Aig_Obj_t * pObj ) { return pObj->Id; } static inline int Aig_ObjIsMarkA( Aig_Obj_t * pObj ) { return pObj->fMarkA; } static inline void Aig_ObjSetMarkA( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; } @@ -327,7 +328,6 @@ static inline void Aig_ObjSetEquiv( Aig_Man_t * p, Aig_Obj_t * pObj, Aig static inline Aig_Obj_t * Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pReprs? p->pReprs[pObj->Id] : NULL; } static inline void Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr ) { assert(p->pReprs); p->pReprs[pObj->Id] = pRepr; } static inline Aig_Obj_t * Aig_ObjHaig( Aig_Obj_t * pObj ) { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) ); } -static inline int Aig_ObjPioNum( Aig_Obj_t * pObj ) { assert( !Aig_ObjIsNode(pObj) ); return (int)(ABC_PTRINT_T)pObj->pNext; } static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin ) { if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; @@ -658,8 +658,8 @@ extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig ); extern void Aig_ManDump( Aig_Man_t * p ); extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec_Ptr_t * vPoNames ); extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName ); -extern void Aig_ManSetPioNumbers( Aig_Man_t * p ); -extern void Aig_ManCleanPioNumbers( Aig_Man_t * p ); +extern void Aig_ManSetCioIds( Aig_Man_t * p ); +extern void Aig_ManCleanCioIds( Aig_Man_t * p ); extern int Aig_ManChoiceNum( Aig_Man_t * p ); extern char * Aig_FileNameGenericAppend( char * pBase, char * pSuffix ); extern unsigned Aig_ManRandom( int fReset ); diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 20830acb..ace723a2 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -47,7 +47,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p ) { Aig_Obj_t * pObj, * pNext; int i, k, iBox, iTerm1, nTerms; - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); Aig_ManIncrementTravId( p ); Aig_ManForEachObj( p, pObj, i ) { @@ -79,7 +79,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p ) { if ( p->pManTime ) { - iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj) ); + iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) ); if ( iBox >= 0 ) // this is not a true PI { iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox ); @@ -87,7 +87,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p ) for ( k = 0; k < nTerms; k++ ) { pNext = Aig_ManCo( p, iTerm1 + k ); - assert( Tim_ManBoxForCo( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pNext) ) == iBox ); + assert( Tim_ManBoxForCo( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pNext) ) == iBox ); if ( !Aig_ObjIsTravIdCurrent(p,pNext) ) { printf( "Box %d has input %d that is not in a topological order.\n", iBox, pNext->Id ); @@ -101,7 +101,7 @@ int Aig_ManVerifyTopoOrder( Aig_Man_t * p ) assert( 0 ); Aig_ObjSetTravIdCurrent( p, pObj ); } - Aig_ManCleanPioNumbers( p ); + Aig_ManCleanCioIds( p ); return 1; } @@ -505,7 +505,7 @@ void Aig_ManChoiceLevel_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) { if ( p->pManTime ) { - iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj) ); + iBox = Tim_ManBoxForCi( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) ); if ( iBox >= 0 ) // this is not a true PI { iTerm1 = Tim_ManBoxInputFirst( (Tim_Man_t *)p->pManTime, iBox ); @@ -572,7 +572,7 @@ int Aig_ManChoiceLevel( Aig_Man_t * p ) int i, LevelMax = 0; Aig_ManForEachObj( p, pObj, i ) Aig_ObjSetLevel( pObj, 0 ); - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); Aig_ManIncrementTravId( p ); Aig_ManForEachCo( p, pObj, i ) { @@ -587,7 +587,7 @@ int Aig_ManChoiceLevel( Aig_Man_t * p ) if ( LevelMax < Aig_ObjLevel(pObj) ) LevelMax = Aig_ObjLevel(pObj); } - Aig_ManCleanPioNumbers( p ); + Aig_ManCleanCioIds( p ); // Aig_ManForEachNode( p, pObj, i ) // assert( Aig_ObjLevel(pObj) > 0 ); return LevelMax; diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index 9b993c86..97d99128 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -679,16 +679,16 @@ Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder ) int i; assert( Aig_ManCiNum(p) == Aig_ManCiNum(pOrder) ); assert( Aig_ManCoNum(p) == Aig_ManCoNum(pOrder) ); - Aig_ManSetPioNumbers( pOrder ); + Aig_ManSetCioIds( pOrder ); vPios = Vec_PtrAlloc( Aig_ManCiNum(p) + Aig_ManCoNum(p) ); Aig_ManForEachObj( pOrder, pObj, i ) { if ( Aig_ObjIsCi(pObj) ) - Vec_PtrPush( vPios, Aig_ManCi(p, Aig_ObjPioNum(pObj)) ); + Vec_PtrPush( vPios, Aig_ManCi(p, Aig_ObjCioId(pObj)) ); else if ( Aig_ObjIsCo(pObj) ) - Vec_PtrPush( vPios, Aig_ManCo(p, Aig_ObjPioNum(pObj)) ); + Vec_PtrPush( vPios, Aig_ManCo(p, Aig_ObjCioId(pObj)) ); } - Aig_ManCleanPioNumbers( pOrder ); + Aig_ManCleanCioIds( pOrder ); return vPios; } diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c index a6df4a1b..2c524c85 100644 --- a/src/aig/aig/aigJust.c +++ b/src/aig/aig/aigJust.c @@ -114,7 +114,7 @@ int Aig_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Ve // if ( Aig_ObjId(pNode) % 1000 == 0 ) // Value ^= 1; if ( vSuppLits ) - Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) ); + Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjCioId(pNode), !Value ) ); return 1; } assert( Aig_ObjIsNode(pNode) ); diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index ed8cf8e9..a7bd17da 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -455,7 +455,7 @@ void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs ) p->nRegs = nRegs; p->nTruePis = Aig_ManCiNum(p) - nRegs; p->nTruePos = Aig_ManCoNum(p) - nRegs; - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); } /**Function************************************************************* diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index 587596b5..56d2fd3f 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -1133,7 +1133,7 @@ void Aig_ManSupportNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vSupp Aig_ObjSetTravIdCurrent(p, pObj); if ( Aig_ObjIsCi(pObj) ) { - Vec_IntPush( vSupport, Aig_ObjPioNum(pObj) ); + Vec_IntPush( vSupport, Aig_ObjCioId(pObj) ); return; } Aig_ManSupportNodes_rec( p, Aig_ObjFanin0(pObj), vSupport ); @@ -1156,7 +1156,7 @@ Vec_Ptr_t * Aig_ManSupportNodes( Aig_Man_t * p, Vec_Ptr_t * vParts ) Vec_Ptr_t * vPartSupps; Vec_Int_t * vPart, * vSupport; int i, k, iOut; - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); vPartSupps = Vec_PtrAlloc( Vec_PtrSize(vParts) ); Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i ) { @@ -1168,7 +1168,7 @@ Vec_Ptr_t * Aig_ManSupportNodes( Aig_Man_t * p, Vec_Ptr_t * vParts ) // Vec_IntSort( vSupport, 0 ); Vec_PtrPush( vPartSupps, vSupport ); } - Aig_ManCleanPioNumbers( p ); + Aig_ManCleanCioIds( p ); return vPartSupps; } @@ -1392,7 +1392,7 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); // set the PI numbers - Aig_ManSetPioNumbers( pAig ); + Aig_ManSetCioIds( pAig ); // create the total fraiged AIG Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i ) @@ -1425,7 +1425,7 @@ Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfM Vec_VecFree( (Vec_Vec_t *)vParts ); // clear the PI numbers - Aig_ManCleanPioNumbers( pAig ); + Aig_ManCleanCioIds( pAig ); // derive the result of choicing return Aig_ManDupRepr( pAig, 0 ); diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c index 26de9244..5dc79d7f 100644 --- a/src/aig/aig/aigScl.c +++ b/src/aig/aig/aigScl.c @@ -77,15 +77,15 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ) pObj->pData = Aig_NotCond( (Aig_Obj_t *)Aig_Regular(pObjMapped)->pData, Aig_IsComplement(pObjMapped) ); if ( pNew->vFlopReprs && i >= nTruePis && pObj != pObjMapped ) { - Vec_IntPush( pNew->vFlopReprs, Aig_ObjPioNum(pObj) ); + Vec_IntPush( pNew->vFlopReprs, Aig_ObjCioId(pObj) ); if ( Aig_ObjIsConst1( Aig_Regular(pObjMapped) ) ) Vec_IntPush( pNew->vFlopReprs, -1 ); else { assert( !Aig_IsComplement(pObjMapped) ); assert( Aig_ObjIsCi(pObjMapped) ); - assert( Aig_ObjPioNum(pObj) != Aig_ObjPioNum(pObjMapped) ); - Vec_IntPush( pNew->vFlopReprs, Aig_ObjPioNum(pObjMapped) ); + assert( Aig_ObjCioId(pObj) != Aig_ObjCioId(pObjMapped) ); + Vec_IntPush( pNew->vFlopReprs, Aig_ObjCioId(pObjMapped) ); } } } @@ -236,7 +236,7 @@ int Aig_ManSeqCleanup( Aig_Man_t * p ) Vec_PtrFree( vNodes ); p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p); p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p); - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); // remove dangling nodes return Aig_ManCleanup( p ); } diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index c247208f..0cf12370 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -799,16 +799,16 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec // write nodes if ( pConst1 ) fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData ); - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) { fprintf( pFile, ".names" ); if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) ) - fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjPioNum(Aig_ObjFanin0(pObj))) ); + fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) ); else fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData ); if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin1(pObj)) ) - fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjPioNum(Aig_ObjFanin1(pObj))) ); + fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin1(pObj))) ); else fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin1(pObj)->iData ); fprintf( pFile, " n%0*d\n", nDigits, pObj->iData ); @@ -819,16 +819,16 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName, Vec_Ptr_t * vPiNames, Vec { fprintf( pFile, ".names" ); if ( vPiNames && Aig_ObjIsCi(Aig_ObjFanin0(pObj)) ) - fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjPioNum(Aig_ObjFanin0(pObj))) ); + fprintf( pFile, " %s", (char*)Vec_PtrEntry(vPiNames, Aig_ObjCioId(Aig_ObjFanin0(pObj))) ); else fprintf( pFile, " n%0*d", nDigits, Aig_ObjFanin0(pObj)->iData ); if ( vPoNames ) - fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Aig_ObjPioNum(pObj)) ); + fprintf( pFile, " %s\n", (char*)Vec_PtrEntry(vPoNames, Aig_ObjCioId(pObj)) ); else fprintf( pFile, " n%0*d\n", nDigits, pObj->iData ); fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) ); } - Aig_ManCleanPioNumbers( p ); + Aig_ManCleanCioIds( p ); fprintf( pFile, ".end\n\n" ); fclose( pFile ); Vec_PtrFree( vNodes ); @@ -962,14 +962,14 @@ void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName ) SeeAlso [] ***********************************************************************/ -void Aig_ManSetPioNumbers( Aig_Man_t * p ) +void Aig_ManSetCioIds( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; Aig_ManForEachCi( p, pObj, i ) - pObj->PioNum = i; + pObj->CioId = i; Aig_ManForEachCo( p, pObj, i ) - pObj->PioNum = i; + pObj->CioId = i; } /**Function************************************************************* @@ -983,7 +983,7 @@ void Aig_ManSetPioNumbers( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Aig_ManCleanPioNumbers( Aig_Man_t * p ) +void Aig_ManCleanCioIds( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 0f2234b7..8752082f 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -104,13 +104,13 @@ static inline int Saig_ManConstrNum( Aig_Man_t * 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; } +static inline int Saig_ObjIsPi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCi(pObj) && Aig_ObjCioId(pObj) < Saig_ManPiNum(p); } +static inline int Saig_ObjIsPo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCo(pObj) && Aig_ObjCioId(pObj) < Saig_ManPoNum(p); } +static inline int Saig_ObjIsLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCi(pObj) && Aig_ObjCioId(pObj) >= Saig_ManPiNum(p); } +static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjIsCo(pObj) && Aig_ObjCioId(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_ObjCioId(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_ObjCioId(pObj)-Saig_ManPoNum(p)); } +static inline int Saig_ObjRegId( Aig_Man_t * p, Aig_Obj_t * pObj ) { if ( Saig_ObjIsLo(p, pObj) ) return Aig_ObjCioId(pObj)-Saig_ManPiNum(p); if ( Saig_ObjIsLi(p, pObj) ) return Aig_ObjCioId(pObj)-Saig_ManPoNum(p); else assert(0); return -1; } // iterator over the primary inputs/outputs #define Saig_ManForEachPi( p, pObj, i ) \ diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c index d7975d92..7863069f 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/aig/saig/saigAbsCba.c @@ -268,7 +268,7 @@ void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr return; if ( Aig_ObjIsCi(pObj) ) { - Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) ); + Vec_IntPush( vReasons, Aig_ObjCioId(pObj) ); return; } assert( Aig_ObjIsNode(pObj) ); @@ -460,15 +460,15 @@ Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nI pObj->pData = Aig_ManConst1(pFrames); else if ( Saig_ObjIsPi(pAig, pObj) ) { - if ( Aig_ObjPioNum(pObj) < nInputs ) + if ( Aig_ObjCioId(pObj) < nInputs ) { - int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj); + int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj); pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) ); } else { pObj->pData = Aig_ObjCreateCi( pFrames ); - Vec_IntPush( *pvMapPiF2A, Aig_ObjPioNum(pObj) ); + Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) ); Vec_IntPush( *pvMapPiF2A, f ); } } @@ -569,7 +569,7 @@ void Saig_ManCbaShrink( Saig_ManCba_t * p ) continue; pObjLi = Aig_ManObj( p->pAig, ObjId ); assert( Saig_ObjIsLi(p->pAig, pObjLi) ); - Vec_VecPushInt( p->vReg2Value, f, Abc_Var2Lit( Aig_ObjPioNum(pObjLi) - Saig_ManPoNum(p->pAig), Abc_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) ); + Vec_VecPushInt( p->vReg2Value, f, Abc_Var2Lit( Aig_ObjCioId(pObjLi) - Saig_ManPoNum(p->pAig), Abc_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) ); } } // print statistics diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c index b735f3c0..42744459 100644 --- a/src/aig/saig/saigAbsPba.c +++ b/src/aig/saig/saigAbsPba.c @@ -122,7 +122,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec pObj->pData = Aig_ObjChild0Copy(pObj); else if ( Saig_ObjIsPi(pAig, pObj) ) { - Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjPioNum(pObj), Aig_ManCiNum(pFrames) ); + Vec_IntWriteEntry( *pvPiVarMap, f * Saig_ManPiNum(pAig) + Aig_ObjCioId(pObj), Aig_ManCiNum(pFrames) ); pObj->pData = Aig_ObjCreateCi( pFrames ); } else if ( Aig_ObjIsConst1(pObj) ) @@ -144,7 +144,7 @@ Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nStart, int nFrames, Vec { if ( Saig_ObjIsLi(pAig, pObj) ) { - int iFlopNum = Aig_ObjPioNum(pObj) - Saig_ManPoNum(pAig); + int iFlopNum = Aig_ObjCioId(pObj) - Saig_ManPoNum(pAig); assert( iFlopNum >= 0 && iFlopNum < Aig_ManRegNum(pAig) ); Saig_ObjLiToLo(pAig, pObj)->pData = Aig_Mux( pFrames, Aig_ManCi(pFrames,iFlopNum), Aig_ObjCreateCi(pFrames), (Aig_Obj_t *)pObj->pData ); } diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c index d6583862..0054d8b0 100644 --- a/src/aig/saig/saigAbsStart.c +++ b/src/aig/saig/saigAbsStart.c @@ -250,7 +250,7 @@ Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars ) assert( Aig_ManRegNum(p) > 0 ); if ( pPars->fVerbose ) printf( "Performing counter-example-based refinement.\n" ); - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); vFlops = Vec_IntStartNatural( 1 ); /* iFlop = Saig_ManFindFirstFlop( p ); diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index e96d0039..b6558659 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -697,7 +697,7 @@ static inline int Saig_ManBmcSetLiteral( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int Vec_IntPush( p->vVisited, iFrame ); } else if ( iLit != ~0 && Saig_ObjIsPi(p->pAig, pObj) ) // save PI SAT var num - Vec_IntWriteEntry( p->vPiVars, iFrame*Saig_ManPiNum(p->pAig)+Aig_ObjPioNum(pObj), lit_var(iLit) ); + Vec_IntWriteEntry( p->vPiVars, iFrame*Saig_ManPiNum(p->pAig)+Aig_ObjCioId(pObj), lit_var(iLit) ); return iLit; } @@ -1051,7 +1051,7 @@ void Saig_ManBmcMarkPis( Aig_Man_t * pAig, int nPisAbstract ) if ( i < nPisAbstract ) { pObj->fMarkA = 1; -// printf( "%d=%d ", Aig_ObjPioNum(pObj), Aig_ObjRefs(pObj) ); +// printf( "%d=%d ", Aig_ObjCioId(pObj), Aig_ObjRefs(pObj) ); } } // printf( "\n" ); diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c index 466159e6..e50ba4c7 100644 --- a/src/aig/saig/saigCexMin.c +++ b/src/aig/saig/saigCexMin.c @@ -279,7 +279,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * p { 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)) ) ); + Vec_IntPush( vFramePPsOne, Abc_Var2Lit( (f+1) * pCex->nPis - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj)) ) ); else if ( f == 0 ) Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + Saig_ObjRegId(pAig, pObj), 0 ) ); else @@ -333,7 +333,7 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC { 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)) ) ); + Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj)) ) ); else if ( f == 0 ) Vec_IntPush( vFramePPsOne, Abc_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) ); else @@ -369,7 +369,7 @@ void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t if ( Aig_ObjIsCi(pObj) ) { if ( fPiReason && Saig_ObjIsPi(p, pObj) ) - Vec_IntPush( vReason, Abc_Var2Lit( Aig_ObjPioNum(pObj), !Abc_LitIsCompl(pObj->iData) ) ); + Vec_IntPush( vReason, Abc_Var2Lit( Aig_ObjCioId(pObj), !Abc_LitIsCompl(pObj->iData) ) ); else if ( !fPiReason && Saig_ObjIsLo(p, pObj) ) Vec_IntPush( vReason, Abc_Var2Lit( Saig_ObjRegId(p, pObj), !Abc_LitIsCompl(pObj->iData) ) ); return; diff --git a/src/aig/saig/saigCone.c b/src/aig/saig/saigCone.c index a6b0d864..f81a2cbc 100644 --- a/src/aig/saig/saigCone.c +++ b/src/aig/saig/saigCone.c @@ -53,7 +53,7 @@ void Saig_ManSupport_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp ) { if ( Saig_ObjIsLo(p,pObj) ) { - pObj = Saig_ManLi( p, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) ); + pObj = Saig_ManLi( p, Aig_ObjCioId(pObj)-Saig_ManPiNum(p) ); Vec_PtrPush( vSupp, pObj ); } return; @@ -111,7 +111,7 @@ void Saig_ManPrintConeOne( Aig_Man_t * p, Aig_Obj_t * pObj ) // get the current support vCur = Saig_ManSupport( p, vPrev ); Vec_PtrClear( vPrev ); - printf( " PO %3d ", Aig_ObjPioNum(pObj) ); + printf( " PO %3d ", Aig_ObjCioId(pObj) ); // continue computing supports as long as there are now nodes vTotal = Vec_PtrAlloc( 100 ); for ( s = 0; ; s++ ) @@ -167,7 +167,7 @@ void Saig_ManPrintCones( Aig_Man_t * p ) printf( "- c is the number of registers in b that are new (appear for the first time)\n" ); printf( "- d is the number of registers in b in common with the previous time-frame\n" ); printf( "- e is the number of registers in b in common with other time-frames\n" ); - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); Saig_ManForEachPo( p, pObj, i ) Saig_ManPrintConeOne( p, pObj ); } diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c index d3539abb..aedc98e2 100644 --- a/src/aig/saig/saigHaig.c +++ b/src/aig/saig/saigHaig.c @@ -109,7 +109,7 @@ Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames ) Saig_ManForEachLo( pHaig, pObj, i ) pObj->pData = Aig_ObjCreateCi( pFrames ); // add timeframes - Aig_ManSetPioNumbers( pHaig ); + Aig_ManSetCioIds( pHaig ); for ( f = 0; f < nFrames; f++ ) { // create primary inputs @@ -558,7 +558,7 @@ Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig ) Aig_Obj_t * pObj, * pObj1, * pObj2, * pMiter; int Id1, Id2, i; // remove regular POs - Aig_ManSetPioNumbers( pHaig ); + Aig_ManSetCioIds( pHaig ); vTemp = Vec_PtrAlloc( Saig_ManRegNum(pHaig) ); Aig_ManForEachCo( pHaig, pObj, i ) { diff --git a/src/aig/saig/saigInd.c b/src/aig/saig/saigInd.c index 18aebc74..aa417fb0 100644 --- a/src/aig/saig/saigInd.c +++ b/src/aig/saig/saigInd.c @@ -154,7 +154,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, int nOldSize, iReg, iLast, fAdded, nConstrs = 0, nClauses = 0; assert( fUnique == 0 || fUniqueAll == 0 ); assert( Saig_ManPoNum(p) == 1 ); - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); // start the top by including the PO vBot = Vec_PtrAlloc( 100 ); @@ -201,9 +201,9 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, pObjPiCopy = (Aig_Obj_t *)pObjPi->pData; assert( Aig_ObjIsCi(pObjPiCopy) ); if ( Saig_ObjIsPi(p, pObjPi) ) - Vec_IntWriteEntry( vTopVarIds, Aig_ObjPioNum(pObjPi) + Saig_ManRegNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] ); + Vec_IntWriteEntry( vTopVarIds, Aig_ObjCioId(pObjPi) + Saig_ManRegNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] ); else if ( Saig_ObjIsLo(p, pObjPi) ) - Vec_IntWriteEntry( vTopVarIds, Aig_ObjPioNum(pObjPi) - Saig_ManPiNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] ); + Vec_IntWriteEntry( vTopVarIds, Aig_ObjCioId(pObjPi) - Saig_ManPiNum(p), pCnfPart->pVarNums[Aig_ObjId(pObjPiCopy)] ); else assert( 0 ); } } @@ -261,7 +261,7 @@ int Saig_ManInduction( Aig_Man_t * p, int nFramesMax, int nConfMax, int fUnique, Vec_PtrPush( vTop, Saig_ObjLoToLi(p, pObjPi) ); Vec_IntPush( vTopVarNums, pCnfPart->pVarNums[pObjPiCopy->Id] ); - iReg = pObjPi->PioNum - Saig_ManPiNum(p); + iReg = pObjPi->CioId - Saig_ManPiNum(p); assert( iReg >= 0 && iReg < Aig_ManRegNum(p) ); Vec_IntWriteEntry( vState, nOldSize+iReg, pCnfPart->pVarNums[pObjPiCopy->Id] ); } diff --git a/src/aig/saig/saigIoa.c b/src/aig/saig/saigIoa.c index 9eba652d..35d7b7b2 100644 --- a/src/aig/saig/saigIoa.c +++ b/src/aig/saig/saigIoa.c @@ -49,13 +49,13 @@ char * Saig_ObjName( Aig_Man_t * p, Aig_Obj_t * pObj ) if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) ) sprintf( Buffer, "n%0*d", Abc_Base10Log(Aig_ManObjNumMax(p)), Aig_ObjId(pObj) ); else if ( Saig_ObjIsPi(p, pObj) ) - sprintf( Buffer, "pi%0*d", Abc_Base10Log(Saig_ManPiNum(p)), Aig_ObjPioNum(pObj) ); + sprintf( Buffer, "pi%0*d", Abc_Base10Log(Saig_ManPiNum(p)), Aig_ObjCioId(pObj) ); else if ( Saig_ObjIsPo(p, pObj) ) - sprintf( Buffer, "po%0*d", Abc_Base10Log(Saig_ManPoNum(p)), Aig_ObjPioNum(pObj) ); + sprintf( Buffer, "po%0*d", Abc_Base10Log(Saig_ManPoNum(p)), Aig_ObjCioId(pObj) ); else if ( Saig_ObjIsLo(p, pObj) ) - sprintf( Buffer, "lo%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPiNum(p) ); + sprintf( Buffer, "lo%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPiNum(p) ); else if ( Saig_ObjIsLi(p, pObj) ) - sprintf( Buffer, "li%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjPioNum(pObj) - Saig_ManPoNum(p) ); + sprintf( Buffer, "li%0*d", Abc_Base10Log(Saig_ManRegNum(p)), Aig_ObjCioId(pObj) - Saig_ManPoNum(p) ); else assert( 0 ); return Buffer; @@ -82,7 +82,7 @@ void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" ); return; } - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); // write input file pFile = fopen( pFileName, "w" ); if ( pFile == NULL ) diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c index d68819f3..2250126b 100644 --- a/src/aig/saig/saigIso.c +++ b/src/aig/saig/saigIso.c @@ -65,7 +65,7 @@ Vec_Int_t * Saig_ManFindIsoPermCos( Aig_Man_t * pAig, Vec_Int_t * vPermCis ) } Vec_PtrSort( vRoots, (int (*)(void))Iso_ObjCompareByData ); Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i ) - Vec_IntPush( vPermCos, Aig_ObjPioNum(pObj) ); + Vec_IntPush( vPermCos, Aig_ObjCioId(pObj) ); Vec_PtrFree( vRoots ); } // add flop outputs diff --git a/src/aig/saig/saigIsoSlow.c b/src/aig/saig/saigIsoSlow.c index e4c1dc47..3dcd7777 100644 --- a/src/aig/saig/saigIsoSlow.c +++ b/src/aig/saig/saigIsoSlow.c @@ -929,7 +929,7 @@ void Iso_ManPrintClasses( Iso_Man_t * p, int fVerbose, int fVeryVerbose ) for ( pTemp = pIso; pTemp; pTemp = Iso_ManObj(p, pTemp->iClass) ) { if ( fOnlyCis ) - printf( " %d", Aig_ObjPioNum( Iso_AigObj(p, pTemp) ) ); + printf( " %d", Aig_ObjCioId( Iso_AigObj(p, pTemp) ) ); else { Aig_Obj_t * pObj = Iso_AigObj(p, pTemp); @@ -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_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig) ) // flop + if ( Aig_ObjCioId(pObj) >= Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig) ) // flop Vec_PtrPush( p->vTemp2, pObj ); else // PI Vec_PtrPush( p->vTemp1, pObj ); @@ -1119,9 +1119,9 @@ Vec_Int_t * Iso_ManFinalize( Iso_Man_t * p ) // create the result vRes = Vec_IntAlloc( Aig_ManCiNum(p->pAig) ); Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp1, pObj, i ) - Vec_IntPush( vRes, Aig_ObjPioNum(pObj) ); + Vec_IntPush( vRes, Aig_ObjCioId(pObj) ); Vec_PtrForEachEntry( Aig_Obj_t *, p->vTemp2, pObj, i ) - Vec_IntPush( vRes, Aig_ObjPioNum(pObj) ); + Vec_IntPush( vRes, Aig_ObjCioId(pObj) ); return vRes; } diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c index 4c0e9bdf..f7832f10 100644 --- a/src/aig/saig/saigMiter.c +++ b/src/aig/saig/saigMiter.c @@ -906,7 +906,7 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 ) Aig_Obj_t * pObj, * pObj0, * pObj1, * pFlop0, * pFlop1; int i, Counter; assert( Saig_ManRegNum(p) > 0 ); - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); // check if demitering is possible vPairs = Vec_PtrAlloc( 2 * Saig_ManPoNum(p) ); Saig_ManForEachPo( p, pObj, i ) @@ -1274,14 +1274,14 @@ int Saig_ManDemiterNew( Aig_Man_t * pMan ) vSupp0 = Aig_Support( pMan, Aig_Regular(pFan0) ); Vec_PtrForEachEntry( Aig_Obj_t *, vSupp0, pTemp, k ) if ( Saig_ObjIsLo(pMan, pTemp) ) - printf( " %d", Aig_ObjPioNum(pTemp) ); + printf( " %d", Aig_ObjCioId(pTemp) ); printf( "\n" ); Vec_PtrFree( vSupp0 ); vSupp1 = Aig_Support( pMan, Aig_Regular(pFan1) ); Vec_PtrForEachEntry( Aig_Obj_t *, vSupp1, pTemp, k ) if ( Saig_ObjIsLo(pMan, pTemp) ) - printf( " %d", Aig_ObjPioNum(pTemp) ); + printf( " %d", Aig_ObjCioId(pTemp) ); printf( "\n" ); Vec_PtrFree( vSupp1 ); } diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c index f195f36c..6a351e10 100644 --- a/src/aig/saig/saigRefSat.c +++ b/src/aig/saig/saigRefSat.c @@ -124,7 +124,7 @@ void Saig_RefManFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPr Aig_ObjSetTravIdCurrent(p, pObj); if ( Aig_ObjIsCi(pObj) ) { - Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) ); + Vec_IntPush( vReasons, Aig_ObjCioId(pObj) ); return; } assert( Aig_ObjIsNode(pObj) ); @@ -316,15 +316,15 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu pObj->pData = Aig_ManConst1(pFrames); else if ( Saig_ObjIsPi(pAig, pObj) ) { - if ( Aig_ObjPioNum(pObj) < nInputs ) + if ( Aig_ObjCioId(pObj) < nInputs ) { - int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj); + int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj); pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) ); } else { pObj->pData = Aig_ObjCreateCi( pFrames ); - Vec_IntPush( *pvMapPiF2A, Aig_ObjPioNum(pObj) ); + Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) ); Vec_IntPush( *pvMapPiF2A, f ); } } diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c index e43923f8..bf31f996 100644 --- a/src/aig/saig/saigRetStep.c +++ b/src/aig/saig/saigRetStep.c @@ -37,7 +37,7 @@ ABC_NAMESPACE_IMPL_START Description [Returns the pointer to the register output after retiming.] - SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.] + SideEffects [Remember to run Aig_ManSetCioIds() in advance.] SeeAlso [] @@ -62,16 +62,16 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug // skip of they are not register outputs if ( !Saig_ObjIsLo(p, pFanin0) || !Saig_ObjIsLo(p, pFanin1) ) return NULL; - assert( Aig_ObjPioNum(pFanin0) > 0 ); - assert( Aig_ObjPioNum(pFanin1) > 0 ); + assert( Aig_ObjCioId(pFanin0) > 0 ); + assert( Aig_ObjCioId(pFanin1) > 0 ); // skip latch guns if ( !Aig_ObjIsTravIdCurrent(p, pFanin0) && !Aig_ObjIsTravIdCurrent(p, pFanin1) ) return NULL; // get the inputs of these registers - pInput0 = Saig_ManLi( p, Aig_ObjPioNum(pFanin0) - Saig_ManPiNum(p) ); - pInput1 = Saig_ManLi( p, Aig_ObjPioNum(pFanin1) - Saig_ManPiNum(p) ); + pInput0 = Saig_ManLi( p, Aig_ObjCioId(pFanin0) - Saig_ManPiNum(p) ); + pInput1 = Saig_ManLi( p, Aig_ObjCioId(pFanin1) - Saig_ManPiNum(p) ); pInput0 = Aig_ObjChild0( pInput0 ); pInput1 = Aig_ObjChild0( pInput1 ); pInput0 = Aig_NotCond( pInput0, Aig_ObjFaninC0(pObj) ); @@ -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_ManCoNum(p) - 1; + pObjLi->CioId = Aig_ManCoNum(p) - 1; // create new register output pObjLo = Aig_ObjCreateCi( p ); - pObjLo->PioNum = Aig_ManCiNum(p) - 1; + pObjLo->CioId = Aig_ManCiNum(p) - 1; p->nRegs++; // make sure the register is retimable. @@ -113,7 +113,7 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug Description [Returns the pointer to node after retiming.] - SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.] + SideEffects [Remember to run Aig_ManSetCioIds() in advance.] SeeAlso [] @@ -127,11 +127,11 @@ Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo ) int fCompl0, fCompl1; assert( Saig_ManRegNum(p) > 0 ); - assert( Aig_ObjPioNum(pObjLo) > 0 ); + assert( Aig_ObjCioId(pObjLo) > 0 ); assert( Saig_ObjIsLo(p, pObjLo) ); // get the corresponding latch input - pObjLi = Saig_ManLi( p, Aig_ObjPioNum(pObjLo) - Saig_ManPiNum(p) ); + pObjLi = Saig_ManLi( p, Aig_ObjCioId(pObjLo) - Saig_ManPiNum(p) ); // get the node pObj = Aig_ObjFanin0(pObjLi); @@ -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_ManCoNum(p) - 1; + pLi0New->CioId = Aig_ManCoNum(p) - 1; pLi1New = Aig_ObjCreateCo( p, Aig_NotCond(pFanin1, fCompl1) ); - pLi1New->PioNum = Aig_ManCoNum(p) - 1; + pLi1New->CioId = Aig_ManCoNum(p) - 1; // create latch outputs pLo0New = Aig_ObjCreateCi(p); - pLo0New->PioNum = Aig_ManCiNum(p) - 1; + pLo0New->CioId = Aig_ManCiNum(p) - 1; pLo1New = Aig_ObjCreateCi(p); - pLo1New->PioNum = Aig_ManCiNum(p) - 1; + pLo1New->CioId = Aig_ManCiNum(p) - 1; pLo0New = Aig_NotCond( pLo0New, fCompl0 ); pLo1New = Aig_NotCond( pLo1New, fCompl1 ); p->nRegs += 2; @@ -173,7 +173,7 @@ Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo ) Description [Returns the pointer to node after retiming.] - SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.] + SideEffects [Remember to run Aig_ManSetCioIds() in advance.] SeeAlso [] @@ -182,7 +182,7 @@ int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs ) { Aig_Obj_t * pObj, * pObjNew; int RetValue, s, i; - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); Aig_ManFanoutStart( p ); p->fCreatePios = 1; if ( fForward ) diff --git a/src/aig/saig/saigScl.c b/src/aig/saig/saigScl.c index 4b0a3102..d8076196 100644 --- a/src/aig/saig/saigScl.c +++ b/src/aig/saig/saigScl.c @@ -47,7 +47,7 @@ void Saig_ManReportUselessRegisters( Aig_Man_t * pAig ) Aig_Obj_t * pObj, * pDriver; int i, Counter1, Counter2; // set PIO numbers - Aig_ManSetPioNumbers( pAig ); + Aig_ManSetCioIds( pAig ); // check how many POs are driven by a register whose ref count is 1 Counter1 = 0; Saig_ManForEachPo( pAig, pObj, i ) diff --git a/src/aig/saig/saigSimExt2.c b/src/aig/saig/saigSimExt2.c index 70a8892e..f5aecc71 100644 --- a/src/aig/saig/saigSimExt2.c +++ b/src/aig/saig/saigSimExt2.c @@ -235,7 +235,7 @@ void Saig_ManExplorePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax, if ( Saig_ObjIsPi(p, pObj) ) { // propagate implications of this assignment - int i, iPiNum = Aig_ObjPioNum(pObj); + int i, iPiNum = Aig_ObjCioId(pObj); for ( i = fMax; i >= 0; i-- ) if ( i != f ) Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, iPiNum), i, fMax, vSimInfo ); diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c index a134b412..86c45f37 100644 --- a/src/aig/saig/saigSimSeq.c +++ b/src/aig/saig/saigSimSeq.c @@ -124,7 +124,7 @@ int Raig_ManCreate_rec( Raig_Man_t * p, Aig_Obj_t * pObj ) else { iFan0 = iFan1 = 0; - Vec_IntPush( p->vCis2Ids, Aig_ObjPioNum(pObj) ); + Vec_IntPush( p->vCis2Ids, Aig_ObjCioId(pObj) ); } p->pFans0[p->nObjs] = iFan0; p->pFans1[p->nObjs] = iFan1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 1d96edf1..e11dc283 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1630,7 +1630,7 @@ void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig ) } i = 0; - Aig_ManSetPioNumbers( pAig ); + Aig_ManSetCioIds( pAig ); Saig_ManForEachLo( pAig, pFlop, i ) { p_irrelevant[i] = false; @@ -1661,7 +1661,7 @@ void Abc_NtkPrintLatchEquivClasses( Abc_Ntk_t * pNtk, Aig_Man_t * pAig ) } assert( Saig_ObjIsLo( pAig, pRepr ) ); - repr_idx = Aig_ObjPioNum(pRepr) - Saig_ManPiNum(pAig); + repr_idx = Aig_ObjCioId(pRepr) - Saig_ManPiNum(pAig); pReprName = pNames[repr_idx]; Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n", pFlopName, pReprName ); // Abc_Print( 1, "Original flop # %d is proved equivalent to flop # %d.\n", i, repr_idx ); diff --git a/src/opt/cgt/cgtAig.c b/src/opt/cgt/cgtAig.c index 8d403732..047f6875 100644 --- a/src/opt/cgt/cgtAig.c +++ b/src/opt/cgt/cgtAig.c @@ -320,7 +320,7 @@ Aig_Man_t * Cgt_ManDeriveAigForGating( Cgt_Man_t * p ) } } Aig_ManCleanup( pNew ); - Aig_ManSetPioNumbers( pNew ); + Aig_ManSetCioIds( pNew ); return pNew; } @@ -375,14 +375,14 @@ void Cgt_ManConstructCare( Aig_Man_t * pNew, Aig_Man_t * pCare, Vec_Vec_t * vSup Aig_ManIncrementTravId( pCare ); Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, i ) { - pPi = Aig_ManCi( pCare, Aig_ObjPioNum(pLeaf) ); + pPi = Aig_ManCi( pCare, Aig_ObjCioId(pLeaf) ); Aig_ObjSetTravIdCurrent( pCare, pPi ); pPi->pData = pLeaf->pData; } // construct the constraints Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, i ) { - vOuts = Vec_VecEntryInt( vSuppsInv, Aig_ObjPioNum(pLeaf) ); + vOuts = Vec_VecEntryInt( vSuppsInv, Aig_ObjCioId(pLeaf) ); Vec_IntForEachEntry( vOuts, iOut, k ) { pPo = Aig_ManCo( pCare, iOut ); diff --git a/src/opt/cgt/cgtDecide.c b/src/opt/cgt/cgtDecide.c index 3370498e..c5b49bbc 100644 --- a/src/opt/cgt/cgtDecide.c +++ b/src/opt/cgt/cgtDecide.c @@ -103,7 +103,7 @@ int Cgt_ManCheckGateComplete( Aig_Man_t * pAig, Vec_Vec_t * vGatesAll, Aig_Obj_t { if ( Saig_ObjIsPo(pAig, pObj) ) return 0; - vGates = Vec_VecEntry( vGatesAll, Aig_ObjPioNum(pObj) - Saig_ManPoNum(pAig) ); + vGates = Vec_VecEntry( vGatesAll, Aig_ObjCioId(pObj) - Saig_ManPoNum(pAig) ); if ( Vec_PtrFind( vGates, pGate ) == -1 ) return 0; } diff --git a/src/opt/cgt/cgtMan.c b/src/opt/cgt/cgtMan.c index 2ba5baae..68a15381 100644 --- a/src/opt/cgt/cgtMan.c +++ b/src/opt/cgt/cgtMan.c @@ -48,7 +48,7 @@ Cgt_Man_t * Cgt_ManCreate( Aig_Man_t * pAig, Aig_Man_t * pCare, Cgt_Par_t * pPar // prepare the sequential AIG assert( Saig_ManRegNum(pAig) > 0 ); Aig_ManFanoutStart( pAig ); - Aig_ManSetPioNumbers( pAig ); + Aig_ManSetCioIds( pAig ); // create interpolation manager p = ABC_ALLOC( Cgt_Man_t, 1 ); memset( p, 0, sizeof(Cgt_Man_t) ); diff --git a/src/opt/dar/darBalance.c b/src/opt/dar/darBalance.c index 558316a6..a1afd2ad 100644 --- a/src/opt/dar/darBalance.c +++ b/src/opt/dar/darBalance.c @@ -495,7 +495,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) { float arrTime; Tim_ManIncrementTravId( (Tim_Man_t *)p->pManTime ); - Aig_ManSetPioNumbers( p ); + Aig_ManSetCioIds( p ); Aig_ManForEachObj( p, pObj, i ) { if ( Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) ) @@ -507,7 +507,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) pObj->pData = pObjNew; pObjNew->pHaig = pObj->pHaig; // set the arrival time of the new PI - arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj) ); + arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) ); pObjNew->Level = (int)arrTime; } else if ( Aig_ObjIsCo(pObj) ) @@ -518,7 +518,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) ); // save arrival time of the output arrTime = (float)Aig_Regular(pObjNew)->Level; - Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjPioNum(pObj), arrTime ); + Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj), arrTime ); // create PO pObjNew = Aig_ObjCreateCo( pNew, pObjNew ); pObjNew->pHaig = pObj->pHaig; @@ -526,7 +526,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) else assert( 0 ); } - Aig_ManCleanPioNumbers( p ); + Aig_ManCleanCioIds( p ); pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 ); } else diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c index eda4d7cf..1cce1a90 100644 --- a/src/proof/bbr/bbrReach.c +++ b/src/proof/bbr/bbrReach.c @@ -563,7 +563,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars ) vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) ); Saig_ManForEachPi( pInit, pObj, i ) if ( pObj->pData != NULL ) - Vec_IntPush( vInputMap, Aig_ObjPioNum((Aig_Obj_t *)pObj->pData) ); + Vec_IntPush( vInputMap, Aig_ObjCioId((Aig_Obj_t *)pObj->pData) ); else Vec_IntPush( vInputMap, -1 ); // create new pattern diff --git a/src/proof/fra/fraCore.c b/src/proof/fra/fraCore.c index 2148b467..37aaa0da 100644 --- a/src/proof/fra/fraCore.c +++ b/src/proof/fra/fraCore.c @@ -81,7 +81,7 @@ int Fra_FraigMiterStatus( Aig_Man_t * p ) continue; } // check if the output is a primary input - if ( Aig_ObjIsCi(Aig_Regular(pChild)) && Aig_ObjPioNum(Aig_Regular(pChild)) < p->nTruePis ) + if ( Aig_ObjIsCi(Aig_Regular(pChild)) && Aig_ObjCioId(Aig_Regular(pChild)) < p->nTruePis ) { CountNonConst0++; continue; diff --git a/src/proof/live/liveness.c b/src/proof/live/liveness.c index e457b3f8..654e1d68 100644 --- a/src/proof/live/liveness.c +++ b/src/proof/live/liveness.c @@ -527,7 +527,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { - assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch ); } @@ -830,7 +830,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { - assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + liveLatch + fairLatch ); } @@ -2256,7 +2256,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE ) { - assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); //assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch ); } diff --git a/src/proof/live/liveness_sim.c b/src/proof/live/liveness_sim.c index b99df807..f1ad794a 100644 --- a/src/proof/live/liveness_sim.c +++ b/src/proof/live/liveness_sim.c @@ -466,7 +466,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ assert( Aig_ManCheck( pNew ) ); #ifndef DUPLICATE_CKT_DEBUG - assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); assert( Saig_ManPoNum( pNew ) == 1 ); assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) ); assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch ); diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c index a1db70d3..40ca19e5 100644 --- a/src/proof/llb/llb2Flow.c +++ b/src/proof/llb/llb2Flow.c @@ -124,9 +124,9 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp { if ( !Saig_ObjIsPi(p, pObj) ) continue; - if ( piFirst[Aig_ObjPioNum(pObj)] == -1 ) - piFirst[Aig_ObjPioNum(pObj)] = i; - piLast[Aig_ObjPioNum(pObj)] = i; + if ( piFirst[Aig_ObjCioId(pObj)] == -1 ) + piFirst[Aig_ObjCioId(pObj)] = i; + piLast[Aig_ObjCioId(pObj)] = i; } } // PIs feeding into the flops should be extended to the last frame @@ -134,7 +134,7 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp { if ( !Saig_ObjIsPi(p, Aig_ObjFanin0(pObj)) ) continue; - piLast[Aig_ObjPioNum(Aig_ObjFanin0(pObj))] = Vec_PtrSize(vMaps)-1; + piLast[Aig_ObjCioId(Aig_ObjFanin0(pObj))] = Vec_PtrSize(vMaps)-1; } // set the PI map diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c index fcad15e0..2b039c01 100644 --- a/src/proof/pdr/pdrCnf.c +++ b/src/proof/pdr/pdrCnf.c @@ -202,7 +202,7 @@ static inline int Pdr_ObjRegNum2( Pdr_Man_t * p, int k, int iSatVar ) return -1; pObj = Aig_ManObj( p->pAig, ObjId ); if ( Saig_ObjIsLi( p->pAig, pObj ) ) - return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p->pAig); + return Aig_ObjCioId(pObj)-Saig_ManPoNum(p->pAig); assert( 0 ); // should be called for register inputs only return -1; } diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 0547c308..cf4756d1 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -289,14 +289,14 @@ void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCi { if ( Saig_ObjIsPi(pAig, pObj) ) { - Lit = toLitCond( Aig_ObjPioNum(pObj), (Vec_IntEntry(vCiVals, i) == 0) ); + Lit = toLitCond( Aig_ObjCioId(pObj), (Vec_IntEntry(vCiVals, i) == 0) ); Vec_IntPush( vPiLits, Lit ); continue; } assert( Saig_ObjIsLo(pAig, pObj) ); if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) continue; - Lit = toLitCond( Aig_ObjPioNum(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) ); + Lit = toLitCond( Aig_ObjCioId(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) ); Vec_IntPush( vRes, Lit ); } if ( Vec_IntSize(vRes) == 0 ) @@ -323,10 +323,10 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals pBuff[i] = '-'; pBuff[i] = 0; Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i ) - pBuff[Aig_ObjPioNum(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0'); + pBuff[Aig_ObjCioId(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0'); if ( vCi2Rem ) Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i ) - pBuff[Aig_ObjPioNum(pObj)] = 'x'; + pBuff[Aig_ObjCioId(pObj)] = 'x'; Abc_Print( 1, "%s\n", pBuff ); ABC_FREE( pBuff ); } @@ -406,7 +406,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); { if ( !Saig_ObjIsLo( p->pAig, pObj ) ) continue; - Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig); + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) continue; Vec_IntClear( vUndo ); @@ -420,7 +420,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); { if ( !Saig_ObjIsLo( p->pAig, pObj ) ) continue; - Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig); + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) continue; Vec_IntClear( vUndo ); diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c index 9a2cffb2..a47bc9f0 100644 --- a/src/proof/pdr/pdrUtil.c +++ b/src/proof/pdr/pdrUtil.c @@ -616,11 +616,11 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd if ( Aig_ObjIsCi(pNode) ) { // if ( vSuppLits ) -// Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) ); +// Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjCioId(pNode), !Value ) ); if ( Saig_ObjIsLo(pAig, pNode) ) { -// pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), !Value ); - pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), Value ); +// pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), !Value ); + pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), Value ); pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63)); } return 1; diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c index b2920177..ff428fa1 100644 --- a/src/proof/ssw/sswBmc.c +++ b/src/proof/ssw/sswBmc.c @@ -132,7 +132,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo // start managers assert( Saig_ManRegNum(pAig) > 0 ); - Aig_ManSetPioNumbers( pAig ); + Aig_ManSetCioIds( pAig ); pSat = Ssw_SatStart( 0 ); pFrm = Ssw_FrmStart( pAig ); pFrm->pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * 3 ); diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c index f20a7b78..617bb40f 100644 --- a/src/proof/ssw/sswDyn.c +++ b/src/proof/ssw/sswDyn.c @@ -113,10 +113,10 @@ void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos if ( Aig_ObjIsCo(pObj) ) { // skip if it is a register input PO - if ( Aig_ObjPioNum(pObj) >= Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig) ) + if ( Aig_ObjCioId(pObj) >= Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig) ) return; // add the number of this constraint - Vec_IntPush( vNewPos, Aig_ObjPioNum(pObj)/2 ); + Vec_IntPush( vNewPos, Aig_ObjCioId(pObj)/2 ); return; } // visit the fanouts @@ -225,7 +225,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) } assert( !Aig_IsComplement(pObjFraig) ); assert( Aig_ObjIsCi(pObjFraig) ); - pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 ); } // set random simulation info for the second frame @@ -236,7 +236,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) pObjFraig = Ssw_ObjFrame( p, pObj, f ); assert( !Aig_IsComplement(pObjFraig) ); assert( Aig_ObjIsCi(pObjFraig) ); - pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f ); } } @@ -386,7 +386,7 @@ clk = clock(); Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) ); Saig_ManForEachPi( p->pAig, pObj, i ) Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) ); - Aig_ManSetPioNumbers( p->pFrames ); + Aig_ManSetCioIds( p->pFrames ); // label nodes corresponding to primary inputs Ssw_ManLabelPiNodes( p ); p->timeReduce += clock() - clk; diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c index ec6087f0..71f148e3 100644 --- a/src/proof/ssw/sswLcorr.c +++ b/src/proof/ssw/sswLcorr.c @@ -59,7 +59,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p ) } assert( !Aig_IsComplement(pObjFraig) ); assert( Aig_ObjIsCi(pObjFraig) ); - pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 ); } } @@ -116,7 +116,7 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand ) Value = sat_solver_var_value( p->pMSat->pSat, nVarNum ); if ( Value == 0 ) continue; - pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObj) ); Abc_InfoSetBit( pInfo, p->nPatterns ); } } @@ -260,7 +260,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) pTemp = Aig_NotCond( Ssw_ObjFrame(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase ); Ssw_ObjSetFrame( p, pObj, 0, pTemp ); } - Aig_ManSetPioNumbers( p->pFrames ); + Aig_ManSetCioIds( p->pFrames ); // prepare simulation info assert( p->vSimInfo == NULL ); diff --git a/src/proof/ssw/sswMan.c b/src/proof/ssw/sswMan.c index c635569d..e09e0904 100644 --- a/src/proof/ssw/sswMan.c +++ b/src/proof/ssw/sswMan.c @@ -48,7 +48,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) // prepare the sequential AIG assert( Saig_ManRegNum(pAig) > 0 ); Aig_ManFanoutStart( pAig ); - Aig_ManSetPioNumbers( pAig ); + Aig_ManSetCioIds( pAig ); // create interpolation manager p = ABC_ALLOC( Ssw_Man_t, 1 ); memset( p, 0, sizeof(Ssw_Man_t) ); diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c index 550cb4ce..5dd7a1f2 100644 --- a/src/proof/ssw/sswSweep.c +++ b/src/proof/ssw/sswSweep.c @@ -167,7 +167,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p ) assert( nVarNum > 0 ); if ( sat_solver_var_value( p->pMSat->pSat, nVarNum ) ) { - pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) ); + pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObj) ); Abc_InfoSetBit( pInfo, p->nPatterns ); } } diff --git a/src/proof/ssw/sswUnique.c b/src/proof/ssw/sswUnique.c index 8e989531..1bd44a03 100644 --- a/src/proof/ssw/sswUnique.c +++ b/src/proof/ssw/sswUnique.c @@ -108,9 +108,9 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV assert( Aig_ObjIsCi(pTemp) ); if ( !Saig_ObjIsLo(p->pAig, pTemp) ) continue; - assert( Aig_ObjPioNum(pTemp) > 0 ); + assert( Aig_ObjCioId(pTemp) > 0 ); Vec_PtrWriteEntry( p->vCommon, k++, pTemp ); - if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjPioNum(pTemp) - Saig_ManPiNum(p->pAig)) ) + if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjCioId(pTemp) - Saig_ManPiNum(p->pAig)) ) fFeasible = 1; } Vec_PtrShrink( p->vCommon, k ); |