Merge branch 'origin' of https://github.com/CVC4/CVC4.git

Conflicts:
	src/options/quantifiers_options

1 files changed, 6 insertions, 7 deletions

diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index 424530696..ef3337e53 100755
--- 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,8 @@ 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 );
+  bool checkCompleteFor( Node q );
   /** Identify this module */
   std::string identify() const { return "RewriteEngine"; }
 };