Unified the use of counter-examples in three packages.

7 files changed, 98 insertions, 256 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index e3546686..b2f039a7 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -33,6 +33,7 @@
 #include <time.h>
 
 #include "vec.h"
+#include "utilCex.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -788,17 +789,13 @@ extern Vec_Int_t *         Gia_ManCollectPoIds( Gia_Man_t * p );
 extern int                 Gia_ObjIsMuxType( Gia_Obj_t * pNode );
 extern int                 Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** ppFan1 );
 extern Gia_Obj_t *         Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Obj_t ** ppNodeE );
-extern Abc_Cex_t *         Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames );
-extern Abc_Cex_t *         Gia_ManDeriveCexFromArray( Gia_Man_t * pAig, Vec_Int_t * vValues, int nSkip, int iFrame );
-extern Abc_Cex_t *         Gia_ManCreateFromComb( int nRegs, int nRealPis, int iPo, int * pModel );
-extern Abc_Cex_t *         Gia_ManDupCounterExample( Abc_Cex_t * p, int nRegsNew );
-extern int                 Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
-extern void                Gia_ManPrintCounterExample( Abc_Cex_t * p );
 extern int                 Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
 extern int                 Gia_ManHasChoices( Gia_Man_t * p );
 extern int                 Gia_ManHasDangling( Gia_Man_t * p );
 extern Vec_Int_t *         Gia_ManGetDangling( Gia_Man_t * p );
 extern void                Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj );
+extern int                 Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut );
+extern int                 Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p );
 /*=== giaCTas.c ===========================================================*/
 typedef struct Tas_Man_t_  Tas_Man_t;
 extern Tas_Man_t *         Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
@@ -808,8 +805,6 @@ extern void                Tas_ManSatPrintStats( Tas_Man_t * p );
 extern int                 Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
 extern int                 Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
 
- 
-
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 38e010f1..607e5ac6 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -530,8 +530,8 @@ void Gia_ManCexAbstractionStartNew( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
         {
             printf( "Problem is satisfiable. Found counter-example in frame %d.  ", nFrames-1 );
             Abc_PrintTime( 1, "Time", clk );
-            pGia->pCexSeq = Gia_ManDeriveCexFromArray( pGia, vCex, 0, nFrames-1 );
-            if ( !Gia_ManVerifyCounterExample( pGia, pGia->pCexSeq, 0 ) )
+            pGia->pCexSeq = Abc_CexCreate( Gia_ManRegNum(pGia), Gia_ManPiNum(pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 );
+            if ( !Gia_ManVerifyCex( pGia, pGia->pCexSeq, 0 ) )
                 Abc_Print( 1, "Generated counter-example is INVALID.\n" );
             pPars->Status = 0;
         }
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 4ded9a78..71204548 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -416,7 +416,7 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
     }
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     if ( p->pCexSeq )
-        pNew->pCexSeq = Gia_ManDupCounterExample( p->pCexSeq, Gia_ManRegNum(p) );
+        pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
     return pNew;
 }
 
@@ -764,7 +764,7 @@ Gia_Man_t * Gia_ManDupDfs( Gia_Man_t * p )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     if ( p->pCexSeq )
-        pNew->pCexSeq = Gia_ManDupCounterExample( p->pCexSeq, Gia_ManRegNum(p) );
+        pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) );
     return pNew;
 }
 
diff --git a/src/aig/gia/giaEra2.c b/src/aig/gia/giaEra2.c
index 64464832..dedbc032 100644
--- a/src/aig/gia/giaEra2.c
+++ b/src/aig/gia/giaEra2.c
@@ -1758,7 +1758,7 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos
     // verify
     if ( pAig->pCexSeq )
     {
-        if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
+        if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
             printf( "Generated counter-example is INVALID.                       \n" );
         else
             printf( "Generated counter-example verified correctly.               \n" );
@@ -1922,7 +1922,7 @@ Abc_Cex_t * Gia_ManAreDeriveCex( Gia_ManAre_t * p, Gia_StaAre_t * pLast )
             Vec_PtrPush( vStates, pSta );
     assert( Vec_PtrSize(vStates) >= 1 );
     // start the counter-example
-    pCex = Gia_ManAllocCounterExample( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) );
+    pCex = Abc_CexAlloc( Gia_ManRegNum(p->pAig), Gia_ManPiNum(p->pAig), Vec_PtrSize(vStates) );
     pCex->iFrame = Vec_PtrSize(vStates)-1;
     pCex->iPo = p->iOutFail;
     // compute states
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 1de1a2d4..18e02d81 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -436,7 +436,7 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
     Abc_Cex_t * p;
     unsigned * pData;
     int f, i, w, iPioId, Counter;
