Add API unit tests for options (#8339)

This PR adds some unit tests that cover some remaining cases of getOptionInfo() and getDriverOptions().
It also adds some fixes to the java bindings of these methods.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index a4dc4e427fca16c7fa5c6de926ed9973c5459622..459ded7315c05cb8987be2edac952ce8ad1667e5 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -6712,12 +6712,12 @@ std::ostream& operator<<(std::ostream& os, const OptionInfo& oi)
   std::visit(overloaded{
                  [&os](const OptionInfo::VoidInfo& vi) { os << " | void"; },
                  [&os](const OptionInfo::ValueInfo<bool>& vi) {
-                   os << " | bool | " << vi.currentValue << " | default "
-                      << vi.defaultValue;
+                   os << std::boolalpha << " | bool | " << vi.currentValue
+                      << " | default " << vi.defaultValue << std::noboolalpha;
                  },
                  [&os](const OptionInfo::ValueInfo<std::string>& vi) {
-                   os << " | string | " << vi.currentValue << " | default "
-                      << vi.defaultValue;
+                   os << " | string | \"" << vi.currentValue
+                      << "\" | default \"" << vi.defaultValue << "\"";
                  },
                  [&printNum](const OptionInfo::NumberInfo<int64_t>& vi) {
                    printNum("int64_t", vi);

diff --git a/src/api/java/io/github/cvc5/api/OptionInfo.java b/src/api/java/io/github/cvc5/api/OptionInfo.java
index 6f60244208907071c2939a9b45f3ced2f0d69514..1c47eeedb61503c6f72b74ae8f4f47d0550601b5 100644 (file)
--- a/src/api/java/io/github/cvc5/api/OptionInfo.java
+++ b/src/api/java/io/github/cvc5/api/OptionInfo.java
@@ -53,6 +53,11 @@ public class OptionInfo extends AbstractPointer
     return pointer;
   }
 
+  public String toString()
+  {
+    return toString(pointer);
+  }
+
   /**
    * @return a string representation of this optionInfo.
    */
@@ -66,7 +71,7 @@ public class OptionInfo extends AbstractPointer
   }
 
   /** Has the current and the default value */
-  public abstract class ValueInfo<T> extends BaseInfo
+  public class ValueInfo<T> extends BaseInfo
   {
     private final T defaultValue;
     private final T currentValue;

diff --git a/src/api/java/jni/option_info.cpp b/src/api/java/jni/option_info.cpp
index da2a485e3bf313f067810d98d9d3193f7c352af2..f889f7e1273d07540b3c9e029c7dbc1bc10ed050 100644 (file)
--- a/src/api/java/jni/option_info.cpp
+++ b/src/api/java/jni/option_info.cpp
@@ -323,9 +323,22 @@ Java_io_github_cvc5_api_OptionInfo_intValue(JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   OptionInfo* current = reinterpret_cast<OptionInfo*>(pointer);
-  std::int64_t value = current->intValue();
-  jobject ret = getBigIntegerObject<std::int64_t>(env, value);
-  return ret;
+  if (std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(
+          current->valueInfo))
+  {
+    std::uint64_t value = current->uintValue();
+    jobject ret = getBigIntegerObject<std::uint64_t>(env, value);
+    return ret;
+  }
+  if (std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(
+          current->valueInfo))
+  {
+    std::int64_t value = current->intValue();
+    jobject ret = getBigIntegerObject<std::int64_t>(env, value);
+    return ret;
+  }
+  throw CVC5ApiRecoverableException("Option is neither int64_t nor uint64_t");
+  return jobject();
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr);
 }
 

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 2c9b4ee48ad86a58306043e6b8ffe7e646b7939a..b31aa9ad1879fe9b1353a147842b9ed1bf2e2139 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -1530,6 +1530,25 @@ TEST_F(TestApiBlackSolver, getOptionInfo)
     EXPECT_EQ("verbose", info.name);
     EXPECT_EQ(std::vector<std::string>{}, info.aliases);
     EXPECT_TRUE(std::holds_alternative<OptionInfo::VoidInfo>(info.valueInfo));
+    std::stringstream ss;
+    ss << info;
+    ASSERT_EQ(ss.str(), "OptionInfo{ verbose | void }");
+  }
+  {
+    // bool type with default
+    api::OptionInfo info = d_solver.getOptionInfo("print-success");
+    EXPECT_EQ("print-success", info.name);
+    EXPECT_EQ(std::vector<std::string>{}, info.aliases);
+    EXPECT_TRUE(
+        std::holds_alternative<OptionInfo::ValueInfo<bool>>(info.valueInfo));
+    auto valInfo = std::get<OptionInfo::ValueInfo<bool>>(info.valueInfo);
+    EXPECT_EQ(false, valInfo.defaultValue);
+    EXPECT_EQ(false, valInfo.currentValue);
+    ASSERT_EQ(info.boolValue(), false);
+    std::stringstream ss;
+    ss << info;
+    ASSERT_EQ(ss.str(),
+              "OptionInfo{ print-success | bool | false | default false }");
   }
   {
     // int64 type with default
@@ -1543,6 +1562,25 @@ TEST_F(TestApiBlackSolver, getOptionInfo)
     EXPECT_EQ(0, numInfo.currentValue);
     EXPECT_FALSE(numInfo.minimum || numInfo.maximum);
     ASSERT_EQ(info.intValue(), 0);
+    std::stringstream ss;
+    ss << info;
+    ASSERT_EQ(ss.str(), "OptionInfo{ verbosity | int64_t | 0 | default 0 }");
+  }
+  {
+    // uint64 type with default
+    api::OptionInfo info = d_solver.getOptionInfo("rlimit");
+    EXPECT_EQ("rlimit", info.name);
+    EXPECT_EQ(std::vector<std::string>{}, info.aliases);
+    EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(
+        info.valueInfo));
+    auto numInfo = std::get<OptionInfo::NumberInfo<uint64_t>>(info.valueInfo);
+    EXPECT_EQ(0, numInfo.defaultValue);
+    EXPECT_EQ(0, numInfo.currentValue);
+    EXPECT_FALSE(numInfo.minimum || numInfo.maximum);
+    ASSERT_EQ(info.uintValue(), 0);
+    std::stringstream ss;
+    ss << info;
+    ASSERT_EQ(ss.str(), "OptionInfo{ rlimit | uint64_t | 0 | default 0 }");
   }
   {
     auto info = d_solver.getOptionInfo("random-freq");
@@ -1557,6 +1595,27 @@ TEST_F(TestApiBlackSolver, getOptionInfo)
     ASSERT_EQ(*ni.minimum, 0.0);
     ASSERT_EQ(*ni.maximum, 1.0);
     ASSERT_EQ(info.doubleValue(), 0.0);
+    std::stringstream ss;
+    ss << info;
+    ASSERT_EQ(ss.str(),
+              "OptionInfo{ random-freq, random-frequency | double | 0 | "
+              "default 0 | 0 <= x <= 1 }");
+  }
+  {
+    // string type with default
+    api::OptionInfo info = d_solver.getOptionInfo("force-logic");
+    EXPECT_EQ("force-logic", info.name);
+    EXPECT_EQ(std::vector<std::string>{}, info.aliases);
+    EXPECT_TRUE(std::holds_alternative<OptionInfo::ValueInfo<std::string>>(
+        info.valueInfo));
+    auto valInfo = std::get<OptionInfo::ValueInfo<std::string>>(info.valueInfo);
+    EXPECT_EQ("", valInfo.defaultValue);
+    EXPECT_EQ("", valInfo.currentValue);
+    ASSERT_EQ(info.stringValue(), "");
+    std::stringstream ss;
+    ss << info;
+    ASSERT_EQ(ss.str(),
+              "OptionInfo{ force-logic | string | \"\" | default \"\" }");
   }
   {
     // mode option
@@ -1572,9 +1631,22 @@ TEST_F(TestApiBlackSolver, getOptionInfo)
                 != modeInfo.modes.end());
     EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "none")
                 != modeInfo.modes.end());
