diff options
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor.cpp | 35 | ||||
-rw-r--r-- | src/main/command_executor.h | 52 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 34 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 7 | ||||
-rw-r--r-- | src/main/interactive_shell.h | 7 |
5 files changed, 80 insertions, 55 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) 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); diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index f97b037eb..c29212c4f 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -26,6 +26,7 @@ // This must come before PORTFOLIO_BUILD. #include "cvc4autoconfig.h" +#include "api/cvc4cpp.h" #include "base/configuration.h" #include "base/output.h" #include "expr/expr_iomanip.h" @@ -200,10 +201,10 @@ int runCvc4(int argc, char* argv[], Options& opts) { (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage()); // Create the expression manager using appropriate options - ExprManager* exprMgr; + std::unique_ptr<api::Solver> solver; # ifndef PORTFOLIO_BUILD - exprMgr = new ExprManager(opts); - pExecutor = new CommandExecutor(*exprMgr, opts); + solver.reset(new api::Solver(&opts)); + pExecutor = new CommandExecutor(solver.get(), opts); # else OptionsList threadOpts; parseThreadSpecificOptions(threadOpts, opts); @@ -230,19 +231,23 @@ int runCvc4(int argc, char* argv[], Options& opts) { } } // pick appropriate one - if(useParallelExecutor) { - exprMgr = new ExprManager(threadOpts[0]); - pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts); - } else { - exprMgr = new ExprManager(opts); - pExecutor = new CommandExecutor(*exprMgr, opts); + if (useParallelExecutor) + { + solver.reset(&threadOpts[0]); + pExecutor = new CommandExecutorPortfolio(solver.get(), opts, threadOpts); + } + else + { + solver.reset(&opts); + pExecutor = new CommandExecutor(solver.get(), opts); } # endif std::unique_ptr<Parser> replayParser; - if( opts.getReplayInputFilename() != "" ) { + if (opts.getReplayInputFilename() != "") + { std::string replayFilename = opts.getReplayInputFilename(); - ParserBuilder replayParserBuilder(exprMgr, replayFilename, opts); + ParserBuilder replayParserBuilder(solver.get(), replayFilename, opts); if( replayFilename == "-") { if( inputFromStdin ) { @@ -281,7 +286,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; } #endif /* PORTFOLIO_BUILD */ - InteractiveShell shell(*exprMgr); + InteractiveShell shell(solver.get()); if(opts.getInteractivePrompt()) { Message() << Configuration::getPackageName() << " " << Configuration::getVersionString(); @@ -334,7 +339,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { // delete cmd; } - ParserBuilder parserBuilder(exprMgr, filename, opts); + ParserBuilder parserBuilder(solver.get(), filename, opts); if( inputFromStdin ) { #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) @@ -491,7 +496,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; } - ParserBuilder parserBuilder(exprMgr, filename, opts); + ParserBuilder parserBuilder(solver.get(), filename, opts); if( inputFromStdin ) { #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) @@ -578,7 +583,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { // need to be around in that case for main() to print statistics. delete pTotalTime; delete pExecutor; - delete exprMgr; pTotalTime = NULL; pExecutor = NULL; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 2cec42fbf..aeccd3a64 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -37,6 +37,7 @@ # endif /* HAVE_EXT_STDIO_FILEBUF_H */ #endif /* HAVE_LIBREADLINE */ +#include "api/cvc4cpp.h" #include "base/output.h" #include "options/language.h" #include "options/options.h" @@ -87,13 +88,13 @@ static set<string> s_declarations; #endif /* HAVE_LIBREADLINE */ -InteractiveShell::InteractiveShell(ExprManager& exprManager) - : d_options(exprManager.getOptions()), +InteractiveShell::InteractiveShell(api::Solver* solver) + : d_options(solver->getExprManager()->getOptions()), d_in(*d_options.getIn()), d_out(*d_options.getOutConst()), d_quit(false) { - ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, d_options); + ParserBuilder parserBuilder(solver, INPUT_FILENAME, d_options); /* Create parser with bogus input. */ d_parser = parserBuilder.withStringInput("").build(); if(d_options.wasSetByUserForceLogicString()) { diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h index 203dfb766..ac52a78c4 100644 --- a/src/main/interactive_shell.h +++ b/src/main/interactive_shell.h @@ -25,9 +25,12 @@ namespace CVC4 { class Command; -class ExprManager; class Options; +namespace api { +class Solver; +} + namespace parser { class Parser; }/* CVC4::parser namespace */ @@ -47,7 +50,7 @@ class CVC4_PUBLIC InteractiveShell static const unsigned s_historyLimit = 500; public: - InteractiveShell(ExprManager& exprManager); + InteractiveShell(api::Solver* solver); /** * Close out the interactive session. |