diff options
Diffstat (limited to 'src/sat/bmc/bmcCexCare.c')
| -rw-r--r-- | src/sat/bmc/bmcCexCare.c | 38 |
1 files changed, 36 insertions, 2 deletions
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 /// //////////////////////////////////////////////////////////////////////// |