diff options
| -rw-r--r-- | src/base/abci/abc.c | 18 | ||||
| -rw-r--r-- | src/proof/int/int.h | 1 | ||||
| -rw-r--r-- | src/proof/int/intInt.h | 1 | ||||
| -rw-r--r-- | src/proof/int/intMan.c | 8 |
4 files changed, 21 insertions, 7 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b89a6924..239771b5 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -21262,7 +21262,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Inter_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CFTKLrtpomcgbqkdfvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CFTKLIrtpomcgbqkdivh" ) ) != EOF ) { switch ( c ) { @@ -21319,6 +21319,15 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) pLogFileName = argv[globalUtilOptind]; globalUtilOptind++; break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by a file name.\n" ); + goto usage; + } + pPars->pFileName = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'r': pPars->fRewrite ^= 1; break; @@ -21352,7 +21361,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': pPars->fDropSatOuts ^= 1; break; - case 'f': + case 'i': pPars->fDropInvar ^= 1; break; case 'v': @@ -21436,7 +21445,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: int [-CFTK num] [-L file] [-rtpomcgbqkdfvh]\n" ); + Abc_Print( -2, "usage: int [-CFTK num] [-LI file] [-irtpomcgbqkdvh]\n" ); Abc_Print( -2, "\t uses interpolation to prove the property\n" ); Abc_Print( -2, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-F num : the limit on number of frames to unroll [default = %d]\n", pPars->nFramesMax ); @@ -21444,6 +21453,8 @@ usage: Abc_Print( -2, "\t-K num : the number of steps in inductive checking [default = %d]\n", pPars->nFramesK ); Abc_Print( -2, "\t (K = 1 works in all cases; K > 1 works without -t and -b)\n" ); Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" ); + Abc_Print( -2, "\t-I file: the file name for dumping interpolant [default = \"%s\"]\n", pPars->pFileName ? pPars->pFileName : "invar.aig" ); + Abc_Print( -2, "\t-i : toggle dumping interpolant/invariant into a file [default = %s]\n", pPars->fDropInvar? "yes": "no" ); Abc_Print( -2, "\t-r : toggle rewriting of the unrolled timeframes [default = %s]\n", pPars->fRewrite? "yes": "no" ); Abc_Print( -2, "\t-t : toggle adding transition into the initial state [default = %s]\n", pPars->fTransLoop? "yes": "no" ); Abc_Print( -2, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", pPars->fUsePudlak? "yes": "no" ); @@ -21455,7 +21466,6 @@ usage: Abc_Print( -2, "\t-q : toggle using property in two last timeframes [default = %s]\n", pPars->fUseTwoFrames? "yes": "no" ); Abc_Print( -2, "\t-k : toggle solving each output separately [default = %s]\n", pPars->fUseSeparate? "yes": "no" ); Abc_Print( -2, "\t-d : toggle dropping (replacing by 0) SAT outputs (with -k is used) [default = %s]\n", pPars->fDropSatOuts? "yes": "no" ); - Abc_Print( -2, "\t-f : toggle dumping inductive invariant into a file [default = %s]\n", pPars->fDropInvar? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/proof/int/int.h b/src/proof/int/int.h index 97d628b4..906d8aaf 100644 --- a/src/proof/int/int.h +++ b/src/proof/int/int.h @@ -66,6 +66,7 @@ struct Inter_ManParams_t_ int fDropInvar; // dump inductive invariant into file int fVerbose; // print verbose statistics int iFrameMax; // the time frame reached + char * pFileName; // file name to dump interpolant }; //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/int/intInt.h b/src/proof/int/intInt.h index 85b9bfa2..bf591b7a 100644 --- a/src/proof/int/intInt.h +++ b/src/proof/int/intInt.h @@ -69,6 +69,7 @@ struct Inter_Man_t_ int nConfCur; // the current number of conflicts int nConfLimit; // the limit on the number of conflicts int fVerbose; // the verbosiness flag + char * pFileName; // runtime clock_t timeRwr; clock_t timeCnf; diff --git a/src/proof/int/intMan.c b/src/proof/int/intMan.c index e419da86..6dbf6f66 100644 --- a/src/proof/int/intMan.c +++ b/src/proof/int/intMan.c @@ -52,6 +52,7 @@ Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars ) p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) ); p->nConfLimit = pPars->nBTLimit; p->fVerbose = pPars->fVerbose; + p->pFileName = pPars->pFileName; p->pAig = pAig; if ( pPars->fDropInvar ) p->vInters = Vec_PtrAlloc( 100 ); @@ -102,14 +103,15 @@ void Inter_ManClean( Inter_Man_t * p ) ***********************************************************************/ void Inter_ManInterDump( Inter_Man_t * p, int fProved ) { + char * pFileName = p->pFileName ? p->pFileName : "invar.aig"; Aig_Man_t * pMan; pMan = Aig_ManDupArray( p->vInters ); - Ioa_WriteAiger( pMan, "invar.aig", 0, 0 ); + Ioa_WriteAiger( pMan, pFileName, 0, 0 ); Aig_ManStop( pMan ); if ( fProved ) - printf( "Inductive invariant is dumped into file \"invar.aig\".\n" ); + printf( "Inductive invariant is dumped into file \"%s\".\n", pFileName ); else - printf( "Interpolants are dumped into file \"inter.aig\".\n" ); + printf( "Interpolants are dumped into file \"%s\".\n", pFileName ); } /**Function************************************************************* |