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.

5 files changed, 63 insertions, 51 deletions

diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index 7bfe307c3..892e8d888 100644
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -21,6 +21,7 @@
 #include "printer/printer.h"
 #include "smt/command.h"
 #include "smt/command_list.h"
+#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 
 using namespace std;
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 */
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 */
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 6b071f8f7..a9fad80ae 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -21,6 +21,7 @@
 #include "options/quantifiers_modes.h"
 #include "options/quantifiers_options.h"
 #include "proof/proof_manager.h"
+#include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/trigger.h"
diff --git a/src/theory/quantifiers/term_database_sygus.cpp b/src/theory/quantifiers/term_database_sygus.cpp
index 62ba32d1e..0a48b8834 100644
--- a/src/theory/quantifiers/term_database_sygus.cpp
+++ b/src/theory/quantifiers/term_database_sygus.cpp
@@ -16,8 +16,9 @@
 
 #include "expr/datatype.h"
 #include "options/base_options.h"
-#include "options/quantifiers_options.h"
 #include "options/datatypes_options.h"
+#include "options/quantifiers_options.h"
+#include "smt/smt_engine.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fun_def_engine.h"