diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-17 15:31:28 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-06-17 15:31:38 -0500 |
commit | 66ee6c6472264be842f4e80a7106399d7f51d28a (patch) | |
tree | 55c6adcdcadc41c7b34d46eea7081d8bdc2eb7a0 /src/theory/quantifiers_engine.h | |
parent | 8936ca3ab2a1b9e3612e08a73542f7a288ee1df8 (diff) |
Make --var-elim-quant true by default. Add rewrite engine to quantifiers module.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 2ff2100b2..40b043752 100644 --- 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; |