From: Gereon Kremer <nafur42@gmail.com>
Date: Mon, 1 Nov 2021 22:28:54 +0000 (-0700)
Subject: Add explicit option enum value __MAX_VALUE (#7547)
X-Git-Tag: cvc5-1.0.0~914
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3243a93ed9ae38f7789f857b0f8f9cc160139620;p=cvc5.git

Add explicit option enum value __MAX_VALUE (#7547)

This PR fixes a subtle issue with the dict ordering changing across different python versions.
To store the flags of -o, we store a bitset with the index being the enum value cast to size_t. To specify the bitset size, we simply used the last enum value (in the toml file). This, however, assumes that the order within dictionaries is stable: toml simply puts all modes in a python dict.
This PR avoids this issue by introducing an explicit __MAX_VALUE enum value. Note that this also avoids the need to update the bitset definition when new output tags are added.
---

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index d59d9cdea..ec3bd870d 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -185,7 +185,7 @@ name   = "Base"
   name       = "outputTagHolder"
   category   = "undocumented"
   includes   = ["<bitset>"]
-  type       = "std::bitset<static_cast<size_t>(OutputTag::RAW_BENCHMARK)+1>"
+  type       = "std::bitset<static_cast<size_t>(OutputTag::__MAX_VALUE)+1>"
 
 [[option]]
   name       = "printSuccess"
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index dfd48d7f4..0db16e7c6 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -292,7 +292,6 @@ def generate_get_impl(modules):
 
 def _set_handlers(option):
     """Render handler call for options::set()."""
-    optname = option.long_name if option.long else ""
     if option.handler:
         if option.type == 'void':
             return 'opts.handler().{}(name)'.format(option.handler)
@@ -307,7 +306,6 @@ def _set_predicates(option):
     """Render predicate calls for options::set()."""
     if option.type == 'void':
         return []
-    optname = option.long_name if option.long else ""
     assert option.type != 'void'
     res = []
     if option.minimum:
@@ -419,7 +417,8 @@ def generate_module_includes(module):
 
 TPL_MODE_DECL = '''enum class {type}
 {{
-  {values}
+  {values},
+  __MAX_VALUE = {maxvalue}
 }};
 std::ostream& operator<<(std::ostream& os, {type} mode);
 {type} stringTo{type}(const std::string& optarg);
@@ -432,10 +431,11 @@ def generate_module_mode_decl(module):
     for option in module.options:
         if option.name is None or not option.mode:
             continue
+        values = list(option.mode.keys())
         res.append(
             TPL_MODE_DECL.format(type=option.type,
-                                 values=wrap_line(
-                                     ', '.join(option.mode.keys()), 2)))
+                                 values=wrap_line(', '.join(values), 2),
+                                 maxvalue=values[-1]))
     return '\n'.join(res)