From a4ca46db48f8ba450004dd96cce96efbc20b4362 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Mon, 26 May 2014 11:44:38 -0400
Subject: [PATCH] Separating an implicit inclusion of smt_engine.h from
 theory.h.

---
 src/Makefile.am           |  1 +
 src/smt/logic_request.cpp | 17 +++++++++++++++++
 src/smt/logic_request.h   | 10 +++-------
 3 files changed, 21 insertions(+), 7 deletions(-)
 create mode 100644 src/smt/logic_request.cpp

diff --git a/src/Makefile.am b/src/Makefile.am
index 539afc781..ae7cb619a 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -117,6 +117,7 @@ libcvc4_la_SOURCES = \
 	smt/boolean_terms.cpp \
 	smt/logic_exception.h \
 	smt/logic_request.h \
+	smt/logic_request.cpp \
 	smt/simplification_mode.h \
 	smt/simplification_mode.cpp \
 	smt/options_handlers.h \
diff --git a/src/smt/logic_request.cpp b/src/smt/logic_request.cpp
new file mode 100644
index 000000000..a0b6d2bb9
--- /dev/null
+++ b/src/smt/logic_request.cpp
@@ -0,0 +1,17 @@
+
+
+#include "smt/logic_request.h"
+#include "smt/smt_engine.h"
+
+
+namespace CVC4 {
+
+/** Widen the logic to include the given theory. */
+void LogicRequest::widenLogic(theory::TheoryId id) {
+  d_smt.d_logic.getUnlockedCopy();
+  d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
+  d_smt.d_logic.enableTheory(id);
+  d_smt.d_logic.lock();
+}
+
+}/* CVC4 namespace */
diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h
index 4985b0e65..8aad440c6 100644
--- a/src/smt/logic_request.h
+++ b/src/smt/logic_request.h
@@ -27,10 +27,11 @@
 #define __CVC4__LOGIC_REQUEST_H
 
 #include "expr/kind.h"
-#include "smt/smt_engine.h"
 
 namespace CVC4 {
 
+class SmtEngine;
+
 class LogicRequest {
   /** The SmtEngine at play. */
   SmtEngine& d_smt;
@@ -39,12 +40,7 @@ public:
   LogicRequest(SmtEngine& smt) : d_smt(smt) { }
 
   /** Widen the logic to include the given theory. */
-  void widenLogic(theory::TheoryId id) {
-    d_smt.d_logic.getUnlockedCopy();
-    d_smt.d_logic = d_smt.d_logic.getUnlockedCopy();
-    d_smt.d_logic.enableTheory(id);
-    d_smt.d_logic.lock();
-  }
+  void widenLogic(theory::TheoryId id);
 
 };/* class LogicRequest */
 
-- 
2.30.2