diff options
Diffstat (limited to 'src/proof')
72 files changed, 409 insertions, 409 deletions
diff --git a/src/proof/bbr/bbrNtbdd.c b/src/proof/bbr/bbrNtbdd.c index 49c2873b..f61c3d73 100644 --- a/src/proof/bbr/bbrNtbdd.c +++ b/src/proof/bbr/bbrNtbdd.c @@ -135,7 +135,7 @@ int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p ) Aig_Obj_t * pObj; int RetValue, i; // complement the global functions - vFuncsGlob = Vec_PtrAlloc( Aig_ManPoNum(p) ); + vFuncsGlob = Vec_PtrAlloc( Aig_ManCoNum(p) ); Aig_ManForEachCo( p, pObj, i ) Vec_PtrPush( vFuncsGlob, Aig_ObjGlobalBdd(pObj) ); RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) ); @@ -162,7 +162,7 @@ DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropI DdNode * bFunc; int i, Counter; // start the manager - dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + dd = Cudd_Init( Aig_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); // set reordering if ( fReorder ) Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c index 1b5c3984..eda4d7cf 100644 --- a/src/proof/bbr/bbrReach.c +++ b/src/proof/bbr/bbrReach.c @@ -548,7 +548,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars ) return Aig_ManVerifyUsingBdds_int( pInit, pPars ); // create new AIG p = Aig_ManDupTrim( pInit ); - assert( Aig_ManPiNum(p) < Aig_ManPiNum(pInit) ); + assert( Aig_ManCiNum(p) < Aig_ManCiNum(pInit) ); assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) ); RetValue = Aig_ManVerifyUsingBdds_int( p, pPars ); if ( RetValue != 0 ) diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c index 22474042..aa36a28e 100644 --- a/src/proof/cec/cecCec.c +++ b/src/proof/cec/cecCec.c @@ -97,7 +97,7 @@ Abc_PrintTime( 1, "Time", clock() - clkTotal ); Abc_Print( 1, "Counter-example verification has failed.\n" ); else { -// Aig_Obj_t * pObj = Aig_ManPo(pMiterCec, iOut); +// Aig_Obj_t * pObj = Aig_ManCo(pMiterCec, iOut); // Aig_Obj_t * pFan = Aig_ObjFanin0(pObj); Abc_Print( 1, "Primary output %d has failed", iOut ); if ( nOuts-1 >= 0 ) diff --git a/src/proof/dch/dchAig.c b/src/proof/dch/dchAig.c index 59828443..1b6f1539 100644 --- a/src/proof/dch/dchAig.c +++ b/src/proof/dch/dchAig.c @@ -73,8 +73,8 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ) pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 0 ); Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, i ) { - assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) ); - assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) ); + assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pAig2) ); + assert( Aig_ManCoNum(pAig) == Aig_ManCoNum(pAig2) ); nNodes += Aig_ManNodeNum(pAig2); Aig_ManCleanData( pAig2 ); } @@ -87,14 +87,14 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ) { pObjPi = Aig_ObjCreateCi( pAigTotal ); Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k ) - Aig_ManPi( pAig2, i )->pData = pObjPi; + Aig_ManCi( pAig2, i )->pData = pObjPi; } // construct the AIG in the order of POs Aig_ManForEachCo( pAig, pObj, i ) { Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pAig2, k ) { - pObjPo = Aig_ManPo( pAig2, i ); + pObjPo = Aig_ManCo( pAig2, i ); Dch_DeriveTotalAig_rec( pAigTotal, Aig_ObjFanin0(pObjPo) ); } Aig_ObjCreateCo( pAigTotal, Aig_ObjChild0Copy(pObj) ); diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c index 1de11509..7a763d84 100644 --- a/src/proof/dch/dchChoice.c +++ b/src/proof/dch/dchChoice.c @@ -117,7 +117,7 @@ int Dch_ObjCheckTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) // check the trivial cases if ( pObj == NULL ) return 0; - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) return 0; if ( pObj->fMarkA ) return 1; @@ -289,7 +289,7 @@ int Aig_ManCheckAcyclic_rec( Aig_Man_t * p, Aig_Obj_t * pNode, int fVerbose ) { Aig_Obj_t * pFanin; int fAcyclic; - if ( Aig_ObjIsPi(pNode) || Aig_ObjIsConst1(pNode) ) + if ( Aig_ObjIsCi(pNode) || Aig_ObjIsConst1(pNode) ) return 1; assert( Aig_ObjIsNode(pNode) ); // make sure the node is not visited diff --git a/src/proof/dch/dchClass.c b/src/proof/dch/dchClass.c index 24476309..1f974236 100644 --- a/src/proof/dch/dchClass.c +++ b/src/proof/dch/dchClass.c @@ -350,12 +350,12 @@ void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs ) { if ( fLatchCorr ) { - if ( !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsCi(pObj) ) continue; } else { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; // skip the node with more that the given number of levels if ( nMaxLevs && (int)pObj->Level >= nMaxLevs ) @@ -400,7 +400,7 @@ void Dch_ClassesPrepare( Dch_Cla_t * p, int fLatchCorr, int nMaxLevs ) nEntries2 = 0; Aig_ManForEachObj( p->pAig, pObj, i ) { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; nNodes = p->pClassSizes[pObj->Id]; // skip the nodes that are not representatives of non-trivial classes diff --git a/src/proof/dch/dchCnf.c b/src/proof/dch/dchCnf.c index 4175a123..b65b096c 100644 --- a/src/proof/dch/dchCnf.c +++ b/src/proof/dch/dchCnf.c @@ -217,7 +217,7 @@ void Dch_AddClausesSuper( Dch_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) void Dch_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) { // if the new node is complemented or a PI, another gate begins - if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || + if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || (fUseMuxes && Aig_ObjIsMuxType(pObj)) ) { @@ -243,7 +243,7 @@ void Dch_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int void Dch_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) { assert( !Aig_IsComplement(pObj) ); - assert( !Aig_ObjIsPi(pObj) ); + assert( !Aig_ObjIsCi(pObj) ); Vec_PtrClear( vSuper ); Dch_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); } diff --git a/src/proof/dch/dchSimSat.c b/src/proof/dch/dchSimSat.c index 808e754a..6f69b47e 100644 --- a/src/proof/dch/dchSimSat.c +++ b/src/proof/dch/dchSimSat.c @@ -113,7 +113,7 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) ) return; Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { Aig_Obj_t * pObjFraig; int nVarNum; @@ -151,7 +151,7 @@ void Dch_ManResimulateOther_rec( Dch_Man_t * p, Aig_Obj_t * pObj ) if ( Aig_ObjIsTravIdCurrent(p->pAigTotal, pObj) ) return; Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { // set random value pObj->fMarkB = Aig_ManRandom(0) & 1; diff --git a/src/proof/fra/fraBmc.c b/src/proof/fra/fraBmc.c index b0dd3c86..2ddecf48 100644 --- a/src/proof/fra/fraBmc.c +++ b/src/proof/fra/fraBmc.c @@ -395,10 +395,10 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew if ( fVerbose ) { printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", - Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), Aig_ManRegNum(pAig), + Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), Aig_ManRegNum(pAig), Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); printf( "Time-frames (%d): PI/PO = %d/%d. Node = %6d. Lev = %5d. ", - nFrames, Aig_ManPiNum(pBmc->pAigFrames), Aig_ManPoNum(pBmc->pAigFrames), + nFrames, Aig_ManCiNum(pBmc->pAigFrames), Aig_ManCoNum(pBmc->pAigFrames), Aig_ManNodeNum(pBmc->pAigFrames), Aig_ManLevelNum(pBmc->pAigFrames) ); ABC_PRT( "Time", clock() - clk ); } @@ -417,7 +417,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew clk = clock(); iOutput = Fra_FraigMiterAssertedOutput( pBmc->pAigFrames ); if ( iOutput >= 0 ) - pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput ); + pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput ); else { pBmc->pAigFraig = Fra_FraigEquivence( pBmc->pAigFrames, nBTLimit, 1 ); @@ -428,7 +428,7 @@ void Fra_BmcPerformSimple( Aig_Man_t * pAig, int nFrames, int nBTLimit, int fRew ABC_FREE( pBmc->pAigFraig->pData ); } else if ( iOutput >= 0 ) - pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig), iOutput ); + pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig), Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig), iOutput ); } if ( fVerbose ) { diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c index ac11b0bb..0acca245 100644 --- a/src/proof/fra/fraCec.c +++ b/src/proof/fra/fraCec.c @@ -60,8 +60,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi pMan->pData = NULL; // derive CNF - pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); - // pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); + pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) ); + // pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) ); if ( fFlipBits ) Cnf_DataTranformPolarity( pCnf, 0 ); @@ -166,8 +166,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi pMan->pData = NULL; // derive CNF - pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) ); - // pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) ); + pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) ); + // pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) ); if ( fFlipBits ) Cnf_DataTranformPolarity( pCnf, 0 ); @@ -293,8 +293,8 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose ) // assert( RetValue == -1 ); if ( RetValue == 0 ) { - pAig->pData = ABC_ALLOC( int, Aig_ManPiNum(pAig) ); - memset( pAig->pData, 0, sizeof(int) * Aig_ManPiNum(pAig) ); + pAig->pData = ABC_ALLOC( int, Aig_ManCiNum(pAig) ); + memset( pAig->pData, 0, sizeof(int) * Aig_ManCiNum(pAig) ); return RetValue; } @@ -406,7 +406,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimi if ( fVerbose ) { printf( "Verifying part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", - i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAig), Aig_ManPoNum(pAig), + i+1, Vec_PtrSize(vParts), Aig_ManCiNum(pAig), Aig_ManCoNum(pAig), Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); fflush( stdout ); } @@ -459,18 +459,18 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose ); int RetValue, clkTotal = clock(); - if ( Aig_ManPiNum(pMan1) != Aig_ManPiNum(pMan1) ) + if ( Aig_ManCiNum(pMan1) != Aig_ManCiNum(pMan1) ) { printf( "Abc_CommandAbc8Cec(): Miters have different number of PIs.\n" ); return 0; } - if ( Aig_ManPoNum(pMan1) != Aig_ManPoNum(pMan1) ) + if ( Aig_ManCoNum(pMan1) != Aig_ManCoNum(pMan1) ) { printf( "Abc_CommandAbc8Cec(): Miters have different number of POs.\n" ); return 0; } - assert( Aig_ManPiNum(pMan1) == Aig_ManPiNum(pMan1) ); - assert( Aig_ManPoNum(pMan1) == Aig_ManPoNum(pMan1) ); + assert( Aig_ManCiNum(pMan1) == Aig_ManCiNum(pMan1) ); + assert( Aig_ManCoNum(pMan1) == Aig_ManCoNum(pMan1) ); // make sure that the first miter has more nodes if ( Aig_ManNodeNum(pMan1) < Aig_ManNodeNum(pMan2) ) @@ -484,7 +484,7 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n if ( nPartSize ) RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, nPartSize, fSmart, fVerbose ); else // no partitioning - RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManPoNum(pMan1), 0, fVerbose ); + RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManCoNum(pMan1), 0, fVerbose ); // report the miter if ( RetValue == 1 ) diff --git a/src/proof/fra/fraClass.c b/src/proof/fra/fraClass.c index f7850241..cef2f673 100644 --- a/src/proof/fra/fraClass.c +++ b/src/proof/fra/fraClass.c @@ -291,12 +291,12 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs ) { if ( fLatchCorr ) { - if ( !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsCi(pObj) ) continue; } else { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; // skip the node with more that the given number of levels if ( nMaxLevs && (int)pObj->Level > nMaxLevs ) @@ -349,7 +349,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs ) nEntries = 0; Aig_ManForEachObj( p->pAig, pObj, i ) { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; // skip the nodes that are not representatives of non-trivial classes if ( pObj->fMarkA == 0 ) @@ -800,7 +800,7 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ) Aig_Obj_t ** pLatches, ** ppEquivs; int i, k, f, nFramesAll = nFramesK + 1; assert( Aig_ManRegNum(p->pAig) > 0 ); - assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) ); assert( nFramesK > 0 ); // start the fraig package pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll ); @@ -832,7 +832,7 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ) if ( f == nFramesAll - 1 ) break; if ( f == nFramesAll - 2 ) - pManFraig->nAsserts = Aig_ManPoNum(pManFraig); + pManFraig->nAsserts = Aig_ManCoNum(pManFraig); // save the latch input values k = 0; Aig_ManForEachLiSeq( p->pAig, pObj, i ) @@ -845,9 +845,9 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ) ABC_FREE( pLatches ); ABC_FREE( ppEquivs ); // mark the asserts - assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 ); + assert( Aig_ManCoNum(pManFraig) % nFramesAll == 0 ); printf( "Assert miters = %6d. Output miters = %6d.\n", - pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts ); + pManFraig->nAsserts, Aig_ManCoNum(pManFraig) - pManFraig->nAsserts ); // remove dangling nodes Aig_ManCleanup( pManFraig ); return pManFraig; diff --git a/src/proof/fra/fraClau.c b/src/proof/fra/fraClau.c index 28e9e9b9..6c692afa 100644 --- a/src/proof/fra/fraClau.c +++ b/src/proof/fra/fraClau.c @@ -108,7 +108,7 @@ Vec_Int_t * Fra_ClauSaveOutputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf ) Vec_Int_t * vVars; Aig_Obj_t * pObj; int i; - vVars = Vec_IntAlloc( Aig_ManPoNum(pMan) ); + vVars = Vec_IntAlloc( Aig_ManCoNum(pMan) ); Aig_ManForEachCo( pMan, pObj, i ) Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] ); return vVars; @@ -130,7 +130,7 @@ Vec_Int_t * Fra_ClauSaveInputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int nStar Vec_Int_t * vVars; Aig_Obj_t * pObj; int i; - vVars = Vec_IntAlloc( Aig_ManPiNum(pMan) - nStarting ); + vVars = Vec_IntAlloc( Aig_ManCiNum(pMan) - nStarting ); Aig_ManForEachCi( pMan, pObj, i ) { if ( i < nStarting ) @@ -217,7 +217,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) Aig_Man_t * pFramesMain; Aig_Man_t * pFramesTest; Aig_Man_t * pFramesBmc; - assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 ); + assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 ); // start the manager p = ABC_ALLOC( Cla_Man_t, 1 ); @@ -232,8 +232,8 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) // derive two timeframes to be checked pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, 0, NULL ); // nFrames, fInit, fOuts, fRegs //Aig_ManShow( pFramesMain, 0, NULL ); - assert( Aig_ManPoNum(pFramesMain) == 2 ); - Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output + assert( Aig_ManCoNum(pFramesMain) == 2 ); + Aig_ObjChild0Flip( Aig_ManCo(pFramesMain, 0) ); // complement the first output pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 ); //Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 ); p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 ); @@ -249,7 +249,7 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) // derive one timeframe to be checked pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL ); - assert( Aig_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) ); + assert( Aig_ManCoNum(pFramesTest) == Aig_ManRegNum(pMan) ); pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) ); p->pSatTest = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 ); p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest ); @@ -257,12 +257,12 @@ Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan ) // derive one timeframe to be checked for BMC pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, 0, NULL ); //Aig_ManShow( pFramesBmc, 0, NULL ); - assert( Aig_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) ); + assert( Aig_ManCoNum(pFramesBmc) == Aig_ManRegNum(pMan) ); pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) ); p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 ); // create variable sets - p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(pMan)-Aig_ManRegNum(pMan)) ); + p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManCiNum(pMan)-Aig_ManRegNum(pMan)) ); p->vSatVarsTestCs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 1 ); p->vSatVarsTestNs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 0 ); p->vSatVarsBmcNs = Fra_ClauSaveOutputVars( pFramesBmc, pCnfBmc ); @@ -638,7 +638,7 @@ int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose ) { Cla_Man_t * p; int Iter, RetValue, fFailed, i; - assert( Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 ); + assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 ); // create the manager p = Fra_ClauStart( pMan ); if ( p == NULL ) diff --git a/src/proof/fra/fraClaus.c b/src/proof/fra/fraClaus.c index f27c63ce..571cc510 100644 --- a/src/proof/fra/fraClaus.c +++ b/src/proof/fra/fraClaus.c @@ -97,7 +97,7 @@ int Fra_ClausRunBmc( Clu_Man_t * p ) int Lits[2], nLitsTot, RetValue, i; // set the output literals nLitsTot = 2 * p->pCnf->nVars; - pObj = Aig_ManPo(p->pAig, 0); + pObj = Aig_ManCo(p->pAig, 0); for ( i = 0; i < p->nPref + p->nFrames; i++ ) { Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); @@ -126,7 +126,7 @@ int Fra_ClausRunSat( Clu_Man_t * p ) int i, RetValue; pLits = ABC_ALLOC( int, p->nFrames + 1 ); // set the output literals - pObj = Aig_ManPo(p->pAig, 0); + pObj = Aig_ManCo(p->pAig, 0); for ( i = 0; i <= p->nFrames; i++ ) pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames ); // try to solve the problem @@ -154,7 +154,7 @@ int Fra_ClausRunSat0( Clu_Man_t * p ) { Aig_Obj_t * pObj; int Lits[2], RetValue; - pObj = Aig_ManPo(p->pAig, 0); + pObj = Aig_ManCo(p->pAig, 0); Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 ); RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); if ( RetValue == l_False ) @@ -523,7 +523,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq ) { Aig_Obj_t * pObj; int Lits[1]; - pObj = Aig_ManPo( p->pAig, 0 ); + pObj = Aig_ManCo( p->pAig, 0 ); Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 1 ); Vec_IntPush( p->vLits, Lits[0] ); Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) ); @@ -1242,7 +1242,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p ) Aig_Obj_t * pObj; int Lits[2]; // set the output literals - pObj = Aig_ManPo(p->pAig, 0); + pObj = Aig_ManCo(p->pAig, 0); Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 1 ); // add the clause RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 ); @@ -1637,9 +1637,9 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p ) pVar2Id[ p->pCnf->pVarNums[i] ] = i; } // get storage for one assignment and all assignments - assert( Aig_ManPoNum(p->pAig) > 2 ); - pResultOne = Fra_ObjSim( pComb, Aig_ManPo(p->pAig, 0)->Id ); - pResultTot = Fra_ObjSim( pComb, Aig_ManPo(p->pAig, 1)->Id ); + assert( Aig_ManCoNum(p->pAig) > 2 ); + pResultOne = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 0)->Id ); + pResultTot = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 1)->Id ); // start the OR of don't-cares for ( w = 0; w < nCombSimWords; w++ ) pResultTot[w] = 0; @@ -1693,13 +1693,13 @@ if ( p->fVerbose ) //ABC_PRT( "Sim-seq", clock() - clk ); } - assert( !p->fTarget || Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 ); + assert( !p->fTarget || Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig) == 1 ); clk = clock(); // derive CNF // if ( p->fTarget ) // p->pAig->nRegs++; - p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManPoNum(p->pAig) ); + p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManCoNum(p->pAig) ); // if ( p->fTarget ) // p->pAig->nRegs--; if ( fVerbose ) @@ -1846,8 +1846,8 @@ clk = clock(); assert( p->nBatches == 1 ); pTable = fopen( "stats.txt", "a+" ); fprintf( pTable, "%s ", pAig->pName ); - fprintf( pTable, "%d ", Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig) ); - fprintf( pTable, "%d ", Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig) ); + fprintf( pTable, "%d ", Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig) ); + fprintf( pTable, "%d ", Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig) ); fprintf( pTable, "%d ", Aig_ManRegNum(pAig) ); fprintf( pTable, "%d ", Aig_ManNodeNum(pAig) ); fprintf( pTable, "%d ", p->nCuts ); diff --git a/src/proof/fra/fraCnf.c b/src/proof/fra/fraCnf.c index 5021e750..7024c0f4 100644 --- a/src/proof/fra/fraCnf.c +++ b/src/proof/fra/fraCnf.c @@ -167,7 +167,7 @@ void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) void Fra_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) { // if the new node is complemented or a PI, another gate begins - if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || + if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || (fUseMuxes && Aig_ObjIsMuxType(pObj)) ) { Vec_PtrPushUnique( vSuper, pObj ); @@ -193,7 +193,7 @@ Vec_Ptr_t * Fra_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes ) { Vec_Ptr_t * vSuper; assert( !Aig_IsComplement(pObj) ); - assert( !Aig_ObjIsPi(pObj) ); + assert( !Aig_ObjIsCi(pObj) ); vSuper = Vec_PtrAlloc( 4 ); Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); return vSuper; diff --git a/src/proof/fra/fraCore.c b/src/proof/fra/fraCore.c index 1969b36d..2148b467 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_ObjIsPi(Aig_Regular(pChild)) && Aig_ObjPioNum(Aig_Regular(pChild)) < p->nTruePis ) + if ( Aig_ObjIsCi(Aig_Regular(pChild)) && Aig_ObjPioNum(Aig_Regular(pChild)) < p->nTruePis ) { CountNonConst0++; continue; @@ -97,7 +97,7 @@ int Fra_FraigMiterStatus( Aig_Man_t * p ) /* if ( p->pParams->fVerbose ) { - printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) ); + printf( "Miter has %d outputs. ", Aig_ManCoNum(p->pManAig) ); printf( "Const0 = %d. ", CountConst0 ); printf( "NonConst0 = %d. ", CountNonConst0 ); printf( "Undecided = %d. ", CountUndecided ); @@ -187,7 +187,7 @@ void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex ) { Aig_Obj_t * pObj, ** ppClass; int i, c; - assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) ); + assert( Aig_ManCiNum(p->pManAig) == Vec_IntSize(vCex) ); // make sure the input pattern is not used Aig_ManForEachObj( p->pManAig, pObj, i ) assert( !pObj->fMarkB ); diff --git a/src/proof/fra/fraHot.c b/src/proof/fra/fraHot.c index 03dd468a..338b5717 100644 --- a/src/proof/fra/fraHot.c +++ b/src/proof/fra/fraHot.c @@ -137,7 +137,7 @@ Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim ) Vec_Int_t * vOneHots; Aig_Obj_t * pObj1, * pObj2; int i, k; - int nTruePis = Aig_ManPiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig); + int nTruePis = Aig_ManCiNum(pSim->pAig) - Aig_ManRegNum(pSim->pAig); assert( pSim->pAig == p->pManAig ); vOneHots = Vec_IntAlloc( 100 ); Aig_ManForEachLoSeq( pSim->pAig, pObj1, i ) @@ -146,8 +146,8 @@ Vec_Int_t * Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim ) continue; assert( i-nTruePis >= 0 ); // Aig_ManForEachLoSeq( pSim->pAig, pObj2, k ) -// Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManPiNum(p)-Aig_ManRegNum(p) ) - Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, i+1 ) +// Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vPis, pObj2, k, Aig_ManCiNum(p)-Aig_ManRegNum(p) ) + Vec_PtrForEachEntryStart( Aig_Obj_t *, pSim->pAig->vCis, pObj2, k, i+1 ) { if ( fSkipConstEqu && Fra_OneHotNodeIsConst(pSim, pObj2) ) continue; @@ -192,7 +192,7 @@ void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots ) { Aig_Obj_t * pObj1, * pObj2; int i, Out1, Out2, pLits[2]; - int nPiNum = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); + int nPiNum = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); assert( p->pPars->nFramesK == 1 ); // add to only one frame for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 ) { @@ -200,8 +200,8 @@ void Fra_OneHotAssume( Fra_Man_t * p, Vec_Int_t * vOneHots ) Out2 = Vec_IntEntry( vOneHots, i+1 ); if ( Out1 == 0 && Out2 == 0 ) continue; - pObj1 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out1) ); - pObj2 = Aig_ManPi( p->pManFraig, nPiNum + Fra_LitReg(Out2) ); + pObj1 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out1) ); + pObj2 = Aig_ManCi( p->pManFraig, nPiNum + Fra_LitReg(Out2) ); pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), Fra_LitSign(Out1) ); pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), Fra_LitSign(Out2) ); // add constraint to solver @@ -230,15 +230,15 @@ void Fra_OneHotCheck( Fra_Man_t * p, Vec_Int_t * vOneHots ) { Aig_Obj_t * pObj1, * pObj2; int RetValue, i, Out1, Out2; - int nTruePos = Aig_ManPoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); + int nTruePos = Aig_ManCoNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 ) { Out1 = Vec_IntEntry( vOneHots, i ); Out2 = Vec_IntEntry( vOneHots, i+1 ); if ( Out1 == 0 && Out2 == 0 ) continue; - pObj1 = Aig_ManPo( p->pManFraig, nTruePos + Fra_LitReg(Out1) ); - pObj2 = Aig_ManPo( p->pManFraig, nTruePos + Fra_LitReg(Out2) ); + pObj1 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out1) ); + pObj2 = Aig_ManCo( p->pManFraig, nTruePos + Fra_LitReg(Out2) ); RetValue = Fra_NodesAreClause( p, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) ); if ( RetValue != 1 ) { @@ -267,7 +267,7 @@ int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots ) { Aig_Obj_t * pObj1, * pObj2; int i, Out1, Out2, RetValue = 0; - int nPiNum = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); + int nPiNum = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); assert( p->pSml->pAig == p->pManAig ); for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 ) { @@ -276,8 +276,8 @@ int Fra_OneHotRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vOneHots ) if ( Out1 == 0 && Out2 == 0 ) continue; // get the corresponding nodes - pObj1 = Aig_ManPi( p->pManAig, nPiNum + Fra_LitReg(Out1) ); - pObj2 = Aig_ManPi( p->pManAig, nPiNum + Fra_LitReg(Out2) ); + pObj1 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out1) ); + pObj2 = Aig_ManCi( p->pManAig, nPiNum + Fra_LitReg(Out2) ); // check if implication holds using this simulation info if ( !Fra_OneHotNodesAreClause( p->pSml, pObj1, pObj2, Fra_LitSign(Out1), Fra_LitSign(Out2) ) ) { @@ -405,22 +405,22 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots ) // Aig_ObjCreateCi(pNew); Aig_ManForEachCi( p->pManAig, pObj, i ) Aig_ObjCreateCi(pNew); - nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); + nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 ) { Out1 = Vec_IntEntry( vOneHots, i ); Out2 = Vec_IntEntry( vOneHots, i+1 ); if ( Out1 == 0 && Out2 == 0 ) continue; - pObj1 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out1) ); - pObj2 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out2) ); + pObj1 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out1) ); + pObj2 = Aig_ManCi( pNew, nTruePis + Fra_LitReg(Out2) ); pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) ); pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) ); pObj = Aig_Or( pNew, pObj1, pObj2 ); Aig_ObjCreateCo( pNew, pObj ); } Aig_ManCleanup(pNew); -// printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) ); +// printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManCoNum(pNew) ); return pNew; } @@ -450,8 +450,8 @@ void Fra_OneHotAddKnownConstraint( Fra_Man_t * p, Vec_Ptr_t * vOnehots ) Vec_IntForEachEntry( vGroup, Out1, i ) Vec_IntForEachEntryStart( vGroup, Out2, j, i+1 ) { - pObj1 = Aig_ManPi( p->pManFraig, Out1 ); - pObj2 = Aig_ManPi( p->pManFraig, Out2 ); + pObj1 = Aig_ManCi( p->pManFraig, Out1 ); + pObj2 = Aig_ManCi( p->pManFraig, Out2 ); pLits[0] = toLitCond( Fra_ObjSatNum(pObj1), 1 ); pLits[1] = toLitCond( Fra_ObjSatNum(pObj2), 1 ); // add constraint to solver diff --git a/src/proof/fra/fraImp.c b/src/proof/fra/fraImp.c index de24f179..f65aca5c 100644 --- a/src/proof/fra/fraImp.c +++ b/src/proof/fra/fraImp.c @@ -170,12 +170,12 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr ) // skip non-PI and non-internal nodes if ( fLatchCorr ) { - if ( !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsCi(pObj) ) continue; } else { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; } // skip nodes participating in the classes @@ -203,12 +203,12 @@ Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr ) // skip non-PI and non-internal nodes if ( fLatchCorr ) { - if ( !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsCi(pObj) ) continue; } else { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; } // skip nodes participating in the classes @@ -708,7 +708,7 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ) if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 ) return; // go through the implication - nPosOld = Aig_ManPoNum(pNew); + nPosOld = Aig_ManCoNum(pNew); Vec_IntForEachEntry( p->pCla->vImps, Imp, i ) { pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) ); @@ -719,7 +719,7 @@ void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew ) Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) ); Aig_ObjCreateCo( pNew, pMiter ); } - pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld; + pNew->nAsserts = Aig_ManCoNum(pNew) - nPosOld; } //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/fra/fraInd.c b/src/proof/fra/fraInd.c index b8a1e6bf..29a76eea 100644 --- a/src/proof/fra/fraInd.c +++ b/src/proof/fra/fraInd.c @@ -61,16 +61,16 @@ void Fra_FraigInductionRewrite( Fra_Man_t * p ) // transfer PI/register pointers assert( p->pManFraig->nRegs == pTemp->nRegs ); assert( p->pManFraig->nAsserts == pTemp->nAsserts ); - nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); + nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) ); Aig_ManForEachPiSeq( p->pManAig, pObj, i ) - Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManPi(pTemp,nTruePis*p->pPars->nFramesK+i) ); + Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManCi(pTemp,nTruePis*p->pPars->nFramesK+i) ); k = 0; - assert( Aig_ManRegNum(p->pManAig) == Aig_ManPoNum(pTemp) - pTemp->nAsserts ); + assert( Aig_ManRegNum(p->pManAig) == Aig_ManCoNum(pTemp) - pTemp->nAsserts ); Aig_ManForEachLoSeq( p->pManAig, pObj, i ) { - pObjPo = Aig_ManPo(pTemp, pTemp->nAsserts + k++); + pObjPo = Aig_ManCo(pTemp, pTemp->nAsserts + k++); Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) ); } // exchange @@ -133,7 +133,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) int i, k, f; assert( p->pManFraig == NULL ); assert( Aig_ManRegNum(p->pManAig) > 0 ); - assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) ); + assert( Aig_ManRegNum(p->pManAig) < Aig_ManCiNum(p->pManAig) ); // start the fraig package pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll ); @@ -170,7 +170,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) } // pManFraig->fAddStrash = 0; // mark the asserts - pManFraig->nAsserts = Aig_ManPoNum(pManFraig); + pManFraig->nAsserts = Aig_ManCoNum(pManFraig); // add the POs for the latch outputs of the last frame Aig_ManForEachLoSeq( p->pManAig, pObj, i ) Aig_ObjCreateCo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) ); @@ -291,7 +291,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL ); Ioa_WriteAiger( pTemp, Buffer, 0, 0 ); printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", - i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) ); + i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) ); Aig_ManStop( pTemp ); } } @@ -309,7 +309,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars ) nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack ); if ( fVerbose ) printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", - i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses ); + i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses ); Aig_ManStop( pNew ); Aig_ManStop( pTemp ); ABC_FREE( pMapBack ); @@ -637,8 +637,8 @@ p->timeTotal = clock() - clk; finish: Fra_ManStop( p ); // check the output -// if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 ) -// if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) ) +// if ( Aig_ManCoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 ) +// if ( Aig_ObjChild0( Aig_ManCo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) ) // printf( "Proved output constant 0.\n" ); pParams->nIters = nIter; return pManAigNew; diff --git a/src/proof/fra/fraIndVer.c b/src/proof/fra/fraIndVer.c index 64437607..7c5e9e70 100644 --- a/src/proof/fra/fraIndVer.c +++ b/src/proof/fra/fraIndVer.c @@ -59,14 +59,14 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve } // derive CNF - pCnf = Cnf_DeriveSimple( pAig, Aig_ManPoNum(pAig) ); + pCnf = Cnf_DeriveSimple( pAig, Aig_ManCoNum(pAig) ); /* // add the property { Aig_Obj_t * pObj; int Lits[1]; - pObj = Aig_ManPo( pAig, 0 ); + pObj = Aig_ManCo( pAig, 0 ); Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 1 ); Vec_IntPush( vLits, Lits[0] ); diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c index d24b37f6..8ea6d297 100644 --- a/src/proof/fra/fraLcr.c +++ b/src/proof/fra/fraLcr.c @@ -83,10 +83,10 @@ Fra_Lcr_t * Lcr_ManAlloc( Aig_Man_t * pAig ) p = ABC_ALLOC( Fra_Lcr_t, 1 ); memset( p, 0, sizeof(Fra_Lcr_t) ); p->pAig = pAig; - p->pInToOutPart = ABC_ALLOC( int, Aig_ManPiNum(pAig) ); - memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManPiNum(pAig) ); - p->pInToOutNum = ABC_ALLOC( int, Aig_ManPiNum(pAig) ); - memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManPiNum(pAig) ); + p->pInToOutPart = ABC_ALLOC( int, Aig_ManCiNum(pAig) ); + memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManCiNum(pAig) ); + p->pInToOutNum = ABC_ALLOC( int, Aig_ManCiNum(pAig) ); + memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManCiNum(pAig) ); p->vFraigs = Vec_PtrAlloc( 1000 ); return p; } @@ -205,8 +205,8 @@ int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) Aig_Man_t * pFraig; Aig_Obj_t * pOut0, * pOut1; int nPart0, nPart1; - assert( Aig_ObjIsPi(pObj0) ); - assert( Aig_ObjIsPi(pObj1) ); + assert( Aig_ObjIsCi(pObj0) ); + assert( Aig_ObjIsCi(pObj1) ); // find the partition to which these nodes belong nPart0 = pLcr->pInToOutPart[(long)pObj0->pNext]; nPart1 = pLcr->pInToOutPart[(long)pObj1->pNext]; @@ -220,8 +220,8 @@ int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 ) assert( nPart0 == nPart1 ); pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart0 ); // get the fraig outputs - pOut0 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj0->pNext] ); - pOut1 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj1->pNext] ); + pOut0 = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj0->pNext] ); + pOut1 = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj1->pNext] ); return Aig_ObjFanin0(pOut0) == Aig_ObjFanin0(pOut1); } @@ -243,12 +243,12 @@ int Fra_LcrNodeIsConst( Aig_Obj_t * pObj ) Aig_Man_t * pFraig; Aig_Obj_t * pOut; int nPart; - assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsCi(pObj) ); // find the partition to which these nodes belong nPart = pLcr->pInToOutPart[(long)pObj->pNext]; pFraig = (Aig_Man_t *)Vec_PtrEntry( pLcr->vFraigs, nPart ); // get the fraig outputs - pOut = Aig_ManPo( pFraig, pLcr->pInToOutNum[(long)pObj->pNext] ); + pOut = Aig_ManCo( pFraig, pLcr->pInToOutNum[(long)pObj->pNext] ); return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig); } @@ -306,7 +306,7 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr ) pObj->pNext = (Aig_Obj_t *)(long)i; } // compute the LO/LI offset - Offset = Aig_ManPoNum(pLcr->pAig) - Aig_ManPiNum(pLcr->pAig); + Offset = Aig_ManCoNum(pLcr->pAig) - Aig_ManCiNum(pLcr->pAig); // create the PIs Aig_ManCleanData( pLcr->pAig ); pNew = Aig_ManStartFrom( pLcr->pAig ); @@ -316,8 +316,8 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr ) pMiter = Aig_ManConst0(pNew); for ( c = 0; ppClass[c]; c++ ) { - assert( Aig_ObjIsPi(ppClass[c]) ); - pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)ppClass[c]->pNext ); + assert( Aig_ObjIsCi(ppClass[c]) ); + pObjPo = Aig_ManCo( pLcr->pAig, Offset+(long)ppClass[c]->pNext ); pObjNew = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) ); pMiter = Aig_Exor( pNew, pMiter, pObjNew ); } @@ -326,8 +326,8 @@ Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr ) // go over the constant candidates Vec_PtrForEachEntry( Aig_Obj_t *, pLcr->pCla->vClasses1, pObj, i ) { - assert( Aig_ObjIsPi(pObj) ); - pObjPo = Aig_ManPo( pLcr->pAig, Offset+(long)pObj->pNext ); + assert( Aig_ObjIsCi(pObj) ); + pObjPo = Aig_ManCo( pLcr->pAig, Offset+(long)pObj->pNext ); pMiter = Fra_LcrManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) ); Aig_ObjCreateCo( pNew, pMiter ); } @@ -351,7 +351,7 @@ void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOu Aig_Obj_t ** ppClass, * pObjPi; int Out, Offset, i, k, c; // compute the LO/LI offset - Offset = Aig_ManPoNum(pCla->pAig) - Aig_ManPiNum(pCla->pAig); + Offset = Aig_ManCoNum(pCla->pAig) - Aig_ManCiNum(pCla->pAig); Vec_PtrForEachEntry( Vec_Int_t *, vParts, vOne, i ) { vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) ); @@ -398,7 +398,7 @@ Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t if ( Aig_ObjIsTravIdCurrent(p, pObj) ) return (Aig_Obj_t *)pObj->pData; Aig_ObjSetTravIdCurrent(p, pObj); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { // Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj); Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id]; @@ -439,7 +439,7 @@ Aig_Man_t * Fra_LcrCreatePart( Fra_Lcr_t * p, Vec_Int_t * vPart ) Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew); Vec_IntForEachEntry( vPart, Out, i ) { - pObj = Aig_ManPo( p->pAig, Out ); + pObj = Aig_ManCo( p->pAig, Out ); if ( pObj->fMarkA ) { pObjNew = Fra_LcrCreatePart_rec( p->pCla, pNew, p->pAig, Aig_ObjFanin0(pObj) ); @@ -468,18 +468,18 @@ void Fra_ClassNodesMark( Fra_Lcr_t * p ) Aig_Obj_t * pObj, ** ppClass; int i, c, Offset; // compute the LO/LI offset - Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig); + Offset = Aig_ManCoNum(p->pCla->pAig) - Aig_ManCiNum(p->pCla->pAig); // mark the nodes remaining in the classes Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i ) { - pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)pObj->pNext ); + pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)pObj->pNext ); pObj->fMarkA = 1; } Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i ) { for ( c = 0; ppClass[c]; c++ ) { - pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext ); + pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext ); pObj->fMarkA = 1; } } @@ -501,18 +501,18 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p ) Aig_Obj_t * pObj, ** ppClass; int i, c, Offset; // compute the LO/LI offset - Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig); + Offset = Aig_ManCoNum(p->pCla->pAig) - Aig_ManCiNum(p->pCla->pAig); // mark the nodes remaining in the classes Vec_PtrForEachEntry( Aig_Obj_t *, p->pCla->vClasses1, pObj, i ) { - pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)pObj->pNext ); + pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)pObj->pNext ); pObj->fMarkA = 0; } Vec_PtrForEachEntry( Aig_Obj_t **, p->pCla->vClasses, ppClass, i ) { for ( c = 0; ppClass[c]; c++ ) { - pObj = Aig_ManPo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext ); + pObj = Aig_ManCo( p->pCla->pAig, Offset+(long)ppClass[c]->pNext ); pObj->fMarkA = 0; } } diff --git a/src/proof/fra/fraMan.c b/src/proof/fra/fraMan.c index 67832f83..5ffbc778 100644 --- a/src/proof/fra/fraMan.c +++ b/src/proof/fra/fraMan.c @@ -114,7 +114,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) p->nSizeAlloc = Aig_ManObjNumMax( pManAig ); p->nFramesAll = pPars->nFramesK + 1; // allocate storage for sim pattern - p->nPatWords = Abc_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) ); + p->nPatWords = Abc_BitWordNum( (Aig_ManCiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) ); p->pPatWords = ABC_ALLOC( unsigned, p->nPatWords ); p->vPiVars = Vec_PtrAlloc( 100 ); // equivalence classes diff --git a/src/proof/fra/fraPart.c b/src/proof/fra/fraPart.c index 6594ac0b..e3bb2850 100644 --- a/src/proof/fra/fraPart.c +++ b/src/proof/fra/fraPart.c @@ -74,7 +74,7 @@ ABC_PRT( "Supports", clock() - clk ); // create reverse supports clk = clock(); - vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) ); + vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) ); Aig_ManForEachCo( p, pObj, i ) { vSup = Vec_VecEntryInt( vSupps, i ); @@ -86,10 +86,10 @@ ABC_PRT( "Inverse ", clock() - clk ); clk = clock(); // compute extended supports Largest = 0; - vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) ); - vOverNew = Vec_IntAlloc( Aig_ManPoNum(p) ); - vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) ); -// pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) ); + vSuppsNew = Vec_PtrAlloc( Aig_ManCoNum(p) ); + vOverNew = Vec_IntAlloc( Aig_ManCoNum(p) ); + vQuantNew = Vec_IntAlloc( Aig_ManCoNum(p) ); +// pProgress = Bar_ProgressStart( stdout, Aig_ManCoNum(p) ); Aig_ManForEachCo( p, pObj, i ) { // Bar_ProgressUpdate( pProgress, i, NULL ); @@ -160,9 +160,9 @@ ABC_PRT( "Scanning", clock() - clk ); // print cumulative statistics printf( "PIs = %6d. POs = %6d. Lim = %3d. AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n", - Aig_ManPiNum(p), Aig_ManPoNum(p), nComLim, - nTotalSupp/Aig_ManPoNum(p), nTotalSupp2/Aig_ManPoNum(p), - Ratio/Aig_ManPoNum(p), Largest ); + Aig_ManCiNum(p), Aig_ManCoNum(p), nComLim, + nTotalSupp/Aig_ManCoNum(p), nTotalSupp2/Aig_ManCoNum(p), + Ratio/Aig_ManCoNum(p), Largest ); Vec_VecFree( vSupps ); Vec_VecFree( vSuppsIn ); @@ -208,7 +208,7 @@ ABC_PRT( "Supports", clock() - clk ); // create reverse supports clk = clock(); - vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) ); + vSuppsIn = Vec_VecStart( Aig_ManCiNum(p) ); Aig_ManForEachCo( p, pObj, i ) { if ( i == p->nAsserts ) @@ -221,13 +221,13 @@ ABC_PRT( "Inverse ", clock() - clk ); // create affective supports clk = clock(); - pSupp = ABC_ALLOC( char, Aig_ManPiNum(p) ); + pSupp = ABC_ALLOC( char, Aig_ManCiNum(p) ); Aig_ManForEachCo( p, pObj, i ) { if ( i % 50 != 0 ) continue; vSup = Vec_VecEntryInt( vSupps, i ); - memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) ); + memset( pSupp, 0, sizeof(char) * Aig_ManCiNum(p) ); // go through each input of this output Vec_IntForEachEntry( vSup, Entry, k ) { @@ -246,7 +246,7 @@ clk = clock(); } // count the entries Counter = 0; - for ( m = 0; m < Aig_ManPiNum(p); m++ ) + for ( m = 0; m < Aig_ManCiNum(p); m++ ) Counter += pSupp[m]; printf( "%d(%d) ", Vec_IntSize(vSup), Counter ); } diff --git a/src/proof/fra/fraSat.c b/src/proof/fra/fraSat.c index 38702d5e..2702113c 100644 --- a/src/proof/fra/fraSat.c +++ b/src/proof/fra/fraSat.c @@ -507,7 +507,7 @@ int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, i return 0; Aig_ObjSetTravIdCurrent(p->pManFraig, pObj); // add the PI to the list - if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsPi(pObj) ) + if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsCi(pObj) ) return 0; // set the factor of this variable // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump diff --git a/src/proof/fra/fraSec.c b/src/proof/fra/fraSec.c index 8067b8c2..cde56809 100644 --- a/src/proof/fra/fraSec.c +++ b/src/proof/fra/fraSec.c @@ -142,8 +142,8 @@ clk = clock(); if ( pParSec->fPhaseAbstract ) { extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose ); - pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); - pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 ); Aig_ManStop( pTemp ); if ( pParSec->fVerbose ) @@ -301,8 +301,8 @@ ABC_PRT( "Time", clock() - clk ); { // extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); clk = clock(); - pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); - pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); // pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 ); Aig_ManStop( pTemp ); @@ -391,8 +391,8 @@ ABC_PRT( "Time", clock() - clk ); { // extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose ); clk = clock(); - pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); - pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); // pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 ); Aig_ManStop( pTemp ); @@ -580,8 +580,8 @@ ABC_PRT( "Time", clock() - clk ); pPars->fReorderImage = 1; pPars->fVerbose = 0; pPars->fSilent = pParSec->fSilent; - pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); - pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePis = Aig_ManCiNum(pNew) - Aig_ManRegNum(pNew); + pNew->nTruePos = Aig_ManCoNum(pNew) - Aig_ManRegNum(pNew); RetValue = Aig_ManVerifyUsingBdds( pNew, pPars ); } diff --git a/src/proof/fra/fraSim.c b/src/proof/fra/fraSim.c index e54846bc..66579be3 100644 --- a/src/proof/fra/fraSim.c +++ b/src/proof/fra/fraSim.c @@ -221,7 +221,7 @@ void Fra_SmlSavePattern1( Fra_Man_t * p, int fInit ) if ( !fInit ) return; // clear the state bits to correspond to all-0 initial state - nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); + nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); k = 0; Aig_ManForEachLoSeq( p->pManAig, pObj, i ) Abc_InfoXorBit( p->pPatWords, nTruePis * p->nFramesAll + k++ ); @@ -251,9 +251,9 @@ void Fra_SmlSavePattern( Fra_Man_t * p ) if ( p->vCex ) { Vec_IntClear( p->vCex ); - for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ ) + for ( i = 0; i < Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ ) Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) ); - for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ ) + for ( i = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManCiNum(p->pManFraig); i++ ) Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) ); } @@ -298,13 +298,13 @@ void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObjPo ) // determine the best pattern BestPat = i * 32 + k; // fill in the counter-example data - pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pManFraig)+1 ); + pModel = ABC_ALLOC( int, Aig_ManCiNum(p->pManFraig)+1 ); Aig_ManForEachCi( p->pManAig, pObjPi, i ) { pModel[i] = Abc_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat); // printf( "%d", pModel[i] ); } - pModel[Aig_ManPiNum(p->pManAig)] = pObjPo->Id; + pModel[Aig_ManCiNum(p->pManAig)] = pObjPo->Id; // printf( "\n" ); // set the model assert( p->pManFraig->pData == NULL ); @@ -328,7 +328,7 @@ int Fra_SmlCheckOutput( Fra_Man_t * p ) Aig_Obj_t * pObj; int i; // make sure the reference simulation pattern does not detect the bug - pObj = Aig_ManPo( p->pManAig, 0 ); + pObj = Aig_ManCo( p->pManAig, 0 ); assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); Aig_ManForEachCo( p->pManAig, pObj, i ) { @@ -359,7 +359,7 @@ void Fra_SmlAssignRandom( Fra_Sml_t * p, Aig_Obj_t * pObj ) { unsigned * pSims; int i; - assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsCi(pObj) ); pSims = Fra_ObjSim( p, pObj->Id ); for ( i = 0; i < p->nWordsTotal; i++ ) pSims[i] = Fra_ObjRandomSim(); @@ -380,7 +380,7 @@ void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFram { unsigned * pSims; int i; - assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsCi(pObj) ); pSims = Fra_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; for ( i = 0; i < p->nWordsFrame; i++ ) pSims[i] = fConst1? ~(unsigned)0 : 0; @@ -404,7 +404,7 @@ void Fra_SmlInitialize( Fra_Sml_t * p, int fInit ) if ( fInit ) { assert( Aig_ManRegNum(p->pAig) > 0 ); - assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) ); // assign random info for primary inputs Aig_ManForEachPiSeq( p->pAig, pObj, i ) Fra_SmlAssignRandom( p, pObj ); @@ -441,16 +441,16 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat ) Aig_ManForEachCi( p->pAig, pObj, i ) Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 ); // flip one bit - Limit = Abc_MinInt( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 ); + Limit = Abc_MinInt( Aig_ManCiNum(p->pAig), p->nWordsTotal * 32 - 1 ); for ( i = 0; i < Limit; i++ ) - Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 ); + Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManCi(p->pAig,i)->Id ), i+1 ); } else { int fUseDist1 = 0; // copy the PI info for each frame - nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig); + nTruePis = Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig); for ( f = 0; f < p->nFrames; f++ ) Aig_ManForEachPiSeq( p->pAig, pObj, i ) Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f ); @@ -458,14 +458,14 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat ) k = 0; Aig_ManForEachLoSeq( p->pAig, pObj, i ) Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 ); -// assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) ); +// assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManCiNum(p->pManFraig) ); // flip one bit of the last frame if ( fUseDist1 ) //&& p->nFrames == 2 ) { Limit = Abc_MinInt( nTruePis, p->nWordsFrame * 32 - 1 ); for ( i = 0; i < Limit; i++ ) - Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 ); + Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 ); } } } @@ -581,7 +581,7 @@ void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) unsigned * pSims, * pSims0; int fCompl, fCompl0, i; assert( !Aig_IsComplement(pObj) ); - assert( Aig_ObjIsPo(pObj) ); + assert( Aig_ObjIsCo(pObj) ); assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal ); // get hold of the simulation information pSims = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame; @@ -615,8 +615,8 @@ void Fra_SmlNodeTransferNext( Fra_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int i; assert( !Aig_IsComplement(pOut) ); assert( !Aig_IsComplement(pIn) ); - assert( Aig_ObjIsPo(pOut) ); - assert( Aig_ObjIsPi(pIn) ); + assert( Aig_ObjIsCo(pOut) ); + assert( Aig_ObjIsCi(pIn) ); assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal ); // get hold of the simulation information pSims0 = Fra_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame; @@ -918,12 +918,12 @@ Abc_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p ) } break; } - assert( iPo < Aig_ManPoNum(p->pAig)-Aig_ManRegNum(p->pAig) ); + assert( iPo < Aig_ManCoNum(p->pAig)-Aig_ManRegNum(p->pAig) ); assert( iFrame < p->nFrames ); assert( iBit < 32 * p->nWordsFrame ); // allocate the counter example - pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 ); + pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 ); pCex->iPo = iPo; pCex->iFrame = iFrame; @@ -972,16 +972,16 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in // get the number of frames assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManRegNum(pFrames) == 0 ); - nTruePis = Aig_ManPiNum(pAig)-Aig_ManRegNum(pAig); - nTruePos = Aig_ManPoNum(pAig)-Aig_ManRegNum(pAig); - nFrames = Aig_ManPiNum(pFrames) / nTruePis; - assert( nTruePis * nFrames == Aig_ManPiNum(pFrames) ); - assert( nTruePos * nFrames == Aig_ManPoNum(pFrames) ); + nTruePis = Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig); + nTruePos = Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig); + nFrames = Aig_ManCiNum(pFrames) / nTruePis; + assert( nTruePis * nFrames == Aig_ManCiNum(pFrames) ); + assert( nTruePos * nFrames == Aig_ManCoNum(pFrames) ); // find the PO that failed iPo = -1; iFrame = -1; Aig_ManForEachCo( pFrames, pObj, i ) - if ( pObj->Id == pModel[Aig_ManPiNum(pFrames)] ) + if ( pObj->Id == pModel[Aig_ManCiNum(pFrames)] ) { iPo = i % nTruePos; iFrame = i / nTruePos; @@ -994,7 +994,7 @@ Abc_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, in pCex->iFrame = iFrame; // copy the bit data - for ( i = 0; i < Aig_ManPiNum(pFrames); i++ ) + for ( i = 0; i < Aig_ManCiNum(pFrames); i++ ) { if ( pModel[i] ) Abc_InfoSetBit( pCex->pData, pCex->nRegs + i ); diff --git a/src/proof/int/intCheck.c b/src/proof/int/intCheck.c index 57d6e7d0..2b14d8ae 100644 --- a/src/proof/int/intCheck.c +++ b/src/proof/int/intCheck.c @@ -112,10 +112,10 @@ Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK ) p->vAssLits = Vec_IntAlloc( 100 ); // generate the timeframes p->pFrames = Inter_ManUnrollFrames( pTrans, nFramesK ); - assert( Aig_ManPiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) ); - assert( Aig_ManPoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) ); + assert( Aig_ManCiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) ); + assert( Aig_ManCoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) ); // convert to CNF - p->pCnf = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) ); + p->pCnf = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) ); p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 ); // assign parameters p->nFramesK = nFramesK; @@ -221,9 +221,9 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut { Aig_Obj_t * pObj, * pObj2; int i, f, VarA, VarB, RetValue, Entry, status; - int nRegs = Aig_ManPiNum(pCnfInt->pMan); - assert( Aig_ManPoNum(p->pCnf->pMan) == p->nFramesK * nRegs ); - assert( Aig_ManPoNum(pCnfInt->pMan) == 1 ); + int nRegs = Aig_ManCiNum(pCnfInt->pMan); + assert( Aig_ManCoNum(p->pCnf->pMan) == p->nFramesK * nRegs ); + assert( Aig_ManCoNum(pCnfInt->pMan) == 1 ); // set runtime limit if ( nTimeNewOut ) @@ -242,7 +242,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut // add equality clauses for the flop variables Aig_ManForEachCi( pCnfInt->pMan, pObj, i ) { - pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(p->pFrames, i); + pObj2 = f ? Aig_ManCo(p->pFrames, i + (f-1) * nRegs) : Aig_ManCi(p->pFrames, i); Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] ); } // add final clauses @@ -251,14 +251,14 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut if ( f == Vec_IntSize(p->vOrLits) ) // find time here { // add literal to this frame - VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ]; + VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ]; Vec_IntPush( p->vOrLits, VarB ); } else { // add OR gate for this frame VarA = Vec_IntEntry( p->vOrLits, f ); - VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ]; + VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ]; Inter_CheckAddOrGate( p, VarA, VarB, p->nVars + pCnfInt->nVars ); Vec_IntWriteEntry( p->vOrLits, f, p->nVars + pCnfInt->nVars ); // using var ID! } @@ -266,7 +266,7 @@ int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut else { // add AND gate for this frame - VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ]; + VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ]; Vec_IntPush( p->vAndLits, VarB ); } // update variable IDs diff --git a/src/proof/int/intContain.c b/src/proof/int/intContain.c index 213c557c..a031c7a4 100644 --- a/src/proof/int/intContain.c +++ b/src/proof/int/intContain.c @@ -161,7 +161,7 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew { Aig_Obj_t * pObj; int i; - assert( Aig_ManPoNum(pOld) == 1 ); + assert( Aig_ManCoNum(pOld) == 1 ); // create the PIs Aig_ManCleanData( pOld ); Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew); @@ -171,7 +171,7 @@ void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNew Aig_ManForEachNode( pOld, pObj, i ) pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); // add one PO to new - pObj = Aig_ManPo( pOld, 0 ); + pObj = Aig_ManCo( pOld, 0 ); Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) ); } @@ -283,7 +283,7 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf return 1; // assert( Saig_ManPoNum(p) == 1 ); assert( Aig_ManRegNum(p) > 0 ); - assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) ); + assert( Aig_ManRegNum(p) < Aig_ManCiNum(p) ); // get the counter-example vPis = Vec_IntAlloc( 100 ); @@ -303,12 +303,12 @@ int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf for ( i = 0; i < nFrames; i++ ) Aig_ManForEachPiSeq( p, pObj, k ) Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], i ); - assert( iBit == Aig_ManPiNum(pCnf->pMan) ); + assert( iBit == Aig_ManCiNum(pCnf->pMan) ); // run simulation Fra_SmlSimulateOne( pSml ); // check if the given output has failed -// RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, 0) ); +// RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManCo(pAig, 0) ); // assert( RetValue ); // check values at the internal nodes diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c index 10a8fc74..8bef9c59 100644 --- a/src/proof/int/intCore.c +++ b/src/proof/int/intCore.c @@ -139,7 +139,7 @@ clk2 = clock(); p->pInter = Inter_ManStartOneOutput( pAig, 1 ); else p->pInter = Inter_ManStartInitState( Aig_ManRegNum(pAig) ); - assert( Aig_ManPoNum(p->pInter) == 1 ); + assert( Aig_ManCoNum(p->pInter) == 1 ); clk = clock(); p->pCnfInter = Cnf_Derive( p->pInter, 0 ); p->timeCnf += clock() - clk; @@ -157,7 +157,7 @@ p->timeRwr += clock() - clk; // can also do SAT sweeping on the timeframes... clk = clock(); if ( pPars->fUseBackward ) - p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) ); + p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) ); else // p->pCnfFrames = Cnf_Derive( p->pFrames, 0 ); p->pCnfFrames = Cnf_DeriveSimple( p->pFrames, 0 ); @@ -285,7 +285,7 @@ clk = clock(); p->timeRwr += clock() - clk; // check if interpolant is trivial - if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManPo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) ) + if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManCo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) ) { // printf( "interpolant is constant 0\n" ); if ( pPars->fVerbose ) @@ -300,7 +300,7 @@ p->timeRwr += clock() - clk; clk = clock(); if ( pPars->fCheckKstep ) // k-step unique-state induction { - if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) ) + if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) ) { if ( pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1 ) { @@ -326,7 +326,7 @@ timeTemp = clock() - clk2; } else // combinational containment { - if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) ) + if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) ) Status = Inter_ManCheckContainment( p->pInterNew, p->pInter ); else Status = 0; diff --git a/src/proof/int/intCtrex.c b/src/proof/int/intCtrex.c index 22e689f4..04aaa271 100644 --- a/src/proof/int/intCtrex.c +++ b/src/proof/int/intCtrex.c @@ -75,7 +75,7 @@ Aig_Man_t * Inter_ManFramesBmc( Aig_Man_t * pAig, int nFrames ) pObjLo->pData = pObjLi->pData; } // create POs for the output of the last frame - pObj = Aig_ManPo( pAig, 0 ); + pObj = Aig_ManCo( pAig, 0 ); Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) ); Aig_ManCleanup( pFrames ); return pFrames; diff --git a/src/proof/int/intDup.c b/src/proof/int/intDup.c index adc692cb..d7bc73d6 100644 --- a/src/proof/int/intDup.c +++ b/src/proof/int/intDup.c @@ -141,7 +141,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo ) } // set registers pNew->nRegs = fAddFirstPo? 0 : p->nRegs; - pNew->nTruePis = fAddFirstPo? Aig_ManPiNum(p) + 1 : p->nTruePis + 1; + pNew->nTruePis = fAddFirstPo? Aig_ManCiNum(p) + 1 : p->nTruePis + 1; pNew->nTruePos = fAddFirstPo + Saig_ManConstrNum(p); // duplicate internal nodes Aig_ManForEachNode( p, pObj, i ) @@ -158,7 +158,7 @@ Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo ) // add the PO if ( fAddFirstPo ) { - pObj = Aig_ManPo( p, 0 ); + pObj = Aig_ManCo( p, 0 ); Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) ); } else diff --git a/src/proof/int/intFrames.c b/src/proof/int/intFrames.c index 8e74d99a..7c5231b7 100644 --- a/src/proof/int/intFrames.c +++ b/src/proof/int/intFrames.c @@ -99,7 +99,7 @@ Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts // create the only PO of the manager else { - pObj = Aig_ManPo( pAig, 0 ); + pObj = Aig_ManCo( pAig, 0 ); Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) ); } Aig_ManCleanup( pFrames ); diff --git a/src/proof/int/intInter.c b/src/proof/int/intInter.c index ef32294b..ffc462d3 100644 --- a/src/proof/int/intInter.c +++ b/src/proof/int/intInter.c @@ -45,10 +45,10 @@ ABC_NAMESPACE_IMPL_START Aig_Man_t * Inter_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther ) { Aig_Man_t * pInterC; - assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) ); + assert( Aig_ManCiNum(pInter) <= Aig_ManCiNum(pOther) ); pInterC = Aig_ManDupSimple( pInter ); - Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 ); - assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) ); + Aig_IthVar( pInterC, Aig_ManCiNum(pOther)-1 ); + assert( Aig_ManCiNum(pInterC) == Aig_ManCiNum(pOther) ); return pInterC; } diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c index c37cb2c6..ed3ef80e 100644 --- a/src/proof/int/intM114.c +++ b/src/proof/int/intM114.c @@ -61,10 +61,10 @@ sat_solver * Inter_ManDeriveSatSolver( assert( Aig_ManRegNum(pInter) == 0 ); assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManRegNum(pFrames) == 0 ); - assert( Aig_ManPoNum(pInter) == 1 ); - assert( Aig_ManPoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 ); - assert( fUseBackward || Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) ); -// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); + assert( Aig_ManCoNum(pInter) == 1 ); + assert( Aig_ManCoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 ); + assert( fUseBackward || Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) ); +// assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); // prepare CNFs Cnf_DataLift( pCnfAig, pCnfFrames->nVars ); @@ -93,12 +93,12 @@ sat_solver * Inter_ManDeriveSatSolver( { Saig_ManForEachLi( pAig, pObj2, i ) { - if ( Saig_ManRegNum(pAig) == Aig_ManPiNum(pInter) ) - pObj = Aig_ManPi( pInter, i ); + if ( Saig_ManRegNum(pAig) == Aig_ManCiNum(pInter) ) + pObj = Aig_ManCi( pInter, i ); else { - assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pInter) ); - pObj = Aig_ManPi( pInter, Aig_ManPiNum(pAig)-Saig_ManRegNum(pAig) + i ); + assert( Aig_ManCiNum(pAig) == Aig_ManCiNum(pInter) ); + pObj = Aig_ManCi( pInter, Aig_ManCiNum(pAig)-Saig_ManRegNum(pAig) + i ); } Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 ); diff --git a/src/proof/int/intM114p.c b/src/proof/int/intM114p.c index 6164a389..f143dc39 100644 --- a/src/proof/int/intM114p.c +++ b/src/proof/int/intM114p.c @@ -59,10 +59,10 @@ M114p_Solver_t Inter_ManDeriveSatSolverM114p( assert( Aig_ManRegNum(pInter) == 0 ); assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManRegNum(pFrames) == 0 ); - assert( Aig_ManPoNum(pInter) == 1 ); - assert( Aig_ManPoNum(pFrames) == 1 ); - assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) ); -// assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); + assert( Aig_ManCoNum(pInter) == 1 ); + assert( Aig_ManCoNum(pFrames) == 1 ); + assert( Aig_ManCiNum(pInter) == Aig_ManRegNum(pAig) ); +// assert( (Aig_ManCiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 ); // prepare CNFs Cnf_DataLift( pCnfAig, pCnfFrames->nVars ); diff --git a/src/proof/live/liveness.c b/src/proof/live/liveness.c index d961e509..e457b3f8 100644 --- a/src/proof/live/liveness.c +++ b/src/proof/live/liveness.c @@ -122,12 +122,12 @@ char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pA Aig_ManForEachCi( pAigNew, pObj, index ) if( pObj == pObjPivot ) break; - assert( index < Aig_ManPiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) ); + assert( index < Aig_ManCiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) ); if( index == Saig_ManPiNum( pAigNew ) - 1 ) return "SAVE_BIERE"; else { - pObjOld = Aig_ManPi( pAigOld, index ); + pObjOld = Aig_ManCi( pAigOld, index ); pNode = Abc_NtkPi( pNtkOld, index ); assert( pObjOld->pData == pObjPivot ); return Abc_ObjName( pNode ); @@ -148,7 +148,7 @@ char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNe if( index < originalLatchNum ) { oldIndex = Saig_ManPiNum( pAigOld ) + index; - pObjOld = Aig_ManPi( pAigOld, oldIndex ); + pObjOld = Aig_ManCi( pAigOld, oldIndex ); pNode = Abc_NtkCi( pNtkOld, oldIndex ); assert( pObjOld->pData == pObjPivot ); return Abc_ObjName( pNode ); @@ -158,7 +158,7 @@ char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t *pAigNe else if( index > originalLatchNum && index < 2 * originalLatchNum + 1 ) { oldIndex = Saig_ManPiNum( pAigOld ) + index - originalLatchNum - 1; - pObjOld = Aig_ManPi( pAigOld, oldIndex ); + pObjOld = Aig_ManCi( pAigOld, oldIndex ); pNode = Abc_NtkCi( pNtkOld, oldIndex ); sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "SHADOW"); return dummyStr; @@ -219,26 +219,26 @@ Vec_Ptr_t *vecPis, *vecPiNames; Vec_Ptr_t *vecLos, *vecLoNames; -int Aig_ManPiCleanupBiere( Aig_Man_t * p ) +int Aig_ManCiCleanupBiere( Aig_Man_t * p ) { - int nPisOld = Aig_ManPiNum(p); + int nPisOld = Aig_ManCiNum(p); - p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis ); + p->nObjs[AIG_OBJ_CI] = Vec_PtrSize( p->vCis ); if ( Aig_ManRegNum(p) ) - p->nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p); + p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p); - return nPisOld - Aig_ManPiNum(p); + return nPisOld - Aig_ManCiNum(p); } -int Aig_ManPoCleanupBiere( Aig_Man_t * p ) +int Aig_ManCoCleanupBiere( Aig_Man_t * p ) { - int nPosOld = Aig_ManPoNum(p); + int nPosOld = Aig_ManCoNum(p); - p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos ); + p->nObjs[AIG_OBJ_CO] = Vec_PtrSize( p->vCos ); if ( Aig_ManRegNum(p) ) - p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p); - return nPosOld - Aig_ManPoNum(p); + p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p); + return nPosOld - Aig_ManCoNum(p); } Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_t * p, @@ -518,8 +518,8 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_ Aig_ManSetRegNum( pNew, nRegCount ); - Aig_ManPiCleanupBiere( pNew ); - Aig_ManPoCleanupBiere( pNew ); + Aig_ManCiCleanupBiere( pNew ); + Aig_ManCoCleanupBiere( pNew ); Aig_ManCleanup( pNew ); @@ -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->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(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 ); } @@ -821,8 +821,8 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M Aig_ManSetRegNum( pNew, nRegCount ); - Aig_ManPiCleanupBiere( pNew ); - Aig_ManPoCleanupBiere( pNew ); + Aig_ManCiCleanupBiere( pNew ); + Aig_ManCoCleanupBiere( pNew ); Aig_ManCleanup( pNew ); @@ -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->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(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 ); } @@ -1128,8 +1128,8 @@ Aig_Man_t * LivenessToSafetyTransformationOneStepLoop( int mode, Abc_Ntk_t * pNt //printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vPis ), pNew->nRegs ); - Aig_ManPiCleanupBiere( pNew ); - Aig_ManPoCleanupBiere( pNew ); + Aig_ManCiCleanupBiere( pNew ); + Aig_ManCoCleanupBiere( pNew ); Aig_ManCleanup( pNew ); @@ -1151,7 +1151,7 @@ Vec_Ptr_t * populateLivenessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) //if( strstr( Abc_ObjName( pNode ), "assert_fair") != NULL ) if( nodeName_starts_with( pNode, "assert_fair" ) ) { - Vec_PtrPush( vLive, Aig_ManPo( pAig, i ) ); + Vec_PtrPush( vLive, Aig_ManCo( pAig, i ) ); liveCounter++; } printf("Number of liveness property found = %d\n", liveCounter); @@ -1169,7 +1169,7 @@ Vec_Ptr_t * populateFairnessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) //if( strstr( Abc_ObjName( pNode ), "assume_fair") != NULL ) if( nodeName_starts_with( pNode, "assume_fair" ) ) { - Vec_PtrPush( vFair, Aig_ManPo( pAig, i ) ); + Vec_PtrPush( vFair, Aig_ManCo( pAig, i ) ); fairCounter++; } printf("Number of fairness property found = %d\n", fairCounter); @@ -1187,7 +1187,7 @@ Vec_Ptr_t * populateSafetyAssertionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL ) if( nodeName_starts_with( pNode, "assert_safety" ) || nodeName_starts_with( pNode, "Assert" )) { - Vec_PtrPush( vAssertSafety, Aig_ManPo( pAig, i ) ); + Vec_PtrPush( vAssertSafety, Aig_ManCo( pAig, i ) ); assertSafetyCounter++; } printf("Number of safety property found = %d\n", assertSafetyCounter); @@ -1205,7 +1205,7 @@ Vec_Ptr_t * populateSafetyAssumptionVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) //if( strstr( Abc_ObjName( pNode ), "Assert") != NULL ) if( nodeName_starts_with( pNode, "assume_safety" ) || nodeName_starts_with( pNode, "Assume" )) { - Vec_PtrPush( vAssumeSafety, Aig_ManPo( pAig, i ) ); + Vec_PtrPush( vAssumeSafety, Aig_ManCo( pAig, i ) ); assumeSafetyCounter++; } printf("Number of assume_safety property found = %d\n", assumeSafetyCounter); @@ -2247,8 +2247,8 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A Aig_ManSetRegNum( pNew, nRegCount ); - Aig_ManPiCleanupBiere( pNew ); - Aig_ManPoCleanupBiere( pNew ); + Aig_ManCiCleanupBiere( pNew ); + Aig_ManCoCleanupBiere( pNew ); Aig_ManCleanup( pNew ); @@ -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->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(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 552c5204..b99df807 100644 --- a/src/proof/live/liveness_sim.c +++ b/src/proof/live/liveness_sim.c @@ -85,12 +85,12 @@ static char * retrieveTruePiName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Ma Aig_ManForEachCi( pAigNew, pObj, index ) if( pObj == pObjPivot ) break; - assert( index < Aig_ManPiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) ); + assert( index < Aig_ManCiNum( pAigNew ) - Aig_ManRegNum( pAigNew ) ); if( index == Saig_ManPiNum( pAigNew ) - 1 ) return "SAVE_BIERE"; else { - pObjOld = Aig_ManPi( pAigOld, index ); + pObjOld = Aig_ManCi( pAigOld, index ); pNode = Abc_NtkPi( pNtkOld, index ); assert( pObjOld->pData == pObjPivot ); return Abc_ObjName( pNode ); @@ -111,7 +111,7 @@ static char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t if( index < originalLatchNum ) { oldIndex = Saig_ManPiNum( pAigOld ) + index; - pObjOld = Aig_ManPi( pAigOld, oldIndex ); + pObjOld = Aig_ManCi( pAigOld, oldIndex ); pNode = Abc_NtkCi( pNtkOld, oldIndex ); assert( pObjOld->pData == pObjPivot ); return Abc_ObjName( pNode ); @@ -121,7 +121,7 @@ static char * retrieveLOName( Abc_Ntk_t *pNtkOld, Aig_Man_t *pAigOld, Aig_Man_t else if( index > originalLatchNum && index < 2 * originalLatchNum + 1 ) { oldIndex = Saig_ManPiNum( pAigOld ) + index - originalLatchNum - 1; - pObjOld = Aig_ManPi( pAigOld, oldIndex ); + pObjOld = Aig_ManCi( pAigOld, oldIndex ); pNode = Abc_NtkCi( pNtkOld, oldIndex ); sprintf( dummyStr, "%s__%s", Abc_ObjName( pNode ), "SHADOW"); return dummyStr; @@ -172,26 +172,26 @@ extern Vec_Ptr_t *vecPis, *vecPiNames; extern Vec_Ptr_t *vecLos, *vecLoNames; -static int Aig_ManPiCleanupBiere( Aig_Man_t * p ) +static int Aig_ManCiCleanupBiere( Aig_Man_t * p ) { - int nPisOld = Aig_ManPiNum(p); + int nPisOld = Aig_ManCiNum(p); - p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis ); + p->nObjs[AIG_OBJ_CI] = Vec_PtrSize( p->vCis ); if ( Aig_ManRegNum(p) ) - p->nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p); + p->nTruePis = Aig_ManCiNum(p) - Aig_ManRegNum(p); - return nPisOld - Aig_ManPiNum(p); + return nPisOld - Aig_ManCiNum(p); } -static int Aig_ManPoCleanupBiere( Aig_Man_t * p ) +static int Aig_ManCoCleanupBiere( Aig_Man_t * p ) { - int nPosOld = Aig_ManPoNum(p); + int nPosOld = Aig_ManCoNum(p); - p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos ); + p->nObjs[AIG_OBJ_CO] = Vec_PtrSize( p->vCos ); if ( Aig_ManRegNum(p) ) - p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p); - return nPosOld - Aig_ManPoNum(p); + p->nTruePos = Aig_ManCoNum(p) - Aig_ManRegNum(p); + return nPosOld - Aig_ManCoNum(p); } static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_t * p, Vec_Ptr_t *vLive, Vec_Ptr_t *vFair ) @@ -459,14 +459,14 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_ Aig_ManSetRegNum( pNew, nRegCount ); - Aig_ManPiCleanupBiere( pNew ); - Aig_ManPoCleanupBiere( pNew ); + Aig_ManCiCleanupBiere( pNew ); + Aig_ManCoCleanupBiere( pNew ); Aig_ManCleanup( pNew ); assert( Aig_ManCheck( pNew ) ); #ifndef DUPLICATE_CKT_DEBUG - assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vPos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi); + assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(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 ); @@ -680,10 +680,10 @@ static Aig_Man_t * LivenessToSafetyTransformationOneStepLoopSim( Abc_Ntk_t * pNt Aig_ManSetRegNum( pNew, nRegCount ); - printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vPis ), pNew->nRegs ); + printf("\nSaig_ManPiNum = %d, Reg Num = %d, before everything, before Pi cleanup\n", Vec_PtrSize( pNew->vCis ), pNew->nRegs ); - Aig_ManPiCleanupBiere( pNew ); - Aig_ManPoCleanupBiere( pNew ); + Aig_ManCiCleanupBiere( pNew ); + Aig_ManCoCleanupBiere( pNew ); Aig_ManCleanup( pNew ); @@ -704,7 +704,7 @@ static Vec_Ptr_t * populateLivenessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) Abc_NtkForEachPo( pNtk, pNode, i ) if( strstr( Abc_ObjName( pNode ), "assert_fair") != NULL ) { - Vec_PtrPush( vLive, Aig_ManPo( pAig, i ) ); + Vec_PtrPush( vLive, Aig_ManCo( pAig, i ) ); liveCounter++; } printf("\nNumber of liveness property found = %d\n", liveCounter); @@ -721,7 +721,7 @@ static Vec_Ptr_t * populateFairnessVector( Abc_Ntk_t *pNtk, Aig_Man_t *pAig ) Abc_NtkForEachPo( pNtk, pNode, i ) if( strstr( Abc_ObjName( pNode ), "assume_fair") != NULL ) { - Vec_PtrPush( vFair, Aig_ManPo( pAig, i ) ); + Vec_PtrPush( vFair, Aig_ManCo( pAig, i ) ); fairCounter++; } printf("\nNumber of fairness property found = %d\n", fairCounter); diff --git a/src/proof/live/ltl_parser.c b/src/proof/live/ltl_parser.c index 5572611f..de567576 100644 --- a/src/proof/live/ltl_parser.c +++ b/src/proof/live/ltl_parser.c @@ -762,8 +762,8 @@ void populateBoolWithAigNodePtr( Abc_Ntk_t *pNtk, Aig_Man_t *pAigOld, Aig_Man_t Abc_NtkForEachPo( pNtk, pNode, i ) if( strcmp( Abc_ObjName( pNode ), targetName ) == 0 ) { - pObj = Aig_ManPo( pAigOld, i ); - assert( Aig_ObjIsPo( pObj )); + pObj = Aig_ManCo( pAigOld, i ); + assert( Aig_ObjIsCo( pObj )); pDriverImage = Aig_NotCond((Aig_Obj_t *)Aig_Regular(Aig_ObjChild0( pObj ))->pData, Aig_ObjFaninC0(pObj)); topASTNode->pObj = pDriverImage; return; diff --git a/src/proof/llb/llb1Constr.c b/src/proof/llb/llb1Constr.c index 4ce911db..1ef4ce14 100644 --- a/src/proof/llb/llb1Constr.c +++ b/src/proof/llb/llb1Constr.c @@ -150,7 +150,7 @@ void Llb_ManComputeIndCase( Aig_Man_t * p, DdManager * dd, Vec_Int_t * vNodes ) Vec_PtrWriteEntry( vBdds, Aig_ObjId(Aig_ManConst1(p)), bFunc ); Saig_ManForEachPi( p, pObj, i ) { - bFunc = Cudd_bddIthVar( dd, Aig_ManPiNum(p) + i ); Cudd_Ref( bFunc ); + bFunc = Cudd_bddIthVar( dd, Aig_ManCiNum(p) + i ); Cudd_Ref( bFunc ); Vec_PtrWriteEntry( vBdds, Aig_ObjId(pObj), bFunc ); } Saig_ManForEachLi( p, pObj, i ) @@ -201,11 +201,11 @@ Vec_Int_t * Llb_ManComputeBaseCase( Aig_Man_t * p, DdManager * dd ) Vec_Int_t * vNodes; Aig_Obj_t * pObj, * pRoot; int i; - pRoot = Aig_ManPo( p, 0 ); + pRoot = Aig_ManCo( p, 0 ); vNodes = Vec_IntStartFull( Aig_ManObjNumMax(p) ); Aig_ManForEachObj( p, pObj, i ) { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; if ( Cudd_bddLeq( dd, (DdNode *)pObj->pData, Cudd_Not(pRoot->pData) ) ) Vec_IntWriteEntry( vNodes, i, 1 ); @@ -232,7 +232,7 @@ DdManager * Llb_ManConstructGlobalBdds( Aig_Man_t * p ) DdNode * bBdd0, * bBdd1; Aig_Obj_t * pObj; int i; - dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + dd = Cudd_Init( Aig_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); pObj = Aig_ManConst1(p); pObj->pData = Cudd_ReadOne(dd); Cudd_Ref( (DdNode *)pObj->pData ); diff --git a/src/proof/llb/llb1Core.c b/src/proof/llb/llb1Core.c index ee697748..56e0cc6b 100644 --- a/src/proof/llb/llb1Core.c +++ b/src/proof/llb/llb1Core.c @@ -89,7 +89,7 @@ void Llb_ManPrintAig( Llb_Man_t * p ) Abc_Print( 1, "pi =%3d ", Saig_ManPiNum(p->pAig) ); Abc_Print( 1, "po =%3d ", Saig_ManPoNum(p->pAig) ); Abc_Print( 1, "ff =%3d ", Saig_ManRegNum(p->pAig) ); - Abc_Print( 1, "int =%5d ", Vec_IntSize(p->vVar2Obj)-Aig_ManPiNum(p->pAig)-Saig_ManRegNum(p->pAig) ); + Abc_Print( 1, "int =%5d ", Vec_IntSize(p->vVar2Obj)-Aig_ManCiNum(p->pAig)-Saig_ManRegNum(p->pAig) ); Abc_Print( 1, "var =%5d ", Vec_IntSize(p->vVar2Obj) ); Abc_Print( 1, "part =%5d ", Vec_PtrSize(p->vGroups)-2 ); Abc_Print( 1, "and =%5d ", Aig_ManNodeNum(p->pAig) ); diff --git a/src/proof/llb/llb1Group.c b/src/proof/llb/llb1Group.c index c61f3a30..1099b2cd 100644 --- a/src/proof/llb/llb1Group.c +++ b/src/proof/llb/llb1Group.c @@ -95,7 +95,7 @@ void Llb_ManGroupCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Ptr_t * vN Aig_ObjSetTravIdCurrent(pAig, pObj); if ( Aig_ObjIsConst1(pObj) ) return; - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { Llb_ManGroupCollect_rec( pAig, Aig_ObjFanin0(pObj), vNodes ); return; @@ -180,7 +180,7 @@ Llb_Grp_t * Llb_ManGroupCreate( Llb_Man_t * pMan, Aig_Obj_t * pObj ) p = Llb_ManGroupAlloc( pMan ); Vec_PtrPush( p->vOuts, pObj ); Aig_ManIncrementTravId( pMan->pAig ); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) Llb_ManGroupCreate_rec( pMan->pAig, Aig_ObjFanin0(pObj), p->vIns ); else { diff --git a/src/proof/llb/llb1Hint.c b/src/proof/llb/llb1Hint.c index 6e705a38..51d3a9fc 100644 --- a/src/proof/llb/llb1Hint.c +++ b/src/proof/llb/llb1Hint.c @@ -103,7 +103,7 @@ Vec_Int_t * Llb_ManCollectHighFanoutObjects( Aig_Man_t * pAig, int nCandMax, int vFanouts = Vec_IntAlloc( 100 ); Aig_ManForEachObj( pAig, pObj, i ) { -// if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) +// if ( !Aig_ObjIsCi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) continue; Vec_IntPush( vFanouts, Aig_ObjRefs(pObj) ); @@ -117,7 +117,7 @@ Vec_Int_t * Llb_ManCollectHighFanoutObjects( Aig_Man_t * pAig, int nCandMax, int vResult = Vec_IntAlloc( 100 ); Aig_ManForEachObj( pAig, pObj, i ) { -// if ( !Aig_ObjIsPi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) +// if ( !Aig_ObjIsCi(pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) if ( !Saig_ObjIsLo(pAig,pObj) && (fCisOnly || !Aig_ObjIsNode(pObj)) ) continue; if ( Aig_ObjRefs(pObj) < PivotValue ) diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c index d8c667ae..60124378 100644 --- a/src/proof/llb/llb1Reach.c +++ b/src/proof/llb/llb1Reach.c @@ -69,7 +69,7 @@ DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); } Vec_PtrFree( vNodes ); - if ( Aig_ObjIsPo(pNode) ) + if ( Aig_ObjIsCo(pNode) ) bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pNode) ); Cudd_Deref( bFunc ); dd->TimeStop = TimeStop; @@ -113,7 +113,7 @@ DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup ) bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes ); Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i ) { - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) ); else bBdd0 = (DdNode *)pObj->pData; @@ -413,7 +413,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs if ( vHints == NULL ) return Cudd_ReadOne( p->dd ); TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0; - assert( Aig_ManPiNum(p->pAig) == Aig_ManPiNum(p->pAigGlo) ); + assert( Aig_ManCiNum(p->pAig) == Aig_ManCiNum(p->pAigGlo) ); // assign const and PI nodes to the original AIG Aig_ManCleanData( p->pAig ); Aig_ManConst1( p->pAig )->pData = Cudd_ReadOne( p->dd ); @@ -431,7 +431,7 @@ DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNs Aig_ManCleanData( p->pAigGlo ); Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd ); Aig_ManForEachCi( p->pAigGlo, pObj, i ) - pObj->pData = Aig_ManPi(p->pAig, i)->pData; + pObj->pData = Aig_ManCi(p->pAig, i)->pData; // derive consraints bConstr = Cudd_ReadOne( p->dd ); Cudd_Ref( bConstr ); Vec_IntForEachEntry( vHints, Entry, i ) @@ -595,7 +595,7 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo assert( p->ddG == NULL ); assert( p->ddR == NULL ); p->dd = Cudd_Init( Vec_IntSize(p->vVar2Obj), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - p->ddR = Cudd_Init( Aig_ManPiNum(p->pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + p->ddR = Cudd_Init( Aig_ManCiNum(p->pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); if ( pddGlo && *pddGlo ) p->ddG = *pddGlo, *pddGlo = NULL; else diff --git a/src/proof/llb/llb2Bad.c b/src/proof/llb/llb2Bad.c index 9aecb9ff..f4359493 100644 --- a/src/proof/llb/llb2Bad.c +++ b/src/proof/llb/llb2Bad.c @@ -48,7 +48,7 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut ) DdNode * bBdd0, * bBdd1, * bTemp, * bResult; Aig_Obj_t * pObj; int i, k; - assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) ); + assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) ); // initialize elementary variables Aig_ManConst1(pInit)->pData = Cudd_ReadOne( dd ); Saig_ManForEachLo( pInit, pObj, i ) @@ -56,7 +56,7 @@ DdNode * Llb_BddComputeBad( Aig_Man_t * pInit, DdManager * dd, int TimeOut ) Saig_ManForEachPi( pInit, pObj, i ) pObj->pData = Cudd_bddIthVar( dd, Aig_ManRegNum(pInit) + i ); // compute internal nodes - vNodes = Aig_ManDfsNodes( pInit, (Aig_Obj_t **)Vec_PtrArray(pInit->vPos), Saig_ManPoNum(pInit) ); + vNodes = Aig_ManDfsNodes( pInit, (Aig_Obj_t **)Vec_PtrArray(pInit->vCos), Saig_ManPoNum(pInit) ); Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) { if ( !Aig_ObjIsNode(pObj) ) @@ -111,7 +111,7 @@ DdNode * Llb_BddQuantifyPis( Aig_Man_t * pInit, DdManager * dd, DdNode * bFunc ) DdNode * bVar, * bCube, * bTemp; Aig_Obj_t * pObj; int i, TimeStop; - assert( Cudd_ReadSize(dd) == Aig_ManPiNum(pInit) ); + assert( Cudd_ReadSize(dd) == Aig_ManCiNum(pInit) ); TimeStop = dd->TimeStop; dd->TimeStop = 0; // create PI cube bCube = Cudd_ReadOne( dd ); Cudd_Ref( bCube ); diff --git a/src/proof/llb/llb2Core.c b/src/proof/llb/llb2Core.c index 626acbd2..3b98c32a 100644 --- a/src/proof/llb/llb2Core.c +++ b/src/proof/llb/llb2Core.c @@ -622,7 +622,7 @@ Llb_Img_t * Llb_CoreStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * p->pPars = pPars; p->dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); p->ddG = Cudd_Init( Aig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - p->ddR = Cudd_Init( Aig_ManPiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + p->ddR = Cudd_Init( Aig_ManCiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT ); Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT ); diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c index 295f0bfe..a1db70d3 100644 --- a/src/proof/llb/llb2Flow.c +++ b/src/proof/llb/llb2Flow.c @@ -194,7 +194,7 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp if ( fShowMatrix ) Aig_ManForEachObj( p, pObj, i ) { - if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) ) + if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) ) continue; Vec_PtrForEachEntry( Vec_Int_t *, vMaps, vMap, k ) if ( Vec_IntEntry(vMap, i) ) @@ -276,7 +276,7 @@ int Llb_ManCutLiNum( Aig_Man_t * p, Vec_Ptr_t * vMinCut ) int i, k, iFanout = -1, Counter = 0; Vec_PtrForEachEntry( Aig_Obj_t *, vMinCut, pObj, i ) { - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) continue; Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, k ) { @@ -547,7 +547,7 @@ void Llb_ManResultPrint( Aig_Man_t * p, Vec_Ptr_t * vResult ) int Llb_ManFlowBwdPath2_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) { Aig_Obj_t * pFanout; - assert( Aig_ObjIsNode(pObj) || Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) ); + assert( Aig_ObjIsNode(pObj) || Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) ); // skip visited nodes if ( Aig_ObjIsTravIdCurrent(p, pObj) ) return 0; @@ -607,7 +607,7 @@ void Llb_ManFlowLabelTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) if ( Aig_ObjIsTravIdCurrent(p, pObj) ) return; Aig_ObjSetTravIdCurrent(p, pObj); - if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) ) + if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) ) return; assert( Aig_ObjIsNode(pObj) ); Llb_ManFlowLabelTfi_rec( p, Aig_ObjFanin0(pObj) ); @@ -638,7 +638,7 @@ void Llb_ManFlowUpdateCut( Aig_Man_t * p, Vec_Ptr_t * vMinCut ) Aig_ManIncrementTravId(p); Aig_ManForEachObj( p, pObj, i ) { - if ( !Aig_ObjIsPo(pObj) && !Aig_ObjIsNode(pObj) ) + if ( !Aig_ObjIsCo(pObj) && !Aig_ObjIsNode(pObj) ) continue; if ( Aig_ObjIsTravIdCurrent(p, pObj) || Aig_ObjIsTravIdPrevious(p, pObj) ) continue; @@ -708,7 +708,7 @@ int Llb_ManFlowVerifyCut_rec( Aig_Man_t * p, Aig_Obj_t * pObj ) // visit the node if ( Aig_ObjIsConst1(pObj) ) return 1; - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) return 0; // explore the fanins assert( Aig_ObjIsNode(pObj) ); @@ -930,7 +930,7 @@ void Llb_ManFlowSetMarkA_rec( Aig_Obj_t * pObj ) if ( pObj->fMarkA ) return; pObj->fMarkA = 1; - if ( Aig_ObjIsPi(pObj) || Aig_ObjIsConst1(pObj) ) + if ( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) ) return; assert( Aig_ObjIsNode(pObj) ); Llb_ManFlowSetMarkA_rec( Aig_ObjFanin0(pObj) ); diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c index 678a6fff..38d9b8ae 100644 --- a/src/proof/llb/llb3Nonlin.c +++ b/src/proof/llb/llb3Nonlin.c @@ -705,17 +705,17 @@ Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * p p->pPars = pPars; p->dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); p->ddG = Cudd_Init( Aig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); - p->ddR = Cudd_Init( Aig_ManPiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + p->ddR = Cudd_Init( Aig_ManCiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT ); Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT ); p->vRings = Vec_PtrAlloc( 100 ); // create leaves - p->vLeaves = Vec_PtrAlloc( Aig_ManPiNum(pAig) ); + p->vLeaves = Vec_PtrAlloc( Aig_ManCiNum(pAig) ); Aig_ManForEachCi( pAig, pObj, i ) Vec_PtrPush( p->vLeaves, pObj ); // create roots - p->vRoots = Vec_PtrAlloc( Aig_ManPoNum(pAig) ); + p->vRoots = Vec_PtrAlloc( Aig_ManCoNum(pAig) ); Saig_ManForEachLi( pAig, pObj, i ) Vec_PtrPush( p->vRoots, pObj ); // variables to quantify diff --git a/src/proof/llb/llb4Cex.c b/src/proof/llb/llb4Cex.c index 69ba6ab1..b5bdb36e 100644 --- a/src/proof/llb/llb4Cex.c +++ b/src/proof/llb/llb4Cex.c @@ -63,7 +63,7 @@ Abc_Cex_t * Llb4_Nonlin4TransformCex( Aig_Man_t * pAig, Vec_Ptr_t * vStates, int */ // derive SAT solver nRegs = Aig_ManRegNum(pAig); pAig->nRegs = 0; - pCnf = Cnf_Derive( pAig, Aig_ManPoNum(pAig) ); + pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); pAig->nRegs = nRegs; // Cnf_DataTranformPolarity( pCnf, 0 ); // convert into SAT solver @@ -249,11 +249,11 @@ Vec_Ptr_t * Llb4_Nonlin4VerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ) } */ assert( iBit == p->nBits ); -// if ( Aig_ManPo(pAig, p->iPo)->fMarkB == 0 ) +// if ( Aig_ManCo(pAig, p->iPo)->fMarkB == 0 ) // Vec_PtrFreeP( &vStates ); for ( i = Saig_ManPoNum(pAig) - 1; i >= 0; i-- ) { - if ( Aig_ManPo(pAig, i)->fMarkB ) + if ( Aig_ManCo(pAig, i)->fMarkB ) { p->iPo = i; break; diff --git a/src/proof/llb/llb4Cluster.c b/src/proof/llb/llb4Cluster.c index c151a618..7e325597 100644 --- a/src/proof/llb/llb4Cluster.c +++ b/src/proof/llb/llb4Cluster.c @@ -49,7 +49,7 @@ void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * v return; Aig_ObjSetTravIdCurrent( pAig, pObj ); assert( Llb_ObjBddVar(vOrder, pObj) < 0 ); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ ); return; @@ -152,11 +152,11 @@ DdNode * Llb_Nonlin4FindPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_In DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar; if ( Aig_ObjIsConst1(pObj) ) return Cudd_ReadOne(dd); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); if ( pObj->pData ) return (DdNode *)pObj->pData; - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { bBdd0 = Cudd_NotCond( Llb_Nonlin4FindPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) ); bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 ); Cudd_Ref( bPart ); diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c index 31f94acf..af8dad75 100644 --- a/src/proof/llb/llb4Nonlin.c +++ b/src/proof/llb/llb4Nonlin.c @@ -84,7 +84,7 @@ DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vO Aig_ManForEachCi( pAig, pObj, i ) pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); // compute internal nodes - vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vPos), Saig_ManPoNum(pAig) ); + vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vCos), Saig_ManPoNum(pAig) ); Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i ) { if ( !Aig_ObjIsNode(pObj) ) @@ -273,7 +273,7 @@ void Llb_Nonlin4CreateOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * return; Aig_ObjSetTravIdCurrent( pAig, pObj ); assert( Llb_ObjBddVar(vOrder, pObj) < 0 ); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { // if ( Saig_ObjIsLo(pAig, pObj) ) // Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), (*pCounter)++ ); @@ -371,7 +371,7 @@ printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) ); // Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), Counter++ ); Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); } - assert( Counter <= Aig_ManPiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) ); + assert( Counter <= Aig_ManCiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) ); Aig_ManCleanMarkA( pAig ); Vec_IntFreeP( &vNodes ); return vOrder; diff --git a/src/proof/llb/llb4Sweep.c b/src/proof/llb/llb4Sweep.c index 292fb176..6b223ab9 100644 --- a/src/proof/llb/llb4Sweep.c +++ b/src/proof/llb/llb4Sweep.c @@ -49,7 +49,7 @@ void Llb_Nonlin4SweepOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * return; Aig_ObjSetTravIdCurrent( pAig, pObj ); assert( Llb_ObjBddVar(vOrder, pObj) < 0 ); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ ); return; @@ -102,7 +102,7 @@ Vec_Int_t * Llb_Nonlin4SweepOrder( Aig_Man_t * pAig, int * pCounter, int fSaveAl Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ ); // assert( Counter == Aig_ManObjNum(pAig) - 1 ); // no dangling nodes if ( pCounter ) - *pCounter = Counter - Aig_ManPiNum(pAig) - Aig_ManPoNum(pAig); + *pCounter = Counter - Aig_ManCiNum(pAig) - Aig_ManCoNum(pAig); return vOrder; } @@ -211,11 +211,11 @@ DdNode * Llb_Nonlin4SweepPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_I DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar; if ( Aig_ObjIsConst1(pObj) ) return Cudd_ReadOne(dd); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ); if ( pObj->pData ) return (DdNode *)pObj->pData; - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { bBdd0 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) ); bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 ); Cudd_Ref( bPart ); @@ -535,9 +535,9 @@ void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nSweepMax, int nClusterMax, DdMana assert( Counter == nCutPoints ); Aig_ManCleanMarkA( pAig ); // compute the BAD states - ddBad = Llb4_Nonlin4SweepBadStates( pAig, vOrder, nCutPoints + Aig_ManPiNum(pAig) + Aig_ManPoNum(pAig) ); + ddBad = Llb4_Nonlin4SweepBadStates( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig) ); // compute the clusters - ddWork = Llb4_Nonlin4SweepGroups( pAig, vOrder, nCutPoints + Aig_ManPiNum(pAig) + Aig_ManPoNum(pAig), &vGroups, nClusterMax, fVerbose ); + ddWork = Llb4_Nonlin4SweepGroups( pAig, vOrder, nCutPoints + Aig_ManCiNum(pAig) + Aig_ManCoNum(pAig), &vGroups, nClusterMax, fVerbose ); // transfer the result from the Bad manager //printf( "Bad before = %d.\n", Cudd_DagSize(ddBad->bFunc) ); ddWork->bFunc = Cudd_bddTransfer( ddBad, ddWork, ddBad->bFunc ); Cudd_Ref( ddWork->bFunc ); diff --git a/src/proof/pdr/pdrClass.c b/src/proof/pdr/pdrClass.c index cbe5e1c2..5dd4c4a9 100644 --- a/src/proof/pdr/pdrClass.c +++ b/src/proof/pdr/pdrClass.c @@ -202,7 +202,7 @@ void Pdr_ManEquivClasses( Aig_Man_t * pAig ) // report the result Abc_Print( 1, "F =%4d : Total = %6d. Nodes = %6d. RedRegs = %6d. Prop = %s\n", f+1, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pTemp), Pdr_ManCountMap(vMap), - Aig_ObjChild0(Aig_ManPo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" ); + Aig_ObjChild0(Aig_ManCo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" ); // recreate the map Pdr_ManPrintMap( vMap ); Vec_IntFree( vMap ); diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c index fddd292b..fcad15e0 100644 --- a/src/proof/pdr/pdrCnf.c +++ b/src/proof/pdr/pdrCnf.c @@ -114,7 +114,7 @@ int Pdr_ObjSatVar2( Pdr_Man_t * p, int k, Aig_Obj_t * pObj ) if ( nVarCount == Vec_IntSize(vVar2Ids) ) return iVarThis; assert( nVarCount + 1 == Vec_IntSize(vVar2Ids) ); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) return iVarThis; nClauses = p->pCnf2->pObj2Count[Aig_ObjId(pObj)]; iFirstClause = p->pCnf2->pObj2Clause[Aig_ObjId(pObj)]; @@ -269,8 +269,8 @@ static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p, if ( p->pCnf1 == NULL ) { int nRegs = p->pAig->nRegs; - p->pAig->nRegs = Aig_ManPoNum(p->pAig); - p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManPoNum(p->pAig) ); + p->pAig->nRegs = Aig_ManCoNum(p->pAig); + p->pCnf1 = Cnf_Derive( p->pAig, Aig_ManCoNum(p->pAig) ); p->pAig->nRegs = nRegs; assert( p->vVar2Reg == NULL ); p->vVar2Reg = Vec_IntStartFull( p->pCnf1->nVars ); diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index c191654a..de661905 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -55,7 +55,7 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k ) Vec_VecExpand( p->vClauses, k ); Vec_IntPush( p->vActVars, 0 ); // add property cone - Pdr_ObjSatVar( p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) ); + Pdr_ObjSatVar( p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) ); return pSat; } @@ -175,7 +175,7 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k ) sat_solver * pSat; int Lit, RetValue; pSat = Pdr_ManSolver(p, k); - Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal + Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 ); assert( RetValue == 1 ); sat_solver_compress( pSat ); @@ -278,7 +278,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr if ( pCube == NULL ) // solve the property { clk = clock(); - Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails) + Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails) RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 ); if ( RetValue == l_Undef ) return -1; diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 428c20c7..0547c308 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -81,13 +81,13 @@ void Pdr_ManCollectCone_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vCi if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) return; Aig_ObjSetTravIdCurrent(pAig, pObj); - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { Vec_IntPush( vCiObjs, Aig_ObjId(pObj) ); return; } Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin0(pObj), vCiObjs, vNodes ); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) return; Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin1(pObj), vCiObjs, vNodes ); Vec_IntPush( vNodes, Aig_ObjId(pObj) ); @@ -133,7 +133,7 @@ int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj ) Value0 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin0(pObj) ); if ( Aig_ObjFaninC0(pObj) ) Value0 = Pdr_ManSimInfoNot( Value0 ); - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { Pdr_ManSimInfoSet( pAig, pObj, Value0 ); return Value0; @@ -228,7 +228,7 @@ int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec assert( Value2 == PDR_UND ); Vec_IntPush( vUndo, Aig_ObjId(pFanout) ); Vec_IntPush( vUndo, Value ); - if ( Aig_ObjIsPo(pFanout) ) + if ( Aig_ObjIsCo(pFanout) ) return 0; assert( Aig_ObjIsNode(pFanout) ); Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) ); @@ -318,8 +318,8 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals { Aig_Obj_t * pObj; int i; - char * pBuff = ABC_ALLOC( char, Aig_ManPiNum(pAig)+1 ); - for ( i = 0; i < Aig_ManPiNum(pAig); i++ ) + char * pBuff = ABC_ALLOC( char, Aig_ManCiNum(pAig)+1 ); + for ( i = 0; i < Aig_ManCiNum(pAig); i++ ) pBuff[i] = '-'; pBuff[i] = 0; Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i ) @@ -368,7 +368,7 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube ) // collect CO objects Vec_IntClear( vCoObjs ); if ( pCube == NULL ) // the target is the property output - Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManPo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); + Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); else // the target is the cube { for ( i = 0; i < pCube->nLits; i++ ) diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c index 97261a7f..9a2cffb2 100644 --- a/src/proof/pdr/pdrUtil.c +++ b/src/proof/pdr/pdrUtil.c @@ -613,7 +613,7 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd return ((int)pNode->fMarkA == Value); Aig_ObjSetTravIdCurrent(pAig, pNode); pNode->fMarkA = Value; - if ( Aig_ObjIsPi(pNode) ) + if ( Aig_ObjIsCi(pNode) ) { // if ( vSuppLits ) // Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) ); diff --git a/src/proof/ssw/sswAig.c b/src/proof/ssw/sswAig.c index 5cdced62..cd0f0c7a 100644 --- a/src/proof/ssw/sswAig.c +++ b/src/proof/ssw/sswAig.c @@ -148,7 +148,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p ) int i, f, iLits; assert( p->pFrames == NULL ); assert( Aig_ManRegNum(p->pAig) > 0 ); - assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) ); p->nConstrTotal = p->nConstrReduced = 0; // start the fraig package @@ -216,7 +216,7 @@ Aig_Man_t * Ssw_SpeculativeReduction( Ssw_Man_t * p ) int i; assert( p->pFrames == NULL ); assert( Aig_ManRegNum(p->pAig) > 0 ); - assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) ); p->nConstrTotal = p->nConstrReduced = 0; // start the fraig package diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c index 0eabaa92..b2920177 100644 --- a/src/proof/ssw/sswBmc.c +++ b/src/proof/ssw/sswBmc.c @@ -51,7 +51,7 @@ Aig_Obj_t * Ssw_BmcUnroll_rec( Ssw_Frm_t * pFrm, Aig_Obj_t * pObj, int f ) pRes = Aig_ManConst1( pFrm->pFrames ); else if ( Saig_ObjIsPi(pFrm->pAig, pObj) ) pRes = Aig_ObjCreateCi( pFrm->pFrames ); - else if ( Aig_ObjIsPo(pObj) ) + else if ( Aig_ObjIsCo(pObj) ) { Ssw_BmcUnroll_rec( pFrm, Aig_ObjFanin0(pObj), f ); pRes = Ssw_ObjChild0Fra_( pFrm, pObj, f ); diff --git a/src/proof/ssw/sswClass.c b/src/proof/ssw/sswClass.c index 95f029d4..581b8aed 100644 --- a/src/proof/ssw/sswClass.c +++ b/src/proof/ssw/sswClass.c @@ -642,7 +642,7 @@ clk = clock(); } else { - if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) ) + if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) ) continue; // skip the node with more that the given number of levels if ( nMaxLevs && (int)pObj->Level > nMaxLevs ) diff --git a/src/proof/ssw/sswCnf.c b/src/proof/ssw/sswCnf.c index 1970c62f..e3b422d5 100644 --- a/src/proof/ssw/sswCnf.c +++ b/src/proof/ssw/sswCnf.c @@ -276,7 +276,7 @@ void Ssw_AddClausesSuper( Ssw_Sat_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper ) void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) { // if the new node is complemented or a PI, another gate begins - if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || + if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || (fUseMuxes && Aig_ObjIsMuxType(pObj)) ) { @@ -303,7 +303,7 @@ void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) { assert( !Aig_IsComplement(pObj) ); - assert( !Aig_ObjIsPi(pObj) ); + assert( !Aig_ObjIsCi(pObj) ); Vec_PtrClear( vSuper ); Ssw_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); } @@ -329,7 +329,7 @@ void Ssw_ObjAddToFrontier( Ssw_Sat_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie return; // pObj->fMarkA = 1; // save PIs (used by register correspondence) - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) Vec_PtrPush( p->vUsedPis, pObj ); Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ ); sat_solver_setnvars( p->pSat, 100 * (1 + p->nSatVars / 100) ); @@ -408,7 +408,7 @@ int Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObj ) return sat_solver_var_value( p->pSat, nVarNum ); // if ( pObj->fMarkA == 1 ) // return 0; - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) return 0; assert( Aig_ObjIsNode(pObj) ); Value0 = Ssw_CnfGetNodeValue( p, Aig_ObjFanin0(pObj) ); diff --git a/src/proof/ssw/sswConstr.c b/src/proof/ssw/sswConstr.c index 6d8a152d..82977edb 100644 --- a/src/proof/ssw/sswConstr.c +++ b/src/proof/ssw/sswConstr.c @@ -51,7 +51,7 @@ Aig_Man_t * Ssw_FramesWithConstraints( Aig_Man_t * p, int nFrames ) int i, f; assert( Saig_ManConstrNum(p) > 0 ); assert( Aig_ManRegNum(p) > 0 ); - assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) ); + assert( Aig_ManRegNum(p) < Aig_ManCiNum(p) ); // start the fraig package pFrames = Aig_ManStart( Aig_ManObjNumMax(p) * nFrames ); // create latches for the first frame @@ -165,7 +165,7 @@ int Ssw_ManSetConstrPhases_( Aig_Man_t * p, int nFrames, Vec_Int_t ** pvInits ) assert( p->nConstrs > 0 ); // create CNF nRegs = p->nRegs; p->nRegs = 0; - pCnf = Cnf_Derive( p, Aig_ManPoNum(p) ); + pCnf = Cnf_Derive( p, Aig_ManCoNum(p) ); p->nRegs = nRegs; // create SAT solver pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 ); @@ -626,18 +626,18 @@ clk = clock(); // create timeframes p->pFrames = Ssw_FramesWithClasses( p ); // add constants - nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig); + nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig); assert( (nConstrPairs & 1) == 0 ); for ( i = 0; i < nConstrPairs; i += 2 ) { - pObj = Aig_ManPo( p->pFrames, i ); - pObj2 = Aig_ManPo( p->pFrames, i+1 ); + pObj = Aig_ManCo( p->pFrames, i ); + pObj2 = Aig_ManCo( p->pFrames, i+1 ); Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) ); } // build logic cones for register inputs for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) { - pObj = Aig_ManPo( p->pFrames, nConstrPairs + i ); + pObj = Aig_ManCo( p->pFrames, nConstrPairs + i ); Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );// } diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c index df48a5b8..c51d421c 100644 --- a/src/proof/ssw/sswCore.c +++ b/src/proof/ssw/sswCore.c @@ -191,13 +191,13 @@ void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose ) Aig_Obj_t * pObj; int i, nTotal = 0, nRemoved = 0; // collect the nodes in the cone of constraints - pArray = (Aig_Obj_t **)Vec_PtrArray(pAig->vPos); + pArray = (Aig_Obj_t **)Vec_PtrArray(pAig->vCos); pArray += Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig); vCones = Aig_ManDfsNodes( pAig, pArray, Saig_ManConstrNum(pAig) ); // remove all the node that are equiv to something and are in the cones Aig_ManForEachObj( pAig, pObj, i ) { - if ( !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) ) + if ( !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) ) continue; if ( pAig->pReprs[i] != NULL ) nTotal++; @@ -213,7 +213,7 @@ void Ssw_ManUpdateEquivs( Ssw_Man_t * p, Aig_Man_t * pAig, int fVerbose ) } } // collect statistics - p->nConesTotal = Aig_ManPiNum(pAig) + Aig_ManNodeNum(pAig); + p->nConesTotal = Aig_ManCiNum(pAig) + Aig_ManNodeNum(pAig); p->nConesConstr = Vec_PtrSize(vCones); p->nEquivsTotal = nTotal; p->nEquivsConstr = nRemoved; @@ -341,7 +341,7 @@ clk = clock(); printf( "R =%4d. ", p->nRecycles-nRecycles ); } printf( "F =%5d. %s ", p->nSatFailsReal-nSatFailsReal, - (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManPo(p->pAig,0))))? "+" : "-" ); + (Saig_ManPoNum(p->pAig)==1 && Ssw_ObjIsConst1Cand(p->pAig,Aig_ObjFanin0(Aig_ManCo(p->pAig,0))))? "+" : "-" ); ABC_PRT( "T", clock() - clk ); } // if ( p->pPars->fDynamic && p->nSatCallsSat-nSatCallsSat < 100 ) diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c index 0f6002fa..f20a7b78 100644 --- a/src/proof/ssw/sswDyn.c +++ b/src/proof/ssw/sswDyn.c @@ -54,7 +54,7 @@ void Ssw_ManLabelPiNodes( Ssw_Man_t * p ) Saig_ManForEachPi( p->pAig, pObj, i ) { pObjFrames = Ssw_ObjFrame( p, pObj, f ); - assert( Aig_ObjIsPi(pObjFrames) ); + assert( Aig_ObjIsCi(pObjFrames) ); assert( pObjFrames->fMarkB == 0 ); pObjFrames->fMarkA = 1; pObjFrames->fMarkB = 1; @@ -79,7 +79,7 @@ void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis ) if ( pObj->fMarkA ) return; pObj->fMarkA = 1; - if ( Aig_ObjIsPi(pObj) ) + if ( Aig_ObjIsCi(pObj) ) { Vec_PtrPush( vNewPis, pObj ); return; @@ -110,10 +110,10 @@ void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos pObj->fMarkB = 1; if ( pObj->Id > p->nSRMiterMaxId ) return; - if ( Aig_ObjIsPo(pObj) ) + if ( Aig_ObjIsCo(pObj) ) { // skip if it is a register input PO - if ( Aig_ObjPioNum(pObj) >= Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig) ) + if ( Aig_ObjPioNum(pObj) >= Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig) ) return; // add the number of this constraint Vec_IntPush( vNewPos, Aig_ObjPioNum(pObj)/2 ); @@ -180,8 +180,8 @@ void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj ) // check if the corresponding pairs are added Vec_IntForEachEntry( p->vNewPos, iConstr, i ) { - pObj0 = Aig_ManPo( p->pFrames, 2*iConstr ); - pObj1 = Aig_ManPo( p->pFrames, 2*iConstr+1 ); + pObj0 = Aig_ManCo( p->pFrames, 2*iConstr ); + pObj1 = Aig_ManCo( p->pFrames, 2*iConstr+1 ); // if ( pObj0->fMarkB && pObj1->fMarkB ) if ( pObj0->fMarkB || pObj1->fMarkB ) { @@ -224,7 +224,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) continue; } assert( !Aig_IsComplement(pObjFraig) ); - assert( Aig_ObjIsPi(pObjFraig) ); + assert( Aig_ObjIsCi(pObjFraig) ); pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 ); } @@ -235,7 +235,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p ) { pObjFraig = Ssw_ObjFrame( p, pObj, f ); assert( !Aig_IsComplement(pObjFraig) ); - assert( Aig_ObjIsPi(pObjFraig) ); + assert( Aig_ObjIsCi(pObjFraig) ); pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f ); } @@ -393,7 +393,7 @@ p->timeReduce += clock() - clk; // prepare simulation info assert( p->vSimInfo == NULL ); - p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 ); + p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 ); Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 ); // sweep internal nodes diff --git a/src/proof/ssw/sswFilter.c b/src/proof/ssw/sswFilter.c index 536316ff..5f467123 100644 --- a/src/proof/ssw/sswFilter.c +++ b/src/proof/ssw/sswFilter.c @@ -162,7 +162,7 @@ void Ssw_ManFindStartingState( Ssw_Man_t * p, Abc_Cex_t * pCex ) } assert( iBit == pCex->nBits ); // check that the output failed as expected -- cannot check because it is not an SRM! -// pObj = Aig_ManPo( p->pAig, pCex->iPo ); +// pObj = Aig_ManCo( p->pAig, pCex->iPo ); // if ( pObj->fMarkB != 1 ) // printf( "The counter-example does not refine the output.\n" ); // record the new pattern diff --git a/src/proof/ssw/sswIslands.c b/src/proof/ssw/sswIslands.c index 3173ec6f..8f54432d 100644 --- a/src/proof/ssw/sswIslands.c +++ b/src/proof/ssw/sswIslands.c @@ -85,14 +85,14 @@ void Ssw_MatchingStart( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_t * vPairs ) // make sure PIs are matched Saig_ManForEachPi( p0, pObj0, i ) { - pObj1 = Aig_ManPi( p1, i ); + pObj1 = Aig_ManCi( p1, i ); assert( pObj0->pData == pObj1 ); assert( pObj1->pData == pObj0 ); } // make sure the POs are not matched Aig_ManForEachCo( p0, pObj0, i ) { - pObj1 = Aig_ManPo( p1, i ); + pObj1 = Aig_ManCo( p1, i ); assert( pObj0->pData == NULL ); assert( pObj1->pData == NULL ); } @@ -135,7 +135,7 @@ void Ssw_MatchingExtendOne( 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 ( pObj->pData != NULL ) continue; @@ -196,7 +196,7 @@ int Ssw_MatchingCountUnmached( 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 ( pObj->pData != NULL ) continue; @@ -230,8 +230,8 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose int nUnmached = Ssw_MatchingCountUnmached(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++ ) { @@ -263,8 +263,8 @@ void Ssw_MatchingExtend( Aig_Man_t * p0, Aig_Man_t * p1, int nDist, int fVerbose { int nUnmached = Ssw_MatchingCountUnmached(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 ); @@ -335,15 +335,15 @@ Vec_Int_t * Ssw_MatchingPairs( Aig_Man_t * p0, Aig_Man_t * p1 ) Aig_Obj_t * pObj0, * pObj1; int i; // check correctness - 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) ); assert( Aig_ManRegNum(p0) == Aig_ManRegNum(p1) ); assert( Aig_ManObjNum(p0) == Aig_ManObjNum(p1) ); // create complete pairs vPairsNew = Vec_IntAlloc( 2*Aig_ManObjNum(p0) ); Aig_ManForEachObj( p0, pObj0, i ) { - if ( Aig_ObjIsPo(pObj0) ) + if ( Aig_ObjIsCo(pObj0) ) continue; pObj1 = (Aig_Obj_t *)pObj0->pData; Vec_IntPush( vPairsNew, pObj0->Id ); @@ -390,7 +390,7 @@ Vec_Int_t * Ssw_MatchingMiter( Aig_Man_t * pMiter, Aig_Man_t * p0, Aig_Man_t * p assert( !Aig_IsComplement(pObj0) ); assert( !Aig_IsComplement(pObj1) ); assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) ); - if ( Aig_ObjIsPo(pObj0) ) + if ( Aig_ObjIsCo(pObj0) ) continue; assert( Aig_ObjIsNode(pObj0) || Saig_ObjIsLo(pMiter, pObj0) ); assert( Aig_ObjIsNode(pObj1) || Saig_ObjIsLo(pMiter, pObj1) ); @@ -519,7 +519,7 @@ Vec_Int_t * Saig_StrSimPerformMatching_hack( Aig_Man_t * p0, Aig_Man_t * p1 ) vPairs = Vec_IntAlloc( 100 ); Aig_ManForEachObj( p0, pObj, i ) { - if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsPi(pObj) && !Aig_ObjIsNode(pObj) ) + if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) ) continue; Vec_IntPush( vPairs, i ); Vec_IntPush( vPairs, i ); diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c index c41a74ef..ec6087f0 100644 --- a/src/proof/ssw/sswLcorr.c +++ b/src/proof/ssw/sswLcorr.c @@ -58,7 +58,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p ) continue; } assert( !Aig_IsComplement(pObjFraig) ); - assert( Aig_ObjIsPi(pObjFraig) ); + assert( Aig_ObjIsCi(pObjFraig) ); pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) ); Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 ); } @@ -160,8 +160,8 @@ void Ssw_ManSweepLatchOne( Ssw_Man_t * p, Aig_Obj_t * pObjRepr, Aig_Obj_t * pObj { Aig_Obj_t * pObjFraig, * pObjReprFraig, * pObjLi; int RetValue, clk; - assert( Aig_ObjIsPi(pObj) ); - assert( Aig_ObjIsPi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) ); + assert( Aig_ObjIsCi(pObj) ); + assert( Aig_ObjIsCi(pObjRepr) || Aig_ObjIsConst1(pObjRepr) ); // check if it makes sense to skip some calls if ( p->nCallsCount > 100 && p->nCallsUnsat < p->nCallsSat ) { @@ -175,7 +175,7 @@ clk = clock(); Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) ); pObjFraig = Ssw_ObjChild0Fra( p, pObjLi, 0 ); // get the fraiged representative - if ( Aig_ObjIsPi(pObjRepr) ) + if ( Aig_ObjIsCi(pObjRepr) ) { pObjLi = Saig_ObjLoToLi( p->pAig, pObjRepr ); Ssw_ManBuildCone_rec( p, Aig_ObjFanin0(pObjLi) ); @@ -264,7 +264,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p ) // prepare simulation info assert( p->vSimInfo == NULL ); - p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 ); + p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManCiNum(p->pFrames), 1 ); Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 ); // go through the registers diff --git a/src/proof/ssw/sswPairs.c b/src/proof/ssw/sswPairs.c index 0aba942f..e356aa60 100644 --- a/src/proof/ssw/sswPairs.c +++ b/src/proof/ssw/sswPairs.c @@ -64,7 +64,7 @@ int Ssw_MiterStatus( Aig_Man_t * p, int fVerbose ) continue; } // check if the output is a primary input - if ( p->nRegs == 0 && Aig_ObjIsPi(Aig_Regular(pChild)) ) + if ( p->nRegs == 0 && Aig_ObjIsCi(Aig_Regular(pChild)) ) { CountNonConst0++; continue; diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c index d2f07dc8..5a3aea10 100644 --- a/src/proof/ssw/sswPart.c +++ b/src/proof/ssw/sswPart.c @@ -90,7 +90,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL ); Ioa_WriteAiger( pTemp, Buffer, 0, 0 ); printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", - i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) ); + i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) ); Aig_ManStop( pTemp ); } } @@ -110,7 +110,7 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars ) nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack ); if ( fVerbose ) printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", - i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses ); + i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses ); Aig_ManStop( pNew ); } Aig_ManStop( pTemp ); diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index 6e36ae12..445dda84 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -831,7 +831,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex } assert( iBit == pCex->nBits ); // check that the output failed as expected -- cannot check because it is not an SRM! -// pObj = Aig_ManPo( pAig, pCex->iPo ); +// pObj = Aig_ManCo( pAig, pCex->iPo ); // if ( pObj->fMarkB != 1 ) // printf( "The counter-example does not refine the output.\n" ); // record the new pattern diff --git a/src/proof/ssw/sswRarity2.c b/src/proof/ssw/sswRarity2.c index dce7ac3e..0851cf3d 100644 --- a/src/proof/ssw/sswRarity2.c +++ b/src/proof/ssw/sswRarity2.c @@ -282,7 +282,7 @@ static Vec_Int_t * Ssw_RarFindStartingState( Aig_Man_t * pAig, Abc_Cex_t * pCex } assert( iBit == pCex->nBits ); // check that the output failed as expected -- cannot check because it is not an SRM! -// pObj = Aig_ManPo( pAig, pCex->iPo ); +// pObj = Aig_ManCo( pAig, pCex->iPo ); // if ( pObj->fMarkB != 1 ) // printf( "The counter-example does not refine the output.\n" ); // record the new pattern diff --git a/src/proof/ssw/sswSim.c b/src/proof/ssw/sswSim.c index 946224cd..b53e8baf 100644 --- a/src/proof/ssw/sswSim.c +++ b/src/proof/ssw/sswSim.c @@ -457,13 +457,13 @@ int * Ssw_SmlCheckOutputSavePattern( Ssw_Sml_t * p, Aig_Obj_t * pObjPo ) // determine the best pattern BestPat = i * 32 + k; // fill in the counter-example data - pModel = ABC_ALLOC( int, Aig_ManPiNum(p->pAig)+1 ); + pModel = ABC_ALLOC( int, Aig_ManCiNum(p->pAig)+1 ); Aig_ManForEachCi( p->pAig, pObjPi, i ) { pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat); // printf( "%d", pModel[i] ); } - pModel[Aig_ManPiNum(p->pAig)] = pObjPo->Id; + pModel[Aig_ManCiNum(p->pAig)] = pObjPo->Id; // printf( "\n" ); return pModel; } @@ -484,7 +484,7 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p ) Aig_Obj_t * pObj; int i; // make sure the reference simulation pattern does not detect the bug - pObj = Aig_ManPo( p->pAig, 0 ); + pObj = Aig_ManCo( p->pAig, 0 ); assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); Aig_ManForEachCo( p->pAig, pObj, i ) { @@ -514,7 +514,7 @@ void Ssw_SmlAssignRandom( Ssw_Sml_t * p, Aig_Obj_t * pObj ) { unsigned * pSims; int i, f; - assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsCi(pObj) ); pSims = Ssw_ObjSim( p, pObj->Id ); for ( i = 0; i < p->nWordsTotal; i++ ) pSims[i] = Ssw_ObjRandomSim(); @@ -540,7 +540,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) unsigned * pSims; int i; assert( iFrame < p->nFrames ); - assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsCi(pObj) ); pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; for ( i = 0; i < p->nWordsFrame; i++ ) pSims[i] = Ssw_ObjRandomSim(); @@ -562,7 +562,7 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF unsigned * pSims; int i; assert( iFrame < p->nFrames ); - assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsCi(pObj) ); pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; for ( i = 0; i < p->nWordsFrame; i++ ) pSims[i] = fConst1? ~(unsigned)0 : 0; @@ -584,7 +584,7 @@ void Ssw_SmlObjAssignConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, in unsigned * pSims; assert( iFrame < p->nFrames ); assert( iWord < p->nWordsFrame ); - assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsCi(pObj) ); pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; pSims[iWord] = fConst1? ~(unsigned)0 : 0; } @@ -604,7 +604,7 @@ void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWor { unsigned * pSims; assert( iFrame < p->nFrames ); - assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsCi(pObj) ); pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame; pSims[iWord] = Word; } @@ -631,16 +631,16 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat ) Aig_ManForEachCi( p->pAig, pObj, i ) Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 ); // flip one bit - Limit = Abc_MinInt( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 ); + Limit = Abc_MinInt( Aig_ManCiNum(p->pAig), p->nWordsTotal * 32 - 1 ); for ( i = 0; i < Limit; i++ ) - Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 ); + Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig,i)->Id ), i+1 ); } else { int fUseDist1 = 0; // copy the PI info for each frame - nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig); + nTruePis = Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig); for ( f = 0; f < p->nFrames; f++ ) Saig_ManForEachPi( p->pAig, pObj, i ) Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f ); @@ -648,14 +648,14 @@ void Ssw_SmlAssignDist1( Ssw_Sml_t * p, unsigned * pPat ) k = 0; Saig_ManForEachLo( p->pAig, pObj, i ) Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 ); -// assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pFrames) ); +// assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManCiNum(p->pFrames) ); // flip one bit of the last frame if ( fUseDist1 ) //&& p->nFrames == 2 ) { Limit = Abc_MinInt( nTruePis, p->nWordsFrame * 32 - 1 ); for ( i = 0; i < Limit; i++ ) - Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 ); + Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 ); } } } @@ -684,7 +684,7 @@ void Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat ) // set distance one PIs for the first frame Limit = Abc_MinInt( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 ); for ( i = 0; i < Limit; i++ ) - Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 ); + Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ), i+1 ); // create random info for the remaining timeframes for ( f = 1; f < p->nFrames; f++ ) @@ -806,7 +806,7 @@ void Ssw_SmlNodeCopyFanin( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame ) int fCompl, fCompl0, i; assert( iFrame < p->nFrames ); assert( !Aig_IsComplement(pObj) ); - assert( Aig_ObjIsPo(pObj) ); + assert( Aig_ObjIsCo(pObj) ); assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal ); // get hold of the simulation information pSims = Ssw_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame; @@ -841,8 +841,8 @@ void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, assert( iFrame < p->nFrames ); assert( !Aig_IsComplement(pOut) ); assert( !Aig_IsComplement(pIn) ); - assert( Aig_ObjIsPo(pOut) ); - assert( Aig_ObjIsPi(pIn) ); + assert( Aig_ObjIsCo(pOut) ); + assert( Aig_ObjIsCi(pIn) ); assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal ); // get hold of the simulation information pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame; @@ -869,8 +869,8 @@ void Ssw_SmlNodeTransferFirst( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn int i; assert( !Aig_IsComplement(pOut) ); assert( !Aig_IsComplement(pIn) ); - assert( Aig_ObjIsPo(pOut) ); - assert( Aig_ObjIsPi(pIn) ); + assert( Aig_ObjIsCo(pOut) ); + assert( Aig_ObjIsCi(pIn) ); assert( p->nWordsFrame < p->nWordsTotal ); // get hold of the simulation information pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * (p->nFrames-1); @@ -899,7 +899,7 @@ void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit ) if ( fInit ) { assert( Aig_ManRegNum(p->pAig) > 0 ); - assert( Aig_ManRegNum(p->pAig) <= Aig_ManPiNum(p->pAig) ); + assert( Aig_ManRegNum(p->pAig) <= Aig_ManCiNum(p->pAig) ); // assign random info for primary inputs Saig_ManForEachPi( p->pAig, pObj, i ) Ssw_SmlAssignRandom( p, pObj ); @@ -931,7 +931,7 @@ void Ssw_SmlInitializeSpecial( Ssw_Sml_t * p, Vec_Int_t * vInit ) int Entry, i, nRegs; nRegs = Aig_ManRegNum(p->pAig); assert( nRegs > 0 ); - assert( nRegs <= Aig_ManPiNum(p->pAig) ); + assert( nRegs <= Aig_ManCiNum(p->pAig) ); assert( Vec_IntSize(vInit) == nRegs * p->nWordsFrame ); // assign random info for primary inputs Saig_ManForEachPi( p->pAig, pObj, i ) @@ -957,7 +957,7 @@ void Ssw_SmlReinitialize( Ssw_Sml_t * p ) Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i; assert( Aig_ManRegNum(p->pAig) > 0 ); - assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); + assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) ); // assign random info for primary inputs Saig_ManForEachPi( p->pAig, pObj, i ) Ssw_SmlAssignRandom( p, pObj ); @@ -1361,12 +1361,12 @@ Abc_Cex_t * Ssw_SmlGetCounterExample( Ssw_Sml_t * p ) } break; } - assert( iPo < Aig_ManPoNum(p->pAig)-Aig_ManRegNum(p->pAig) ); + assert( iPo < Aig_ManCoNum(p->pAig)-Aig_ManRegNum(p->pAig) ); assert( iFrame < p->nFrames ); assert( iBit < 32 * p->nWordsFrame ); // allocate the counter example - pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 ); + pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 ); pCex->iPo = iPo; pCex->iFrame = iFrame; diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c index a3a8d1c8..550cb4ce 100644 --- a/src/proof/ssw/sswSweep.c +++ b/src/proof/ssw/sswSweep.c @@ -48,7 +48,7 @@ int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f ) int fUseNoBoundary = 0; Aig_Obj_t * pObjFraig; int Value; -// assert( Aig_ObjIsPi(pObj) ); +// assert( Aig_ObjIsCi(pObj) ); pObjFraig = Ssw_ObjFrame( p, pObj, f ); if ( fUseNoBoundary ) { @@ -86,12 +86,12 @@ void Ssw_CheckConstraints( Ssw_Man_t * p ) Aig_Obj_t * pObj, * pObj2; int nConstrPairs, i; int Counter = 0; - nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig); + nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig); assert( (nConstrPairs & 1) == 0 ); for ( i = 0; i < nConstrPairs; i += 2 ) { - pObj = Aig_ManPo( p->pFrames, i ); - pObj2 = Aig_ManPo( p->pFrames, i+1 ); + pObj = Aig_ManCo( p->pFrames, i ); + pObj2 = Aig_ManCo( p->pFrames, i+1 ); if ( Ssw_NodesAreEquiv( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) ) != 1 ) { Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) ); @@ -162,7 +162,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p ) // iterate through the PIs of the frames Vec_PtrForEachEntry( Aig_Obj_t *, p->pMSat->vUsedPis, pObj, i ) { - assert( Aig_ObjIsPi(pObj) ); + assert( Aig_ObjIsCi(pObj) ); nVarNum = Ssw_ObjSatNum( p->pMSat, pObj ); assert( nVarNum > 0 ); if ( sat_solver_var_value( p->pMSat->pSat, nVarNum ) ) @@ -373,18 +373,18 @@ clk = clock(); // create timeframes p->pFrames = Ssw_FramesWithClasses( p ); // add constants - nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig); + nConstrPairs = Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig); assert( (nConstrPairs & 1) == 0 ); for ( i = 0; i < nConstrPairs; i += 2 ) { - pObj = Aig_ManPo( p->pFrames, i ); - pObj2 = Aig_ManPo( p->pFrames, i+1 ); + pObj = Aig_ManCo( p->pFrames, i ); + pObj2 = Aig_ManCo( p->pFrames, i+1 ); Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) ); } // build logic cones for register inputs for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ ) { - pObj = Aig_ManPo( p->pFrames, nConstrPairs + i ); + pObj = Aig_ManCo( p->pFrames, nConstrPairs + i ); Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );// } sat_solver_simplify( p->pMSat->pSat ); diff --git a/src/proof/ssw/sswUnique.c b/src/proof/ssw/sswUnique.c index b5f6a853..8e989531 100644 --- a/src/proof/ssw/sswUnique.c +++ b/src/proof/ssw/sswUnique.c @@ -105,7 +105,7 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV k = 0; Vec_PtrForEachEntry( Aig_Obj_t *, p->vCommon, pTemp, i ) { - assert( Aig_ObjIsPi(pTemp) ); + assert( Aig_ObjIsCi(pTemp) ); if ( !Saig_ObjIsLo(p->pAig, pTemp) ) continue; assert( Aig_ObjPioNum(pTemp) > 0 ); |