From 5d717256d3b856d8f29c4a5e442af624f0b0bb69 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 10 Feb 2017 18:14:06 -0800 Subject: Updates to the autotuner. --- src/base/cmd/cmdAuto.c | 209 +++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 186 insertions(+), 23 deletions(-) (limited to 'src/base/cmd') diff --git a/src/base/cmd/cmdAuto.c b/src/base/cmd/cmdAuto.c index 35f155fa..e279b19d 100644 --- a/src/base/cmd/cmdAuto.c +++ b/src/base/cmd/cmdAuto.c @@ -241,7 +241,11 @@ satoko_opts_t * Cmd_DeriveOptionFromSettings( int argc, char ** argv ) satoko_opts_t opts, * pOpts; satoko_default_opts(&opts); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CVWhv" ) ) != EOF ) +#ifdef SATOKO_ACT_VAR_FIXED + while ( ( c = Extra_UtilGetopt( argc, argv, "CPDEFGHIJKLMNOQRSTUhv" ) ) != EOF ) +#else + while ( ( c = Extra_UtilGetopt( argc, argv, "CPDEFGHIJKLMNOQRShv" ) ) != EOF ) +#endif { switch ( c ) { @@ -256,31 +260,190 @@ satoko_opts_t * Cmd_DeriveOptionFromSettings( int argc, char ** argv ) if ( opts.conf_limit < 0 ) return NULL; break; - case 'V': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" ); - return NULL; - } - opts.var_decay = atof(argv[globalUtilOptind]); - globalUtilOptind++; - if ( opts.var_decay < 0 ) - return NULL; - break; - case 'W': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" ); - return NULL; - } - opts.clause_decay = atof(argv[globalUtilOptind]); - globalUtilOptind++; - if ( opts.clause_decay < 0 ) - return NULL; - break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + return NULL; + } + opts.prop_limit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( opts.prop_limit < 0 ) + return NULL; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an float.\n" ); + return NULL; + } + opts.f_rst = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( opts.f_rst < 0 ) + return NULL; + break; + case 'E': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-E\" should be followed by an float.\n" ); + return NULL; + } + opts.b_rst = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( opts.b_rst < 0 ) + return NULL; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + return NULL; + } + opts.fst_block_rst = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + return NULL; + } + opts.sz_lbd_bqueue = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'H': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" ); + return NULL; + } + opts.sz_trail_bqueue = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + return NULL; + } + opts.n_conf_fst_reduce = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'J': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" ); + return NULL; + } + opts.inc_reduce = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + return NULL; + } + opts.inc_special_reduce = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + return NULL; + } + opts.lbd_freeze_clause = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + return NULL; + } + opts.learnt_ratio = atof(argv[globalUtilOptind]) / 100; + globalUtilOptind++; + if ( opts.learnt_ratio < 0 ) + return NULL; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + return NULL; + } + opts.garbage_max_ratio = atof(argv[globalUtilOptind]) / 100; + globalUtilOptind++; + if ( opts.garbage_max_ratio < 0 ) + return NULL; + break; + case 'O': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); + return NULL; + } + opts.clause_max_sz_bin_resol = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'Q': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); + return NULL; + } + opts.clause_min_lbd_bin_resol = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an float.\n" ); + return NULL; + } + opts.clause_decay = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( opts.clause_decay < 0 ) + return NULL; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an float.\n" ); + return NULL; + } + opts.var_decay = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( opts.var_decay < 0 ) + return NULL; + break; +#ifdef SATOKO_ACT_VAR_FIXED + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an float.\n" ); + return NULL; + } + opts.var_act_limit = (unsigned)strtol(argv[globalUtilOptind], NULL, 16); + globalUtilOptind++; + break; + case 'U': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-U\" should be followed by an float.\n" ); + return NULL; + } + opts.var_act_rescale = (unsigned)strtol(argv[globalUtilOptind], NULL, 16); + globalUtilOptind++; + break; +#endif + case 'h': + return NULL; case 'v': opts.verbose ^= 1; break; + default: return NULL; } -- cgit v1.2.3