diff options
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 16 | ||||
| -rw-r--r-- | src/proof/pdr/pdrIncr.c | 47 |
2 files changed, 48 insertions, 15 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 342d667f..8cc79722 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -323,7 +323,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) Pdr_Par_t PdrPars, * pPdrPars = &PdrPars; Pdr_ManSetDefaultParams( pPdrPars ); pPdrPars->fVerbose = pPars->fPdrVerbose; - pPdrPars->fVeryVerbose = 1; + pPdrPars->fVeryVerbose = 0; // perform refinement iterations for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) @@ -368,14 +368,10 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) pAig = Gia_ManToAigSimple( pGia ); pPdr = Pdr_ManStart( pAig, pPdrPars, NULL ); + if ( vClauses ) { - if ( Vec_VecSize( vClauses) == 1 ) { - Vec_VecFree( vClauses ); - vClauses = NULL; - } else { - assert( Vec_VecSize( vClauses) >= 2 ); - IPdr_ManRestore(pPdr, vClauses); - } + assert( Vec_VecSize( vClauses) >= 2 ); + IPdr_ManRestore( pPdr, vClauses ); } RetValue = IPdr_ManSolveInt( pPdr ); @@ -406,7 +402,7 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) } // spurious CEX, continue solving - vClauses = IPdr_ManSaveClauses( pPdr, 0 ); + vClauses = IPdr_ManSaveClauses( pPdr, 1 ); Pdr_ManStop( pPdr ); // update the set of objects to be un-abstracted @@ -465,7 +461,7 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) //pPdrPars->fSkipDown = 0; // use 'pdr -nc' (improved generalization) //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this pPdrPars->fVerbose = pPars->fPdrVerbose; - pPdrPars->fVeryVerbose = 1; + pPdrPars->fVeryVerbose = 0; // perform refinement iterations for ( nIters = 1; nIters < pPars->nIterMax; nIters++ ) { diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index b1f126f4..4f66eeb4 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -77,12 +77,52 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ) SeeAlso [] ***********************************************************************/ +int IPdr_ManCheckClauses( Pdr_Man_t * p ) +{ + Pdr_Set_t * pCubeK; + Vec_Ptr_t * vArrayK; + int j, k, RetValue, kMax = Vec_PtrSize(p->vSolvers)-1; + int iStartFrame = 1; + + Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax ) + { + Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j ) + { + RetValue = Pdr_ManCheckCube( p, k, pCubeK, NULL, 0, 0, 1 ); + + if ( !RetValue ) { + printf( "Cube[%d][%d] not inductive!\n", k, j ); + } + + assert( RetValue == 1 ); + } + } + + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast ) { int i, k; Vec_Vec_t * vClausesSaved; Pdr_Set_t * pCla; + if ( Vec_VecSize( p->vClauses ) == 1 ) + return NULL; + if ( Vec_VecSize( p->vClauses ) == 2 && fDropLast ) + return NULL; + if ( fDropLast ) vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses)-1 ); else @@ -147,9 +187,6 @@ int IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses ) assert(vClauses); - printf( "IPdr restore:\n" ); - IPdr_ManPrintClauses( vClauses, 0, Aig_ManRegNum( p->pAig ) ); - Vec_VecFree(p->vClauses); p->vClauses = vClauses; @@ -197,8 +234,8 @@ int IPdr_ManSolveInt( Pdr_Man_t * p ) if ( Vec_VecSize(p->vClauses) == 0 ) Pdr_ManCreateSolver( p, (iFrame = 0) ); else { - iFrame = Vec_VecSize(p->vClauses); - Pdr_ManCreateSolver( p, iFrame ); + iFrame = Vec_VecSize(p->vClauses) - 1; + IPdr_ManCheckClauses( p ); } while ( 1 ) { |