Commit a4087e45 by Alan Mishchenko

Enabling additional printouts in 'pdr'.

parent 27be3d01
...@@ -2469,6 +2469,13 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2469,6 +2469,13 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) ); printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) );
} }
} }
if ( pAbc->vStatuses )
{
int i, Entry;
Vec_IntForEachEntry( pAbc->vStatuses, Entry, i )
printf( "%d=%d ", i, Entry );
printf( "\n" );
}
return 0; return 0;
usage: usage:
...@@ -738,8 +738,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) ...@@ -738,8 +738,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pTime4Outs[p->iOutCur] == 0 && (p->vCexes == NULL || Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL) ) if ( p->pTime4Outs[p->iOutCur] == 0 && (p->vCexes == NULL || Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL) )
{ {
p->pPars->nDropOuts++; p->pPars->nDropOuts++;
if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 ); if ( p->pPars->vOutMap )
// printf( "Dropping output %d.\n", p->iOutCur ); Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
if ( p->pPars->fVerbose )
printf( "Timing out on output %d.\n", p->iOutCur );
} }
p->timeToStopOne = 0; p->timeToStopOne = 0;
} }
......
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