diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-30 11:38:05 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-30 11:38:05 -0800 |
| commit | f1a52889047dd2fc55df14dc9b5cce2c90884328 (patch) | |
| tree | 8ebeb072dff842ca298fc8431d747d4a7905606c /src/misc/util/utilCex.c | |
| parent | c48e3c7ab43f7aac5b462b1a544d82e1be7cf9ea (diff) | |
| download | abc-f1a52889047dd2fc55df14dc9b5cce2c90884328.tar.gz abc-f1a52889047dd2fc55df14dc9b5cce2c90884328.tar.bz2 abc-f1a52889047dd2fc55df14dc9b5cce2c90884328.zip | |
Counter-example analysis and optimization.
Diffstat (limited to 'src/misc/util/utilCex.c')
| -rw-r--r-- | src/misc/util/utilCex.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index a2226edf..784f8440 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -261,7 +261,7 @@ void Abc_CexPrintStats( Abc_Cex_t * p ) } for ( k = 0; k < p->nBits; k++ ) Counter += Abc_InfoHasBit(p->pData, k); - printf( "CEX: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d nOnes = %5d (%5.2f %%)\n", + printf( "CEX: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits =%8d nOnes =%8d (%5.2f %%)\n", p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / (p->nBits - p->nRegs) ); } void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs ) @@ -278,7 +278,7 @@ void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs ) if ( (k - p->nRegs) % p->nPis < nInputs ) Counter2 += Abc_InfoHasBit(p->pData, k); } - printf( "CEX: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d nOnes = %5d (%5.2f %%) nOnesIn = %5d (%5.2f %%)\n", + printf( "CEX: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits =%8d nOnes =%8d (%5.2f %%) nOnesIn =%8d (%5.2f %%)\n", p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / (p->nBits - p->nRegs), Counter2, 100.0 * Counter2 / (p->nBits - p->nRegs - (p->iFrame + 1) * (p->nPis - nInputs)) ); |