Rename SmtScope to SolverEngineScope. (#7284)

1 files changed, 68 insertions, 0 deletions

diff --git a/src/smt/solver_engine_scope.cpp b/src/smt/solver_engine_scope.cpp
new file mode 100644
index 000000000..6b12e4f74
--- /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