diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-07 23:26:23 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-07 23:26:23 -0700 |
| commit | 5ca4f3cf9f40ab372d9900fc3382aaf9d0adbcc7 (patch) | |
| tree | f8aea25b4d9757d6b44b312c4244f92da7eb95c3 /src/base/abci | |
| parent | 548e04192bb543890d9f6b4dfef7865d6e5553f6 (diff) | |
| download | abc-5ca4f3cf9f40ab372d9900fc3382aaf9d0adbcc7.tar.gz abc-5ca4f3cf9f40ab372d9900fc3382aaf9d0adbcc7.tar.bz2 abc-5ca4f3cf9f40ab372d9900fc3382aaf9d0adbcc7.zip | |
Updating &gla_refine to perform suffic refinement.
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 21 |
1 files changed, 17 insertions, 4 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f24f9e12..3d293ba5 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -27820,12 +27820,13 @@ usage: ***********************************************************************/ int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int fVerbose ); + extern int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFrameExtra, int fVerbose ); int iFrameStart = 0; + int iFrameExtra = 0; int fMinCut = 1; int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Fmvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FGmvh" ) ) != EOF ) { switch ( c ) { @@ -27840,6 +27841,17 @@ int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( iFrameStart < 0 ) goto usage; break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + iFrameExtra = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iFrameExtra < 0 ) + goto usage; + break; case 'm': fMinCut ^= 1; break; @@ -27867,14 +27879,15 @@ int Abc_CommandAbc9GlaRefine( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9GlaRefine(): There is no counter-example.\n" ); return 1; } - pAbc->Status = Gia_ManNewRefine( pAbc->pGia, pAbc->pCex, iFrameStart, fVerbose ); + pAbc->Status = Gia_ManNewRefine( pAbc->pGia, pAbc->pCex, iFrameStart, iFrameExtra, fVerbose ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); return 0; usage: - Abc_Print( -2, "usage: &gla_refine [-F num] [-vh]\n" ); + Abc_Print( -2, "usage: &gla_refine [-FG num] [-vh]\n" ); Abc_Print( -2, "\t refines the pre-computed gate map using the counter-example\n" ); Abc_Print( -2, "\t-F num : starting timeframe for suffix refinement [default = %d]\n", iFrameStart ); + Abc_Print( -2, "\t-G num : the number of additional timeframes to try [default = %d]\n", iFrameExtra ); // Abc_Print( -2, "\t-m : toggle using min-cut to derive the refinements [default = %s]\n", fMinCut? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); |