Add unit test for code not exposed by java API (#8678)

This PR adds a C++ unit test that explicitly calls into API functions that are not exposed by the java 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 java API.
It also corrects a few other minor issues.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 38cb3a04f3055ee1b233d4d8b0a1032ac66006e5..e6e0686614be0aa22a94d107a9a55e9e5a27fe54 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -4650,15 +4650,21 @@ Stat::Stat() {}
 Stat::~Stat() {}
 Stat::Stat(const Stat& s)
     : d_internal(s.d_internal),
-      d_default(s.d_default),
-      d_data(std::make_unique<StatData>(s.d_data->data))
+      d_default(s.d_default)
 {
+  if (s.d_data)
+  {
+    d_data = std::make_unique<StatData>(s.d_data->data);
+  }
 }
 Stat& Stat::operator=(const Stat& s)
 {
   d_internal = s.d_internal;
   d_default = s.d_default;
-  d_data = std::make_unique<StatData>(s.d_data->data);
+  if (s.d_data)
+  {
+    d_data = std::make_unique<StatData>(s.d_data->data);
+  }
   return *this;
 }
 

diff --git a/test/unit/api/java/CMakeLists.txt b/test/unit/api/java/CMakeLists.txt
index ec8c6194be1247d2a458100a5fe018416287b267..4a60ccbce519f874adf53389793d4c2131fe8668 100644 (file)
--- a/test/unit/api/java/CMakeLists.txt
+++ b/test/unit/api/java/CMakeLists.txt
@@ -68,3 +68,5 @@ cvc5_add_java_api_test(ResultTest)
 cvc5_add_java_api_test(SolverTest)
 cvc5_add_java_api_test(SortTest)
 cvc5_add_java_api_test(TermTest)
+
+cvc5_add_unit_test_white(UncoveredTest api/java)

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index de2a8db6bd8ca53724fecde4ffa84f1739c515b4..a13c3c3ec7eee5ba61ea7657f32c3cb4a56b586d 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1714,7 +1714,7 @@ class SolverTest
     for (Statistics.ConstIterator it = stats.iterator(true, true); it.hasNext();)
     {
       Map.Entry<String, Stat> elem = it.next();
-      if (elem.getKey() == "cvc5::CONSTANT")
+      if (elem.getKey().equals("cvc5::CONSTANT"))
       {
         assertFalse(elem.getValue().isInternal());
         assertFalse(elem.getValue().isDefault());
@@ -1723,10 +1723,11 @@ class SolverTest
         assertFalse(hist.isEmpty());
         assertEquals(elem.getValue().toString(), "{ integer type: 1 }");
       }
-      else if (elem.getKey() == "theory::arrays::avgIndexListLength")
+      else if (elem.getKey().equals("theory::arrays::avgIndexListLength"))
       {
         assertTrue(elem.getValue().isInternal());
-        assertTrue(elem.getValue().isDefault());
+        assertTrue(elem.getValue().isDouble());
+        assertTrue(Double.isNaN(elem.getValue().getDouble()));
       }
     }
   }

diff --git a/test/unit/api/java/UncoveredTest.cpp b/test/unit/api/java/UncoveredTest.cpp
new file mode 100644 (file)
index 0000000..1c2cb89
--- /dev/null
+++ b/test/unit/api/java/UncoveredTest.cpp
@@ -0,0 +1,54 @@
+/******************************************************************************
+ * 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 Java 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();
+}
+
+TEST_F(TestApiBlackUncovered, Statistics)
+{
+    Stat stat;
+    stat = Stat();
+    Statistics stats = d_solver.getStatistics();
+    auto it = stats.begin();
+    it++;
+    it--;
+    ++it;
+    --it;
+}
+
+}  // namespace test
+}  // namespace cvc5::internal