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.

8 files changed, 54 insertions, 48 deletions

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
@@ -4106,11 +4106,6 @@ void Solver::push(uint32_t nscopes) const
 }
 
 /**
- *  ( reset )
- */
-void Solver::reset(void) const { d_smtEngine->reset(); }
-
-/**
  *  ( reset-assertions )
  */
 void Solver::resetAssertions(void) const { d_smtEngine->resetAssertions(); }
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
@@ -2762,12 +2762,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 <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)
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)