diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-28 16:55:25 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-28 16:55:25 -0700 |
commit | 9e1765216ba5f64d89a0dc93e33fb95c84a0c779 (patch) | |
tree | a3a35a93e30f5e22f22ee0a8fd51f5d12107d23a /src/proof/int/intMan.c | |
parent | 266667d8b231721c060495e7fb737e35bfbe575b (diff) | |
download | abc-9e1765216ba5f64d89a0dc93e33fb95c84a0c779.tar.gz abc-9e1765216ba5f64d89a0dc93e33fb95c84a0c779.tar.bz2 abc-9e1765216ba5f64d89a0dc93e33fb95c84a0c779.zip |
Added option 'int -I <filename>' to specify file names to dump invariants.
Diffstat (limited to 'src/proof/int/intMan.c')
-rw-r--r-- | src/proof/int/intMan.c | 8 |
1 files changed, 5 insertions, 3 deletions
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************************************************************* |