From: Tim King <taking@cs.nyu.edu>
Date: Mon, 26 May 2014 15:44:38 +0000 (-0400)
Subject: Separating an implicit inclusion of smt_engine.h from theory.h.
X-Git-Tag: cvc5-1.0.0~6891
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a4ca46db48f8ba450004dd96cce96efbc20b4362;p=cvc5.git

Separating an implicit inclusion of smt_engine.h from theory.h.
---

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 */