Add unit test for code not exposed by python API (#8677)

This PR adds a C++ unit test that explicitly calls into API functions that are not exposed by the python API. This fixes the issue of false positives in our API coverage checks, as some parts of the C++ API are legitimately not used by the python API.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index e0983f3af7f7caec16f78c7b37c90148f2fba887..38cb3a04f3055ee1b233d4d8b0a1032ac66006e5 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1038,7 +1038,7 @@ bool SynthResult::isUnknown() const
 
 std::string SynthResult::toString(void) const { return d_result->toString(); }
 
-std::ostream& operator<<(std::ostream& out, const internal::SynthResult& sr)
+std::ostream& operator<<(std::ostream& out, const SynthResult& sr)
 {
   out << sr.toString();
   return out;
@@ -3640,6 +3640,7 @@ bool DatatypeSelector::isNull() const
 std::string DatatypeSelector::toString() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_CHECK_NOT_NULL;
   //////// all checks before this line
   std::stringstream ss;
   ss << *d_stor;

diff --git a/test/unit/api/python/CMakeLists.txt b/test/unit/api/python/CMakeLists.txt
index add579bc5559cc3154d537cc01db089370737c26..9764c864124963c9df2c72706d4dad65ca7f6586 100644 (file)
--- a/test/unit/api/python/CMakeLists.txt
+++ b/test/unit/api/python/CMakeLists.txt
@@ -39,3 +39,5 @@ cvc5_add_python_api_unit_test(test_to_python_obj test_to_python_obj.py)
 cvc5_add_python_api_unit_test(test_op test_op.py)
 cvc5_add_python_api_unit_test(test_result test_result.py)
 cvc5_add_python_api_unit_test(test_synth_result test_synth_result.py)
+
+cvc5_add_unit_test_black(test_uncovered api/python)

diff --git a/test/unit/api/python/test_uncovered.cpp b/test/unit/api/python/test_uncovered.cpp
new file mode 100644 (file)
index 0000000..c64887b
--- /dev/null
+++ b/test/unit/api/python/test_uncovered.cpp
@@ -0,0 +1,95 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Aina Niemetz, Mathias Preiner, Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Testing stuff that is not exposed by the python API to fix code coverage
+ */
+
+#include "test_api.h"
+
+namespace cvc5::internal {
+
+namespace test {
+
+class TestApiBlackUncovered : public TestApi
+{
+};
+
+TEST_F(TestApiBlackUncovered, streaming_operators)
+{
+    std::stringstream ss;
+    ss << cvc5::modes::LearnedLitType::PREPROCESS;
+    ss << cvc5::SynthResult();
+}
+
+TEST_F(TestApiBlackUncovered, Options)
+{
+    auto dopts = d_solver.getDriverOptions();
+    dopts.err();
+    dopts.in();
+    dopts.out();
+
+    std::stringstream ss;
+    {
+        auto info = d_solver.getOptionInfo("verbose");
+        ss << info;
+    }
+    {
+        auto info = d_solver.getOptionInfo("print-success");
+        ss << info;
+        info.boolValue();
+    }
+    {
+        auto info = d_solver.getOptionInfo("verbosity");
+        ss << info;
+        info.intValue();
+    }
+    {
+        auto info = d_solver.getOptionInfo("rlimit");
+        ss << info;
+        info.uintValue();
+    }
+    {
+        auto info = d_solver.getOptionInfo("random-freq");
+        ss << info;
+        info.doubleValue();
+    }
+    {
+        auto info = d_solver.getOptionInfo("force-logic");
+        ss << info;
+        info.stringValue();
+    }
+    {
+        auto info = d_solver.getOptionInfo("simplification");
+        ss << info;
+    }
+}
+
+TEST_F(TestApiBlackUncovered, Statistics)
+{
+    d_solver.assertFormula(d_solver.mkConst(d_solver.getBooleanSort(), "x"));
+    d_solver.checkSat();
+    Statistics stats = d_solver.getStatistics();
+    std::stringstream ss;
+    ss << stats;
+    auto it = stats.begin();
+    ASSERT_NE(it, stats.end());
+    it++;
+    it--;
+    ++it;
+    --it;
+    ASSERT_EQ(it, stats.begin());
+    ss << it->first;
+
+}
+
+}  // namespace test
+}  // namespace cvc5::internal