summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/base/abci/abc.c4
-rw-r--r--src/base/abci/abcCollapse.c2
-rw-r--r--src/sat/bmc/bmcClp.c28
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] );