From: Andrew Reynolds Date: Tue, 4 Jan 2022 18:07:42 +0000 (-0600) Subject: Remove unused shutdown infrastructure (#7872) X-Git-Tag: cvc5-1.0.0~606 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aa805580f35f4906a473d2450bc9f3f5aa9606c3;p=cvc5.git Remove unused shutdown infrastructure (#7872) --- diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index da6a50b9a..53062ad92 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -72,15 +72,6 @@ class PropEngine : protected EnvObj */ void finishInit(); - /** - * This is called by SolverEngine, at shutdown time, just before - * destruction. It is important because there are destruction - * ordering issues between some parts of the system (notably between - * PropEngine and Theory). For now, there's nothing to do here in - * the PropEngine. - */ - void shutdown() {} - /** * Preprocess the given node. Return the REWRITE trust node corresponding to * rewriting node. New lemmas and skolems are added to ppLemmas and diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 25c6f5f9f..c1608a80b 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -111,18 +111,6 @@ void SmtSolver::interrupt() } } -void SmtSolver::shutdown() -{ - if (d_propEngine != nullptr) - { - d_propEngine->shutdown(); - } - if (d_theoryEngine != nullptr) - { - d_theoryEngine->shutdown(); - } -} - Result SmtSolver::checkSatisfiability(Assertions& as, const std::vector& assumptions, bool isEntailmentCheck) diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h index 850c5b9b4..4ee4b0139 100644 --- a/src/smt/smt_solver.h +++ b/src/smt/smt_solver.h @@ -81,13 +81,6 @@ class SmtSolver * isn't currently in a query. */ void interrupt(); - /** - * This is called by the destructor of SolverEngine, just before destroying - * the PropEngine, TheoryEngine, and DecisionEngine (in that order). It is - * important because there are destruction ordering issues between PropEngine - * and Theory. - */ - void shutdown(); /** * Check satisfiability (used to check satisfiability and entailment) * in SolverEngine. This is done via adding assumptions (when necessary) to diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index e7f2e2069..9f4e05409 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -242,9 +242,6 @@ void SolverEngine::finishInit() void SolverEngine::shutdown() { d_state->shutdown(); - - d_smtSolver->shutdown(); - d_env->shutdown(); } diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 80e351466..8f4819405 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -91,8 +91,6 @@ class TheoryArith : public Theory { bool collectModelValues(TheoryModel* m, const std::set& termSet) override; - void shutdown() override {} - void presolve() override; void notifyRestart() override; PPAssertStatus ppAssert(TrustNode tin, diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 2ce2344b9..7c7058049 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -261,7 +261,6 @@ class TheoryArrays : public Theory { void presolve() override; - void shutdown() override {} ///////////////////////////////////////////////////////////////////////////// // MAIN SOLVER diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 2c2da66a8..2d746e664 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -68,7 +68,6 @@ class TheoryArraysRewriter : public TheoryRewriter TrustNode expandDefinition(Node node) override; static inline void init() {} - static inline void shutdown() {} private: /** diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 1d721a0ae..eab31d6d5 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -72,7 +72,6 @@ class TheoryQuantifiers : public Theory { /** Collect model values in m based on the relevant terms given by termSet */ bool collectModelValues(TheoryModel* m, const std::set& termSet) override; - void shutdown() override {} std::string identify() const override { return std::string("TheoryQuantifiers"); diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index b4439c104..91ace5bd1 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -144,7 +144,6 @@ class TheorySep : public Theory { public: void presolve() override; - void shutdown() override {} ///////////////////////////////////////////////////////////////////////////// // MAIN SOLVER diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index fa9262e53..612fc7b54 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -87,8 +87,6 @@ class TheoryStrings : public Theory { TrustNode explain(TNode literal) override; /** presolve */ void presolve() override; - /** shutdown */ - void shutdown() override {} /** preregister term */ void preRegisterTerm(TNode n) override; //--------------------------------- standard check diff --git a/src/theory/theory.h b/src/theory/theory.h index 56b27f6f0..5ef6b337d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -140,17 +140,6 @@ class Theory : protected EnvObj Valuation valuation, std::string instance = ""); // taking : No default. - /** - * This is called at shutdown time by the TheoryEngine, just before - * destruction. It is important because there are destruction - * ordering issues between PropEngine and Theory (based on what - * hard-links to Nodes are outstanding). As the fact queue might be - * nonempty, we ensure here that it's clear. If you overload this, - * you must make an explicit call here to this->Theory::shutdown() - * too. - */ - virtual void shutdown() {} - /** * The output channel for the Theory. */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ae71ac484..c8057606e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -221,7 +221,6 @@ TheoryEngine::TheoryEngine(Env& env) d_relManager(nullptr), d_inConflict(context(), false), d_inSatMode(false), - d_hasShutDown(false), d_incomplete(context(), false), d_incompleteTheory(context(), THEORY_BUILTIN), d_incompleteId(context(), IncompleteId::UNKNOWN), @@ -255,7 +254,6 @@ TheoryEngine::TheoryEngine(Env& env) } TheoryEngine::~TheoryEngine() { - Assert(d_hasShutDown); for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { if(d_theoryTable[theoryId] != NULL) { @@ -717,20 +715,6 @@ bool TheoryEngine::isRelevant(Node lit) const return true; } -void TheoryEngine::shutdown() { - // Set this first; if a Theory shutdown() throws an exception, - // at least the destruction of the TheoryEngine won't confound - // matters. - d_hasShutDown = true; - - // Shutdown all the theories - for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) { - if(d_theoryTable[theoryId]) { - theoryOf(theoryId)->shutdown(); - } - } -} - theory::Theory::PPAssertStatus TheoryEngine::solve( TrustNode tliteral, TrustSubstitutionMap& substitutionOut) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index f1e178055..6b1da1078 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -204,12 +204,6 @@ class TheoryEngine : protected EnvObj * or during LAST_CALL effort. */ bool isRelevant(Node lit) const; - /** - * This is called at shutdown time by the SolverEngine, just before - * destruction. It is important because there are destruction - * ordering issues between PropEngine and Theory. - */ - void shutdown(); /** * Solve the given literal with a theory that owns it. The proof of tliteral @@ -568,12 +562,6 @@ class TheoryEngine : protected EnvObj */ bool d_inSatMode; - /** - * Debugging flag to ensure that shutdown() is called before the - * destructor. - */ - bool d_hasShutDown; - /** * True if a theory has notified us of incompleteness (at this * context level or below).