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 037243ea4f30dc0150191a555ead8e2ca35872a9..f563e83f50254a1594ec82498b76164ac1446516 100644 (file)
--- 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 7ccb73bc372e73b29064b88b4bd02e43b8d7c069..3c99d248091ef8e4445c226a5d74e9f40f563818 100644 (file)
--- 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 d61fed0fcb7e1c74912586444b04ea5730e58861..1887531224212f70453ba47c17b33933daf485af 100644 (file)
--- 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 5dbc50592c7fafb6fcfc379d6787e238143d00c6..9db704621af9baa5e64040f571124a78e37fbae4 100644 (file)
--- 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 3688f592f182bfd60caf40e0f9403857092a9a15..3fc971f5b6fb23eded76e96cd994aca0f4cf1a82 100644 (file)
--- 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 b999fe4b08ccb6227f47903575a164f4c2f0dbd9..be2d0a0f80bfbd02b7ac9ce5eb60bebfef60d172 100644 (file)
--- 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 0416d4f01a8571902667d6d39e3cef422e53662a..b282e69110680ec14d81f346a37958a38e1a1760 100644 (file)
--- 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 (file)
index 0000000..c46fb0a
--- /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)