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

9 files changed, 112 insertions, 16 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index a0216f37..e614d58f 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -154,7 +154,7 @@ struct Aig_Man_t_
     Vec_Int_t *      vFlopNums;      
     Vec_Int_t *      vFlopReprs;      
     Abc_Cex_t *      pSeqModel;
-    Vec_Ptr_t *      pSeqModelVec;   // vector of counter-examples (for sequential miters)
+    Vec_Ptr_t *      vSeqModelVec;   // vector of counter-examples (for sequential miters)
     Aig_Man_t *      pManExdc;
     Vec_Ptr_t *      vOnehots;
     Aig_Man_t *      pManHaig;
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index bce56424..b0544c90 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -211,8 +211,8 @@ void Aig_ManStop( Aig_Man_t * p )
     Vec_IntFreeP( &p->vProbs );
     Vec_IntFreeP( &p->vCiNumsOrig );
     Vec_PtrFreeP( &p->vMapped );
-    if ( p->pSeqModelVec )
-        Vec_PtrFreeFree( p->pSeqModelVec );
+    if ( p->vSeqModelVec )
+        Vec_PtrFreeFree( p->vSeqModelVec );
     ABC_FREE( p->pTerSimData );
     ABC_FREE( p->pFastSim );
     ABC_FREE( p->pData );
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index b984844e..4dc0c714 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -612,8 +612,8 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
     Aig_ManCleanMarkA( p->pAig );
     if ( p->vCexes )
     {
-        assert( p->pAig->pSeqModelVec == NULL );
-        p->pAig->pSeqModelVec = p->vCexes;
+        assert( p->pAig->vSeqModelVec == NULL );
+        p->pAig->vSeqModelVec = p->vCexes;
         p->vCexes = NULL;
     }
 //    Vec_PtrFreeFree( p->vCexes );
@@ -1133,7 +1133,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
             return 0;
         }
         // consider the next timeframe
-        pPars->iFrame = f;
+        if ( RetValue == -1 && pPars->nStart == 0 )
+            pPars->iFrame = f;
         // resize the array
         Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 );
         // map nodes of this section
@@ -1206,6 +1207,7 @@ clkOther += clock() - clk2;
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                 Vec_PtrWriteEntry( p->vCexes, i, pCex );
+                RetValue = 0;
                 continue;
             }
             // solve this output
@@ -1254,6 +1256,7 @@ clkOther += clock() - clk2;
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                 Vec_PtrWriteEntry( p->vCexes, i, pCex );
+                RetValue = 0;
             }
             else 
             {
diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c
index dd88fb70..824f9eb3 100644
--- a/src/aig/saig/saigCexMin.c
+++ b/src/aig/saig/saigCexMin.c
@@ -252,7 +252,7 @@ void Saig_ManCexMinDerivePhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_
   SeeAlso     []
  
 ***********************************************************************/
-Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
+Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
 {
     Vec_Vec_t * vFramePPs;
     Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
@@ -302,6 +302,67 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
     return vFramePPs;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collects phase and priority of all timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
+{
+    Vec_Vec_t * vFramePPs;
+    Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
+    Aig_Obj_t * pObj;
+    int i, f, nPrioOffset;
+
+    // initialize phase and priority
+    Aig_ManForEachObj( pAig, pObj, i )
+        pObj->iData = -1;
+
+    // set the constant node to higher priority than the flops
+    vFramePPs = Vec_VecStart( pCex->iFrame+1 );
+    nPrioOffset = pCex->nRegs;
+    Aig_ManConst1(pAig)->iData = Aig_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 );
+    vRoots = Vec_IntAlloc( 1000 );
+//printf( "Const1 = %d  Offset = %d\n", Aig_ManConst1(pAig)->iData, nPrioOffset ); 
+    for ( f = 0; f <= pCex->iFrame; f++ )
+    {
+        int nPiCount = 0;
+        // fill in PP for the CIs
+        vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
+        vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
+        assert( Vec_IntSize(vFramePPsOne) == 0 );
+        Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
+        {
+            assert( Aig_ObjIsPi(pObj) );
+            if ( Saig_ObjIsPi(pAig, pObj) )
+                Vec_IntPush( vFramePPsOne, Aig_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) );
+            else if ( f == 0 )
+                Vec_IntPush( vFramePPsOne, Aig_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
+            else
+            {
+                Aig_Obj_t * pObj0 = Saig_ObjLoToLi(pAig, pObj);
+                int Value = Saig_ObjLoToLi(pAig, pObj)->iData;
+                Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
+            }
+//printf( "%d ", Vec_IntEntryLast(vFramePPsOne) );
+        }
+//printf( "\n" );
+        // compute the PP info
+        Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
+    }
+    Vec_IntFree( vRoots );
+    // check the output
+    pObj = Aig_ManPo( pAig, pCex->iPo );
+    assert( Aig_LitIsCompl(pObj->iData) );
+    return vFramePPs;
+}
+
 
 /**Function*************************************************************
 
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;