diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2018-09-08 17:15:37 +0300 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2018-09-08 17:15:37 +0300 |
commit | d798d61637ad632fdb3656194fcb8626e8f6df3d (patch) | |
tree | 6c8071ecced7444b56b706c862683a6cbc5b3dd4 /src/base/abci/abc.c | |
parent | c76af92d19388d3fa26595d0698cb33d50dc9629 (diff) | |
download | abc-d798d61637ad632fdb3656194fcb8626e8f6df3d.tar.gz abc-d798d61637ad632fdb3656194fcb8626e8f6df3d.tar.bz2 abc-d798d61637ad632fdb3656194fcb8626e8f6df3d.zip |
Adding timeout to twoexact and lutexact.
Diffstat (limited to 'src/base/abci/abc.c')
-rw-r--r-- | src/base/abci/abc.c | 34 |
1 files changed, 29 insertions, 5 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index afbf7e00..31d75e6a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8293,7 +8293,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INaogvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INTaogvh" ) ) != EOF ) { switch ( c ) { @@ -8319,6 +8319,17 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nNodes < 0 ) goto usage; break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->RuntimeLim = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->RuntimeLim < 0 ) + goto usage; + break; case 'a': pPars->fOnlyAnd ^= 1; break; @@ -8366,10 +8377,11 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: twoexact [-IN <num>] [-aogvh] <hex>\n" ); + Abc_Print( -2, "usage: twoexact [-INT <num>] [-aogvh] <hex>\n" ); Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" ); Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars ); - Abc_Print( -2, "\t-N <num> : the number of MAJ3 nodes [default = %d]\n", pPars->nNodes ); + Abc_Print( -2, "\t-N <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes ); + Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" ); @@ -8405,7 +8417,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INKiaogvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INKTiaogvh" ) ) != EOF ) { switch ( c ) { @@ -8442,6 +8454,17 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nLutSize < 0 ) goto usage; break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->RuntimeLim = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->RuntimeLim < 0 ) + goto usage; + break; case 'i': pPars->fUseIncr ^= 1; break; @@ -8497,11 +8520,12 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutexact [-INK <num>] [-iaogvh] <hex>\n" ); + Abc_Print( -2, "usage: lutexact [-INKT <num>] [-iaogvh] <hex>\n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-K <num> : the number of node fanins [default = %d]\n", pPars->nLutSize ); + Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); |