From: Gereon Kremer Date: Fri, 29 Apr 2022 00:47:10 +0000 (-0700) Subject: Add some missing API tests (#8669) X-Git-Tag: cvc5-1.0.1~206 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=13d891a718e291ec8ea908c7be2367b7d5c8391a;p=cvc5.git Add some missing API tests (#8669) This PR adds a couple of simple API tests for parts of the API that are not covered yet. --- diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp index 8b6157016..b9c059602 100644 --- a/test/unit/api/cpp/op_black.cpp +++ b/test/unit/api/cpp/op_black.cpp @@ -23,6 +23,12 @@ class TestApiBlackOp : public TestApi { }; +TEST_F(TestApiBlackOp, hash) +{ + std::hash h; + ASSERT_NO_THROW(h(d_solver.mkOp(BITVECTOR_EXTRACT, {31, 1}))); +} + TEST_F(TestApiBlackOp, getKind) { Op x; @@ -34,8 +40,9 @@ TEST_F(TestApiBlackOp, isNull) { Op x; ASSERT_TRUE(x.isNull()); - x = d_solver.mkOp(BITVECTOR_EXTRACT, {31, 1}); - ASSERT_FALSE(x.isNull()); + Op y = d_solver.mkOp(BITVECTOR_EXTRACT, {31, 1}); + ASSERT_FALSE(y.isNull()); + ASSERT_NE(x, y); } TEST_F(TestApiBlackOp, opFromKind) @@ -166,6 +173,11 @@ TEST_F(TestApiBlackOp, opScopingToString) std::string op_repr = bitvector_repeat_ot.toString(); Solver solver2; ASSERT_EQ(bitvector_repeat_ot.toString(), op_repr); + { + std::stringstream ss; + ss << bitvector_repeat_ot; + ASSERT_EQ(ss.str(), op_repr); + } } } // namespace test } // namespace cvc5::internal diff --git a/test/unit/api/cpp/result_black.cpp b/test/unit/api/cpp/result_black.cpp index d062a17b2..062d93eb4 100644 --- a/test/unit/api/cpp/result_black.cpp +++ b/test/unit/api/cpp/result_black.cpp @@ -45,9 +45,16 @@ TEST_F(TestApiBlackResult, eq) cvc5::Result res; cvc5::Result res2 = d_solver.checkSat(); cvc5::Result res3 = d_solver.checkSat(); + ASSERT_NE(res, res2); res = res2; ASSERT_EQ(res, res2); ASSERT_EQ(res3, res2); + { + std::stringstream ss; + ss << res; + ASSERT_EQ(res.toString(), "sat"); + ASSERT_EQ(res.toString(), ss.str()); + } } TEST_F(TestApiBlackResult, isSat) @@ -81,6 +88,13 @@ TEST_F(TestApiBlackResult, isUnknown) cvc5::Result res = d_solver.checkSat(); ASSERT_FALSE(res.isSat()); ASSERT_TRUE(res.isUnknown()); + cvc5::UnknownExplanation ue = res.getUnknownExplanation(); + ASSERT_EQ(ue, cvc5::UnknownExplanation::UNKNOWN_REASON); + { + std::stringstream ss; + ss << ue; + ASSERT_EQ(ss.str(), "UNKNOWN_REASON"); + } } } // namespace test diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 9b560535c..e65f5fa43 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -1543,13 +1543,13 @@ TEST_F(TestApiBlackSolver, getOptionNames) TEST_F(TestApiBlackSolver, getOptionInfo) { { - EXPECT_THROW(d_solver.getOptionInfo("asdf-invalid"), CVC5ApiException); + ASSERT_THROW(d_solver.getOptionInfo("asdf-invalid"), CVC5ApiException); } { cvc5::OptionInfo info = d_solver.getOptionInfo("verbose"); - EXPECT_EQ("verbose", info.name); - EXPECT_EQ(std::vector{}, info.aliases); - EXPECT_TRUE(std::holds_alternative(info.valueInfo)); + ASSERT_EQ("verbose", info.name); + ASSERT_EQ(std::vector{}, info.aliases); + ASSERT_TRUE(std::holds_alternative(info.valueInfo)); std::stringstream ss; ss << info; ASSERT_EQ(ss.str(), "OptionInfo{ verbose | void }"); @@ -1557,13 +1557,13 @@ TEST_F(TestApiBlackSolver, getOptionInfo) { // bool type with default cvc5::OptionInfo info = d_solver.getOptionInfo("print-success"); - EXPECT_EQ("print-success", info.name); - EXPECT_EQ(std::vector{}, info.aliases); - EXPECT_TRUE( + ASSERT_EQ("print-success", info.name); + ASSERT_EQ(std::vector{}, info.aliases); + ASSERT_TRUE( std::holds_alternative>(info.valueInfo)); auto valInfo = std::get>(info.valueInfo); - EXPECT_EQ(false, valInfo.defaultValue); - EXPECT_EQ(false, valInfo.currentValue); + ASSERT_EQ(false, valInfo.defaultValue); + ASSERT_EQ(false, valInfo.currentValue); ASSERT_EQ(info.boolValue(), false); std::stringstream ss; ss << info; @@ -1573,14 +1573,14 @@ TEST_F(TestApiBlackSolver, getOptionInfo) { // int64 type with default cvc5::OptionInfo info = d_solver.getOptionInfo("verbosity"); - EXPECT_EQ("verbosity", info.name); - EXPECT_EQ(std::vector{}, info.aliases); - EXPECT_TRUE(std::holds_alternative>( + ASSERT_EQ("verbosity", info.name); + ASSERT_EQ(std::vector{}, info.aliases); + ASSERT_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(0, numInfo.defaultValue); + ASSERT_EQ(0, numInfo.currentValue); + ASSERT_FALSE(numInfo.minimum || numInfo.maximum); ASSERT_EQ(info.intValue(), 0); std::stringstream ss; ss << info; @@ -1589,14 +1589,14 @@ TEST_F(TestApiBlackSolver, getOptionInfo) { // uint64 type with default cvc5::OptionInfo info = d_solver.getOptionInfo("rlimit"); - EXPECT_EQ("rlimit", info.name); - EXPECT_EQ(std::vector{}, info.aliases); - EXPECT_TRUE(std::holds_alternative>( + ASSERT_EQ("rlimit", info.name); + ASSERT_EQ(std::vector{}, info.aliases); + ASSERT_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(0, numInfo.defaultValue); + ASSERT_EQ(0, numInfo.currentValue); + ASSERT_FALSE(numInfo.minimum || numInfo.maximum); ASSERT_EQ(info.uintValue(), 0); std::stringstream ss; ss << info; @@ -1624,13 +1624,13 @@ TEST_F(TestApiBlackSolver, getOptionInfo) { // string type with default cvc5::OptionInfo info = d_solver.getOptionInfo("force-logic"); - EXPECT_EQ("force-logic", info.name); - EXPECT_EQ(std::vector{}, info.aliases); - EXPECT_TRUE(std::holds_alternative>( + ASSERT_EQ("force-logic", info.name); + ASSERT_EQ(std::vector{}, info.aliases); + ASSERT_TRUE(std::holds_alternative>( info.valueInfo)); auto valInfo = std::get>(info.valueInfo); - EXPECT_EQ("", valInfo.defaultValue); - EXPECT_EQ("", valInfo.currentValue); + ASSERT_EQ("", valInfo.defaultValue); + ASSERT_EQ("", valInfo.currentValue); ASSERT_EQ(info.stringValue(), ""); std::stringstream ss; ss << info; @@ -1640,16 +1640,16 @@ TEST_F(TestApiBlackSolver, getOptionInfo) { // mode option cvc5::OptionInfo info = d_solver.getOptionInfo("simplification"); - EXPECT_EQ("simplification", info.name); - EXPECT_EQ(std::vector{"simplification-mode"}, info.aliases); - EXPECT_TRUE(std::holds_alternative(info.valueInfo)); + ASSERT_EQ("simplification", info.name); + ASSERT_EQ(std::vector{"simplification-mode"}, info.aliases); + ASSERT_TRUE(std::holds_alternative(info.valueInfo)); auto modeInfo = std::get(info.valueInfo); - EXPECT_EQ("batch", modeInfo.defaultValue); - EXPECT_EQ("batch", modeInfo.currentValue); - EXPECT_EQ(2, modeInfo.modes.size()); - EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "batch") + ASSERT_EQ("batch", modeInfo.defaultValue); + ASSERT_EQ("batch", modeInfo.currentValue); + ASSERT_EQ(2, modeInfo.modes.size()); + ASSERT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "batch") != modeInfo.modes.end()); - EXPECT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "none") + ASSERT_TRUE(std::find(modeInfo.modes.begin(), modeInfo.modes.end(), "none") != modeInfo.modes.end()); std::stringstream ss; ss << info; @@ -1662,13 +1662,14 @@ TEST_F(TestApiBlackSolver, getOptionInfo) 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()); + ASSERT_EQ(dopts.err().rdbuf(), std::cerr.rdbuf()); + ASSERT_EQ(dopts.in().rdbuf(), std::cin.rdbuf()); + ASSERT_EQ(dopts.out().rdbuf(), std::cout.rdbuf()); } TEST_F(TestApiBlackSolver, getStatistics) { + ASSERT_NO_THROW(cvc5::Stat()); // do some array reasoning to make sure we have a double statistics { Sort s1 = d_solver.getIntegerSort(); @@ -1685,21 +1686,21 @@ TEST_F(TestApiBlackSolver, getStatistics) } { auto s = stats.get("global::totalTime"); - EXPECT_FALSE(s.isInternal()); - EXPECT_FALSE(s.isDefault()); - EXPECT_TRUE(s.isString()); + ASSERT_FALSE(s.isInternal()); + ASSERT_FALSE(s.isDefault()); + ASSERT_TRUE(s.isString()); std::string time = s.getString(); - EXPECT_TRUE(time.rfind("ms") == time.size() - 2); // ends with "ms" - EXPECT_FALSE(s.isDouble()); + ASSERT_TRUE(time.rfind("ms") == time.size() - 2); // ends with "ms" + ASSERT_FALSE(s.isDouble()); s = stats.get("resource::resourceUnitsUsed"); - EXPECT_TRUE(s.isInternal()); - EXPECT_FALSE(s.isDefault()); - EXPECT_TRUE(s.isInt()); - EXPECT_TRUE(s.getInt() >= 0); + ASSERT_TRUE(s.isInternal()); + ASSERT_FALSE(s.isDefault()); + ASSERT_TRUE(s.isInt()); + ASSERT_TRUE(s.getInt() >= 0); } for (const auto& s: stats) { - EXPECT_FALSE(s.first.empty()); + ASSERT_FALSE(s.first.empty()); } for (auto it = stats.begin(true, true); it != stats.end(); ++it) { @@ -1707,33 +1708,33 @@ TEST_F(TestApiBlackSolver, getStatistics) auto tmp1 = it, tmp2 = it; ++tmp1; tmp2++; - EXPECT_EQ(tmp1, tmp2); + ASSERT_EQ(tmp1, tmp2); --tmp1; tmp2--; - EXPECT_EQ(tmp1, tmp2); - EXPECT_EQ(tmp1, it); - EXPECT_EQ(it, tmp2); + ASSERT_EQ(tmp1, tmp2); + ASSERT_EQ(tmp1, it); + ASSERT_EQ(it, tmp2); } const auto& s = *it; // check some basic utility methods - EXPECT_TRUE(!(it == stats.end())); - EXPECT_EQ(s.first, it->first); + ASSERT_TRUE(!(it == stats.end())); + ASSERT_EQ(s.first, it->first); if (s.first == "cvc5::CONSTANT") { - EXPECT_FALSE(s.second.isInternal()); - EXPECT_FALSE(s.second.isDefault()); - EXPECT_TRUE(s.second.isHistogram()); + ASSERT_FALSE(s.second.isInternal()); + ASSERT_FALSE(s.second.isDefault()); + ASSERT_TRUE(s.second.isHistogram()); auto hist = s.second.getHistogram(); - EXPECT_FALSE(hist.empty()); + ASSERT_FALSE(hist.empty()); std::stringstream ss; ss << s.second; - EXPECT_EQ(ss.str(), "{ integer type: 1 }"); + ASSERT_EQ(ss.str(), "{ integer type: 1 }"); } else if (s.first == "theory::arrays::avgIndexListLength") { - EXPECT_TRUE(s.second.isInternal()); - EXPECT_TRUE(s.second.isDouble()); - EXPECT_TRUE(std::isnan(s.second.getDouble())); + ASSERT_TRUE(s.second.isInternal()); + ASSERT_TRUE(s.second.isDouble()); + ASSERT_TRUE(std::isnan(s.second.getDouble())); } } } diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index 38b781def..7070c6acc 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -49,6 +49,12 @@ class TestApiBlackSort : public TestApi } }; +TEST_F(TestApiBlackSort, hash) +{ + std::hash h; + ASSERT_NO_THROW(h(d_solver.getIntegerSort())); +} + TEST_F(TestApiBlackSort, operators_comparison) { ASSERT_NO_THROW(d_solver.getIntegerSort() == Sort()); diff --git a/test/unit/api/cpp/synth_result_black.cpp b/test/unit/api/cpp/synth_result_black.cpp index 8ba5b0215..025e62772 100644 --- a/test/unit/api/cpp/synth_result_black.cpp +++ b/test/unit/api/cpp/synth_result_black.cpp @@ -43,6 +43,7 @@ TEST_F(TestApiBlackSynthResult, hasSolution) ASSERT_TRUE(res.hasSolution()); ASSERT_FALSE(res.hasNoSolution()); ASSERT_FALSE(res.isUnknown()); + ASSERT_EQ(res.toString(), "(SOLUTION)"); } TEST_F(TestApiBlackSynthResult, hasNoSolution) diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java index 6ee172862..7113e9db6 100644 --- a/test/unit/api/java/OpTest.java +++ b/test/unit/api/java/OpTest.java @@ -55,8 +55,9 @@ class OpTest { Op x = d_solver.getNullOp(); assertTrue(x.isNull()); - x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); - assertFalse(x.isNull()); + Op y = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); + assertFalse(y.isNull()); + assertTrue(x != y); } @Test diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java index ab4569a74..78f0e1289 100644 --- a/test/unit/api/java/ResultTest.java +++ b/test/unit/api/java/ResultTest.java @@ -59,12 +59,14 @@ class ResultTest Sort u_sort = d_solver.mkUninterpretedSort(); Term x = d_solver.mkConst(u_sort, "x"); d_solver.assertFormula(x.eqTerm(x)); - Result res; + Result res = null; Result res2 = d_solver.checkSat(); Result res3 = d_solver.checkSat(); + assertTrue(res != res2); res = res2; assertEquals(res, res2); assertEquals(res3, res2); + assertEquals(res.toString(), "sat"); } @Test @@ -101,5 +103,8 @@ class ResultTest Result res = d_solver.checkSat(); assertFalse(res.isSat()); assertTrue(res.isUnknown()); + UnknownExplanation ue = res.getUnknownExplanation(); + assertEquals(ue, UnknownExplanation.UNKNOWN_REASON); + assertEquals(ue.toString(), "UNKNOWN_REASON"); } } diff --git a/test/unit/api/java/SynthResultTest.java b/test/unit/api/java/SynthResultTest.java index 06330cc3f..24a33cbdb 100644 --- a/test/unit/api/java/SynthResultTest.java +++ b/test/unit/api/java/SynthResultTest.java @@ -60,6 +60,7 @@ class SynthResultTest assertTrue(res.hasSolution()); assertFalse(res.hasNoSolution()); assertFalse(res.isUnknown()); + assertEquals(res.toString(), "(SOLUTION)"); } @Test diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py index c8cde5bb1..00af24c4f 100644 --- a/test/unit/api/python/test_op.py +++ b/test/unit/api/python/test_op.py @@ -27,6 +27,9 @@ def solver(): return cvc5.Solver() +def test_hash(solver): + hash(solver.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1)) + def test_get_kind(solver): x = solver.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1) x.getKind() @@ -35,8 +38,9 @@ def test_get_kind(solver): def test_is_null(solver): x = Op(solver) assert x.isNull() - x = solver.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1) - assert not x.isNull() + y = solver.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1) + assert not y.isNull() + assert x != y def test_op_from_kind(solver): diff --git a/test/unit/api/python/test_result.py b/test/unit/api/python/test_result.py index 195e193a8..4f5a91fbd 100644 --- a/test/unit/api/python/test_result.py +++ b/test/unit/api/python/test_result.py @@ -45,9 +45,12 @@ def test_eq(solver): solver.assertFormula(x.eqTerm(x)) res2 = solver.checkSat() res3 = solver.checkSat() + res = Result() + assert res != res2 res = res2 assert res == res2 assert res3 == res2 + assert str(res) == "sat" def test_is_sat(solver): @@ -78,3 +81,6 @@ def test_is_sat_unknown(solver): res = solver.checkSat() assert not res.isSat() assert res.isUnknown() + ue = res.getUnknownExplanation() + assert ue == UnknownExplanation.UNKNOWN_REASON + assert str(ue) == "UnknownExplanation.UNKNOWN_REASON" diff --git a/test/unit/api/python/test_synth_result.py b/test/unit/api/python/test_synth_result.py index 892e641a1..d07e7e5fa 100644 --- a/test/unit/api/python/test_synth_result.py +++ b/test/unit/api/python/test_synth_result.py @@ -42,6 +42,7 @@ def test_has_solution(solver): assert res.hasSolution() assert not res.hasNoSolution() assert not res.isUnknown() + assert str(res) == '(SOLUTION)' def test_has_no_solution(solver): res_null = SynthResult(solver)