diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-19 09:55:58 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-19 09:55:58 -0800 |
| commit | 6cf289dadd41354eb03ef1fa0a4d366ab5f62f8c (patch) | |
| tree | 3e431a17544f528d4f00ea0995e557978fa38ff2 /src/proof | |
| parent | 24fdcecb2d034af4d7f7c26ec083f6baf1434018 (diff) | |
| download | abc-6cf289dadd41354eb03ef1fa0a4d366ab5f62f8c.tar.gz abc-6cf289dadd41354eb03ef1fa0a4d366ab5f62f8c.tar.bz2 abc-6cf289dadd41354eb03ef1fa0a4d366ab5f62f8c.zip | |
working on pdr with wla
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/pdr/pdrIncr.c | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index aa07b668..2a718577 100644 --- a/src/proof/pdr/pdrIncr.c +++ b/src/proof/pdr/pdrIncr.c @@ -77,14 +77,17 @@ void IPdr_ManPrintClauses( Vec_Vec_t * vClauses, int kStart, int nRegs ) SeeAlso [] ***********************************************************************/ -Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p ) +Vec_Vec_t * IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast ) { int i, k; Vec_Vec_t * vClausesSaved; Pdr_Set_t * pCla; - // Note that the last frame is empty - vClausesSaved = Vec_VecStart(Vec_VecSize(p->vClauses)-1); + if ( fDropLast ) + vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses)-1 ); + else + vClausesSaved = Vec_VecStart( Vec_VecSize(p->vClauses) ); + Vec_VecForEachEntryStartStop( Pdr_Set_t *, p->vClauses, pCla, i, k, 0, Vec_VecSize(vClausesSaved) ) Vec_VecPush(vClausesSaved, i, Pdr_SetDup(pCla)); @@ -555,7 +558,7 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars ) RetValue = IPdr_ManSolveInt( p ); if ( RetValue == -1 && pPars->iFrame == pPars->nFrameMax) { - vClausesSaved = IPdr_ManSaveClauses( p ); + vClausesSaved = IPdr_ManSaveClauses( p, 1 ); Pdr_ManStop( p ); |