diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-03-09 19:50:18 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-03-09 19:50:18 -0800 |
| commit | c46c957a0721004eb21c5f3d3f316ba1c8ab8df1 (patch) | |
| tree | ede7a13119d06c192e7da95992d503107d2f1651 /src/proof/fra/fraCec.c | |
| parent | 2c8f1a67ec9295450a72fc27cbb3ed1177945734 (diff) | |
| download | abc-c46c957a0721004eb21c5f3d3f316ba1c8ab8df1.tar.gz abc-c46c957a0721004eb21c5f3d3f316ba1c8ab8df1.tar.bz2 abc-c46c957a0721004eb21c5f3d3f316ba1c8ab8df1.zip | |
Renamed Aig_ObjIsPi/Po to be ...Ci/Co and Aig_Man(Pi/Po)Num to be ...(Ci/Co)...
Diffstat (limited to 'src/proof/fra/fraCec.c')
| -rw-r--r-- | src/proof/fra/fraCec.c | 24 |
1 files changed, 12 insertions, 12 deletions
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 ) |