From 72fd917fcdba452d25828e970471a4588ccb2404 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Thu, 28 Apr 2022 20:21:12 -0700
Subject: [PATCH] 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.
---
 src/api/cpp/cvc5.cpp                 | 12 +++++--
 test/unit/api/java/CMakeLists.txt    |  2 ++
 test/unit/api/java/SolverTest.java   |  7 ++--
 test/unit/api/java/UncoveredTest.cpp | 54 ++++++++++++++++++++++++++++
 4 files changed, 69 insertions(+), 6 deletions(-)
 create mode 100644 test/unit/api/java/UncoveredTest.cpp

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 38cb3a04f..e6e068661 100644
--- 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 ec8c6194b..4a60ccbce 100644
--- 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 de2a8db6b..a13c3c3ec 100644
--- 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
index 000000000..1c2cb89ce
--- /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
-- 
2.30.2