diff options
| -rw-r--r-- | src/base/abci/abc.c | 4 | ||||
| -rw-r--r-- | src/base/abci/abcCollapse.c | 2 | ||||
| -rw-r--r-- | src/sat/bmc/bmcClp.c | 28 |
3 files changed, 21 insertions, 13 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 91f128b6..2a71fd7a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3177,7 +3177,7 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pNtkRes == NULL ) { Abc_Print( -1, "Collapsing has failed.\n" ); - return 1; + return 0; } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); @@ -8290,7 +8290,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( !Abc_NtkToSop(pNtk, fMode, nCubeLimit) ) { Abc_Print( -1, "Converting to SOP has failed.\n" ); - return 1; + return 0; } return 0; diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index 6c401fd2..e4bfa885 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -298,7 +298,7 @@ Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); Gia_Man_t * pGia = Abc_NtkClpOneGia( pNtk, iCo, vSupp ); if ( fVerbose ) - printf( "Output %d: \n", iCo ); + printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) ); vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); Gia_ManStop( pGia ); if ( vSop == NULL ) diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c index fff4d75f..291c6465 100644 --- a/src/sat/bmc/bmcClp.c +++ b/src/sat/bmc/bmcClp.c @@ -624,17 +624,25 @@ cleanup: vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL; if ( iCube > 1 ) Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars ); - if ( fVeryVerbose ) + } + if ( fVeryVerbose ) + { + int fProfile = 0; + printf( "Processed output with %d supp vars. ", nVars ); + if ( vRes == NULL ) + printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim ); + else + printf( "The best cover contains %d cubes.\n", iCube ); + Abc_PrintTime( 1, "Onset minterm", Time[0][0] ); + Abc_PrintTime( 1, "Onset expand ", Time[0][1] ); + Abc_PrintTime( 1, "Offset minterm", Time[1][0] ); + Abc_PrintTime( 1, "Offset expand ", Time[1][1] ); + if ( fProfile ) { - printf( "Processed output with %d supp vars and %d cubes.\n", nVars, Vec_StrSize(vRes)/(nVars +3) ); - Abc_PrintTime( 1, "Onset minterm", Time[0][0] ); - Abc_PrintTime( 1, "Onset expand ", Time[0][1] ); - Abc_PrintTime( 1, "Offset minterm", Time[1][0] ); - Abc_PrintTime( 1, "Offset expand ", Time[1][1] ); - //Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0; - //Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0; - //Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0; - //Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0; + Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0; + Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0; + Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0; + Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0; } } Vec_StrFreeP( &vSop[0] ); |