Rename SmtScope to SolverEngineScope. (#7284)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 583ce8bc5d53e9e5caae53ff0cce6af45a2b3efc..61be39f97c2a451195476995d24cebc779764378 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -349,8 +349,8 @@ libcvc5_add_sources(
   smt/set_defaults.h
   smt/solver_engine.cpp
   smt/solver_engine.h
-  smt/smt_engine_scope.cpp
-  smt/smt_engine_scope.h
+  smt/solver_engine_scope.cpp
+  smt/solver_engine_scope.h
   smt/smt_engine_state.cpp
   smt/smt_engine_state.h
   smt/smt_engine_stats.cpp

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 16ecc2d6a2e0c40bb0e1196c014bd48e59c7ca2e..3da75beb2552003c50fc9d055d3c8141749c4969 100644 (file)
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -17,9 +17,9 @@
 
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_preprocess.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"

diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 758f119f538270c560a01d711be94ece9f40a93e..244e551f7f4f0aa6ce174127f5d7f604c8a4888f 100644 (file)
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -21,8 +21,8 @@
 #include "smt/dump.h"
 #include "smt/env.h"
 #include "smt/output_manager.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/solver_engine_scope.h"
 #include "util/statistics_stats.h"
 
 namespace cvc5 {
@@ -65,9 +65,7 @@ PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext,
 {
 }
 
-PreprocessingPass::~PreprocessingPass() {
-  Assert(smt::smtEngineInScope());
-}
+PreprocessingPass::~PreprocessingPass() { Assert(smt::solverEngineInScope()); }
 
 }  // namespace preprocessing
 }  // namespace cvc5

diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index f7e600fe8bb040468384a98b4019d8617cd564cd..e2e3e85fef169596267d93682821ca77acc32615 100644 (file)
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -19,7 +19,7 @@
 #include "expr/expr_iomanip.h"
 #include "options/base_options.h"
 #include "printer/printer.h"
