From feedbc744955df2b142d6a0b9dc62814567f5fc2 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Fri, 5 Aug 2022 14:28:13 +0200
Subject: read_cex: Faster parsing and care bits for verification

---
 src/sat/bmc/bmcCexTools.c | 47 +++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

(limited to 'src/sat/bmc/bmcCexTools.c')

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
@@ -374,6 +374,53 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
     return Gia_ObjTerSimGet1(pObj);
 }
 
+/**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.]
-- 
cgit v1.2.3