From 01dd4f1aadcfc05f26f2ca00bd8afaa5c63ecb6c Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 17 May 2021 19:08:51 +0200 Subject: [PATCH] Replace smt_name by aliases (#6541) This PR replaces the confusing co-existence of long and smt_name for options by long and a list of alias. --- src/options/arith_options.toml | 2 - src/options/base_options.toml | 12 +- src/options/bv_options.toml | 3 - src/options/datatypes_options.toml | 1 - src/options/decision_options.toml | 2 +- src/options/expr_options.toml | 1 - src/options/mkoptions.py | 140 ++++++++++++---------- src/options/parser_options.toml | 5 +- src/options/prop_options.toml | 3 +- src/options/resource_manager_options.toml | 5 +- src/options/smt_options.toml | 15 +-- src/options/theory_options.toml | 1 - src/options/uf_options.toml | 2 +- 13 files changed, 94 insertions(+), 98 deletions(-) diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 3005829e0..a52f2144e 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -137,7 +137,6 @@ name = "Arithmetic theory" [[option]] name = "arithMLTrick" - smt_name = "miplib-trick" category = "regular" long = "miplib-trick" type = "bool" @@ -146,7 +145,6 @@ name = "Arithmetic theory" [[option]] name = "arithMLTrickSubstitutions" - smt_name = "miplib-trick-subs" category = "regular" long = "miplib-trick-subs=N" type = "unsigned" diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 2c61e057c..7b2cde54a 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -29,7 +29,7 @@ name = "Base" [[option]] name = "inputLanguage" - smt_name = "input-language" + alias = ["input-language"] category = "common" short = "L" long = "lang=LANG" @@ -41,7 +41,7 @@ name = "Base" [[option]] name = "outputLanguage" - smt_name = "output-language" + alias = ["output-language"] category = "common" long = "output-lang=LANG" type = "OutputLanguage" @@ -57,7 +57,7 @@ name = "Base" [[option]] name = "verbosity" - smt_name = "verbosity" + long = "verbosity=N" category = "regular" type = "int" default = "0" @@ -82,7 +82,6 @@ name = "Base" [[option]] name = "statistics" - smt_name = "stats" long = "stats" category = "common" type = "bool" @@ -91,7 +90,6 @@ name = "Base" [[option]] name = "statisticsAll" - smt_name = "stats-all" long = "stats-all" category = "expert" type = "bool" @@ -100,7 +98,6 @@ name = "Base" [[option]] name = "statisticsExpert" - smt_name = "stats-expert" long = "stats-expert" category = "expert" type = "bool" @@ -109,7 +106,6 @@ name = "Base" [[option]] name = "statisticsEveryQuery" - smt_name = "stats-every-query" long = "stats-every-query" category = "regular" type = "bool" @@ -132,7 +128,6 @@ name = "Base" help = "exit after preprocessing input" [[option]] - smt_name = "trace" category = "regular" short = "t" long = "trace=TAG" @@ -141,7 +136,6 @@ name = "Base" help = "trace something (e.g. -t pushpop), can repeat" [[option]] - smt_name = "debug" category = "regular" short = "d" long = "debug=TAG" diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index 34bdfcdaa..6cbf9cf37 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -3,7 +3,6 @@ name = "Bitvector theory" [[option]] name = "bvSatSolver" - smt_name = "bv-sat-solver" category = "expert" long = "bv-sat-solver=MODE" type = "SatSolverMode" @@ -22,7 +21,6 @@ name = "Bitvector theory" [[option]] name = "bitblastMode" - smt_name = "bitblast" category = "regular" long = "bitblast=MODE" type = "BitblastMode" @@ -104,7 +102,6 @@ name = "Bitvector theory" [[option]] name = "boolToBitvector" - smt_name = "bool-to-bv" category = "regular" long = "bool-to-bv=MODE" type = "BoolToBVMode" diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index 107c7dd94..7c6a55095 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -23,7 +23,6 @@ name = "Datatypes theory" [[option]] name = "dtPoliteOptimize" - smt_name = "dt-polite-optimize" category = "experimental" long = "dt-polite-optimize" type = "bool" diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml index d8c8a15b6..b3d18aebf 100644 --- a/src/options/decision_options.toml +++ b/src/options/decision_options.toml @@ -3,7 +3,7 @@ name = "Decision heuristics" [[option]] name = "decisionMode" - smt_name = "decision-mode" + alias = ["decision-mode"] category = "regular" long = "decision=MODE" type = "DecisionMode" diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml index 52f351348..94a9db05b 100644 --- a/src/options/expr_options.toml +++ b/src/options/expr_options.toml @@ -12,7 +12,6 @@ name = "Expression package" [[option]] name = "defaultDagThresh" - smt_name = "dag-thresh" category = "regular" long = "dag-thresh=N" type = "int" diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index a9ef65899..4c3524456 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -55,7 +55,8 @@ MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option'] OPTION_ATTR_REQ = ['category', 'type'] OPTION_ATTR_ALL = OPTION_ATTR_REQ + [ - 'name', 'help', 'help_mode', 'smt_name', 'short', 'long', 'default', + 'name', 'short', 'long', 'alias', + 'help', 'help_mode', 'default', 'includes', 'handler', 'predicates', 'alternate', 'mode' ] @@ -288,6 +289,13 @@ class Option(object): assert attr in self.__dict__ if attr == 'alternate' or val: self.__dict__[attr] = val + self.long_name = None + self.long_opt = None + if self.long: + r = self.long.split('=', 1) + self.long_name = r[0] + if len(r) > 1: + self.long_opt = r[1] def die(msg): @@ -351,13 +359,13 @@ def long_get_option(name): return name.split('=')[0] -def get_smt_name(option): +def get_long_name(option): """ - Determine the name of the option used as SMT option name. If no smt_name is - given it defaults to the long option name. + Determine the name of the option used as option name. """ - assert option.smt_name or option.long - return option.smt_name if option.smt_name else long_get_option(option.long) + if option.long: + return long_get_option(option.long) + return None def is_numeric_cpp_type(ctype): @@ -381,24 +389,29 @@ def format_include(include): return '#include "{}"'.format(include) -def help_format_options(short_name, long_name): +def help_format_options(option): """ Format short and long options for the cmdline documentation - (--long | -short). + (--long | --alias | -short). """ opts = [] - arg = None - if long_name: - opts.append('--{}'.format(long_name)) - long_name = long_name.split('=') - if len(long_name) > 1: - arg = long_name[1] - - if short_name: - if arg: - opts.append('-{} {}'.format(short_name, arg)) + if option.long: + if option.long_opt: + opts.append('--{}={}'.format(option.long_name, option.long_opt)) else: - opts.append('-{}'.format(short_name)) + opts.append('--{}'.format(option.long_name)) + + if option.alias: + if option.long_opt: + opts.extend(['--{}={}'.format(a, option.long_opt) for a in option.alias]) + else: + opts.extend(['--{}'.format(a) for a in option.alias]) + + if option.short: + if option.long_opt: + opts.append('-{} {}'.format(option.short, option.long_opt)) + else: + opts.append('-{}'.format(option.short)) return ' | '.join(opts) @@ -571,41 +584,32 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): modes=''.join(mode_impl))) -def docgen(category, name, smt_name, short_name, long_name, ctype, default, - help_msg, alternate, help_common, help_others): +def docgen_option(option, help_common, help_others): """ - Generate the documentation for --help. + Generate documentation for options. """ - ### Generate documentation - if category == 'common': - doc_cmd = help_common - else: - doc_cmd = help_others + if option.category == 'undocumented': + return - help_msg = help_msg if help_msg else '[undocumented]' - if category == 'expert': + help_msg = option.help + if option.category == 'expert': help_msg += ' (EXPERTS only)' - opts = help_format_options(short_name, long_name) + opts = help_format_options(option) # Generate documentation for cmdline options - if opts and category != 'undocumented': + if opts and option.category != 'undocumented': help_cmd = help_msg - if ctype == 'bool' and alternate: + if option.type == 'bool' and option.alternate: help_cmd += ' [*]' - doc_cmd.extend(help_format(help_cmd, opts)) - + + res = help_format(help_cmd, opts) -def docgen_option(option, help_common, help_others): - """ - Generate documentation for options. - """ - docgen(option.category, option.name, option.smt_name, - option.short, option.long, option.type, option.default, - option.help, option.alternate, - help_common, - help_others) + if option.category == 'common': + help_common.extend(res) + else: + help_others.extend(res) def add_getopt_long(long_name, argument_req, getopt_long): @@ -651,7 +655,7 @@ def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp): for option in \ sorted(module.options, key=lambda x: x.long if x.long else x.name): assert option.type != 'void' or option.name is None - assert option.name or option.smt_name or option.short or option.long + assert option.name or option.short or option.long argument_req = option.type not in ['bool', 'void'] docgen_option(option, help_common, help_others) @@ -694,10 +698,17 @@ def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp): if option.long: cases.append( - 'case {}:// --{}'.format( + 'case {}: // --{}'.format( g_getopt_long_start + len(getopt_long), option.long)) add_getopt_long(option.long, argument_req, getopt_long) + if option.alias: + for alias in option.alias: + cases.append( + 'case {}: // --{}'.format( + g_getopt_long_start + len(getopt_long), + alias)) + add_getopt_long(alias, argument_req, getopt_long) if cases: if option.type == 'bool' and option.name: @@ -715,45 +726,43 @@ def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp): elif handler: cases.append('{};'.format(handler)) - cases.append(' break;\n') + cases.append(' break;') options_handler.extend(cases) # Generate handlers for setOption/getOption - if option.smt_name or option.long: - # Make smt_name and long name available via set/get-option + if option.long: + # Make long and alias names available via set/get-option keys = set() - if option.smt_name: - keys.add(option.smt_name) if option.long: keys.add(long_get_option(option.long)) + if option.alias: + keys.update(option.alias) assert keys cond = ' || '.join( ['key == "{}"'.format(x) for x in sorted(keys)]) - smtname = get_smt_name(option) - setoption_handlers.append('if({}) {{'.format(cond)) if option.type == 'bool': setoption_handlers.append( TPL_CALL_ASSIGN_BOOL.format( name=option.name, - option='"{}"'.format(smtname), + option='key', value='optionarg == "true"')) elif argument_req and option.name: setoption_handlers.append( TPL_CALL_ASSIGN.format( name=option.name, - option='"{}"'.format(smtname))) + option='key')) elif option.handler: h = 'handler->{handler}("{smtname}"' if argument_req: h += ', optionarg' h += ');' setoption_handlers.append( - h.format(handler=option.handler, smtname=smtname)) + h.format(handler=option.handler, smtname=option.long_name)) setoption_handlers.append('return;') setoption_handlers.append('}') @@ -785,17 +794,26 @@ def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp): 'case {}:// --no-{}'.format( g_getopt_long_start + len(getopt_long), option.long)) + + add_getopt_long('no-{}'.format(option.long), argument_req, + getopt_long) + if option.alias: + for alias in option.alias: + cases.append( + 'case {}:// --no-{}'.format( + g_getopt_long_start + len(getopt_long), + alias)) + add_getopt_long('no-{}'.format(alias), argument_req, + getopt_long) + cases.append( TPL_CALL_ASSIGN_BOOL.format( name=option.name, option='option', value='false')) - cases.append(' break;\n') + cases.append(' break;') options_handler.extend(cases) - add_getopt_long('no-{}'.format(option.long), argument_req, - getopt_long) - - optname = option.smt_name if option.smt_name else option.long + optname = option.long # collect options available to the SMT-frontend if optname: options_smt.append('"{}",'.format(optname)) @@ -822,7 +840,7 @@ def codegen_all_modules(modules, dst_dir, tpl_options_h, tpl_options_cpp): tpl = None if option.type == 'bool': tpl = TPL_IMPL_ASSIGN_BOOL - elif option.short or option.long or option.smt_name: + elif option.short or option.long: tpl = TPL_IMPL_ASSIGN if tpl: custom_handlers.append(tpl.format( diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml index 4b3d01b99..6fc683368 100644 --- a/src/options/parser_options.toml +++ b/src/options/parser_options.toml @@ -17,7 +17,7 @@ name = "Parser" [[option]] name = "semanticChecks" - smt_name = "semantic-checks" + long = "semantic-checks" category = "regular" type = "bool" default = "DO_SEMANTIC_CHECKS_BY_DEFAULT" @@ -25,7 +25,7 @@ name = "Parser" [[option]] name = "globalDeclarations" - smt_name = "global-declarations" + long = "global-declarations" category = "regular" type = "bool" default = "false" @@ -52,7 +52,6 @@ name = "Parser" [[option]] name = "forceLogicString" - smt_name = "force-logic" category = "expert" long = "force-logic=LOGIC" type = "std::string" diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml index 9cddc9470..69dad8d63 100644 --- a/src/options/prop_options.toml +++ b/src/options/prop_options.toml @@ -3,7 +3,7 @@ name = "SAT layer" [[option]] name = "satRandomFreq" - smt_name = "random-frequency" + alias = ["random-frequency"] category = "regular" long = "random-freq=P" type = "double" @@ -13,7 +13,6 @@ name = "SAT layer" [[option]] name = "satRandomSeed" - smt_name = "random-seed" category = "regular" long = "random-seed=S" type = "uint32_t" diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml index 96bc30aaa..88bacce1b 100644 --- a/src/options/resource_manager_options.toml +++ b/src/options/resource_manager_options.toml @@ -3,7 +3,6 @@ name = "Resource Manager options" [[option]] name = "cumulativeMillisecondLimit" - smt_name = "tlimit" category = "common" long = "tlimit=MS" type = "uint64_t" @@ -11,7 +10,6 @@ name = "Resource Manager options" [[option]] name = "perCallMillisecondLimit" - smt_name = "tlimit-per" category = "common" long = "tlimit-per=MS" type = "uint64_t" @@ -19,7 +17,6 @@ name = "Resource Manager options" [[option]] name = "cumulativeResourceLimit" - smt_name = "rlimit" category = "common" long = "rlimit=N" type = "uint64_t" @@ -27,7 +24,7 @@ name = "Resource Manager options" [[option]] name = "perCallResourceLimit" - smt_name = "reproducible-resource-limit" + alias = ["reproducible-resource-limit"] category = "common" long = "rlimit-per=N" type = "uint64_t" diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 7328c44ad..22d05f6f7 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -3,7 +3,6 @@ name = "SMT layer" [[option]] name = "dumpModeString" - smt_name = "dump" category = "common" long = "dump=MODE" type = "std::string" @@ -11,7 +10,6 @@ name = "SMT layer" [[option]] name = "dumpToFileName" - smt_name = "dump-to" category = "common" long = "dump-to=FILE" type = "std::string" @@ -27,7 +25,7 @@ name = "SMT layer" [[option]] name = "simplificationMode" - smt_name = "simplification-mode" + alias = ["simplification-mode"] category = "regular" long = "simplification=MODE" type = "SimplificationMode" @@ -51,7 +49,7 @@ name = "SMT layer" [[option]] name = "expandDefinitions" - smt_name = "expand-definitions" + long = "expand-definitions" category = "regular" type = "bool" default = "false" @@ -193,7 +191,6 @@ name = "SMT layer" [[option]] name = "unsatCoresMode" - smt_name = "unsat-cores-mode" category = "regular" long = "unsat-cores-mode=MODE" type = "UnsatCoresMode" @@ -265,7 +262,7 @@ name = "SMT layer" [[option]] name = "interactiveMode" - smt_name = "interactive-mode" + long = "interactive-mode" category = "undocumented" type = "bool" predicates = ["setProduceAssertions"] @@ -384,7 +381,7 @@ name = "SMT layer" [[option]] name = "modelUninterpPrint" - smt_name = "model-uninterp-print" + alias = ["model-uninterp-print"] category = "regular" long = "model-u-print=MODE" type = "ModelUninterpPrintMode" @@ -415,14 +412,14 @@ name = "SMT layer" [[option]] name = "regularChannelName" - smt_name = "regular-output-channel" + long = "regular-output-channel=CHANNEL" category = "regular" type = "std::string" help = "set the regular output channel of the solver" [[option]] name = "diagnosticChannelName" - smt_name = "diagnostic-output-channel" + long = "diagnostic-output-channel=CHANNEL" category = "regular" type = "std::string" help = "set the diagnostic output channel of the solver" diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 0c4fa7aca..ec11d17ec 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -3,7 +3,6 @@ name = "Theory layer" [[option]] name = "theoryOfMode" - smt_name = "theoryof-mode" category = "expert" long = "theoryof-mode=MODE" type = "TheoryOfMode" diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index 8b99493e1..81b119964 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -3,7 +3,7 @@ name = "Uninterpreted functions theory" [[option]] name = "ufSymmetryBreaker" - smt_name = "uf-symmetry-breaker" + alias = ["uf-symmetry-breaker"] category = "regular" long = "symmetry-breaker" type = "bool" -- 2.30.2