diff options
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/abci/abc.c | 19 | ||||
| -rw-r--r-- | src/base/abci/abcDar.c | 14 |
2 files changed, 25 insertions, 8 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ee0c98ff..980ba7ed 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -19546,19 +19546,21 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv ) int nConfMax; int fUnique; int fUniqueAll; + int fGetCex; int fVerbose; int fVeryVerbose; int c; - extern int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose ); + extern int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose ); // set defaults nFramesMax = 100; nConfMax = 1000; fUnique = 0; fUniqueAll = 0; + fGetCex = 0; fVerbose = 0; fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCuavwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCuaxvwh" ) ) != EOF ) { switch ( c ) { @@ -19590,6 +19592,9 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': fUniqueAll ^= 1; break; + case 'x': + fGetCex ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -19629,15 +19634,21 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - pAbc->Status = Abc_NtkDarInduction( pNtk, nFramesMax, nConfMax, fUnique, fUniqueAll, fVerbose, fVeryVerbose ); + pAbc->Status = Abc_NtkDarInduction( pNtk, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose ); + if ( fGetCex ) + { + Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); + printf( "The current CEX in ABC is set to be the CEX to induction.\n" ); + } return 0; usage: - Abc_Print( -2, "usage: ind [-FC num] [-uavwh]\n" ); + Abc_Print( -2, "usage: ind [-FC num] [-uaxvwh]\n" ); Abc_Print( -2, "\t runs the inductive case of the K-step induction\n" ); Abc_Print( -2, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax ); Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax ); Abc_Print( -2, "\t-u : toggle adding uniqueness constraints on demand [default = %s]\n", fUnique? "yes": "no" ); Abc_Print( -2, "\t-a : toggle adding uniqueness constraints always [default = %s]\n", fUniqueAll? "yes": "no" ); + Abc_Print( -2, "\t-x : toggle returning CEX to induction for the top frame [default = %s]\n", fGetCex? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing additional verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 695ae4ef..c0822ba9 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -3151,16 +3151,15 @@ Abc_Ntk_t * Abc_NtkDarTempor( Abc_Ntk_t * pNtk, int nFrames, int TimeOut, int nC SeeAlso [] ***********************************************************************/ -int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fVerbose, int fVeryVerbose ) +int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fUnique, int fUniqueAll, int fGetCex, int fVerbose, int fVeryVerbose ) { - Aig_Man_t * pMan, * pTemp; + Aig_Man_t * pMan; int clkTotal = clock(); int RetValue; pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return -1; - RetValue = Saig_ManInduction( pTemp = pMan, nFramesMax, nConfMax, fUnique, fUniqueAll, fVerbose, fVeryVerbose ); - Aig_ManStop( pTemp ); + RetValue = Saig_ManInduction( pMan, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose ); if ( RetValue == 1 ) { printf( "Networks are equivalent. " ); @@ -3176,6 +3175,13 @@ ABC_PRT( "Time", clock() - clkTotal ); printf( "Networks are UNDECIDED. " ); ABC_PRT( "Time", clock() - clkTotal ); } + if ( fGetCex ) + { + ABC_FREE( pNtk->pModel ); + ABC_FREE( pNtk->pSeqModel ); + pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; + } + Aig_ManStop( pMan ); return RetValue; } |