From fda46132b3f5c945a2b5e75bfa6bd5c84525fee6 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 30 Jul 2021 18:21:36 -0700 Subject: [PATCH] Perform statistics printing via the API (#6952) This PR changes how the command executor prints the statistics by moving stuff around a bit, eventually using only proper API methods of api::Solver. This PR also removes the smt_engine.h include from command_executor.cpp. --- src/api/cpp/cvc5.cpp | 21 ++++++++++++--------- src/api/cpp/cvc5.h | 5 +++++ src/main/command_executor.cpp | 11 ++--------- src/smt/smt_engine.cpp | 14 +++++++++++--- src/smt/smt_engine.h | 2 +- 5 files changed, 31 insertions(+), 22 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 4252cd45e..69aa720ea 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -4762,7 +4762,9 @@ struct Stat::StatData Stat::~Stat() {} Stat::Stat(const Stat& s) - : d_expert(s.d_expert), d_data(std::make_unique(s.d_data->data)) + : d_expert(s.d_expert), + d_default(s.d_default), + d_data(std::make_unique(s.d_data->data)) { } Stat& Stat::operator=(const Stat& s) @@ -5387,6 +5389,11 @@ void Solver::resetStatistics() } } +void Solver::printStatisticsSafe(int fd) const +{ + d_smtEngine->printStatisticsSafe(fd); +} + /* Helpers for mkTerm checks. */ /* .......................................................................... */ @@ -6640,8 +6647,7 @@ Result Solver::checkEntailed(const Term& term) const "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM(term); //////// all checks before this line - cvc5::Result r = d_smtEngine->checkEntailed(*term.d_node); - return Result(r); + return d_smtEngine->checkEntailed(*term.d_node); //////// CVC5_API_TRY_CATCH_END; } @@ -6684,8 +6690,7 @@ Result Solver::checkSat(void) const << "Cannot make multiple queries unless incremental solving is enabled " "(try --incremental)"; //////// all checks before this line - cvc5::Result r = d_smtEngine->checkSat(); - return Result(r); + return d_smtEngine->checkSat(); //////// CVC5_API_TRY_CATCH_END; } @@ -6700,8 +6705,7 @@ Result Solver::checkSatAssuming(const Term& assumption) const "(try --incremental)"; CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(assumption, getBooleanSort()); //////// all checks before this line - cvc5::Result r = d_smtEngine->checkSat(*assumption.d_node); - return Result(r); + return d_smtEngine->checkSat(*assumption.d_node); //////// CVC5_API_TRY_CATCH_END; } @@ -6721,8 +6725,7 @@ Result Solver::checkSatAssuming(const std::vector& assumptions) const CVC5_API_SOLVER_CHECK_TERM(term); } std::vector eassumptions = Term::termVectorToNodes(assumptions); - cvc5::Result r = d_smtEngine->checkSat(eassumptions); - return Result(r); + return d_smtEngine->checkSat(eassumptions); //////// CVC5_API_TRY_CATCH_END; } diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 672ccf8f8..e41df9593 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4161,6 +4161,11 @@ 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 mk-functions that call d_nodeMgr->mkConst(). */ diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 55b93a15c..ce7a46b4e 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -29,7 +29,6 @@ #include "options/base_options.h" #include "options/main_options.h" #include "smt/command.h" -#include "smt/smt_engine.h" namespace cvc5 { namespace main { @@ -68,7 +67,7 @@ void CommandExecutor::printStatistics(std::ostream& out) const { if (d_solver->getOptions().base.statistics) { - getSmtEngine()->printStatistics(out); + out << d_solver->getStatistics(); } } @@ -76,7 +75,7 @@ void CommandExecutor::printStatisticsSafe(int fd) const { if (d_solver->getOptions().base.statistics) { - getSmtEngine()->printStatisticsSafe(fd); + d_solver->printStatisticsSafe(fd); } } @@ -152,12 +151,6 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) d_result = res = q->getResult(); } - if ((cs != nullptr || q != nullptr) - && d_solver->getOptions().base.statisticsEveryQuery) - { - getSmtEngine()->printStatisticsDiff(*d_solver->getOptions().base.err); - } - bool isResultUnsat = res.isUnsat() || res.isEntailed(); // dump the model/proof/unsat core if option is set diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bbd65c24f..d3eb5c48a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -935,7 +935,10 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, checkUnsatCore(); } } - + if (d_env->getOptions().base.statisticsEveryQuery) + { + printStatisticsDiff(); + } return r; } catch (UnsafeInterruptException& e) @@ -948,6 +951,11 @@ Result SmtEngine::checkSatInternal(const std::vector& assumptions, Result::UnknownExplanation why = getResourceManager()->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT; + + if (d_env->getOptions().base.statisticsEveryQuery) + { + printStatisticsDiff(); + } return Result(Result::SAT_UNKNOWN, why, d_state->getFilename()); } } @@ -1925,9 +1933,9 @@ void SmtEngine::printStatisticsSafe(int fd) const d_env->getStatisticsRegistry().printSafe(fd); } -void SmtEngine::printStatisticsDiff(std::ostream& out) const +void SmtEngine::printStatisticsDiff() const { - d_env->getStatisticsRegistry().printDiff(out); + d_env->getStatisticsRegistry().printDiff(*d_env->getOptions().base.err); d_env->getStatisticsRegistry().storeSnapshot(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 02e5c6b06..0e4e03f3a 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -828,7 +828,7 @@ class CVC5_EXPORT SmtEngine * time. Internally prints the diff and then stores a snapshot for the next * call. */ - void printStatisticsDiff(std::ostream&) const; + void printStatisticsDiff() const; /** * Set user attribute. -- 2.30.2