diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 220 |
1 files changed, 10 insertions, 210 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 933f9778..f10be02b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -23320,222 +23320,22 @@ usage: ***********************************************************************/ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv ) { - abctime clk; - int c; - satoko_opts_t opts; + extern satoko_opts_t * Cmd_DeriveOptionFromSettings( int argc, char ** argv ); + // create default options + satoko_opts_t opts, * popts; satoko_default_opts(&opts); - Extra_UtilGetoptReset(); -#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 ) - { - case 'C': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); - goto usage; - } - opts.conf_limit = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( opts.conf_limit < 0 ) - goto usage; - break; - case 'P': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); - goto usage; - } - opts.prop_limit = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( opts.prop_limit < 0 ) - goto usage; - break; - case 'D': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-D\" should be followed by an float.\n" ); - goto usage; - } - opts.f_rst = atof(argv[globalUtilOptind]); - globalUtilOptind++; - if ( opts.f_rst < 0 ) - goto usage; - break; - case 'E': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-E\" should be followed by an float.\n" ); - goto usage; - } - opts.b_rst = atof(argv[globalUtilOptind]); - globalUtilOptind++; - if ( opts.b_rst < 0 ) - goto usage; - break; - case 'F': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); - goto usage; - } - 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" ); - goto usage; - } - 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" ); - goto usage; - } - 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" ); - goto usage; - } - 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" ); - goto usage; - } - 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" ); - goto usage; - } - 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" ); - goto usage; - } - 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" ); - goto usage; - } - opts.learnt_ratio = atof(argv[globalUtilOptind]) / 100; - globalUtilOptind++; - if ( opts.learnt_ratio < 0 ) - goto usage; - break; - case 'N': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); - goto usage; - } - opts.garbage_max_ratio = atof(argv[globalUtilOptind]) / 100; - globalUtilOptind++; - if ( opts.garbage_max_ratio < 0 ) - goto usage; - break; - case 'O': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); - goto usage; - } - 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" ); - goto usage; - } - 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" ); - goto usage; - } - opts.clause_decay = atof(argv[globalUtilOptind]); - globalUtilOptind++; - if ( opts.clause_decay < 0 ) - goto usage; - break; - case 'S': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-S\" should be followed by an float.\n" ); - goto usage; - } - opts.var_decay = atof(argv[globalUtilOptind]); - globalUtilOptind++; - if ( opts.var_decay < 0 ) - goto usage; - 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" ); - goto usage; - } - 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" ); - goto usage; - } - opts.var_act_rescale = (unsigned)strtol(argv[globalUtilOptind], NULL, 16); - globalUtilOptind++; - break; -#endif - case 'h': - goto usage; - case 'v': - opts.verbose ^= 1; - break; - default: - goto usage; - } - } + // override default options + popts = Cmd_DeriveOptionFromSettings( argc, argv ); + if ( popts == NULL ) + goto usage; + memcpy( &opts, popts, sizeof(satoko_opts_t) ); + ABC_FREE( popts ); if ( argc == globalUtilOptind + 1 ) { + abctime clk; char * pFileName = argv[globalUtilOptind]; satoko_t * p; int status; |