summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2022-08-05 14:28:13 +0200
committerJannis Harder <me@jix.one>2022-08-05 15:11:34 +0200
commitfeedbc744955df2b142d6a0b9dc62814567f5fc2 (patch)
treeb4e27d16b65767eee5dca7e0e91bf8aae702a667 /src/sat
parent8c923ad4929870d4e819b84f62c7f9177b0d0d17 (diff)
downloadabc-feedbc744955df2b142d6a0b9dc62814567f5fc2.tar.gz
abc-feedbc744955df2b142d6a0b9dc62814567f5fc2.tar.bz2
abc-feedbc744955df2b142d6a0b9dc62814567f5fc2.zip
read_cex: Faster parsing and care bits for verification
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bmc/bmc.h4
-rw-r--r--src/sat/bmc/bmcCexCare.c38
-rw-r--r--src/sat/bmc/bmcCexTools.c47
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 []