Consolidate solver resets (#6986)

This PR consolidates the two different reset implementations into a single function.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 5431a83487f35fe488f3364d24cb66494d936273..4e25e984d77bb7379ea36a9844919677d5bae05e 100644 (file)
--- 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 14866cd28d935ab6bc0242735cc551cb6e984efc..ff7b89928bf6d13e0dee1f4be01c2d4c93dc0a39 100644 (file)
--- 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 342931912493721c08de1e7ec670719bbc7ebb72..bb501fa5ccaf62df89d6cd24286b8c1c26d4252e 100644 (file)
--- 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 590fcace3c38cf4a5ea2d2dad5ff570495156aa4..5a67e66854a18b8b46409842531c0b87a6dff775 100644 (file)
--- 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,