From 07c4b6c27aac497c74695dd559adfee0d9e8e83f Mon Sep 17 00:00:00 2001 From: Tim King Date: Wed, 31 Aug 2016 23:06:39 -0700 Subject: [PATCH] Removing the forward declaration of QuantInfo from rewrite_engine.h. --- src/theory/quantifiers/rewrite_engine.cpp | 1 + src/theory/quantifiers/rewrite_engine.h | 12 +++++------- src/theory/theory_engine.h | 1 - 3 files changed, 6 insertions(+), 8 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 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 86c45a0e6..bb7946dd8 100644 --- 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" -- 2.30.2