Removing the forward declaration of QuantInfo from rewrite_engine.h.

diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 2c58b8f778af0be92473dd647b92cf2b23ab7c5c..3add7a9d7bfdd705d513677f10fae283a6f5ef14 100644 (file)
--- 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 424530696a514775628bbd907d512568de44cd65..8d0678724e02baf67dc62e4c3cb4f6a2d7854b41 100644 (file)
--- 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"; }
 };

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 86c45a0e64e37b563d6610c03ad46b2ec5c004f2..bb7946dd833315fb1ce4a120fa8177dc15d7f5c3 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -35,7 +35,6 @@
 #include "theory/atom_requests.h"
 #include "theory/bv/bv_to_bool.h"
 #include "theory/interrupted.h"
-#include "theory/quantifiers/quant_conflict_find.h"
 #include "theory/rewriter.h"
 #include "theory/shared_terms_database.h"
 #include "theory/sort_inference.h"