From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Thu, 1 Apr 2021 11:35:20 +0000 (+0200)
Subject: Make ResetCommand go through APISolver (#6172)
X-Git-Tag: cvc5-1.0.0~1996
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b371364633912a681696eb7bda4a631a74b0539d;p=cvc5.git

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.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 66ddff9d4..1c1b6b28c 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4063,10 +4063,14 @@ size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
 Solver::Solver(Options* opts)
 {
   d_nodeMgr.reset(new NodeManager());
-  d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), opts));
+  d_originalOptions.reset(new Options());
+  if (opts != nullptr)
+  {
+    d_originalOptions->copyValues(*opts);
+  }
+  d_smtEngine.reset(new SmtEngine(d_nodeMgr.get(), d_originalOptions.get()));
   d_smtEngine->setSolver(this);
-  Options& o = d_smtEngine->getOptions();
-  d_rng.reset(new Random(o[options::seed]));
+  d_rng.reset(new Random(d_smtEngine->getOptions()[options::seed]));
 #if CVC4_STATISTICS_ON
   d_stats.reset(new Statistics());
   d_smtEngine->getStatisticsRegistry()->registerStat(&d_stats->d_consts);
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 8e5ddf28d..99c2d1182 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -58,6 +58,7 @@ class GetQuantifierEliminationCommand;
 class GetUnsatCoreCommand;
 class GetValueCommand;
 class NodeManager;
+class ResetCommand;
 class SetUserAttributeCommand;
 class SimplifyCommand;
 class SmtEngine;
@@ -2322,6 +2323,7 @@ class CVC4_EXPORT Solver
   friend class DatatypeSelector;
   friend class Grammar;
   friend class Op;
+  friend class CVC5::ResetCommand;
   friend class Sort;
   friend class Term;
 
@@ -3693,6 +3695,8 @@ class CVC4_EXPORT Solver
   /** Increment the vars stats (if 'is_var') or consts stats counter. */
   void increment_vars_consts_stats(const Sort& sort, bool is_var) const;
 
+  /** Keep a copy of the original option settings (for resets). */
+  std::unique_ptr<Options> d_originalOptions;
   /** The node manager of this solver. */
   std::unique_ptr<NodeManager> d_nodeMgr;
   /** The statistics collected on the Api level. */
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;