+    std::stringstream ss;
+    ss << info;
+    ASSERT_EQ(ss.str(),
+              "OptionInfo{ simplification, simplification-mode | mode | batch "
+              "| default batch | modes: batch, none }");
   }
 }
 
+TEST_F(TestApiBlackSolver, getDriverOptions)
+{
+  auto dopts = d_solver.getDriverOptions();
+  EXPECT_EQ(dopts.err().rdbuf(), std::cerr.rdbuf());
+  EXPECT_EQ(dopts.in().rdbuf(), std::cin.rdbuf());
+  EXPECT_EQ(dopts.out().rdbuf(), std::cout.rdbuf());
+}
+  
 TEST_F(TestApiBlackSolver, getStatistics)
 {
   // do some array reasoning to make sure we have a double statistics

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 1c01e32b5d091da14ad5e93939c0b4f3e4351866..5c759b9ea7e7217f39d0fdc106e05eda36942331 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1502,6 +1502,22 @@ class SolverTest
       assertions.add(
           () -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases())));
       assertions.add(() -> assertTrue(info.getBaseInfo() instanceof OptionInfo.VoidInfo));
+      assertions.add(() -> assertEquals(info.toString(), "OptionInfo{ verbose | void }"));
+    }
+    {
+      // bool type with default
+      OptionInfo info = d_solver.getOptionInfo("print-success");
+      assertions.add(() -> assertEquals("print-success", info.getName()));
+      assertions.add(
+          () -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases())));
+      assertions.add(
+          () -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ValueInfo.class));
+      OptionInfo.ValueInfo<Boolean> valInfo =
+          (OptionInfo.ValueInfo<Boolean>) info.getBaseInfo();
+      assertions.add(() -> assertEquals(false, valInfo.getDefaultValue().booleanValue()));
+      assertions.add(() -> assertEquals(false, valInfo.getCurrentValue().booleanValue()));
+      assertions.add(() -> assertEquals(info.booleanValue(), false));
+      assertions.add(() -> assertEquals(info.toString(), "OptionInfo{ print-success | bool | false | default false }"));
     }
     {
       // int64 type with default
@@ -1516,10 +1532,24 @@ class SolverTest
       assertions.add(() -> assertEquals(0, numInfo.getDefaultValue().intValue()));
       assertions.add(() -> assertEquals(0, numInfo.getCurrentValue().intValue()));
       assertions.add(
-          () -> assertFalse(numInfo.getMinimum() != null || numInfo.getMaximum() != null));
+          () -> assertTrue(numInfo.getMinimum() == null && numInfo.getMaximum() == null));
       assertions.add(() -> assertEquals(info.intValue().intValue(), 0));
