diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/pdr/pdr.h | 2 | ||||
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 19 | ||||
| -rw-r--r-- | src/proof/pdr/pdrMan.c | 6 |
3 files changed, 15 insertions, 12 deletions
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h index 97a71512..10d2af3b 100644 --- a/src/proof/pdr/pdr.h +++ b/src/proof/pdr/pdr.h @@ -67,7 +67,7 @@ struct Pdr_Par_t_ int(*pFuncStop)(int); // callback to terminate int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode clock_t timeLastSolved; // the time when the last output was solved - int * pOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided) + Vec_Int_t * vOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided) }; //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index afcb45b4..f2ba7ba6 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -592,7 +592,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) return 0; // SAT } p->pPars->nFailOuts++; - if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0; + if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); Abc_Print( 1, "Output %*d was trivially 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 ) @@ -684,7 +684,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) return 0; // SAT } p->pPars->nFailOuts++; - if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0; + if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) ); assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ); @@ -719,7 +719,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) if ( p->pTime4Outs[p->iOutCur] == 0 && p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL ) { p->pPars->nDropOuts++; - if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = -1; + if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 ); // printf( "Dropping output %d.\n", p->iOutCur ); } } @@ -765,10 +765,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) // count the number of UNSAT outputs p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts; // convert previously 'unknown' into 'unsat' - if ( p->pPars->pOutMap ) + if ( p->pPars->vOutMap ) for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ ) - if ( p->pPars->pOutMap[k] == -2 ) // unknown - p->pPars->pOutMap[k] = 1; // unsat + if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown + Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat return p->vCexes ? 0 : 1; // UNSAT } if ( p->pPars->fVerbose ) @@ -836,7 +836,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p ) int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) { Pdr_Man_t * p; - int RetValue; + int k, RetValue; clock_t clk = clock(); if ( pPars->nTimeOutOne ) pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1; @@ -871,6 +871,11 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) p->tTotal += clock() - clk; Pdr_ManStop( p ); pPars->iFrame--; + // convert all -2 (unknown) entries into -1 (undec) + if ( pPars->vOutMap ) + for ( k = 0; k < Saig_ManPoNum(pAig); k++ ) + if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown + Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec return RetValue; } diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index ef930beb..36a62029 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -83,10 +83,8 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio } if ( pPars->fSolveAll ) { - int i; - pPars->pOutMap = ABC_ALLOC( int, Saig_ManPoNum(pAig) ); - for ( i = 0; i < Saig_ManPoNum(pAig); i++ ) - pPars->pOutMap[i] = -2; // unknown + p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) ); + Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 ); } return p; } |