From b371364633912a681696eb7bda4a631a74b0539d Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 1 Apr 2021 13:35:20 +0200 Subject: [PATCH] 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. --- src/api/cvc4cpp.cpp | 10 +++++++--- src/api/cvc4cpp.h | 4 ++++ src/smt/command.cpp | 10 +++++++++- src/smt/smt_engine.cpp | 20 -------------------- src/smt/smt_engine.h | 13 ------------- 5 files changed, 20 insertions(+), 37 deletions(-) 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 d_originalOptions; /** The node manager of this solver. */ std::unique_ptr 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; -- 2.30.2