From: Gereon Kremer Date: Sat, 26 Mar 2022 00:42:26 +0000 (+0100) Subject: Add API unit tests for options (#8339) X-Git-Tag: cvc5-1.0.0~163 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=129a79d959448bc32619db85f86542d9e05605e4;p=cvc5.git 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 a4dc4e427..459ded731 100644 --- 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& vi) { - os << " | bool | " << vi.currentValue << " | default " - << vi.defaultValue; + os << std::boolalpha << " | bool | " << vi.currentValue + << " | default " << vi.defaultValue << std::noboolalpha; }, [&os](const OptionInfo::ValueInfo& vi) { - os << " | string | " << vi.currentValue << " | default " - << vi.defaultValue; + os << " | string | \"" << vi.currentValue + << "\" | default \"" << vi.defaultValue << "\""; }, [&printNum](const OptionInfo::NumberInfo& 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 6f6024420..1c47eeedb 100644 --- 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 extends BaseInfo + public class ValueInfo 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 da2a485e3..f889f7e12 100644 --- 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(pointer); - std::int64_t value = current->intValue(); - jobject ret = getBigIntegerObject(env, value); - return ret; + if (std::holds_alternative>( + current->valueInfo)) + { + std::uint64_t value = current->uintValue(); + jobject ret = getBigIntegerObject(env, value); + return ret; + } + if (std::holds_alternative>( + current->valueInfo)) + { + std::int64_t value = current->intValue(); + jobject ret = getBigIntegerObject(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 2c9b4ee48..b31aa9ad1 100644 --- 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{}, info.aliases); EXPECT_TRUE(std::holds_alternative(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{}, info.aliases); + EXPECT_TRUE( + std::holds_alternative>(info.valueInfo)); + auto valInfo = std::get>(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{}, info.aliases); + EXPECT_TRUE(std::holds_alternative>( + info.valueInfo)); + auto numInfo = std::get>(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{}, info.aliases); + EXPECT_TRUE(std::holds_alternative>( + info.valueInfo)); + auto valInfo = std::get>(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 1c01e32b5..5c759b9ea 100644 --- 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 valInfo = + (OptionInfo.ValueInfo) 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 ni = (OptionInfo.NumberInfo) 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 ni = (OptionInfo.ValueInfo) 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); }