From 1332dc419fb65f74a1547d937a52d52d33f9b69c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 22 Oct 2015 11:45:23 -0700 Subject: Minor tuning in 'satclp'. --- src/sat/bmc/bmcClp.c | 28 ++++++++++++++++++---------- 1 file changed, 18 insertions(+), 10 deletions(-) (limited to 'src/sat') 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] ); -- cgit v1.2.3