diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-07-30 18:21:36 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-31 01:21:36 +0000 |
| commit | fda46132b3f5c945a2b5e75bfa6bd5c84525fee6 (patch) | |
| tree | 3f3882072b96373e8d20749e248a0f3b648459cd /src/smt | |
| parent | e7fdbc4d74ccb37efdd118eca519cb23bd350cad (diff) | |
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.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 14 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 2 |
2 files changed, 12 insertions, 4 deletions
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<Node>& assumptions, checkUnsatCore(); } } - + if (d_env->getOptions().base.statisticsEveryQuery) + { + printStatisticsDiff(); + } return r; } catch (UnsafeInterruptException& e) @@ -948,6 +951,11 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& 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. |