diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-28 16:18:39 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-11-28 16:18:39 -0800 |
| commit | 661265984c6b9e32fcaece8aa361b06476756783 (patch) | |
| tree | c766135e7705cc3d3a9e8d8fcded64eed5225dec /src/base/abci/abc.c | |
| parent | b2fd119933166ad7d9e4132ebb8aaf422bfcdb8a (diff) | |
| download | abc-661265984c6b9e32fcaece8aa361b06476756783.tar.gz abc-661265984c6b9e32fcaece8aa361b06476756783.tar.bz2 abc-661265984c6b9e32fcaece8aa361b06476756783.zip | |
Counter-example analysis and optimization.
Diffstat (limited to 'src/base/abci/abc.c')
| -rw-r--r-- | src/base/abci/abc.c | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index de37c441..7c10aa64 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -30136,6 +30136,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern void Gia_VtaTest( Gia_Man_t * p, int nFramesStart, int nFramesMax, int nConfMax, int nTimeMax, int fVerbose ); // extern void Gia_IsoTest( Gia_Man_t * p, int fVerbose ); extern void Ga2_ManComputeTest( Gia_Man_t * p ); + extern void Bmc_CexTest( Gia_Man_t * p, Abc_Cex_t * pCex ); + Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF ) @@ -30159,6 +30161,11 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" ); return 1; } + if ( pAbc->pCex == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Test(): There is no CEX.\n" ); + return 1; + } // Gia_ManFrontTest( pAbc->pGia ); // Gia_ManReduceConst( pAbc->pGia, 1 ); // Sat_ManTest( pAbc->pGia, Gia_ManCo(pAbc->pGia, 0), 0 ); @@ -30174,7 +30181,8 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_ManSuppSizeTest( pAbc->pGia ); // Gia_VtaTest( pAbc->pGia, 10, 100000, 0, 0, 1 ); // Gia_IsoTest( pAbc->pGia, fVerbose ); - Ga2_ManComputeTest( pAbc->pGia ); +// Ga2_ManComputeTest( pAbc->pGia ); + Bmc_CexTest( pAbc->pGia, pAbc->pCex ); return 0; usage: Abc_Print( -2, "usage: &test [-svh]\n" ); |