-#include "smt/smt_engine_scope.h"
+#include "smt/solver_engine_scope.h"
 
 namespace cvc5 {
 

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index e04651fc3b8c8e6057095cff5bc2b9df28d9b474..1bac953fdd87f58d4f84c99702eb3594a36b5af6 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -28,8 +28,8 @@
 #include "prop/theory_proxy.h"
 #include "smt/dump.h"
 #include "smt/env.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/solver_engine_scope.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 

diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index f10d039b8376b5bd56a67b9278b3ec5dcedde386..de6368951acb40028218c761151014f56edbe134 100644 (file)
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -23,8 +23,8 @@
 #include "smt/dump.h"
 #include "smt/dump_manager.h"
 #include "smt/node_command.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 
 namespace cvc5 {
 namespace smt {
@@ -33,8 +33,8 @@ ResourceOutListener::ResourceOutListener(SolverEngine& slv) : d_slv(slv) {}
 
 void ResourceOutListener::notify()
 {
-  SmtScope scope(&d_slv);
-  Assert(smt::smtEngineInScope());
+  SolverEngineScope scope(&d_slv);
+  Assert(smt::solverEngineInScope());
   d_slv.interrupt();
 }
 

diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
deleted file mode 100644 (file)
index 07a0c1e..0000000
--- a/src/smt/smt_engine_scope.cpp
+++ /dev/null
@@ -1,67 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andres Noetzli, Andrew Reynolds, Morgan Deters
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- * \todo document this file
- */
-
-#include "smt/smt_engine_scope.h"
-
-#include "base/check.h"
-#include "base/configuration_private.h"
-#include "base/output.h"
-#include "smt/solver_engine.h"
-
-namespace cvc5 {
-namespace smt {
-
-thread_local SolverEngine* s_slvEngine_current = nullptr;
-
-SolverEngine* currentSolverEngine()
-{
-  Assert(s_slvEngine_current != nullptr);
-  return s_slvEngine_current;
-}
-
-bool smtEngineInScope() { return s_slvEngine_current != nullptr; }
-
-ResourceManager* currentResourceManager()
-{
-  return s_slvEngine_current->getResourceManager();
-}
-
-SmtScope::SmtScope(const SolverEngine* smt)
-    : d_oldSlvEngine(s_slvEngine_current),
-      d_optionsScope(smt ? &const_cast<SolverEngine*>(smt)->getOptions()
-                         : nullptr)
-{
-  Assert(smt != nullptr);
-  s_slvEngine_current = const_cast<SolverEngine*>(smt);
-  Debug("current") << "smt scope: " << s_slvEngine_current << std::endl;
-}
-
-SmtScope::~SmtScope() {
-  s_slvEngine_current = d_oldSlvEngine;
-  Debug("current") << "smt scope: returning to " << s_slvEngine_current
-                   << std::endl;
-}
-
-StatisticsRegistry& SmtScope::currentStatisticsRegistry()
-{
-  Assert(smtEngineInScope());
-  return s_slvEngine_current->getStatisticsRegistry();
-}
-
-}  // namespace smt
-}  // namespace cvc5

diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
deleted file mode 100644 (file)
index a4c1f0e..0000000
--- a/src/smt/smt_engine_scope.h
+++ /dev/null
@@ -1,62 +0,0 @@
-/******************************************************************************
- * Top contributors (to current version):
- *   Andrew Reynolds, Andres Noetzli, Tim King
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
- * in the top-level source directory and their institutional affiliations.
- * All rights reserved.  See the file COPYING in the top-level source
- * directory for licensing information.
- * ****************************************************************************
- *
- * [[ Add one-line brief description here ]]
- *
- * [[ Add lengthier description here ]]
- * \todo document this file
- */
-
-#include "cvc5_private.h"
-
-#ifndef CVC5__SMT__SMT_ENGINE_SCOPE_H
-#define CVC5__SMT__SMT_ENGINE_SCOPE_H
-
-#include "expr/node_manager.h"
-
-#include "options/options.h"
-
-namespace cvc5 {
-
-class SolverEngine;
-class StatisticsRegistry;
-
-namespace smt {
-
-SolverEngine* currentSolverEngine();
-bool smtEngineInScope();
-
-/** get the current resource manager */
-ResourceManager* currentResourceManager();
-
-class SmtScope
-{
- public:
-  SmtScope(const SolverEngine* smt);
-  ~SmtScope();
-  /**
-   * This returns the StatisticsRegistry attached to the currently in scope
-   * SolverEngine.
-   */
-  static StatisticsRegistry& currentStatisticsRegistry();
-
- private:
-  /** The old SolverEngine, to be restored on destruction. */
-  SolverEngine* d_oldSlvEngine;
-  /** Options scope */
-  Options::OptionsScope d_optionsScope;
-};/* class SmtScope */
-
-}  // namespace smt
-}  // namespace cvc5
-
-#endif /* CVC5__SMT__SMT_ENGINE_SCOPE_H */

diff --git a/src/smt/smt_statistics_registry.cpp b/src/smt/smt_statistics_registry.cpp
index 1c948df6063055f1aba85b0aec04a192ffe5954c..74f60ba75feb64d25b7f0fd8944d593c0f185663 100644 (file)
--- a/src/smt/smt_statistics_registry.cpp
+++ b/src/smt/smt_statistics_registry.cpp
@@ -15,14 +15,14 @@
 
 #include "smt/smt_statistics_registry.h"
 
-#include "smt/smt_engine_scope.h"
+#include "smt/solver_engine_scope.h"
 #include "util/statistics_stats.h"
 
 namespace cvc5 {
 
 StatisticsRegistry& smtStatisticsRegistry()
 {
-  return smt::SmtScope::currentStatisticsRegistry();
+  return smt::SolverEngineScope::currentStatisticsRegistry();
 }
 
 }  // namespace cvc5

diff --git a/src/smt/smt_statistics_registry.h b/src/smt/smt_statistics_registry.h
index 66e8b522d327f08475f8f76a5769471a49ca9aba..d2b59820988ffc61812ff3079035ef5c72816576 100644 (file)
--- a/src/smt/smt_statistics_registry.h
+++ b/src/smt/smt_statistics_registry.h
@@ -25,7 +25,7 @@ namespace cvc5 {
 /**
  * This returns the StatisticsRegistry attached to the currently in scope
  * SolverEngine. This is a synonym for
- * smt::SmtScope::currentStatisticsRegistry().
+ * smt::SolverEngineScope::currentStatisticsRegistry().
  */
 StatisticsRegistry& smtStatisticsRegistry();
 

diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 52f47f037294da7cb70c94a588095e89dac9f355..4c8ec4ff2f4b1ee076b76ceae950378306a124b2 100644 (file)
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -53,10 +53,10 @@
 #include "smt/proof_manager.h"
 #include "smt/quant_elim_solver.h"
 #include "smt/set_defaults.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_engine_state.h"
 #include "smt/smt_engine_stats.h"
 #include "smt/smt_solver.h"
+#include "smt/solver_engine_scope.h"
 #include "smt/sygus_solver.h"
 #include "smt/unsat_core_manager.h"
 #include "theory/quantifiers/instantiation_list.h"
@@ -115,7 +115,7 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr)
   // SolverEngine. Thus the hack here does not break this use case. On the other
   // hand, this hack breaks use cases where multiple SolverEngine objects are
   // created by the user.
-  d_scope.reset(new SmtScope(this));
+  d_scope.reset(new SolverEngineScope(this));
   // listen to node manager events
   getNodeManager()->subscribeEvents(d_snmListener.get());
   // listen to resource out
@@ -276,7 +276,7 @@ void SolverEngine::shutdown()
 
 SolverEngine::~SolverEngine()
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
 
   try
   {
@@ -318,7 +318,7 @@ SolverEngine::~SolverEngine()
 
 void SolverEngine::setLogic(const LogicInfo& logic)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   if (d_state->isFullyInited())
   {
     throw ModalException(
@@ -332,7 +332,7 @@ void SolverEngine::setLogic(const LogicInfo& logic)
 
 void SolverEngine::setLogic(const std::string& s)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   try
   {
     setLogic(LogicInfo(s));
@@ -370,7 +370,7 @@ void SolverEngine::setLogicInternal()
 
 void SolverEngine::setInfo(const std::string& key, const std::string& value)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
 
   Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
 
@@ -429,7 +429,7 @@ bool SolverEngine::isValidGetInfoFlag(const std::string& key) const
 
 std::string SolverEngine::getInfo(const std::string& key) const
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
 
   Trace("smt") << "SMT getInfo(" << key << ")" << endl;
   if (key == "all-statistics")
@@ -572,7 +572,7 @@ void SolverEngine::defineFunction(Node func,
                                   Node formula,
                                   bool global)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   d_state->doPendingPops();
   Trace("smt") << "SMT defineFunction(" << func << ")" << endl;
@@ -610,7 +610,7 @@ void SolverEngine::defineFunctionsRec(
     const std::vector<Node>& formulas,
     bool global)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   d_state->doPendingPops();
   Trace("smt") << "SMT defineFunctionsRec(...)" << endl;
@@ -843,7 +843,7 @@ Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions,
 {
   try
   {
-    SmtScope smts(this);
+    SolverEngineScope smts(this);
     finishInit();
 
     Trace("smt") << "SolverEngine::"
@@ -921,7 +921,7 @@ Result SolverEngine::checkSatInternal(const std::vector<Node>& assumptions,
 std::vector<Node> SolverEngine::getUnsatAssumptions(void)
 {
   Trace("smt") << "SMT getUnsatAssumptions()" << endl;
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   if (!d_env->getOptions().smt.unsatAssumptions)
   {
     throw ModalException(
@@ -954,7 +954,7 @@ std::vector<Node> SolverEngine::getUnsatAssumptions(void)
 
 Result SolverEngine::assertFormula(const Node& formula)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   d_state->doPendingPops();
 
@@ -975,7 +975,7 @@ Result SolverEngine::assertFormula(const Node& formula)
 
 void SolverEngine::declareSygusVar(Node var)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   d_sygusSolver->declareSygusVar(var);
 }
 
@@ -984,7 +984,7 @@ void SolverEngine::declareSynthFun(Node func,
                                    bool isInv,
                                    const std::vector<Node>& vars)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   d_state->doPendingPops();
   d_sygusSolver->declareSynthFun(func, sygusType, isInv, vars);
@@ -1000,7 +1000,7 @@ void SolverEngine::declareSynthFun(Node func,
 
 void SolverEngine::assertSygusConstraint(Node n, bool isAssume)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   d_sygusSolver->assertSygusConstraint(n, isAssume);
 }
@@ -1010,14 +1010,14 @@ void SolverEngine::assertSygusInvConstraint(Node inv,
                                             Node trans,
                                             Node post)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   d_sygusSolver->assertSygusInvConstraint(inv, pre, trans, post);
 }
 
 Result SolverEngine::checkSynth()
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   return d_sygusSolver->checkSynth(*d_asserts);
 }
@@ -1039,7 +1039,7 @@ void SolverEngine::declarePool(const Node& p,
 
 Node SolverEngine::simplify(const Node& ex)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   d_state->doPendingPops();
   // ensure we've processed assertions
@@ -1050,7 +1050,7 @@ Node SolverEngine::simplify(const Node& ex)
 Node SolverEngine::expandDefinitions(const Node& ex)
 {
   getResourceManager()->spendResource(Resource::PreprocessStep);
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   d_state->doPendingPops();
   return d_smtSolver->getPreprocessor()->expandDefinitions(ex);
@@ -1059,7 +1059,7 @@ Node SolverEngine::expandDefinitions(const Node& ex)
 // TODO(#1108): Simplify the error reporting of this method.
 Node SolverEngine::getValue(const Node& ex) const
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
 
   Trace("smt") << "SMT getValue(" << ex << ")" << endl;
   if (Dump.isOn("benchmark"))
@@ -1132,7 +1132,7 @@ std::vector<Node> SolverEngine::getModelDomainElements(TypeNode tn) const
 
 bool SolverEngine::isModelCoreSymbol(Node n)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   Assert(n.isVar());
   const Options& opts = d_env->getOptions();
   if (opts.smt.modelCoresMode == options::ModelCoresMode::NONE)
@@ -1159,7 +1159,7 @@ bool SolverEngine::isModelCoreSymbol(Node n)
 std::string SolverEngine::getModel(const std::vector<TypeNode>& declaredSorts,
                                    const std::vector<Node>& declaredFuns)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   // !!! Note that all methods called here should have a version at the API
   // level. This is to ensure that the information associated with a model is
   // completely accessible by the user. This is currently not rigorously
@@ -1204,7 +1204,7 @@ std::string SolverEngine::getModel(const std::vector<TypeNode>& declaredSorts,
 Result SolverEngine::blockModel()
 {
   Trace("smt") << "SMT blockModel()" << endl;
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
 
   finishInit();
 
@@ -1233,7 +1233,7 @@ Result SolverEngine::blockModel()
 Result SolverEngine::blockModelValues(const std::vector<Node>& exprs)
 {
   Trace("smt") << "SMT blockModelValues()" << endl;
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
 
   finishInit();
 
@@ -1303,7 +1303,7 @@ void SolverEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
         "Cannot declare heap if not using the separation logic theory.";
     throw RecoverableModalException(msg);
   }
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   TheoryEngine* te = getTheoryEngine();
   te->declareSepHeap(locT, dataT);
@@ -1311,7 +1311,7 @@ void SolverEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
 
 bool SolverEngine::getSepHeapTypes(TypeNode& locT, TypeNode& dataT)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   TheoryEngine* te = getTheoryEngine();
   return te->getSepHeapTypes(locT, dataT);
@@ -1535,7 +1535,7 @@ void SolverEngine::checkModel(bool hardFailure)
 UnsatCore SolverEngine::getUnsatCore()
 {
   Trace("smt") << "SMT getUnsatCore()" << std::endl;
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   if (Dump.isOn("benchmark"))
   {
@@ -1560,7 +1560,7 @@ void SolverEngine::getRelevantInstantiationTermVectors(
 std::string SolverEngine::getProof()
 {
   Trace("smt") << "SMT getProof()\n";
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   if (Dump.isOn("benchmark"))
   {
@@ -1588,7 +1588,7 @@ std::string SolverEngine::getProof()
 
 void SolverEngine::printInstantiations(std::ostream& out)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations");
 
@@ -1682,7 +1682,7 @@ void SolverEngine::printInstantiations(std::ostream& out)
 void SolverEngine::getInstantiationTermVectors(
     std::map<Node, std::vector<std::vector<Node>>>& insts)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   QuantifiersEngine* qe =
       getAvailableQuantifiersEngine("getInstantiationTermVectors");
@@ -1692,14 +1692,14 @@ void SolverEngine::getInstantiationTermVectors(
 
 bool SolverEngine::getSynthSolutions(std::map<Node, Node>& solMap)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   return d_sygusSolver->getSynthSolutions(solMap);
 }
 
 Node SolverEngine::getQuantifierElimination(Node q, bool doFull, bool strict)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   const LogicInfo& logic = getLogicInfo();
   if (!logic.isPure(THEORY_ARITH) && strict)
@@ -1715,7 +1715,7 @@ bool SolverEngine::getInterpol(const Node& conj,
                                const TypeNode& grammarType,
                                Node& interpol)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   std::vector<Node> axioms = getExpandedAssertions();
   bool success =
@@ -1736,7 +1736,7 @@ bool SolverEngine::getAbduct(const Node& conj,
                              const TypeNode& grammarType,
                              Node& abd)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   std::vector<Node> axioms = getExpandedAssertions();
   bool success = d_abductSolver->getAbduct(axioms, conj, grammarType, abd);
@@ -1754,7 +1754,7 @@ bool SolverEngine::getAbduct(const Node& conj, Node& abd)
 
 void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   QuantifiersEngine* qe =
       getAvailableQuantifiersEngine("getInstantiatedQuantifiedFormulas");
   qe->getInstantiatedQuantifiedFormulas(qs);
@@ -1763,7 +1763,7 @@ void SolverEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
 void SolverEngine::getInstantiationTermVectors(
     Node q, std::vector<std::vector<Node>>& tvecs)
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   QuantifiersEngine* qe =
       getAvailableQuantifiersEngine("getInstantiationTermVectors");
   qe->getInstantiationTermVectors(q, tvecs);
@@ -1771,7 +1771,7 @@ void SolverEngine::getInstantiationTermVectors(
 
 std::vector<Node> SolverEngine::getAssertions()
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   d_state->doPendingPops();
   if (Dump.isOn("benchmark"))
@@ -1792,7 +1792,7 @@ std::vector<Node> SolverEngine::getAssertions()
 void SolverEngine::getDifficultyMap(std::map<Node, Node>& dmap)
 {
   Trace("smt") << "SMT getDifficultyMap()\n";
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   if (Dump.isOn("benchmark"))
   {
@@ -1814,7 +1814,7 @@ void SolverEngine::getDifficultyMap(std::map<Node, Node>& dmap)
 
 void SolverEngine::push()
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   d_state->doPendingPops();
   Trace("smt") << "SMT push()" << endl;
@@ -1828,7 +1828,7 @@ void SolverEngine::push()
 
 void SolverEngine::pop()
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
   finishInit();
   Trace("smt") << "SMT pop()" << endl;
   if (Dump.isOn("benchmark"))
@@ -1850,7 +1850,7 @@ void SolverEngine::pop()
 
 void SolverEngine::resetAssertions()
 {
-  SmtScope smts(this);
+  SolverEngineScope smts(this);
 
   if (!d_state->isFullyInited())
   {

diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h
index 0cb83cb0b6bfcc6f22fc372d7224e00cc4407a44..8ec0b15f37c501f399335b487ed112826d4de6aa 100644 (file)
--- a/src/smt/solver_engine.h
+++ b/src/smt/solver_engine.h
@@ -94,7 +94,7 @@ class InterpolationSolver;
 class QuantElimSolver;
 
 struct SmtEngineStatistics;
-class SmtScope;
+class SolverEngineScope;
 class PfManager;
 class UnsatCoreManager;
 
@@ -114,7 +114,7 @@ class CVC5_EXPORT SolverEngine
 {
   friend class ::cvc5::api::Solver;
   friend class ::cvc5::smt::SmtEngineState;
-  friend class ::cvc5::smt::SmtScope;
+  friend class ::cvc5::smt::SolverEngineScope;
 
   /* .......................................................................  */
  public:
@@ -1111,7 +1111,7 @@ class CVC5_EXPORT SolverEngine
    * SolverEngine in scope. It says the SolverEngine in scope until it is
    * destructed, or another SolverEngine is created.
    */
-  std::unique_ptr<smt::SmtScope> d_scope;
+  std::unique_ptr<smt::SolverEngineScope> d_scope;
 }; /* class SolverEngine */
 
 /* -------------------------------------------------------------------------- */

diff --git a/src/smt/solver_engine_scope.cpp b/src/smt/solver_engine_scope.cpp
new file mode 100644 (file)
index 0000000..6b12e4f
--- /dev/null
+++ b/src/smt/solver_engine_scope.cpp
@@ -0,0 +1,68 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andres Noetzli, Andrew Reynolds, Morgan Deters
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
+
+#include "smt/solver_engine_scope.h"
+
+#include "base/check.h"
+#include "base/configuration_private.h"
+#include "base/output.h"
+#include "smt/solver_engine.h"
+
+namespace cvc5 {
+namespace smt {
+
+thread_local SolverEngine* s_slvEngine_current = nullptr;
+
+SolverEngine* currentSolverEngine()
+{
+  Assert(s_slvEngine_current != nullptr);
+  return s_slvEngine_current;
+}
+
+bool solverEngineInScope() { return s_slvEngine_current != nullptr; }
+
+ResourceManager* currentResourceManager()
+{
+  return s_slvEngine_current->getResourceManager();
+}
+
+SolverEngineScope::SolverEngineScope(const SolverEngine* smt)
+    : d_oldSlvEngine(s_slvEngine_current),
+      d_optionsScope(smt ? &const_cast<SolverEngine*>(smt)->getOptions()
+                         : nullptr)
+{
+  Assert(smt != nullptr);
+  s_slvEngine_current = const_cast<SolverEngine*>(smt);
+  Debug("current") << "smt scope: " << s_slvEngine_current << std::endl;
+}
+
+SolverEngineScope::~SolverEngineScope()
+{
+  s_slvEngine_current = d_oldSlvEngine;
+  Debug("current") << "smt scope: returning to " << s_slvEngine_current
+                   << std::endl;
+}
+
+StatisticsRegistry& SolverEngineScope::currentStatisticsRegistry()
+{
+  Assert(solverEngineInScope());
+  return s_slvEngine_current->getStatisticsRegistry();
+}
+
+}  // namespace smt
+}  // namespace cvc5

diff --git a/src/smt/solver_engine_scope.h b/src/smt/solver_engine_scope.h
new file mode 100644 (file)
index 0000000..309321d
--- /dev/null
+++ b/src/smt/solver_engine_scope.h
@@ -0,0 +1,61 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds, Andres Noetzli, Tim King
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * [[ Add one-line brief description here ]]
+ *
+ * [[ Add lengthier description here ]]
+ * \todo document this file
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__SMT__SOLVER_ENGINE_SCOPE_H
+#define CVC5__SMT__SOLVER_ENGINE_SCOPE_H
+
+#include "expr/node_manager.h"
+#include "options/options.h"
+
+namespace cvc5 {
+
+class SolverEngine;
+class StatisticsRegistry;
+
+namespace smt {
+
+SolverEngine* currentSolverEngine();
+bool solverEngineInScope();
+
+/** get the current resource manager */
+ResourceManager* currentResourceManager();
+
+class SolverEngineScope
+{
+ public:
+  SolverEngineScope(const SolverEngine* smt);
+  ~SolverEngineScope();
+  /**
+   * This returns the StatisticsRegistry attached to the currently in scope
+   * SolverEngine.
+   */
+  static StatisticsRegistry& currentStatisticsRegistry();
+
+ private:
+  /** The old SolverEngine, to be restored on destruction. */
+  SolverEngine* d_oldSlvEngine;
+  /** Options scope */
+  Options::OptionsScope d_optionsScope;
+}; /* class SolverEngineScope */
+
+}  // namespace smt
+}  // namespace cvc5
+
+#endif /* CVC5__SMT__SMT_ENGINE_SCOPE_H */

diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index 1c4633b5ac725b1163e941aa8119b93d773ec8ce..3d25f19d6f3fe653b53fc8b04584d91a6b1f3f79 100644 (file)
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -19,9 +19,7 @@
 #include "options/bv_options.h"
 #include "printer/printer.h"
 #include "smt/dump.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
-#include "smt/solver_engine.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "util/bitvector.h"

diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h
index 17c233789a30aa88e2d4244943ae39e516817e74..0471f11e5581bd397e482265c315e2901ab443e9 100644 (file)
--- a/src/theory/bv/bitblast/bitblaster.h
+++ b/src/theory/bv/bitblast/bitblaster.h
@@ -28,7 +28,7 @@
 #include "prop/registrar.h"
 #include "prop/sat_solver.h"
 #include "prop/sat_solver_types.h"
-#include "smt/smt_engine_scope.h"
+#include "smt/solver_engine_scope.h"
 #include "theory/bv/bitblast/bitblast_strategies_template.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"

diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 27afdbbaa4216f39bc8b85e5a372fb754b0fd66f..e607444c2cb8945b07024402ccce9d2a3234827a 100644 (file)
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -20,9 +20,9 @@
 #include "options/bv_options.h"
 #include "printer/printer.h"
 #include "smt/dump.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "smt_util/boolean_simplification.h"
 #include "theory/bv/bv_quick_check.h"
 #include "theory/bv/bv_solver_layered.h"

diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 638c2aa265f092ee964366edcac0334ecd58c417..f893c89d7113361069c4fe1af46f63b724218126 100644 (file)
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -25,8 +25,8 @@
 #include "context/context.h"
 #include "printer/printer.h"
 #include "smt/dump.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/theory.h"
 #include "util/statistics_stats.h"

diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index eda56ef52d80dca632c07345adddb782988e7bd7..3b4babe75ff7ffecb4fe172afc0fe0db84a4df97 100644 (file)
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -17,9 +17,9 @@
 
 #include "options/base_options.h"
 #include "printer/printer.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"

diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index f891b0e99a2414f22a872c9b928d8147a59c61c5..583a70e3dc99ccb89bec41ea4fbd5f30da07bb52 100644 (file)
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -18,8 +18,8 @@
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "options/quantifiers_options.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_state.h"

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 4c23db9bc8e84ff5f840e269b371c5bbd8f0ccd0..234b3d142c186e1478c37ee529dcf01d01be5723 100644 (file)
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -17,9 +17,9 @@
 
 #include "options/theory_options.h"
 #include "proof/conv_proof_generator.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "theory/builtin/proof_checker.h"
 #include "theory/evaluator.h"
 #include "theory/quantifiers/extended_rewrite.h"
@@ -197,13 +197,14 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
   rewriteStack.push_back(RewriteStackElement(node, theoryId));
 
   ResourceManager* rm = NULL;
-  bool hasSmtEngine = smt::smtEngineInScope();
-  if (hasSmtEngine) {
+  bool hasSlvEngine = smt::solverEngineInScope();
+  if (hasSlvEngine)
+  {
     rm = smt::currentResourceManager();
   }
   // Rewrite until the stack is empty
   for (;;){
-    if (hasSmtEngine)
+    if (hasSlvEngine)
     {
       rm->spendResource(Resource::RewriteStep);
     }

diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index fb0a2dbda0a7b80354f0633a262db03b38d2cb32..99e3f7768610a8abd07287e73d007b8c4977a18f 100644 (file)
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -17,8 +17,8 @@
 #include "theory/smt_engine_subsolver.h"
 
 #include "smt/env.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "theory/rewriter.h"
 
 namespace cvc5 {

diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 08d713b0f19f57d9b9c453537f0f2f901648db35..5fc94614779eae6d446dc1217a70a950720dd93c 100644 (file)
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -15,8 +15,8 @@
 
 #include "theory/theory_inference_manager.h"
 
-#include "smt/smt_engine_scope.h"
 #include "smt/smt_statistics_registry.h"
+#include "smt/solver_engine_scope.h"
 #include "theory/output_channel.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"

diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp
index fef1184a25eed6f3b557db45a4a028ef029896ce..b69ba203c1a5cabacb7dbbcfa2d2c27b5122341f 100644 (file)
--- a/test/unit/node/attribute_white.cpp
+++ b/test/unit/node/attribute_white.cpp
@@ -22,8 +22,8 @@
 #include "expr/node_manager.h"
 #include "expr/node_manager_attributes.h"
 #include "expr/node_value.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "test_node.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index aca4239d561afab3e2f5f8e46b0ffe40d5994386..eb462006c6995908e74d118767d8ac45c4cc5ff2 100644 (file)
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -22,8 +22,8 @@
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/passes/bv_gauss.h"
 #include "preprocessing/preprocessing_pass_context.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "test_smt.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"

diff --git a/test/unit/test_env.h b/test/unit/test_env.h
index 4b4fb72e9c8b0a755408ac408a6c7eee667c78bf..b06254e7e8348764b55b2e8f6fa17e54eea7b551 100644 (file)
--- a/test/unit/test_env.h
+++ b/test/unit/test_env.h
@@ -20,8 +20,8 @@
 #include "expr/skolem_manager.h"
 #include "options/options.h"
 #include "smt/env.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "test.h"
 
 namespace cvc5 {

diff --git a/test/unit/test_node.h b/test/unit/test_node.h
index 08fa8eb305c88b3f84b28426e2c88fea5278dadd..7d3db971ce89c82d2adcfbdec3abe7df5d120ba6 100644 (file)
--- a/test/unit/test_node.h
+++ b/test/unit/test_node.h
@@ -18,8 +18,8 @@
 
 #include "expr/node_manager.h"
 #include "expr/skolem_manager.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "test.h"
 
 namespace cvc5 {

diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h
index 9dda1e588889a88b7ea15d67941ad3e6d722033e..f97b01931f1d263d603419eee635023c259f22ab 100644 (file)
--- a/test/unit/test_smt.h
+++ b/test/unit/test_smt.h
@@ -21,8 +21,8 @@
 #include "expr/node_manager.h"
 #include "expr/skolem_manager.h"
 #include "proof/proof_checker.h"
-#include "smt/smt_engine_scope.h"
 #include "smt/solver_engine.h"
+#include "smt/solver_engine_scope.h"
 #include "test.h"
 #include "theory/output_channel.h"
 #include "theory/rewriter.h"

diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp
index 9a98b174deedde0b3ef13143e104914ed3e6fd2b..c6b92154281a47e9a2fbe922203113b1006b1242 100644 (file)
--- a/test/unit/theory/regexp_operation_black.cpp
+++ b/test/unit/theory/regexp_operation_black.cpp
@@ -20,7 +20,7 @@
 #include "api/cpp/cvc5.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
-#include "smt/smt_engine_scope.h"
+#include "smt/solver_engine_scope.h"
 #include "test_smt.h"
 #include "theory/rewriter.h"
 #include "theory/strings/regexp_entail.h"