From ce63869fe7ebb0e22af4833454daea0c5977f32f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 9 Dec 2012 17:33:44 -0800 Subject: Enabling multi-output solving in 'pdr'. --- src/proof/pdr/pdrCore.c | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'src/proof/pdr/pdrCore.c') 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 ); -- cgit v1.2.3