Commit 4aa434ad by Alan Mishchenko

Updated CEX code to handle trivial CEX of the type (Abc_Cex_t*)1.

parent 55744840
...@@ -146,6 +146,8 @@ Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew ) ...@@ -146,6 +146,8 @@ Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew )
{ {
Abc_Cex_t * pCex; Abc_Cex_t * pCex;
int i; int i;
if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
return p;
if ( nRegsNew == -1 ) if ( nRegsNew == -1 )
nRegsNew = p->nRegs; nRegsNew = p->nRegs;
pCex = Abc_CexAlloc( nRegsNew, p->nPis, p->iFrame+1 ); pCex = Abc_CexAlloc( nRegsNew, p->nPis, p->iFrame+1 );
...@@ -259,6 +261,11 @@ void Abc_CexPrintStats( Abc_Cex_t * p ) ...@@ -259,6 +261,11 @@ void Abc_CexPrintStats( Abc_Cex_t * p )
printf( "The counter example is NULL.\n" ); printf( "The counter example is NULL.\n" );
return; return;
} }
if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
{
printf( "The counter example is present but not available (pointer has value \"1\").\n" );
return;
}
for ( k = 0; k < p->nBits; k++ ) for ( k = 0; k < p->nBits; k++ )
Counter += Abc_InfoHasBit(p->pData, k); Counter += Abc_InfoHasBit(p->pData, k);
printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%)\n", printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%)\n",
...@@ -273,6 +280,11 @@ void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs ) ...@@ -273,6 +280,11 @@ void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs )
printf( "The counter example is NULL.\n" ); printf( "The counter example is NULL.\n" );
return; return;
} }
if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
{
printf( "The counter example is present but not available (pointer has value \"1\").\n" );
return;
}
for ( k = 0; k < p->nBits; k++ ) for ( k = 0; k < p->nBits; k++ )
{ {
Counter += Abc_InfoHasBit(p->pData, k); Counter += Abc_InfoHasBit(p->pData, k);
...@@ -304,6 +316,11 @@ void Abc_CexPrint( Abc_Cex_t * p ) ...@@ -304,6 +316,11 @@ void Abc_CexPrint( Abc_Cex_t * p )
printf( "The counter example is NULL.\n" ); printf( "The counter example is NULL.\n" );
return; return;
} }
if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
{
printf( "The counter example is present but not available (pointer has value \"1\").\n" );
return;
}
Abc_CexPrintStats( p ); Abc_CexPrintStats( p );
printf( "State : " ); printf( "State : " );
for ( k = 0; k < p->nRegs; k++ ) for ( k = 0; k < p->nRegs; k++ )
...@@ -350,6 +367,8 @@ void Abc_CexFreeP( Abc_Cex_t ** p ) ...@@ -350,6 +367,8 @@ void Abc_CexFreeP( Abc_Cex_t ** p )
***********************************************************************/ ***********************************************************************/
void Abc_CexFree( Abc_Cex_t * p ) void Abc_CexFree( Abc_Cex_t * p )
{ {
if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
return;
ABC_FREE( p ); ABC_FREE( p );
} }
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment