Better CEX minimization and renaming of write_counter into write_cex.

4 files changed, 307 insertions, 2 deletions

diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 0bc7bb3f..3eeeb7b5 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -126,11 +126,17 @@ extern void              Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
 extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
 /*=== bmcBmcAnd.c ==========================================================*/
 extern int               Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars );
+/*=== bmcCexCare.c ==========================================================*/
+extern Abc_Cex_t *       Bmc_CexCareMinimize( Aig_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose );
+extern void              Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
 /*=== bmcCexCut.c ==========================================================*/
 extern Gia_Man_t *       Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
 extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
 /*=== bmcCexMin.c ==========================================================*/
 extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
+/*=== bmcCexTool.c ==========================================================*/
+extern void              Bmc_CexPrint( Abc_Cex_t * pCex, int nInputs, int fVerbose );
+extern int               Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
 /*=== bmcICheck.c ==========================================================*/
 extern void              Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
 extern Vec_Int_t *       Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose );
diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c
new file mode 100644
index 00000000..addb89fd
--- /dev/null
+++ b/src/sat/bmc/bmcCexCare.c
@@ -0,0 +1,298 @@
+/**CFile****************************************************************
+
+  FileName    [bmcCexCare.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [Computing care set of the counter-example.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcCexCare.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+#include "aig/gia/giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Backward propagation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bmc_CexCarePropagateFwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, int fGrow )
+{
+    Gia_Obj_t * pObj;
+    int Prio, Prio0, Prio1;
+    int i, Phase0, Phase1;
+    if ( (fGrow & 2) )
+    {
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->Value = Abc_Var2Lit( f * pCex->nPis + (pCex->nPis-1-i) + 1, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) );
+    }
+    else
+    {
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->Value = Abc_Var2Lit( f * pCex->nPis + i + 1, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) );
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        Prio0  = Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value);
+        Prio1  = Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value);
+        Phase0 = Abc_LitIsCompl(Gia_ObjFanin0(pObj)->Value) ^ Gia_ObjFaninC0(pObj);
+        Phase1 = Abc_LitIsCompl(Gia_ObjFanin1(pObj)->Value) ^ Gia_ObjFaninC1(pObj);
+        if ( Phase0 && Phase1 )
+            Prio = (fGrow & 1) ? Abc_MinInt(Prio0, Prio1) : Abc_MaxInt(Prio0, Prio1);
+        else if ( Phase0 && !Phase1 )
+            Prio = Prio1;
+        else if ( !Phase0 && Phase1 )
+            Prio = Prio0;
+        else // if ( !Phase0 && !Phase1 )
+            Prio = (fGrow & 1) ? Abc_MaxInt(Prio0, Prio1) : Abc_MinInt(Prio0, Prio1);
+        pObj->Value = Abc_Var2Lit( Prio, Phase0 & Phase1 );
+    }
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
+}
+void Bmc_CexCarePropagateFwd( Gia_Man_t * p, Abc_Cex_t * pCex, int fGrow, Vec_Int_t * vPrios )
+{
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    int f, i;
+    Gia_ManConst0( p )->Value = 0;
+    Gia_ManForEachRi( p, pObj, i )
+        pObj->Value = 0;
+    Vec_IntClear( vPrios );
+    for ( f = 0; f <= pCex->iFrame; f++ )
+    {
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+            Vec_IntPush( vPrios, (pObjRo->Value = pObjRi->Value) );
+        Bmc_CexCarePropagateFwdOne( p, pCex, f, fGrow );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Forward propagation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bmc_CexCarePropagateBwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, Abc_Cex_t * pCexMin )
+{
+    Gia_Obj_t * pObj;
+    int i, Phase0, Phase1;
+    Gia_ManForEachCand( p, pObj, i )
+        pObj->fPhase = 0;
+    Gia_ManForEachCo( p, pObj, i )
+        if ( pObj->fPhase )
+            Gia_ObjFanin0(pObj)->fPhase = 1;
+    Gia_ManForEachAndReverse( p, pObj, i )
+    {
+        if ( !pObj->fPhase )
+            continue;
+        Phase0 = Abc_LitIsCompl(Gia_ObjFanin0(pObj)->Value) ^ Gia_ObjFaninC0(pObj);
+        Phase1 = Abc_LitIsCompl(Gia_ObjFanin1(pObj)->Value) ^ Gia_ObjFaninC1(pObj);
+        if ( Phase0 && Phase1 )
+        {
+            Gia_ObjFanin0(pObj)->fPhase = 1;
+            Gia_ObjFanin1(pObj)->fPhase = 1;
+        }
+        else if ( Phase0 && !Phase1 )
+            Gia_ObjFanin1(pObj)->fPhase = 1;
+        else if ( !Phase0 && Phase1 )
+            Gia_ObjFanin0(pObj)->fPhase = 1;
+        else // if ( !Phase0 && !Phase1 )
+        {
+            if ( Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value) <= Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value) )
+                Gia_ObjFanin0(pObj)->fPhase = 1;
+            else
+                Gia_ObjFanin1(pObj)->fPhase = 1;
+        }
+    }
+    Gia_ManForEachPi( p, pObj, i )
+        if ( pObj->fPhase )
+            Abc_InfoSetBit( pCexMin->pData, pCexMin->nRegs + pCexMin->nPis * f + i );
+}
+Abc_Cex_t * Bmc_CexCarePropagateBwd( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vPrios, int fGrow )
+{
+    Abc_Cex_t * pCexMin;
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    int f, i;
+    pCexMin = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 );
+    pCexMin->iPo    = pCex->iPo;
+    pCexMin->iFrame = pCex->iFrame;
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->fPhase = 0;
+    for ( f = pCex->iFrame; f >= 0; f-- )
+    {
+        Gia_ManPo(p, pCex->iPo)->fPhase = (int)(f == pCex->iFrame);
+        Gia_ManForEachRo( p, pObj, i )
+            pObj->Value = Vec_IntEntry( vPrios, f * pCex->nRegs + i );
+        Bmc_CexCarePropagateFwdOne( p, pCex, f, fGrow );
+        Bmc_CexCarePropagateBwdOne( p, pCex, f, pCexMin );
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+            pObjRi->fPhase = pObjRo->fPhase;
+    }
+    return pCexMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the care set of the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose )
+{
+    int nTryCexes = 4; // belongs to range [1;4]
+    Abc_Cex_t * pCexBest, * pCexMin[4] = {NULL};
+    int k, nOnesBest, nOnesCur;
+    Vec_Int_t * vPrios;
+    if ( pCex->nPis != Gia_ManPiNum(p) )
+    {
+        printf( "Given CEX does to have same number of inputs as the AIG.\n" );
+        return NULL;
+    }
+    if ( pCex->nRegs != Gia_ManRegNum(p) )
+    {
+        printf( "Given CEX does to have same number of flops as the AIG.\n" );
+        return NULL;
+    }
+    if ( !(pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p)) )
+    {
+        printf( "Given CEX has PO whose index is out of range for the AIG.\n" );
+        return NULL;
+    }
+    assert( pCex->nPis == Gia_ManPiNum(p) );
+    assert( pCex->nRegs == Gia_ManRegNum(p) );
+    assert( pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p) );
+    if ( fVerbose )
+    {
+        printf( "Original :    " );
+        Bmc_CexPrint( pCex, Gia_ManPiNum(p), 0 );
+    }
+    vPrios = Vec_IntAlloc( pCex->nRegs * (pCex->iFrame + 1) );
+    for ( k = 0; k < nTryCexes; k++ )
+    {
+        Bmc_CexCarePropagateFwd(p, pCex, k, vPrios );
+        assert( Vec_IntSize(vPrios) == pCex->nRegs * (pCex->iFrame + 1) );
+        if ( !Abc_LitIsCompl(Gia_ManPo(p, pCex->iPo)->Value) )
+        {
+            printf( "Counter-example is invalid.\n" );
+            Vec_IntFree( vPrios );
+            return NULL;
+        }
+        pCexMin[k] = Bmc_CexCarePropagateBwd( p, pCex, vPrios, k );
+        if ( fVerbose )
+        {
+            if ( (k & 1) )
+                printf( "Decrease :    " );
+            else
+                printf( "Increase :    " );
+            Bmc_CexPrint( pCexMin[k], Gia_ManPiNum(p), 0 );
+        }
+    }
+    Vec_IntFree( vPrios );
+    // select the best one
+    pCexBest  = pCexMin[0];
+    nOnesBest = Abc_CexCountOnes(pCexMin[0]);
+    for ( k = 1; k < nTryCexes; k++ )
+    {
+        nOnesCur = Abc_CexCountOnes(pCexMin[k]);
+        if ( nOnesBest > nOnesCur )
+        {
+            nOnesBest = nOnesCur;
+            pCexBest  = pCexMin[k];
+        }
+    }
+    for ( k = 0; k < nTryCexes; k++ )
+        if ( pCexBest != pCexMin[k] )
+            Abc_CexFreeP( &pCexMin[k] );
+    // verify and return
+    if ( fVerbose )
+    {
+        printf( "Final    :    " );
+        Bmc_CexPrint( pCexBest, Gia_ManPiNum(p), 0 );
+    }
+    if ( !Bmc_CexVerify( p, pCex, pCexBest ) )
+        printf( "Counter-example verification has failed.\n" );
+    else if ( fCheck ) 
+        printf( "Counter-example verification succeeded.\n" );
+    return pCexBest;
+}
+Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose )
+{
+    Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
+    Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, pCex, fCheck, fVerbose );
+    Gia_ManStop( pGia );
+    return pCexMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies the care set of the counter-example.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
+{
+    Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
+    if ( fVerbose )
+    {
+        printf( "Original :    " );
+        Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 );
+        printf( "Minimized:    " );
+        Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
+    }
+    if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
+        printf( "Counter-example verification has failed.\n" );
+    else 
+        printf( "Counter-example verification succeeded.\n" );
+    Gia_ManStop( pGia );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index 811a90b7..05dade97 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -348,7 +348,7 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
     Gia_Obj_t * pObj;
     int i, k;
     assert( pCex->nRegs > 0 );
-    assert( pCexCare->nRegs == 0 );
+//    assert( pCexCare->nRegs == 0 );
     Gia_ObjTerSimSet0( Gia_ManConst0(p) );
     Gia_ManForEachRi( p, pObj, k )
         Gia_ObjTerSimSet0( pObj );
@@ -356,7 +356,7 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
     {
         Gia_ManForEachPi( p, pObj, k )
         {
-            if ( !Abc_InfoHasBit( pCexCare->pData, i * pCexCare->nPis + k ) )
+            if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
                 Gia_ObjTerSimSetX( pObj );
             else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
                 Gia_ObjTerSimSet1( pObj );
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index 3ff4b100..6deb9eb1 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -3,6 +3,7 @@ SRC +=    src/sat/bmc/bmcBmc.c \
     src/sat/bmc/bmcBmc3.c \
     src/sat/bmc/bmcBmcAnd.c \
     src/sat/bmc/bmcBmci.c \
+    src/sat/bmc/bmcCexCare.c \
     src/sat/bmc/bmcCexCut.c \
     src/sat/bmc/bmcCexDepth.c \
     src/sat/bmc/bmcCexMin1.c \