From a796c4d8461f22aa523edd3031290e0ba03edd60 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 4 Aug 2021 16:46:49 -0700
Subject: [PATCH] Consolidate solver resets (#6986)

This PR consolidates the two different reset implementations into a single function.
---
 src/main/command_executor.cpp | 11 ++---------
 src/main/command_executor.h   |  5 -----
 src/smt/command.cpp           | 23 ++++++++++++++---------
 src/smt/command.h             |  6 ++++++
 4 files changed, 22 insertions(+), 23 deletions(-)

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 5431a8348..4e25e984d 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -52,7 +52,6 @@ void setNoLimitCPU() {
 CommandExecutor::CommandExecutor(const Options& options)
     : d_solver(new api::Solver(&options)),
       d_symman(new SymbolManager(d_solver.get())),
-      d_driverOptions(&options),
       d_result()
 {
 }
@@ -118,14 +117,8 @@ bool CommandExecutor::doCommand(Command* cmd)
 void CommandExecutor::reset()
 {
   printStatistics(*d_solver->getOptions().base.err);
-  /* We have to keep options passed via CL on reset. These options are stored
-   * in CommandExecutor::d_driverOptions (populated and created in the driver),
-   * and CommandExecutor::d_driverOptions only contains *these* options since
-   * the SmtEngine copies them into its own options object before configuring
-   * additional options based on the given CL options.
-   * We can thus safely reuse CommandExecutor::d_driverOptions here.
-   */
-  d_solver.reset(new api::Solver(d_driverOptions));
+
+  Command::resetSolver(d_solver.get());
 }
 
 bool CommandExecutor::doCommandSingleton(Command* cmd)
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 14866cd28..ff7b89928 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -52,11 +52,6 @@ class CommandExecutor
    * symbol manager.
    */
   std::unique_ptr<SymbolManager> d_symman;
-  /**
-   * A pointer to the original options from the driver. Contain options as
-   * parsed from the command line. Used when the solver is reset.
-   */
-  const Options* d_driverOptions;
 
   api::Result d_result;
 
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 342931912..bb501fa5c 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -239,6 +239,19 @@ void Command::printResult(std::ostream& out, uint32_t verbosity) const
   }
 }
 
+void Command::resetSolver(api::Solver* solver)
+{
+  std::unique_ptr<Options> opts = std::make_unique<Options>();
+  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.get());
+}
+
 Node Command::termToNode(const api::Term& term) { return term.getNode(); }
 
 std::vector<Node> Command::termVectorToNodes(
@@ -917,15 +930,7 @@ void ResetCommand::invoke(api::Solver* solver, SymbolManager* sm)
   try
   {
     sm->reset();
-    Options opts;
-    opts.copyValues(getOriginalOptionsFrom(solver));
-    // 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);
+    resetSolver(solver);
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
diff --git a/src/smt/command.h b/src/smt/command.h
index 590fcace3..5a67e6685 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -278,6 +278,12 @@ class CVC5_EXPORT Command
    */
   bool d_muted;
 
+  /**
+   * Reset the given solver in-place (keep the object at the same memory
+   * location).
+   */
+  static void resetSolver(api::Solver* solver);
+
  protected:
   // These methods rely on Command being a friend of classes in the API.
   // Subclasses of command should use these methods for conversions,
-- 
2.30.2