Removing the forward declaration of QuantInfo from rewrite_engine.h.

2 files changed, 6 insertions, 7 deletions

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 2c58b8f77..3add7a9d7 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/inst_match_generator.h"
 #include "theory/quantifiers/model_engine.h"
+#include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/theory_engine.h"
diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 424530696..8d0678724 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -18,19 +18,17 @@
 #ifndef __CVC4__REWRITE_ENGINE_H
 #define __CVC4__REWRITE_ENGINE_H
 
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/trigger.h"
-
+#include "context/cdchunk_list.h"
 #include "context/context.h"
 #include "context/context_mm.h"
-#include "context/cdchunk_list.h"
+#include "theory/quantifiers/trigger.h"
+#include "theory/quantifiers/quant_conflict_find.h"
+#include "theory/quantifiers_engine.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class QuantInfo;
-
 class RewriteEngine : public QuantifiersModule
 {
   typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
@@ -57,7 +55,7 @@ public:
   bool needsCheck( Theory::Effort e );
   void check( Theory::Effort e, unsigned quant_e );
   void registerQuantifier( Node f );
-  void assertNode( Node n );  
+  void assertNode( Node n );
   /** Identify this module */
   std::string identify() const { return "RewriteEngine"; }
 };