From 7b8531e83dd4c95a5b0eaa4927da5228c6942b7c Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 14 Aug 2017 15:32:23 -0700
Subject: Move function defns from smt_engine_scope.h to cpp (#216)

Additionally, this commit removes unnecessary includes, adds includes to
smt_engine.h in files that require it and removes s_smtEngine_current from
smt_engine_scope.h.
---
 src/smt/smt_engine_scope.h | 65 ++++++++++++----------------------------------
 1 file changed, 16 insertions(+), 49 deletions(-)

(limited to 'src/smt/smt_engine_scope.h')

diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index a3f716238..fda4d5e10 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -17,76 +17,43 @@
 
 #include "cvc4_private.h"
 
-#pragma once
+#ifndef __CVC4__SMT__SMT_ENGINE_SCOPE_H
+#define __CVC4__SMT__SMT_ENGINE_SCOPE_H
 
-#include "base/configuration_private.h"
-#include "base/cvc4_assert.h"
-#include "base/output.h"
-#include "base/tls.h"
 #include "expr/node_manager.h"
-#include "proof/proof.h"
-#include "proof/proof_manager.h"
-#include "options/smt_options.h"
-#include "smt/smt_engine.h"
-
 
 namespace CVC4 {
 
 class ProofManager;
+class SmtEngine;
+class StatisticsRegistry;
 
 namespace smt {
 
-extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
-
-inline SmtEngine* currentSmtEngine() {
-  Assert(s_smtEngine_current != NULL);
-  return s_smtEngine_current;
-}
-inline bool smtEngineInScope() {
-  return s_smtEngine_current != NULL;
-}
+SmtEngine* currentSmtEngine();
+bool smtEngineInScope();
 
 // FIXME: Maybe move into SmtScope?
-inline ProofManager* currentProofManager() {
-#if IS_PROOFS_BUILD
-  Assert(s_smtEngine_current != NULL);
-  return s_smtEngine_current->d_proofManager;
-#else /* IS_PROOFS_BUILD */
-  InternalError("proofs/unsat cores are not on, but ProofManager requested");
-  return NULL;
-#endif /* IS_PROOFS_BUILD */
-}
+ProofManager* currentProofManager();
 
 class SmtScope : public NodeManagerScope {
   /** The old NodeManager, to be restored on destruction. */
   SmtEngine* d_oldSmtEngine;
 
 public:
+ SmtScope(const SmtEngine* smt);
+ ~SmtScope();
 
-  SmtScope(const SmtEngine* smt) :
-    NodeManagerScope(smt->d_nodeManager),
-    d_oldSmtEngine(s_smtEngine_current) {
-    Assert(smt != NULL);
-    s_smtEngine_current = const_cast<SmtEngine*>(smt);
-    Debug("current") << "smt scope: " << s_smtEngine_current << std::endl;
-  }
-
-  ~SmtScope() {
-    s_smtEngine_current = d_oldSmtEngine;
-    Debug("current") << "smt scope: returning to " << s_smtEngine_current << std::endl;
-  }
-
-  /**
-   * This returns the StatisticsRegistry attached to the currently in scope
-   * SmtEngine.
-   */
-  static StatisticsRegistry* currentStatisticsRegistry() {
-    Assert(smtEngineInScope());
-    return s_smtEngine_current->d_statisticsRegistry;
-  }
+ /**
+  * This returns the StatisticsRegistry attached to the currently in scope
+  * SmtEngine.
+  */
+ static StatisticsRegistry* currentStatisticsRegistry();
 
 };/* class SmtScope */
 
 
 }/* CVC4::smt namespace */
 }/* CVC4 namespace */
+
+#endif /* __CVC4__SMT__SMT_ENGINE_SCOPE_H */
-- 
cgit v1.2.3