Make printStatisticsSafe public (#8721)

Solver::printStatisticsSafe() is private right now. There is no real reason for that, and as we claim that the driver is only using the regular API we should just make it public.

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 6be6831d759bf7e3e957bd2ea330c65d573069f5..5043970d9cb3c523a14197c868caa994206831cf 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4945,6 +4945,12 @@ class CVC5_EXPORT Solver
    */
   Statistics getStatistics() const;
 
+  /**
+   * Print the statistics to the given file descriptor, suitable for usage in
+   * signal handlers.
+   */
+  void printStatisticsSafe(int fd) const;
+
   /**
    * Determione the output stream for the given tag is enabled. Tags can be
    * enabled with the `output` option (and `-o <tag>` on the command line).
@@ -4967,12 +4973,6 @@ class CVC5_EXPORT Solver
   /** Reset the API statistics */
   void resetStatistics();
 
-  /**
-   * Print the statistics to the given file descriptor, suitable for usage in
-   * signal handlers.
-   */
-  void printStatisticsSafe(int fd) const;
-
   /** Helper to check for API misuse in mkOp functions. */
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
   /** Helper for creating operators. */

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index a25669474d208177df9054dd7c1a4e66b458e5b3..577c8ad4c33d638dfca6eddbd4b6de6752e3c6ee 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -1759,6 +1759,13 @@ TEST_F(TestApiBlackSolver, getStatistics)
   }
 }
 
+TEST_F(TestApiBlackSolver, printStatisticsSafe)
+{
+  testing::internal::CaptureStdout();
+  d_solver.printStatisticsSafe(STDOUT_FILENO);
+  testing::internal::GetCapturedStdout();
+}
+
 TEST_F(TestApiBlackSolver, getUnsatAssumptions1)
 {
   d_solver.setOption("incremental", "false");

diff --git a/test/unit/api/cpp/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp
index 93f229f17ce4de8e5fd04dc49c83f9b3b2bd1fed..35911b4e8a93a919552cd7f04cb404958426f7a0 100644 (file)
--- a/test/unit/api/cpp/solver_white.cpp
+++ b/test/unit/api/cpp/solver_white.cpp
@@ -50,12 +50,5 @@ TEST_F(TestApiWhiteSolver, getOp)
   ASSERT_EQ(listhead.getOp(), Op(&d_solver, APPLY_SELECTOR));
 }
 
-TEST_F(TestApiWhiteSolver, printStatisticsSafe)
-{
-  testing::internal::CaptureStdout();
-  d_solver.printStatisticsSafe(STDOUT_FILENO);
-  testing::internal::GetCapturedStdout();
-}
-
 }  // namespace test
 }  // namespace cvc5::internal

diff --git a/test/unit/api/java/UncoveredTest.cpp b/test/unit/api/java/UncoveredTest.cpp
index a041db700da9112dad0bdd12232121d55e836514..076eb1b4e925b9643efa84997f1e08e03ecdccad 100644 (file)
--- a/test/unit/api/java/UncoveredTest.cpp
+++ b/test/unit/api/java/UncoveredTest.cpp
@@ -86,6 +86,9 @@ TEST_F(TestApiBlackUncovered, Statistics)
     it--;
     ++it;
     --it;
+    testing::internal::CaptureStdout();
+    d_solver.printStatisticsSafe(STDOUT_FILENO);
+    testing::internal::GetCapturedStdout();
 }
 
 }  // namespace test

diff --git a/test/unit/api/python/test_uncovered.cpp b/test/unit/api/python/test_uncovered.cpp
index fbeef181e1aeaa1604dba7eda04128827a79b130..eaea0a5e2ca2968a90aa7f528427ba3f7311fb7c 100644 (file)
--- a/test/unit/api/python/test_uncovered.cpp
+++ b/test/unit/api/python/test_uncovered.cpp
@@ -131,6 +131,9 @@ TEST_F(TestApiBlackUncovered, Statistics)
     ASSERT_EQ(it, stats.begin());
     ss << it->first;
 
+    testing::internal::CaptureStdout();
+    d_solver.printStatisticsSafe(STDOUT_FILENO);
+    testing::internal::GetCapturedStdout();
 }
 
 }  // namespace test