diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 14:46:16 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 14:46:16 -0800 |
commit | 58d4012a558cbf5f6786dc9fdcadc3f1538bdbe2 (patch) | |
tree | 871796cca031fc63f082a66277cd9c2de1e71e5b /src/misc | |
parent | 9f396a0d7e652c420f4af74e4c8db06068bea862 (diff) | |
download | abc-58d4012a558cbf5f6786dc9fdcadc3f1538bdbe2.tar.gz abc-58d4012a558cbf5f6786dc9fdcadc3f1538bdbe2.tar.bz2 abc-58d4012a558cbf5f6786dc9fdcadc3f1538bdbe2.zip |
Enabling multi-output solving in 'pdr'.
Diffstat (limited to 'src/misc')
-rw-r--r-- | src/misc/util/utilCex.c | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 2f205d2e..75b99492 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -261,8 +261,9 @@ 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 =%8d nOnes =%8d (%5.2f %%)\n", - p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / (p->nBits - p->nRegs) ); + printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%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 +279,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 =%8d nOnes =%8d (%5.2f %%) nOnesIn =%8d (%5.2f %%)\n", + printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%) 1sIn =%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)) ); |