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 8b615701670a3f0a091a8f5e5e6d77e1ee4f6ed9..b9c059602289a57e38cb19ea0d41c630332f4153 100644 (file)
--- 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<cvc5::Op> 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 d062a17b2611b5a59eac6a7789a4ce66ea79ba06..062d93eb489b6310b9fd2e1a5d2c0aa1de2a03db 100644 (file)
--- 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 9b560535c29dfe180e18761aaf221ec95ff0ecdf..e65f5fa43cfab4641a575f494e35be2e047ac5d0 100644 (file)
--- 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<std::string>{}, info.aliases);
-    EXPECT_TRUE(std::holds_alternative<OptionInfo::VoidInfo>(info.valueInfo));
+    ASSERT_EQ("verbose", info.name);
+    ASSERT_EQ(std::vector<std::string>{}, info.aliases);
+    ASSERT_TRUE(std::holds_alternative<OptionInfo::VoidInfo>(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<std::string>{}, info.aliases);
-    EXPECT_TRUE(
+    ASSERT_EQ("print-success", info.name);
+    ASSERT_EQ(std::vector<std::string>{}, info.aliases);
+    ASSERT_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(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<std::string>{}, info.aliases);
-    EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(
+    ASSERT_EQ("verbosity", info.name);
+    ASSERT_EQ(std::vector<std::string>{}, info.aliases);
+    ASSERT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<int64_t>>(
         info.valueInfo));
     auto numInfo = std::get<OptionInfo::NumberInfo<int64_t>>(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<std::string>{}, info.aliases);
-    EXPECT_TRUE(std::holds_alternative<OptionInfo::NumberInfo<uint64_t>>(
+    ASSERT_EQ("rlimit", info.name);
+    ASSERT_EQ(std::vector<std::string>{}, info.aliases);
+    ASSERT_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(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<std::string>{}, info.aliases);
-    EXPECT_TRUE(std::holds_alternative<OptionInfo::ValueInfo<std::string>>(
+    ASSERT_EQ("force-logic", info.name);
+    ASSERT_EQ(std::vector<std::string>{}, info.aliases);
+    ASSERT_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("", 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<std::string>{"simplification-mode"}, info.aliases);
-    EXPECT_TRUE(std::holds_alternative<OptionInfo::ModeInfo>(info.valueInfo));
+    ASSERT_EQ("simplification", info.name);
+    ASSERT_EQ(std::vector<std::string>{"simplification-mode"}, info.aliases);
+    ASSERT_TRUE(std::holds_alternative<OptionInfo::ModeInfo>(info.valueInfo));
     auto modeInfo = std::get<OptionInfo::ModeInfo>(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 38b781defa751e493756f939c450479ad39423b7..7070c6acc49afca4b680c7d9d9f76084ffabd80b 100644 (file)
--- 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<cvc5::Sort> 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 8ba5b0215e5bba0e92b972f8ab9c92163fcd235a..025e62772ba9431f7ccadc3b18841b2210cceb09 100644 (file)
--- 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 6ee1728628c9578c4aec35100ed039d78c6f71d4..7113e9db6fe76edb49499073cb9e5040d5f9097a 100644 (file)
--- 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 ab4569a74ecf2b6f3a2ccbf44b37876320d7ab08..78f0e1289626e28cbf9392370492531f3b6cee39 100644 (file)
--- 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 06330cc3f0ae50401f9835e8dc86767cc51bc0ea..24a33cbdbb4337937b7ca5ec4b613cc46d52455f 100644 (file)
--- 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 c8cde5bb1d3ab199537640b851226fac9eb36daa..00af24c4f8d72c2eeb963db880f8cf370d63b329 100644 (file)
--- 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 195e193a8b102d4ce8db0d4435109fb9be06a53b..4f5a91fbd2566f5044f5ff6b8d6bb44828cf6422 100644 (file)
--- 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 892e641a1d26e4ca4aef2b08b5327bc67ed94bab..d07e7e5fa82e66a014de6b1299b454c87cc9adea 100644 (file)
--- 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)