Make ResetCommand go through APISolver (#6172)

This PR changes ResetCommand to not call SmtEngine::reset but instead reconstruct the api::Solver object. This makes SmtEngine::reset obsolete and removes it, and moves the original options from SmtEngine to api::Solver.
The motivation for this change is twofold:

The ResetCommand should not use SmtEngine directly, but only through the API (i.e. Solver).
As soon as the statistics data lives within the registry, we need to re-register statistics after resetting the SmtEngine. We can now do this within the api::Solver constructor.

3 files changed, 9 insertions, 34 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index f29b67d6d..6d9b1a5ec 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -865,7 +865,15 @@ void ResetCommand::invoke(api::Solver* solver, SymbolManager* sm)
   try
   {
     sm->reset();
-    solver->getSmtEngine()->reset();
+    Options opts;
+    opts.copyValues(*solver->d_originalOptions);
+    // This reconstructs a new solver object at the same memory location as the
+    // current one. Note that this command does not own the solver object!
+    // It may be safer to instead make the ResetCommand a special case in the
+    // CommandExecutor such that this reconstruction can be done within the
+    // CommandExecutor, who actually owns the solver.
+    solver->~Solver();
+    new (solver) api::Solver(&opts);
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a7e464008..db67af2f0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -98,7 +98,6 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
       d_abductSolver(nullptr),
       d_interpolSolver(nullptr),
       d_quantElimSolver(nullptr),
-      d_originalOptions(),
       d_isInternalSubsolver(false),
       d_stats(nullptr),
       d_outMgr(this),
@@ -412,7 +411,6 @@ void SmtEngine::notifyStartParsing(const std::string& filename)
   // Copy the original options. This is called prior to beginning parsing.
   // Hence reset should revert to these options, which note is after reading
   // the command line.
-  d_originalOptions.copyValues(getOptions());
 }
 
 const std::string& SmtEngine::getFilename() const
@@ -1783,24 +1781,6 @@ void SmtEngine::pop() {
   // SMT-LIBv2 spec seems to imply no, but it would make sense to..
 }
 
-void SmtEngine::reset()
-{
-  // save pointer to the current node manager
-  NodeManager* nm = getNodeManager();
-  Trace("smt") << "SMT reset()" << endl;
-  if (Dump.isOn("benchmark"))
-  {
-    getPrinter().toStreamCmdReset(getOutputManager().getDumpOut());
-  }
-  std::string filename = d_state->getFilename();
-  Options opts;
-  opts.copyValues(d_originalOptions);
-  this->~SmtEngine();
-  new (this) SmtEngine(nm, &opts);
-  // Restore data set after creation
-  notifyStartParsing(filename);
-}
-
 void SmtEngine::resetAssertions()
 {
   SmtScope smts(this);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 21250dc30..dd23ac949 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -724,13 +724,6 @@ class CVC4_EXPORT SmtEngine
    */
   void pop();
 
-  /**
-   * Completely reset the state of the solver, as though destroyed and
-   * recreated.  The result is as if newly constructed (so it still
-   * retains the same options structure and NodeManager).
-   */
-  void reset();
-
   /** Reset all assertions, global declarations, etc.  */
   void resetAssertions();
 
@@ -1128,12 +1121,6 @@ class CVC4_EXPORT SmtEngine
    */
   LogicInfo d_userLogic;
 
-  /**
-   * Keep a copy of the original option settings (for reset()). The current
-   * options live in the Env object.
-   */
-  Options d_originalOptions;
-
   /** Whether this is an internal subsolver. */
   bool d_isInternalSubsolver;