diff options
Diffstat (limited to 'src/main/command_executor.cpp')
-rw-r--r-- | src/main/command_executor.cpp | 35 |
1 files changed, 25 insertions, 10 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 0fd421b24..40c31de99 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -24,6 +24,7 @@ #include <string> #include <vector> +#include "api/cvc4cpp.h" #include "main/main.h" #include "smt/command.h" @@ -48,15 +49,29 @@ void setNoLimitCPU() { void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString); -CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) : - d_exprMgr(exprMgr), - d_smtEngine(new SmtEngine(&exprMgr)), - d_options(options), - d_stats("driver"), - d_result(), - d_replayStream(NULL) +CommandExecutor::CommandExecutor(api::Solver* solver, Options& options) + : d_solver(solver), + d_smtEngine(d_solver->getSmtEngine()), + d_options(options), + d_stats("driver"), + d_result(), + d_replayStream(NULL) {} +void CommandExecutor::flushStatistics(std::ostream& out) const +{ + d_solver->getExprManager()->getStatistics().flushInformation(out); + d_smtEngine->getStatistics().flushInformation(out); + d_stats.flushInformation(out); +} + +void CommandExecutor::safeFlushStatistics(int fd) const +{ + d_solver->getExprManager()->safeFlushStatistics(fd); + d_smtEngine->safeFlushStatistics(fd); + d_stats.safeFlushInformation(fd); +} + void CommandExecutor::setReplayStream(ExprStream* replayStream) { assert(d_replayStream == NULL); d_replayStream = replayStream; @@ -92,11 +107,11 @@ bool CommandExecutor::doCommand(Command* cmd) void CommandExecutor::reset() { - if(d_options.getStatistics()) { + if (d_options.getStatistics()) + { flushStatistics(*d_options.getErr()); } - delete d_smtEngine; - d_smtEngine = new SmtEngine(&d_exprMgr); + d_solver->reset(); } bool CommandExecutor::doCommandSingleton(Command* cmd) |