Remove unused shutdown infrastructure (#7872)

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index da6a50b9ac2075be2ddab0144cfb97348a858a76..53062ad92b10a9a4a9a2a83e54fa4958fb484275 100644 (file)
--- 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 25c6f5f9fb68385b5a93c45782cc021976560c69..c1608a80b2fe2429502865a72863be7e9939b59f 100644 (file)
--- 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<Node>& assumptions,
                                       bool isEntailmentCheck)

diff --git a/src/smt/smt_solver.h b/src/smt/smt_solver.h
index 850c5b9b4391f22b5002ac8e9532fae66f7074c3..4ee4b013984fb6f7ec56454f8b2de03188f74aaa 100644 (file)
--- 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 e7f2e2069a73b9f4ca701d5b5c13003746bc29cd..9f4e054093e85550c8d5365843a5ee634abc5450 100644 (file)
--- 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 80e351466981984bdab32a89a1d1d486d4544713..8f48194059c0a4ab5e379cd5d94f128d20016c6c 100644 (file)
--- 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<Node>& 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 2ce2344b93315f1f562d9601c1b4d87137e66fde..7c705804908d95782a8bd01c3e7035151c093de8 100644 (file)
--- 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 2c2da66a88aed12ac1f410e6eafc4d59a91633d2..2d746e6646aff7b689abd8f4789905e565d5660a 100644 (file)
--- 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 1d721a0aeb284274aa761196232cfd0d69aef532..eab31d6d5bbf61892fe88734c83e098fb4303f1f 100644 (file)
--- 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<Node>& 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 b4439c104e3a34aebe0027a9ce573bec5869e090..91ace5bd105a4d380746441f4054b7c26c91f338 100644 (file)
--- 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 fa9262e53f5ce2d7fbbed810261b2071e34feaf5..612fc7b54e3df5735a80fc580652977093443b70 100644 (file)
--- 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 56b27f6f02605605c8c626f71f7001b7f9b37166..5ef6b337ddd0b902fe3f7a7b1b8437e78b93e6cf 100644 (file)
--- 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 ae71ac4842715e1436edb1140671ac7a0918e144..c8057606e4e49bfedbaf5e261da55be286c3e5c8 100644 (file)
--- 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 f1e178055dd55e0ac256a743029f5f014769f613..6b1da10782b9f543eae6c25273b245daad56c1bc 100644 (file)
--- 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).