diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-27 15:18:35 -0700 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-03-27 15:18:35 -0700 |
| commit | 758270d66350b36f4b3a8ceeefcea3a3efe230f1 (patch) | |
| tree | e316abf13a0570e4b0afb3cbc5f7bc89074bfbae | |
| parent | e6098d20beeb5b05ad6b113ff35c62ba2a386e47 (diff) | |
| download | abc-758270d66350b36f4b3a8ceeefcea3a3efe230f1.tar.gz abc-758270d66350b36f4b3a8ceeefcea3a3efe230f1.tar.bz2 abc-758270d66350b36f4b3a8ceeefcea3a3efe230f1.zip | |
%pdra: refactor
| -rw-r--r-- | src/base/wlc/wlcAbs.c | 7 | ||||
| -rw-r--r-- | src/proof/pdr/pdrIncr.c | 14 |
2 files changed, 3 insertions, 18 deletions
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index 5293de9e..a98ae70d 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -213,7 +213,7 @@ void Wlc_NtkAbsAnalyzeRefine( Wlc_Ntk_t * p, Vec_Int_t * vBlacks, Vec_Bit_t * vU Vec_IntFree( vSuppRefs ); } -static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num_sel_pis, int num_other_pis, Vec_Bit_t * vMark, int sel_pi_first, int nConfLimit, Wlc_Par_t * pPars ) +static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int first_sel_pi, int num_sel_pis, Vec_Bit_t * vMark, int nConfLimit, Wlc_Par_t * pPars ) { Vec_Int_t * vCores = NULL; Aig_Man_t * pAigFrames = Gia_ManToAigSimple( pFrames ); @@ -249,7 +249,6 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int num int status; Vec_Int_t* vLits = Vec_IntAlloc(100); Vec_Int_t* vMapVar2Sel = Vec_IntStart( pCnf->nVars ); - int first_sel_pi = sel_pi_first ? 0 : num_other_pis; for ( i = 0; i < num_sel_pis; ++i ) { int cur_pi = first_sel_pi + i; @@ -604,9 +603,9 @@ static int Wlc_NtkProofRefine( Wlc_Ntk_t * p, Wlc_Par_t * pPars, Abc_Cex_t * pCe pGiaFrames = Wlc_NtkUnrollWithCex( pNtkWithChoices, pCex, Wlc_NtkNumPiBits( p ), Vec_IntSize( vBlacks ), &num_ppis, 0, pPars->fProofUsePPI ); if ( !pPars->fProofUsePPI ) - vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), num_ppis, vChoiceMark, 0, 0, pPars ); + vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, num_ppis, Vec_IntSize( vBlacks ), vChoiceMark, 0, pPars ); else - vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, Vec_IntSize( vBlacks ), 0, vChoiceMark, 0, 0, pPars ); + vCoreSels = Wlc_NtkGetCoreSels( pGiaFrames, pCex->iFrame+1, 0, Vec_IntSize( vBlacks ), vChoiceMark, 0, pPars ); Wlc_NtkFree( pNtkWithChoices ); Gia_ManStop( pGiaFrames ); diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index abf8ab93..1f578242 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -309,20 +309,6 @@ int IPdr_ManRebuildClauses( Pdr_Man_t * p, Vec_Vec_t * vClauses ) Abc_Print( 1, " %d", Vec_PtrSize( vArrayK ) ); Abc_Print( 1, "\n" ); - /* - for ( i = 1; i < Vec_VecSize(p->vClauses); ++i ) - IPdr_ManSetSolver( p, i, 0 ); - - p->iUseFrame = Vec_VecSize(p->vClauses) - 1; - RetValue = Pdr_ManPushClauses( p ); - - if ( RetValue == 1 ) - { - Abc_Print( 1, "Found an invariant!\n"); - return 1; - } - */ - Vec_VecFree( vClauses ); return 0; } |