diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-22 11:45:23 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-10-22 11:45:23 -0700 |
| commit | 1332dc419fb65f74a1547d937a52d52d33f9b69c (patch) | |
| tree | 48499f6c6e603749fcac6b5522b786e8c77587ac /src/sat/bmc/bmcClp.c | |
| parent | 2c37498bfb297c00e9b5eee8472acc134d9aba73 (diff) | |
| download | abc-1332dc419fb65f74a1547d937a52d52d33f9b69c.tar.gz abc-1332dc419fb65f74a1547d937a52d52d33f9b69c.tar.bz2 abc-1332dc419fb65f74a1547d937a52d52d33f9b69c.zip | |
Minor tuning in 'satclp'.
Diffstat (limited to 'src/sat/bmc/bmcClp.c')
| -rw-r--r-- | src/sat/bmc/bmcClp.c | 28 |
1 files changed, 18 insertions, 10 deletions
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] ); |