diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-03-12 12:04:48 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-12 14:04:48 -0500 |
commit | 83a18f98dddbd635db3823dd18b7bdf22b020869 (patch) | |
tree | f2efd227b8896ded2e97cb8bbc956443885aede6 /src/main | |
parent | f906530aa75e9c21e7877cac30cd3cb8245e3058 (diff) |
New C++ API: Remove support for (reset). (#4037)
Supporting SMT-LIB's (reset) command on the API level is dangerous and not required -- it's sufficient to just destroy the solver object and create a new one if necessary. It's dangerous because invalidated objects can be passed in after a reset, and we would need to find a clean way to guard against this. We want to guard against this in the future, but for now it is cleaner to make it explicit (by not having this functionality in the API but forcing the user to destroy and recreate the solver object) that these objects can't be reused.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/command_executor.cpp | 18 | ||||
-rw-r--r-- | src/main/command_executor.h | 45 | ||||
-rw-r--r-- | src/main/driver_unified.cpp | 15 |
3 files changed, 44 insertions, 34 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 5dbc50592..9db704621 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -24,7 +24,6 @@ #include <string> #include <vector> -#include "api/cvc4cpp.h" #include "main/main.h" #include "smt/command.h" @@ -49,14 +48,15 @@ void setNoLimitCPU() { void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString, const std::string& curStatsString); -CommandExecutor::CommandExecutor(api::Solver* solver, Options& options) - : d_solver(solver), +CommandExecutor::CommandExecutor(Options& options) + : d_solver(new api::Solver(&options)), d_smtEngine(d_solver->getSmtEngine()), d_options(options), d_stats("driver"), d_result(), - d_replayStream(NULL) -{} + d_replayStream(nullptr) +{ +} void CommandExecutor::flushStatistics(std::ostream& out) const { @@ -112,7 +112,13 @@ void CommandExecutor::reset() { flushStatistics(*d_options.getErr()); } - d_solver->reset(); + /* We have to keep options passed via CL on reset. These options are stored + * in CommandExecutor::d_options (populated and created in the driver), and + * CommandExecutor::d_options only contains *these* options since the + * NodeManager copies the options into a new options object before SmtEngine + * configures additional options based on the given CL options. + * We can thus safely reuse CommandExecutor::d_options here. */ + d_solver.reset(new api::Solver(&d_options)); } bool CommandExecutor::doCommandSingleton(Command* cmd) diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 3688f592f..3fc971f5b 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -18,6 +18,7 @@ #include <iosfwd> #include <string> +#include "api/cvc4cpp.h" #include "expr/expr_manager.h" #include "options/options.h" #include "smt/command.h" @@ -32,27 +33,28 @@ class Solver; namespace main { -class CommandExecutor { -private: +class CommandExecutor +{ + private: std::string d_lastStatistics; -protected: - api::Solver* d_solver; - SmtEngine* d_smtEngine; - Options& d_options; - StatisticsRegistry d_stats; - Result d_result; - ExprStream* d_replayStream; - -public: - CommandExecutor(api::Solver* solver, Options& options); - - virtual ~CommandExecutor() - { - if (d_replayStream != NULL) - { - delete d_replayStream; - } + protected: + std::unique_ptr<api::Solver> d_solver; + SmtEngine* d_smtEngine; + Options& d_options; + StatisticsRegistry d_stats; + Result d_result; + ExprStream* d_replayStream; + + public: + CommandExecutor(Options& options); + + virtual ~CommandExecutor() + { + if (d_replayStream != NULL) + { + delete d_replayStream; + } } /** @@ -62,6 +64,9 @@ public: */ bool doCommand(CVC4::Command* cmd); + /** Get a pointer to the solver object owned by this CommandExecutor. */ + api::Solver* getSolver() { return d_solver.get(); } + Result getResult() const { return d_result; } void reset(); @@ -96,7 +101,7 @@ protected: private: CommandExecutor(); -};/* class CommandExecutor */ +}; /* class CommandExecutor */ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out); diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index b999fe4b0..be2d0a0f8 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -181,16 +181,15 @@ int runCvc4(int argc, char* argv[], Options& opts) { // important even for muzzled builds (to get result output right) (*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage()); - // Create the expression manager using appropriate options - std::unique_ptr<api::Solver> solver; - solver.reset(new api::Solver(&opts)); - pExecutor = new CommandExecutor(solver.get(), opts); + // Create the command executor to execute the parsed commands + pExecutor = new CommandExecutor(opts); std::unique_ptr<Parser> replayParser; if (opts.getReplayInputFilename() != "") { std::string replayFilename = opts.getReplayInputFilename(); - ParserBuilder replayParserBuilder(solver.get(), replayFilename, opts); + ParserBuilder replayParserBuilder( + pExecutor->getSolver(), replayFilename, opts); if( replayFilename == "-") { if( inputFromStdin ) { @@ -229,7 +228,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { pExecutor->doCommand(cmd); delete cmd; } - InteractiveShell shell(solver.get()); + InteractiveShell shell(pExecutor->getSolver()); if(opts.getInteractivePrompt()) { Message() << Configuration::getPackageName() << " " << Configuration::getVersionString(); @@ -282,7 +281,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { // delete cmd; } - ParserBuilder parserBuilder(solver.get(), filename, opts); + ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts); if( inputFromStdin ) { #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) @@ -443,7 +442,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; } - ParserBuilder parserBuilder(solver.get(), filename, opts); + ParserBuilder parserBuilder(pExecutor->getSolver(), filename, opts); if( inputFromStdin ) { #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK) |