Make --var-elim-quant true by default. Add rewrite engine to quantifiers module.

[cvc5.git] / src / theory / quantifiers_engine.h

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 2ff2100b2ed70f59d9d69734a7a020d0a4eaf217..40b043752a9c07baae5916815f5a4e46aa5fea8b 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -60,11 +60,13 @@ public:
 };/* class QuantifiersModule */
 
 namespace quantifiers {
-  class InstantiationEngine;
-  class ModelEngine;
   class TermDb;
   class FirstOrderModel;
+  //modules
+  class InstantiationEngine;
+  class ModelEngine;
   class BoundedIntegers;
+  class RewriteEngine;
 }/* CVC4::theory::quantifiers */
 
 namespace inst {
@@ -88,10 +90,6 @@ private:
   TheoryEngine* d_te;
   /** vector of modules for quantifiers */
   std::vector< QuantifiersModule* > d_modules;
-  /** instantiation engine */
-  quantifiers::InstantiationEngine* d_inst_engine;
-  /** model engine */
-  quantifiers::ModelEngine* d_model_engine;
   /** equality query class */
   EqualityQueryQuantifiersEngine* d_eq_query;
   /** for computing relevance of quantifiers */
@@ -100,8 +98,14 @@ private:
   std::map< Node, QuantPhaseReq* > d_phase_reqs;
   /** efficient e-matcher */
   EfficientEMatcher* d_eem;
+  /** instantiation engine */
+  quantifiers::InstantiationEngine* d_inst_engine;
+  /** model engine */
+  quantifiers::ModelEngine* d_model_engine;
   /** bounded integers utility */
   quantifiers::BoundedIntegers * d_bint;
+  /** rewrite rules utility */
+  quantifiers::RewriteEngine * d_rr_engine;
 private:
   /** list of all quantifiers seen */
   std::vector< Node > d_quants;