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

Fixing several bugs, which led to unsound results produced by 'pdr -a' with per-output timeout.

This commit is contained in:
Alan Mishchenko 2013-09-13 19:44:54 -07:00
parent a4087e45f0
commit 60fae35d36
3 changed files with 15 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/proof/pdr/pdrCore.c
View File

@ -491,8 +491,16 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
// check other frames
assert( pPred == NULL );
for ( k = pThis->iFrame; k < kMax; k++ )
if ( !Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 ) )
{
RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, 0 );
if ( RetValue == -1 )
{
Pdr_OblDeref( pThis );
return -1;
}
if ( !RetValue )
break;
}
// add new clause
if ( p->pPars->fVeryVerbose )
@ -740,8 +748,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
p->pPars->nDropOuts++;
if ( p->pPars->vOutMap )
Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
if ( p->pPars->fVerbose )
printf( "Timing out on output %d.\n", p->iOutCur );
if ( !p->pPars->fNotVerbose )
Abc_Print( 1, "Timing out on output %*d.\n", nOutDigits, p->iOutCur );
}
p->timeToStopOne = 0;
}

2
src/proof/pdr/pdrInv.c
View File

@ -336,7 +336,7 @@ void Pdr_ManVerifyInvariant( Pdr_Man_t * p )
kThis = Vec_PtrSize(p->vSolvers);
pSat = Pdr_ManCreateSolver( p, kThis );
// add the property output
Pdr_ManSetPropertyOutput( p, kThis );
// Pdr_ManSetPropertyOutput( p, kThis );
// add the clauses
Vec_PtrForEachEntry( Pdr_Set_t *, vCubes, pCube, i )
{

3
src/proof/pdr/pdrSat.c
View File

@ -185,6 +185,9 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
// skip solved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
continue;
// skip timedout outputs
if ( p->pPars->vOutMap && Vec_IntEntry(p->pPars->vOutMap, i) == -1 )
continue;
Lit = toLitCond( Pdr_ObjSatVar(p, k, 1, pObj), 1 ); // neg literal
RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue == 1 );