diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 17:33:44 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 17:33:44 -0800 |
commit | ce63869fe7ebb0e22af4833454daea0c5977f32f (patch) | |
tree | 3f54e3de794394829c48eac43db28b350dbbea73 /src/proof/pdr | |
parent | 8761942258497dbd95f5ffca3eef1cf3d053f269 (diff) | |
download | abc-ce63869fe7ebb0e22af4833454daea0c5977f32f.tar.gz abc-ce63869fe7ebb0e22af4833454daea0c5977f32f.tar.bz2 abc-ce63869fe7ebb0e22af4833454daea0c5977f32f.zip |
Enabling multi-output solving in 'pdr'.
Diffstat (limited to 'src/proof/pdr')
-rw-r--r-- | src/proof/pdr/pdrCore.c | 10 | ||||
-rw-r--r-- | src/proof/pdr/pdrSat.c | 3 | ||||
-rw-r--r-- | src/proof/pdr/pdrTsim.c | 5 | ||||
-rw-r--r-- | src/proof/pdr/pdrUtil.c | 1 |
4 files changed, 14 insertions, 5 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 85ad580e..46288925 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -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 ); diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c index f0aff8bb..8bd45026 100644 --- a/src/proof/pdr/pdrSat.c +++ b/src/proof/pdr/pdrSat.c @@ -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 ); diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index fcd17fad..1865e14b 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -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; } //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c index c70554e3..1536c1cc 100644 --- a/src/proof/pdr/pdrUtil.c +++ b/src/proof/pdr/pdrUtil.c @@ -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************************************************************* |