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

diff --git a/src/Makefile.am b/src/Makefile.am
index 539afc7810cd6415a8fd0c6453fe85f6a1677d3c..ae7cb619a416894b940f03df4e7d87c9ffd24f86 100644 (file)
--- 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 (file)
index 0000000..a0b6d2b
--- /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 4985b0e652ed79fce8e187c10931b10040240fc4..8aad440c6e7cd92929599f62eaac51773c9765cf 100644 (file)
--- 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 */