Enabled saving vector of counter-examples in the ABC framework.

5 files changed, 41 insertions, 9 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e707c57e..0d59d7e0 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -203,7 +203,7 @@ struct Abc_Ntk_t_
     Vec_Ptr_t *       vSupps;        // CO support information
     int *             pModel;        // counter-example (for miters)
     Abc_Cex_t *       pSeqModel;     // counter-example (for sequential miters)
-    Vec_Ptr_t *       pSeqModelVec;  // vector of counter-examples (for sequential miters)
+    Vec_Ptr_t *       vSeqModelVec;  // vector of counter-examples (for sequential miters)
     Abc_Ntk_t *       pExdc;         // the EXDC network (if given)
     void *            pExcare;       // the EXDC network (if given)
     void *            pData;         // misc
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index ac488114..4295835d 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -995,8 +995,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     if ( pNtk->vLevelsR ) Vec_IntFree( pNtk->vLevelsR );
     ABC_FREE( pNtk->pModel );
     ABC_FREE( pNtk->pSeqModel );
-    if ( pNtk->pSeqModelVec )
-        Vec_PtrFreeFree( pNtk->pSeqModelVec );
+    if ( pNtk->vSeqModelVec )
+        Vec_PtrFreeFree( pNtk->vSeqModelVec );
     TotalMemory  = 0;
     TotalMemory += pNtk->pMmObj? Mem_FixedReadMemUsage(pNtk->pMmObj)  : 0;
     TotalMemory += pNtk->pMmStep? Mem_StepReadMemUsage(pNtk->pMmStep) : 0;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5e9041b1..3a28d169 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -410,9 +410,38 @@ extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc,
 ***********************************************************************/
 void Abc_FrameReplaceCex( Abc_Frame_t * pAbc, Abc_Cex_t ** ppCex )
 {
+    // update CEX
     ABC_FREE( pAbc->pCex );
     pAbc->pCex = *ppCex;
     *ppCex = NULL;
+    // remove CEX vector
+    if ( pAbc->vCexVec )
+    {
+        Vec_PtrFreeFree( pAbc->vCexVec );
+        pAbc->vCexVec = NULL;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FrameReplaceCexVec( Abc_Frame_t * pAbc, Vec_Ptr_t ** pvCexVec )
+{
+    // update CEX vector
+    if ( pAbc->vCexVec )
+        Vec_PtrFreeFree( pAbc->vCexVec );
+    pAbc->vCexVec = *pvCexVec;
+    *pvCexVec = NULL;
+    // remove CEX
+    ABC_FREE( pAbc->pCex );
 }
 
 /**Function*************************************************************
@@ -19015,14 +19044,14 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "bmc3" );
     if ( pPars->fSolveAll && pPars->fDropSatOuts )
     {
-        if ( pNtk->pSeqModelVec == NULL )
+        if ( pNtk->vSeqModelVec == NULL )
             printf( "The array of counter-examples is not available.\n" );
-        else if ( Vec_PtrSize(pNtk->pSeqModelVec) != Abc_NtkPoNum(pNtk) )
+        else if ( Vec_PtrSize(pNtk->vSeqModelVec) != Abc_NtkPoNum(pNtk) )
             printf( "The array size does not match the number of outputs.\n" );
         else
         {
             extern void Abc_NtkDropSatOutputs( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCexes, int fVerbose );
-            Abc_NtkDropSatOutputs( pNtk, pNtk->pSeqModelVec, pPars->fVerbose );
+            Abc_NtkDropSatOutputs( pNtk, pNtk->vSeqModelVec, pPars->fVerbose );
             pNtkRes = Abc_NtkDarLatchSweep( pNtk, 1, 1, 1, 0 );
             if ( pNtkRes == NULL )
             {
@@ -19032,6 +19061,8 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
         }
     }
+    if ( pNtk->vSeqModelVec )
+        Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
     return 0;
 
 usage:
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 064529cc..ebeafa86 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1824,9 +1824,9 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars )
                 printf( "(timeout %d sec). ", pPars->nTimeOut );
             else
                 printf( "(conf limit %d). ", pPars->nConfLimit );
-            if ( pNtk->pSeqModelVec )
-                Vec_PtrFreeFree( pNtk->pSeqModelVec );
-            pNtk->pSeqModelVec = pMan->pSeqModelVec;  pMan->pSeqModelVec = NULL;
+            if ( pNtk->vSeqModelVec )
+                Vec_PtrFreeFree( pNtk->vSeqModelVec );
+            pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
         }
     }
     else // if ( RetValue == 0 )
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index d3a1fc9f..c008fc8b 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -98,6 +98,7 @@ struct Abc_Frame_t_
     Gia_Man_t *     pGia;
     Gia_Man_t *     pGia2;
     Abc_Cex_t *     pCex; 
+    Vec_Ptr_t *     vCexVec;
 
     void *          pSave1; 
     void *          pSave2;