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/sat/bmc/bmc.h     |  1 +
 src/sat/bmc/bmcBmc3.c | 46 +++++++++++++++++++++++++++++++++-------------
 2 files changed, 34 insertions(+), 13 deletions(-)

(limited to 'src/sat/bmc')

diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index e799bea9..93bfd78a 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -51,6 +51,7 @@ struct Saig_ParBmc_t_
     int         nTimeOutGap;    // approximate timeout in seconds since the last change
     int         nPisAbstract;   // the number of PIs to abstract
     int         fSolveAll;      // does not stop at the first SAT output
+    int         fStoreCex;      // enable storing CEXes in the MO mode
     int         fDropSatOuts;   // replace sat outputs by constant 0
     int         nFfToAddMax;    // max number of flops to add during CBA
     int         fSkipRand;      // skip random decisions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 28bb7729..0c828dbd 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1336,6 +1336,33 @@ clock_t Saig_ManBmcTimeToStop( Saig_ParBmc_t * pPars, clock_t nTimeToStopNG )
     return nTimeToStop;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i )
+{
+    Aig_Obj_t * pObjPi;
+    Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), f*Saig_ManPoNum(p->pAig)+i );
+    int j, k, iBit = Saig_ManRegNum(p->pAig);
+    for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(p->pAig) )
+        Saig_ManForEachPi( p->pAig, pObjPi, k )
+        {
+            int iLit = Saig_ManBmcLiteral( p, pObjPi, j );
+            if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
+                Abc_InfoSetBit( pCex->pData, iBit + k );
+        }
+    return pCex;
+}
+
+
 /**Function*************************************************************
 
   Synopsis    [Bounded model checking engine.]
@@ -1465,7 +1492,10 @@ clkOther += clock() - clk2;
                         nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
-                Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 );
+                if ( pPars->fStoreCex )
+                    Vec_PtrWriteEntry( p->vCexes, i, Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ) );
+                else
+                    Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 );
                 RetValue = 0;
                 // reset the timeout
                 pPars->timeLastSolved = clock();
@@ -1506,16 +1536,6 @@ nTimeSat += clock() - clk2;
                 fFirst = 0;
                 if ( !pPars->fSolveAll )
                 {
-                    Aig_Obj_t * pObjPi;
-                    Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
-                    int j, iBit = Saig_ManRegNum(pAig);
-                    for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(pAig) )
-                        Saig_ManForEachPi( p->pAig, pObjPi, k )
-                        {
-                            int iLit = Saig_ManBmcLiteral( p, pObjPi, j );
-                            if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
-                                Abc_InfoSetBit( pCex->pData, iBit + k );
-                        }
                     if ( pPars->fVerbose )
                     {
                         printf( "%4d %s : ", f,  fUnfinished ? "-" : "+" );
@@ -1537,7 +1557,7 @@ nTimeSat += clock() - clk2;
                         fflush( stdout );
                     }
                     ABC_FREE( pAig->pSeqModel );
-                    pAig->pSeqModel = pCex;
+                    pAig->pSeqModel = Saig_ManGenerateCex( p, f, i );
                     RetValue = 0;
                     goto finish;
                 }
@@ -1547,7 +1567,7 @@ nTimeSat += clock() - clk2;
                         nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
-                Vec_PtrWriteEntry( p->vCexes, i, (void *)(ABC_PTRINT_T)1 );
+                Vec_PtrWriteEntry( p->vCexes, i, pPars->fStoreCex? Saig_ManGenerateCex( p, f, i ) : (void *)(ABC_PTRINT_T)1 );
                 RetValue = 0;
                 // reset the timeout
                 pPars->timeLastSolved = clock();
-- 
cgit v1.2.3