Unified the use of counter-examples in three packages.

7 files changed, 99 insertions, 15 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index b1017bdb..bf5681b9 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -149,6 +149,8 @@ extern Aig_Man_t *       Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFr
 extern Aig_Man_t *       Saig_ManDupOrpos( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs );
 extern Aig_Man_t *       Saig_ManDeriveAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops );
+extern int               Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p );
+extern int               Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p );
 /*=== saigHaig.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
 /*=== saigInd.c ==========================================================*/
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index 938a66e2..471d5d2d 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -101,12 +101,12 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA
     Abc_Cex_t * pCex;
     Aig_Obj_t * pObj;
     int i, f;
-    if ( !Ssw_SmlRunCounterExample( pAbs, pCexAbs ) )
+    if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
         printf( "Saig_ManCexRemap(): The intial counter-example is invalid.\n" );
     else
         printf( "Saig_ManCexRemap(): The intial counter-example is correct.\n" );
     // start the counter-example
-    pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
     pCex->iFrame = pCexAbs->iFrame;
     pCex->iPo    = pCexAbs->iPo;
     // copy the bit data
@@ -121,10 +121,10 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA
         }
     }
     // verify the counter example
-    if ( !Ssw_SmlRunCounterExample( p, pCex ) )
+    if ( !Saig_ManVerifyCex( p, pCex ) )
     {
         printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" );
-        Ssw_SmlFreeCounterExample( pCex );
+        Abc_CexFree( pCex );
         pCex = NULL;
     }
     else
@@ -194,7 +194,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
             printf( "Running property directed reachability...\n" );
         RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex );
         if ( pCex )
-            pCex->iPo = Ssw_SmlFindOutputCounterExample( pAbs, pCex );
+            pCex->iPo = Saig_ManFindFailedPoCex( pAbs, pCex );
         Aig_ManStop( pAbsOrpos );
         pAbs->pSeqModel = pCex;
         if ( RetValue )
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 8aa3af80..cb506054 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -301,11 +301,10 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
             }
             else if ( status == l_True )
             {
-//                extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
                 Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
                 int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
                 pModel[Aig_ManPiNum(pFrames)] = pObj->Id;
-                pAig->pSeqModel = (Abc_Cex_t *)Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
+                pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
                 ABC_FREE( pModel );
                 Vec_IntFree( vCiIds );
 
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index 3d57ae6e..9c36deb3 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -637,7 +637,7 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
     Aig_Obj_t * pObj, * pObjFrm;
     int i, f, iVarNum;
     // start the counter-example
-    pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
     pCex->iFrame = p->iFrameFail;
     pCex->iPo    = p->iOutputFail;
     // copy the bit data
@@ -656,10 +656,10 @@ Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
         }
     }
     // verify the counter example
-    if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) )
+    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
     {
         printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" );
-        Ssw_SmlFreeCounterExample( pCex );
+        Abc_CexFree( pCex );
         pCex = NULL;
     }
     return pCex;
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index a75297f7..570e8a26 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -1108,8 +1108,7 @@ clkOther += clock() - clk2;
                 continue;
             if ( Lit == 1 )
             {
-                extern Abc_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
-                Abc_Cex_t * pCex = Fra_SmlTrivCounterExample( pAig, f*Saig_ManPoNum(pAig)+i );
+                Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
                 printf( "Output %d is trivially SAT in frame %d.\n", i, f );
                 if ( !pPars->fSolveAll )
                 {
@@ -1137,9 +1136,8 @@ clkOther += clock() - clk2;
             }
             else if ( status == l_True )
             {
-//                extern void * Fra_SmlSimpleCounterExample( Aig_Man_t * p, int * pModel, int iFrame, int iPo );
                 int * pModel = Sat_SolverGetModel( p->pSat, Vec_IntArray(p->vPiVars), Vec_IntSize(p->vPiVars) );
-                Abc_Cex_t * pCex = Fra_SmlSimpleCounterExample( pAig, pModel, f, i );
+                Abc_Cex_t * pCex = Abc_CexCreate( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), pModel, f, i, 1 );
                 ABC_FREE( pModel );
                 fFirst = 0;
                 if ( !pPars->fSolveAll )
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index f4e557f8..b2b33bdb 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -265,6 +265,91 @@ Aig_Man_t * Saig_ManDeriveAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p )
+{
+    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    Aig_ManCleanMarkB(pAig);
+    Aig_ManConst1(pAig)->fMarkB = 1;
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Saig_ManForEachPi( pAig, pObj, k )
+            pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+        Aig_ManForEachNode( pAig, pObj, k )
+            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+        Aig_ManForEachPo( pAig, pObj, k )
+            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMarkB = pObjRi->fMarkB;
+    }
+    assert( iBit == p->nBits );
+    RetValue = Aig_ManPo(pAig, p->iPo)->fMarkB;
+    Aig_ManCleanMarkB(pAig);
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManFindFailedPoCex( Aig_Man_t * pAig, Abc_Cex_t * p )
+{
+    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    Aig_ManCleanMarkB(pAig);
+    Aig_ManConst1(pAig)->fMarkB = 1;
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Saig_ManForEachPi( pAig, pObj, k )
+            pObj->fMarkB = Aig_InfoHasBit(p->pData, iBit++);
+        Aig_ManForEachNode( pAig, pObj, k )
+            pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
+                           (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
+        Aig_ManForEachPo( pAig, pObj, k )
+            pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMarkB = pObjRi->fMarkB;
+    }
+    assert( iBit == p->nBits );
+    // remember the number of failed output
+    RetValue = -1;
+    Saig_ManForEachPo( pAig, pObj, i )
+        if ( pObj->fMarkB )
+        {
+            RetValue = i;
+            break;
+        }
+    Aig_ManCleanMarkB(pAig);
+    return RetValue;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigSimSeq.c b/src/aig/saig/saigSimSeq.c
index 37bb12b5..cc5a9e05 100644
--- a/src/aig/saig/saigSimSeq.c
+++ b/src/aig/saig/saigSimSeq.c
@@ -418,7 +418,7 @@ Abc_Cex_t * Raig_ManGenerateCounter( Aig_Man_t * pAig, int iFrame, int iOut, int
     Abc_Cex_t * p;
     unsigned * pData;
     int f, i, w, iPioId, Counter;
-    p = Ssw_SmlAllocCounterExample( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
+    p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
     p->iFrame = iFrame;
     p->iPo = iOut;
     // fill in the binary data