luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Enhancing printing of counter-examples.

This commit is contained in:
Alan Mishchenko 2011-07-25 20:33:55 +07:00
parent c4dd8067fd
commit 67e84b719d
2 changed files with 33 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

35
src/misc/util/utilCex.c
View File

@ -174,6 +174,31 @@ Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int i
return pCex;
}
/**Function*************************************************************
Synopsis [Prints out the counter-example.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_CexPrintStats( Abc_Cex_t * p )
{
int k, Counter = 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);
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 );
}
/**Function*************************************************************
Synopsis [Prints out the counter-example.]
@ -188,15 +213,19 @@ Abc_Cex_t * Abc_CexDeriveFromCombModel( int * pModel, int nPis, int nRegs, int i
void Abc_CexPrint( Abc_Cex_t * p )
{
int i, f, k;
printf( "Counter-example: iPo = %d iFrame = %d nRegs = %d nPis = %d nBits = %d\n",
p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits );
if ( p == NULL )
{
printf( "The counter example is NULL.\n" );
return;
}
Abc_CexPrintStats( p );
printf( "State : " );
for ( k = 0; k < p->nRegs; k++ )
printf( "%d", Abc_InfoHasBit(p->pData, k) );
printf( "\n" );
for ( f = 0; f <= p->iFrame; f++ )
{
printf( "Frame %2d : ", f );
printf( "Frame %3d : ", f );
for ( i = 0; i < p->nPis; i++ )
printf( "%d", Abc_InfoHasBit(p->pData, k++) );
printf( "\n" );

1
src/misc/util/utilCex.h
View File

@ -61,6 +61,7 @@ extern Abc_Cex_t * Abc_CexMakeTriv( int nRegs, int nTruePis, int nTruePos, int
extern Abc_Cex_t * Abc_CexCreate( int nRegs, int nTruePis, int * pArray, int iFrame, int iPo, int fSkipRegs );
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 void Abc_CexPrintStats( Abc_Cex_t * p );
extern void Abc_CexPrint( Abc_Cex_t * p );
extern void Abc_CexFree( Abc_Cex_t * p );