From: Gereon Kremer <gkremer@stanford.edu>
Date: Wed, 17 Nov 2021 01:45:32 +0000 (-0800)
Subject: make default and modes strings instead of enum values (#7656)
X-Git-Tag: cvc5-1.0.0~809
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4c9df988d43b237c22bd3b667f7e5c35cf0a737a;p=cvc5.git

make default and modes strings instead of enum values (#7656)

For mode options, getOptionInfo would hold the name of the enum values for the default value and the available modes. This PR changes this to hold the string values instead, which is what users can actually use via the API.
---

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 23a69219d..3022c5d4b 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -393,7 +393,9 @@ def generate_getinfo_impl(modules):
         elif option.type == 'double' or is_numeric_cpp_type(option.type):
             constr = 'OptionInfo::NumberInfo<{type}>{{{default}, {value}, {minimum}, {maximum}}}'
         elif option.mode:
-            fmt['modes'] = ', '.join(['"{}"'.format(s) for s in sorted(option.mode.keys())])
+            modes = { key: value[0]['name'] for key,value in option.mode.items() }
+            fmt['modes'] = ', '.join(['"{}"'.format(s) for s in sorted(modes.values())])
+            fmt['default'] = modes[fmt['default']]
             constr = 'OptionInfo::ModeInfo{{"{default}", {value}, {{ {modes} }}}}'
         else:
             constr = 'OptionInfo::VoidInfo{{}}'
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index b24c85496..ba5bd655a 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -1390,9 +1390,9 @@ TEST_F(TestApiBlackSolver, getOptionInfo)
     EXPECT_EQ(std::vector<std::string>{}, info.aliases);
     EXPECT_TRUE(std::holds_alternative<OptionInfo::ModeInfo>(info.valueInfo));
     auto modeInfo = std::get<OptionInfo::ModeInfo>(info.valueInfo);
-    EXPECT_EQ("NONE", modeInfo.defaultValue);
+    EXPECT_EQ("none", modeInfo.defaultValue);
     EXPECT_EQ("none", modeInfo.currentValue);
-    EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "NONE")
+    EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "none")
                 != modeInfo.modes.end());
   }
 }
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 40a7d4157..ed2f7491d 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1435,9 +1435,9 @@ class SolverTest
           () -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases())));
       assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ModeInfo.class));
       OptionInfo.ModeInfo modeInfo = (OptionInfo.ModeInfo) info.getBaseInfo();
-      assertions.add(() -> assertEquals("NONE", modeInfo.getDefaultValue()));
+      assertions.add(() -> assertEquals("none", modeInfo.getDefaultValue()));
       assertions.add(() -> assertEquals("none", modeInfo.getCurrentValue()));
-      assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("NONE")));
+      assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("none")));
     }
     assertAll(assertions);
   }