-    p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
+    p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
     p->iFrame = iFrame;
     p->iPo    = iOut;
     // fill in the binary data
@@ -513,7 +513,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
             pPars->iOutFail = iOut;
             pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
             Abc_Print( 1, "Networks are NOT EQUIVALENT.   Output %d was asserted in frame %d.  ", iOut, i );
-            if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
+            if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
             {
 //                Abc_Print( 1, "\n" );
                 Abc_Print( 1, "\nGenerated counter-example is INVALID.                    " );
diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c
index 4131f942..e1a5aa07 100644
--- a/src/aig/gia/giaSim2.c
+++ b/src/aig/gia/giaSim2.c
@@ -606,7 +606,7 @@ Abc_Cex_t * Gia_Sim2GenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
     Abc_Cex_t * p;
     unsigned * pData;
     int f, i, w, Counter;
-    p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
+    p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
     p->iFrame = iFrame;
     p->iPo = iOut;
     // fill in the binary data
@@ -663,7 +663,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
             pPars->iOutFail = iOut;
             pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat );
             Abc_Print( 1, "Networks are NOT EQUIVALENT.   Output %d was asserted in frame %d.  ", iOut, i );
-            if ( !Gia_ManVerifyCounterExample( pAig, pAig->pCexSeq, 0 ) )
+            if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
             {
 //                Abc_Print( 1, "\n" );
                 Abc_Print( 1, "\nGenerated counter-example is INVALID.                    " );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 82bdb367..2794956a 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -829,244 +829,6 @@ Gia_Obj_t * Gia_ObjRecognizeMux( Gia_Obj_t * pNode, Gia_Obj_t ** ppNodeT, Gia_Ob
 
 /**Function*************************************************************
 
-  Synopsis    [Allocates a counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Gia_ManAllocCounterExample( int nRegs, int nRealPis, int nFrames )
-{
-    Abc_Cex_t * pCex;
-    int nWords = Gia_BitWordNum( nRegs + nRealPis * nFrames );
-    pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
-    memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
-    pCex->nRegs  = nRegs;
-    pCex->nPis   = nRealPis;
-    pCex->nBits  = nRegs + nRealPis * nFrames;
-    return pCex;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManPrintCex( Abc_Cex_t * p )
-{
-    int i, f, k;
-    for ( k = 0; k < p->nRegs; k++ )
-        printf( "%d", Gia_InfoHasBit(p->pData, k) );
-    printf( "\n" );
-    for ( f = 0; f <= p->iFrame; f++ )
-    {
-        for ( i = 0; i < p->nPis; i++ )
-            printf( "%d", Gia_InfoHasBit(p->pData, k++) );
-        printf( "\n" );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Gia_ManDeriveCexFromArray( Gia_Man_t * pAig, Vec_Int_t * vValues, int nSkip, int iFrame )
-{
-    Abc_Cex_t * pCex;
-    int i;
-    pCex = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
-    assert( Vec_IntSize(vValues) == nSkip + pCex->nBits );
-    pCex->iPo    = 0;
-    pCex->iFrame = iFrame;
-    for ( i = 0; i < pCex->nBits; i++ )
-        if ( Vec_IntEntry(vValues, nSkip + i) )
-            Gia_InfoSetBit( pCex->pData, i );
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates a counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Gia_ManCreateFromComb( int nRegs, int nRealPis, int iPo, int * pModel )
-{
-    Abc_Cex_t * pCex;
-    int i;
-    pCex = Gia_ManAllocCounterExample( nRegs, nRealPis, 1 );
-    pCex->iPo    = iPo;
-    pCex->iFrame = 0;
-    for ( i = pCex->nRegs; i < pCex->nBits; i++ )
-        if ( pModel[i-pCex->nRegs] )
-            Gia_InfoSetBit( pCex->pData, i );
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
-{
-    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
-    int RetValue, i, k, iBit = 0;
-    Gia_ManCleanMark0(pAig);
-    Gia_ManForEachRo( pAig, pObj, i )
-        pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
-    for ( i = 0; i <= p->iFrame; i++ )
-    {
-        Gia_ManForEachPi( pAig, pObj, k )
-            pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
-        Gia_ManForEachAnd( pAig, pObj, k )
-            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
-                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
-        Gia_ManForEachCo( pAig, pObj, k )
-            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
-        if ( i == p->iFrame )
-            break;
-        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
-        {
-            pObjRo->fMark0 = pObjRi->fMark0;
-        }
-    }
-    assert( iBit == p->nBits );
-    if ( fDualOut )
-        RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
-    else
-        RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
-    Gia_ManCleanMark0(pAig);
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManVerifyCounterExampleAllOuts( Gia_Man_t * pAig, Abc_Cex_t * p )
-{
-    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
-    int RetValue, i, k, iBit = 0;
-    Gia_ManCleanMark0(pAig);
-    Gia_ManForEachRo( pAig, pObj, i )
-        pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
-    for ( i = 0; i <= p->iFrame; i++ )
-    {
-        Gia_ManForEachPi( pAig, pObj, k )
-            pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
-        Gia_ManForEachAnd( pAig, pObj, k )
-            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
-                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
-        Gia_ManForEachCo( pAig, pObj, k )
-            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
-        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
-            pObjRo->fMark0 = pObjRi->fMark0;
-    }
-    assert( iBit == p->nBits );
-    // remember the number of failed output
-    RetValue = -1;
-    Gia_ManForEachPo( pAig, pObj, i )
-        if ( Gia_ManPo(pAig, i)->fMark0 )
-        {
-            RetValue = i;
-            break;
-        }
-    Gia_ManCleanMark0(pAig);
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Make the trivial counter-example for the trivially asserted output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Gia_ManDupCounterExample( Abc_Cex_t * p, int nRegsNew )
-{
-    Abc_Cex_t * pCex;
-    int i;
-    pCex = Gia_ManAllocCounterExample( nRegsNew, p->nPis, p->iFrame+1 );
-    pCex->iPo    = p->iPo;
-    pCex->iFrame = p->iFrame;
-    for ( i = p->nRegs; i < p->nBits; i++ )
-        if ( Gia_InfoHasBit(p->pData, i) )
-            Gia_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs );
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints out the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManPrintCounterExample( Abc_Cex_t * p )
-{
-    int i, f, k;
-    printf( "Counter-example: iPo = %d  iFrame = %d  nRegs = %d  nPis = %d  nBits = %d\n", 
-        p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits );
-    printf( "State    : " );
-    for ( k = 0; k < p->nRegs; k++ )
-        printf( "%d", Gia_InfoHasBit(p->pData, k) );
-    printf( "\n" );
-    for ( f = 0; f <= p->iFrame; f++ )
-    {
-        printf( "Frame %2d : ", f );
-        for ( i = 0; i < p->nPis; i++ )
-            printf( "%d", Gia_InfoHasBit(p->pData, k++) );
-        printf( "\n" );
-    }
-    assert( k == p->nBits );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Dereferences the node's MFFC.]
 
   Description []
@@ -1371,6 +1133,91 @@ void Gia_ObjPrint( Gia_Man_t * p, Gia_Obj_t * pObj )
 */
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManVerifyCex( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
+{
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    Gia_ManCleanMark0(pAig);
+    Gia_ManForEachRo( pAig, pObj, i )
+        pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Gia_ManForEachPi( pAig, pObj, k )
+            pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+        Gia_ManForEachAnd( pAig, pObj, k )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachCo( pAig, pObj, k )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
+        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
+        {
+            pObjRo->fMark0 = pObjRi->fMark0;
+        }
+    }
+    assert( iBit == p->nBits );
+    if ( fDualOut )
+        RetValue = Gia_ManPo(pAig, 2*p->iPo)->fMark0 ^ Gia_ManPo(pAig, 2*p->iPo+1)->fMark0;
+    else
+        RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
+    Gia_ManCleanMark0(pAig);
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManFindFailedPoCex( Gia_Man_t * pAig, Abc_Cex_t * p )
+{
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, i, k, iBit = 0;
+    Gia_ManCleanMark0(pAig);
+    Gia_ManForEachRo( pAig, pObj, i )
+        pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+    for ( i = 0; i <= p->iFrame; i++ )
+    {
+        Gia_ManForEachPi( pAig, pObj, k )
+            pObj->fMark0 = Gia_InfoHasBit(p->pData, iBit++);
+        Gia_ManForEachAnd( pAig, pObj, k )
+            pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & 
+                           (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachCo( pAig, pObj, k )
+            pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
+            pObjRo->fMark0 = pObjRi->fMark0;
+    }
+    assert( iBit == p->nBits );
+    // remember the number of failed output
+    RetValue = -1;
+    Gia_ManForEachPo( pAig, pObj, i )
+        if ( Gia_ManPo(pAig, i)->fMark0 )
+        {
+            RetValue = i;
+            break;
+        }
+    Gia_ManCleanMark0(pAig);
+    return RetValue;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///