From 4876f1e21cd395e94435aaafeaeec05839a32181 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 9 Apr 2013 16:26:28 -0700
Subject: Added switch '-x' to save CEXes in 'bmc3' and 'pdr' in multi-output
 mode.

---
 src/proof/pdr/pdr.h     | 1 +
 src/proof/pdr/pdrCore.c | 8 +++-----
 2 files changed, 4 insertions(+), 5 deletions(-)

(limited to 'src/proof/pdr')

diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index e55eebb6..6e157aad 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -57,6 +57,7 @@ struct Pdr_Par_t_
     int fNotVerbose;      // not printing line by line progress
     int fSilent;          // totally silent execution
     int fSolveAll;        // do not stop when found a SAT output
+    int fStoreCex;        // enable storing counter-examples in MO mode
     int nFailOuts;        // the number of failed outputs
     int iFrame;           // explored up to this frame
     int RunId;            // PDR id in this run 
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index a7c4dc35..eb21edfc 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -590,7 +590,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
                 assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
-                Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) );
+                Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 );
                 if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                     return 0; // all SAT
                 p->pPars->timeLastSolved = clock();
@@ -640,7 +640,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     }
                     if ( RetValue == 0 )
                     {
-                        Abc_Cex_t * pCex;
                         if ( fPrintClauses )
                         {
                             Abc_Print( 1, "*** Clauses after frame %d:\n", k );
@@ -659,11 +658,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                         if ( p->vCexes == NULL )
                             p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
                         assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
-                        pCex = Pdr_ManDeriveCex(p);
-                        Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCex );
+                        Vec_PtrWriteEntry( p->vCexes, p->iOutCur, p->pPars->fStoreCex ? Pdr_ManDeriveCex(p) : (void *)(ABC_PTRINT_T)1 );
                         if ( !p->pPars->fNotVerbose )
                             Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",  
-                                nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
+                                nOutDigits, p->iOutCur, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                         if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                             return 0; // all SAT
                         Pdr_QueueClean( p );
-- 
cgit v1.2.3