From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Wed, 4 May 2022 17:21:41 +0000 (-0700)
Subject: Make printStatisticsSafe public (#8721)
X-Git-Tag: cvc5-1.0.1~172
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3db254027b7e73d009dc7e587b4582b3372bb5ad;p=cvc5.git

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 6be6831d7..5043970d9 100644
--- 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 a25669474..577c8ad4c 100644
--- 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 93f229f17..35911b4e8 100644
--- 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 a041db700..076eb1b4e 100644
--- 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 fbeef181e..eaea0a5e2 100644
--- 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