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.cpp | |
parent | 8936ca3ab2a1b9e3612e08a73542f7a288ee1df8 (diff) |
Make --var-elim-quant true by default. Add rewrite engine to quantifiers module.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index c663e1aa2..94bc475d0 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -28,6 +28,7 @@ #include "theory/rewriterules/efficient_e_matching.h" #include "theory/rewriterules/rr_trigger.h" #include "theory/quantifiers/bounded_integers.h" +#include "theory/quantifiers/rewrite_engine.h" using namespace std; using namespace CVC4; @@ -62,9 +63,15 @@ d_lemmas_produced_c(u){ }else{ d_inst_engine = NULL; } - if( options::finiteModelFind() ){ + bool reqModel = options::finiteModelFind() || options::rewriteRulesAsAxioms(); + if( reqModel ){ d_model_engine = new quantifiers::ModelEngine( c, this ); d_modules.push_back( d_model_engine ); + }else{ + d_model_engine = NULL; + } + + if( options::finiteModelFind() ){ if( options::fmfBoundInt() ){ d_bint = new quantifiers::BoundedIntegers( c, this ); d_modules.push_back( d_bint ); @@ -72,9 +79,14 @@ d_lemmas_produced_c(u){ d_bint = NULL; } }else{ - d_model_engine = NULL; d_bint = NULL; } + if( options::rewriteRulesAsAxioms() ){ + d_rr_engine = new quantifiers::RewriteEngine( c, this ); + d_modules.push_back(d_rr_engine); + }else{ + d_rr_engine = NULL; + } //options d_optInstCheckDuplicate = true; |