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/main | |
| 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/main')
| -rw-r--r-- | src/main/command_executor.cpp | 11 |
1 files changed, 2 insertions, 9 deletions
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 |