From 6cf289dadd41354eb03ef1fa0a4d366ab5f62f8c Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Sun, 19 Feb 2017 09:55:58 -0800 Subject: working on pdr with wla --- src/proof/pdr/pdrIncr.c | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) (limited to 'src/proof') 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 ); -- cgit v1.2.3