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

Enabling multi-output solving in 'pdr'.

This commit is contained in:
Alan Mishchenko 2012-12-09 17:33:44 -08:00
parent 8761942258
commit ce63869fe7
5 changed files with 18 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
src/base/abci/abcDar.c
View File

@ -2719,7 +2719,9 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
RetValue = Pdr_ManSolve( pMan, pPars );
if ( !pPars->fSilent )
{
if ( pPars->fSolveAll )
if ( RetValue == 1 )
Abc_Print( 1, "Property proved. " );
else if ( pPars->fSolveAll )
{
int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
@ -2732,9 +2734,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
}
else
{
if ( RetValue == 1 )
Abc_Print( 1, "Property proved. " );
else if ( RetValue == 0 )
if ( RetValue == 0 )
{
if ( pMan->pSeqModel == NULL )
Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" );

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

@ -590,7 +590,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
return 0; // all SAT
continue;
}
}
// try to solve this output
while ( 1 )
{
@ -624,6 +624,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
}
if ( RetValue == 0 )
{
Abc_Cex_t * pCex;
if ( fPrintClauses )
{
Abc_Print( 1, "*** Clauses after frame %d:\n", k );
@ -639,12 +640,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
return 0; // SAT
}
p->pPars->nFailOuts++;
Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",
nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
if ( p->vCexes == NULL )
p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) );
pCex = Pdr_ManDeriveCex(p);
Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCex );
Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
return 0; // all SAT
Pdr_QueueClean( p );

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

@ -182,6 +182,9 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
pSat = Pdr_ManSolver(p, k);
Saig_ManForEachPo( p->pAig, pObj, i )
{
// skip solved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
continue;
Lit = toLitCond( Pdr_ObjSatVar(p, k, pObj), 1 ); // neg literal
RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
assert( RetValue == 1 );

5
src/proof/pdr/pdrTsim.c
View File

@ -350,6 +350,7 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals
***********************************************************************/
Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
{
Pdr_Set_t * pRes;
Vec_Int_t * vPrio = p->vPrio; // priority flops (flop indices)
Vec_Int_t * vPiLits = p->vLits; // array of literals (0/1 PI values)
Vec_Int_t * vCiObjs = p->vCiObjs; // cone leaves (CI obj IDs)
@ -474,7 +475,9 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
assert( Vec_IntSize(vRes) > 0 );
p->tTsim += clock() - clk;
return Pdr_SetCreate( vRes, vPiLits );
pRes = Pdr_SetCreate( vRes, vPiLits );
assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
return pRes;
}
////////////////////////////////////////////////////////////////////////

1
src/proof/pdr/pdrUtil.c
View File

@ -515,6 +515,7 @@ void Pdr_QueueClean( Pdr_Man_t * p )
Pdr_Obl_t * pThis;
while ( (pThis = Pdr_QueuePop(p)) )
Pdr_OblDeref( pThis );
pThis = NULL;
}
/**Function*************************************************************