diff options
Diffstat (limited to 'src/main/command_executor.h')
-rw-r--r-- | src/main/command_executor.h | 52 |
1 files changed, 27 insertions, 25 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 31a604174..7e7202a5a 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -2,7 +2,7 @@ /*! \file command_executor.h ** \verbatim ** Top contributors (to current version): - ** Kshitij Bansal, Morgan Deters, Tim King + ** Kshitij Bansal, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -25,6 +25,11 @@ #include "util/statistics_registry.h" namespace CVC4 { + +namespace api { +class Solver; +} + namespace main { class CommandExecutor { @@ -32,21 +37,22 @@ private: std::string d_lastStatistics; protected: - ExprManager& d_exprMgr; - SmtEngine* d_smtEngine; - Options& d_options; - StatisticsRegistry d_stats; - Result d_result; - ExprStream* d_replayStream; + api::Solver* d_solver; + SmtEngine* d_smtEngine; + Options& d_options; + StatisticsRegistry d_stats; + Result d_result; + ExprStream* d_replayStream; public: - CommandExecutor(ExprManager &exprMgr, Options &options); - - virtual ~CommandExecutor() { - delete d_smtEngine; - if(d_replayStream != NULL){ - delete d_replayStream; - } + CommandExecutor(api::Solver* solver, Options& options); + + virtual ~CommandExecutor() + { + if (d_replayStream != NULL) + { + delete d_replayStream; + } } /** @@ -63,20 +69,16 @@ public: return d_stats; } - virtual void flushStatistics(std::ostream& out) const { - d_exprMgr.getStatistics().flushInformation(out); - d_smtEngine->getStatistics().flushInformation(out); - d_stats.flushInformation(out); - } + /** + * Flushes statistics to a file descriptor. + */ + virtual void flushStatistics(std::ostream& out) const; /** - * Flushes statistics to a file descriptor. Safe to use in a signal handler. + * Flushes statistics to a file descriptor. + * Safe to use in a signal handler. */ - void safeFlushStatistics(int fd) const { - d_exprMgr.safeFlushStatistics(fd); - d_smtEngine->safeFlushStatistics(fd); - d_stats.safeFlushInformation(fd); - } + void safeFlushStatistics(int fd) const; static void printStatsFilterZeros(std::ostream& out, const std::string& statsString); |