From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Fri, 29 Apr 2022 01:09:03 +0000 (-0700)
Subject: Add unit test for code not exposed by python API (#8677)
X-Git-Tag: cvc5-1.0.1~205
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=08c26d6fe7e44e5016074606d0cd5bc0fb5c40af;p=cvc5.git

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 e0983f3af..38cb3a04f 100644
--- 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 add579bc5..9764c8641 100644
--- 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
index 000000000..c64887b0f
--- /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