read_cex: Faster parsing and care bits for verification

3 files changed, 86 insertions, 3 deletions

diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 12439faa..2c843392 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -219,7 +219,8 @@ extern int               Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars
 extern Abc_Cex_t *       Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
 extern Abc_Cex_t *       Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
 extern Abc_Cex_t *       Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
-extern void              Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
+extern int               Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
+extern int               Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
 extern Abc_Cex_t *       Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose );
 extern Abc_Cex_t *       Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose );
 /*=== bmcCexCut.c ==========================================================*/
@@ -230,6 +231,7 @@ extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pC
 /*=== bmcCexTool.c ==========================================================*/
 extern void              Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose );
 extern int               Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
+extern int               Bmc_CexVerifyAnyPo( 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 fBackTopo, int fDump, int fVerbose );
diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c
index c274b04c..d9a677c3 100644
--- a/src/sat/bmc/bmcCexCare.c
+++ b/src/sat/bmc/bmcCexCare.c
@@ -455,8 +455,9 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
+int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
 {
+    int result;
     Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
     if ( fVerbose )
     {
@@ -465,11 +466,13 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in
         printf( "Minimized:    " );
         Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
     }
-    if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
+    result = Bmc_CexVerify( pGia, pCex, pCexMin );
+    if ( !result )
         printf( "Counter-example verification has failed.\n" );
     else 
         printf( "Counter-example verification succeeded.\n" );
     Gia_ManStop( pGia );
+    return result;
 }
 /*
     {
@@ -480,6 +483,37 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in
     }
 */
 
+/**Function*************************************************************
+
+  Synopsis    [Verifies the care set of the counter-example.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
+{
+    int iPo;
+    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 );
+    }
+    iPo = Bmc_CexVerifyAnyPo( pGia, pCex, pCexMin );
+    if ( iPo < 0 )
+        printf( "Counter-example verification has failed.\n" );
+    else
+        printf( "Counter-example verification succeeded.\n" );
+    Gia_ManStop( pGia );
+    return iPo;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index 6cc29857..6bea6fc5 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -376,6 +376,53 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
 
 /**Function*************************************************************
 
+  Synopsis    [Verifies the care set of the counter-example for an arbitrary PO.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bmc_CexVerifyAnyPo( 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 );
+    Gia_ObjTerSimSet0( Gia_ManConst0(p) );
+    Gia_ManForEachRi( p, pObj, k )
+        Gia_ObjTerSimSet0( pObj );
+    for ( i = 0; i <= pCex->iFrame; i++ )
+    {
+        Gia_ManForEachPi( p, pObj, 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 );
+            else
+                Gia_ObjTerSimSet0( pObj );
+        }
+        Gia_ManForEachRo( p, pObj, k )
+            Gia_ObjTerSimRo( p, pObj );
+        Gia_ManForEachAnd( p, pObj, k )
+            Gia_ObjTerSimAnd( pObj );
+        Gia_ManForEachCo( p, pObj, k )
+            Gia_ObjTerSimCo( pObj );
+    }
+    for (i = 0; i < Gia_ManPoNum(p) - Gia_ManConstrNum(p); i++)
+    {
+        pObj = Gia_ManPo( p, i );
+        if (Gia_ObjTerSimGet1(pObj))
+            return i;
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes internal states of the CEX.]
 
   Description []