From 3db254027b7e73d009dc7e587b4582b3372bb5ad Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 4 May 2022 10:21:41 -0700 Subject: [PATCH] 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. --- src/api/cpp/cvc5.h | 12 ++++++------ test/unit/api/cpp/solver_black.cpp | 7 +++++++ test/unit/api/cpp/solver_white.cpp | 7 ------- test/unit/api/java/UncoveredTest.cpp | 3 +++ test/unit/api/python/test_uncovered.cpp | 3 +++ 5 files changed, 19 insertions(+), 13 deletions(-) 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 ` 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 -- 2.30.2