diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-29 13:34:07 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-29 13:34:07 -0800 |
| commit | c48e3c7ab43f7aac5b462b1a544d82e1be7cf9ea (patch) | |
| tree | 08cfbcd4b36063bc58360dd308e1f7f78131e6ec /src/misc | |
| parent | 661265984c6b9e32fcaece8aa361b06476756783 (diff) | |
| download | abc-c48e3c7ab43f7aac5b462b1a544d82e1be7cf9ea.tar.gz abc-c48e3c7ab43f7aac5b462b1a544d82e1be7cf9ea.tar.bz2 abc-c48e3c7ab43f7aac5b462b1a544d82e1be7cf9ea.zip | |
Counter-example analysis and optimization.
Diffstat (limited to 'src/misc')
| -rw-r--r-- | src/misc/util/utilCex.c | 19 | ||||
| -rw-r--r-- | src/misc/util/utilCex.h | 1 |
2 files changed, 20 insertions, 0 deletions
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 1bdf1276..a2226edf 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -264,6 +264,25 @@ void Abc_CexPrintStats( Abc_Cex_t * p ) printf( "CEX: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d nOnes = %5d (%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 ) +{ + int k, Counter = 0, Counter2 = 0; + if ( p == NULL ) + { + printf( "The counter example is NULL.\n" ); + return; + } + for ( k = 0; k < p->nBits; k++ ) + { + Counter += Abc_InfoHasBit(p->pData, k); + 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", + 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)) ); +} /**Function************************************************************* diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h index 646a2592..862346a1 100644 --- a/src/misc/util/utilCex.h +++ b/src/misc/util/utilCex.h @@ -64,6 +64,7 @@ extern Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew ); extern Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int iPo ); extern Abc_Cex_t * Abc_CexMerge( Abc_Cex_t * pCex, Abc_Cex_t * pPart, int iFrBeg, int iFrEnd ); extern void Abc_CexPrintStats( Abc_Cex_t * p ); +extern void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs ); extern void Abc_CexPrint( Abc_Cex_t * p ); extern void Abc_CexFreeP( Abc_Cex_t ** p ); extern void Abc_CexFree( Abc_Cex_t * p ); |