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

changed how pdr -t cleans up abs flops

This commit is contained in:
Yen-Sheng Ho 2017-02-23 10:54:53 -08:00
parent d5bbf9188c
commit ca0bdde9b3
1 changed files with 15 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/proof/pdr/pdrIncr.c
View File

@ -468,6 +468,9 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
break; // keep solving
}
p->pAig->pSeqModel = pCex;
if ( p->pPars->fVerbose && p->pPars->fUseAbs )
Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
return 0; // SAT
}
p->pPars->nFailOuts++;
@ -517,6 +520,7 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
p->timeToStopOne = 0;
}
}
/*
if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
{
int i, Used;
@ -524,6 +528,17 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
if ( Used && (Vec_IntEntry(p->vPrio, i) >> p->nPrioShift) == 0 )
Vec_IntWriteEntry( p->vAbsFlops, i, 0 );
}
*/
if ( p->pPars->fUseAbs && p->vAbsFlops && !fRefined )
{
Pdr_Set_t * pSet;
int i, j, k;
Vec_IntFill( p->vAbsFlops, Vec_IntSize( p->vAbsFlops ), 0 );
Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pSet, i, j )
for ( k = 0; k < pSet->nLits; k++ )
Vec_IntWriteEntry( p->vAbsFlops, Abc_Lit2Var(pSet->Lits[k]), 1 );
}
if ( p->pPars->fVerbose )
Pdr_ManPrintProgress( p, !fRefined, Abc_Clock() - clkStart );
if ( fRefined )