+      assertions.add(() -> assertEquals(info.toString(), "OptionInfo{ verbosity | int64_t | 0 | default 0 }"));
     }
     assertAll(assertions);
+    {
+      OptionInfo info = d_solver.getOptionInfo("rlimit");
+      assertEquals(info.getName(), "rlimit");
+      assertEquals(
+          Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
+      assertTrue(info.getBaseInfo().getClass() == OptionInfo.NumberInfo.class);
+      OptionInfo.NumberInfo<BigInteger> ni = (OptionInfo.NumberInfo<BigInteger>) info.getBaseInfo();
+      assertEquals(ni.getCurrentValue().intValue(), 0);
+      assertEquals(ni.getDefaultValue().intValue(), 0);
+      assertTrue(ni.getMinimum() == null && ni.getMaximum() == null);
+      assertEquals(info.intValue().intValue(), 0);
+      assertEquals(info.toString(), "OptionInfo{ rlimit | uint64_t | 0 | default 0 }");
+    }
     {
       OptionInfo info = d_solver.getOptionInfo("random-freq");
       assertEquals(info.getName(), "random-freq");
@@ -1533,6 +1563,19 @@ class SolverTest
       assertEquals(ni.getMinimum(), 0.0);
       assertEquals(ni.getMaximum(), 1.0);
       assertEquals(info.doubleValue(), 0.0);
+      assertEquals(info.toString(), "OptionInfo{ random-freq, random-frequency | double | 0 | default 0 | 0 <= x <= 1 }");
+    }
+    {
+      OptionInfo info = d_solver.getOptionInfo("force-logic");
+      assertEquals(info.getName(), "force-logic");
+      assertEquals(
+          Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
+      assertTrue(info.getBaseInfo().getClass() == OptionInfo.ValueInfo.class);
+      OptionInfo.ValueInfo<String> ni = (OptionInfo.ValueInfo<String>) info.getBaseInfo();
+      assertEquals(ni.getCurrentValue(), "");
+      assertEquals(ni.getDefaultValue(), "");
+      assertEquals(info.stringValue(), "");
+      assertEquals(info.toString(), "OptionInfo{ force-logic | string | \"\" | default \"\" }");
     }
     {
       // mode option
@@ -1548,6 +1591,7 @@ class SolverTest
       assertions.add(() -> assertEquals(2, modeInfo.getModes().length));
       assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("batch")));
       assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("none")));
+      assertEquals(info.toString(), "OptionInfo{ simplification, simplification-mode | mode | batch | default batch | modes: batch, none }");
     }
     assertAll(assertions);
   }