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.

1 files changed, 43 insertions, 1 deletions

diff --git a/src/smt/smt_engine_scope.cpp b/src/smt/smt_engine_scope.cpp
index 87823775a..6c360cdc9 100644
--- a/src/smt/smt_engine_scope.cpp
+++ b/src/smt/smt_engine_scope.cpp
@@ -15,13 +15,55 @@
  ** \todo document this file
  **/
 
-#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 
+#include "base/configuration_private.h"
+#include "base/cvc4_assert.h"
+#include "base/output.h"
+#include "base/tls.h"
+#include "proof/proof.h"
+#include "smt/smt_engine.h"
+
 namespace CVC4 {
 namespace smt {
 
 CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current = NULL;
 
+SmtEngine* currentSmtEngine() {
+  Assert(s_smtEngine_current != NULL);
+  return s_smtEngine_current;
+}
+
+bool smtEngineInScope() { return s_smtEngine_current != NULL; }
+
+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 */
+}
+
+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::~SmtScope() {
+  s_smtEngine_current = d_oldSmtEngine;
+  Debug("current") << "smt scope: returning to " << s_smtEngine_current
+                   << std::endl;
+}
+
+StatisticsRegistry* SmtScope::currentStatisticsRegistry() {
+  Assert(smtEngineInScope());
+  return s_smtEngine_current->d_statisticsRegistry;
+}
+
 }/* CVC4::smt namespace */
 }/* CVC4 namespace */