Skip to content

A
abc
Commit f4853496 by Alan Mishchenko
Options

Adding PDR with abstraction.

parent 3fb058a3
Showing with 5 additions and 5 deletions
src/proof/pdr/pdrCore.c
...@@ -862,16 +862,16 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) ...@@ -862,16 +862,16 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
while ( 1 ) while ( 1 )
{ {
int fRefined = 0; int fRefined = 0;
if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 2 ) if ( p->pPars->fUseAbs && p->vAbsFlops == NULL && iFrame == 1 )
{ {
int i, Prio; // int i, Prio;
assert( p->vAbsFlops == NULL ); assert( p->vAbsFlops == NULL );
p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) ); p->vAbsFlops = Vec_IntStart( Saig_ManRegNum(p->pAig) );
p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) ); p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
p->vMapPpi2Ff = Vec_IntAlloc( 100 ); p->vMapPpi2Ff = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( p->vPrio, Prio, i ) // Vec_IntForEachEntry( p->vPrio, Prio, i )
if ( Prio >> p->nPrioShift ) // if ( Prio >> p->nPrioShift )
Vec_IntWriteEntry( p->vAbsFlops, i, 1 ); // Vec_IntWriteEntry( p->vAbsFlops, i, 1 );
} }
//if ( p->pPars->fUseAbs && p->vAbsFlops ) //if ( p->pPars->fUseAbs && p->vAbsFlops )
// printf( "Starting frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) ); // printf( "Starting frame %d with %d (%d) flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops), Vec_IntCountPositive(p->vPrio) );
......
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