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.

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"