From: Aina Niemetz Date: Thu, 12 Mar 2020 19:04:48 +0000 (-0700) Subject: New C++ API: Remove support for (reset). (#4037) X-Git-Tag: cvc5-1.0.0~3501 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=83a18f98dddbd635db3823dd18b7bdf22b020869;p=cvc5.git 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. --- diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 037243ea4..f563e83f5 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -4105,11 +4105,6 @@ void Solver::push(uint32_t nscopes) const CVC4_API_SOLVER_TRY_CATCH_END; } -/** - * ( reset ) - */ -void Solver::reset(void) const { d_smtEngine->reset(); } - /** * ( reset-assertions ) */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 7ccb73bc3..3c99d2480 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -2761,12 +2761,6 @@ class CVC4_PUBLIC Solver */ void push(uint32_t nscopes = 1) const; - /** - * Reset the solver. - * SMT-LIB: ( reset ) - */ - void reset() const; - /** * Remove all assertions. * SMT-LIB: ( reset-assertions ) diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index d61fed0fc..188753122 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -935,9 +935,6 @@ cdef class Solver: def push(self, nscopes=1): self.csolver.push(nscopes) - def reset(self): - self.csolver.reset() - def resetAssertions(self): self.csolver.resetAssertions() 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 #include -#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 #include +#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 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 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 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) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0416d4f01..b282e6911 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -900,6 +900,7 @@ set(regress_0_tests regress0/smtlib/global-decls.smt2 regress0/smtlib/issue4028.smt2 regress0/smtlib/reason-unknown.smt2 + regress0/smtlib/reset.smt2 regress0/smtlib/reset-assertions1.smt2 regress0/smtlib/reset-assertions2.smt2 regress0/smtlib/reset-assertions-global.smt2 diff --git a/test/regress/regress0/smtlib/reset.smt2 b/test/regress/regress0/smtlib/reset.smt2 new file mode 100644 index 000000000..c46fb0a44 --- /dev/null +++ b/test/regress/regress0/smtlib/reset.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --produce-models +; EXPECT: true +; EXPECT: false +; EXPECT: true +(get-option :produce-models) +(set-option :produce-models false) +(get-option :produce-models) +(reset) +(get-option :produce-models)