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/model_builder.cpp | |
| parent | 8936ca3ab2a1b9e3612e08a73542f7a288ee1df8 (diff) | |
Make --var-elim-quant true by default. Add rewrite engine to quantifiers module.
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
| -rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 88fb7cd8f..fbf3ce59c 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -39,6 +39,10 @@ TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe d_addedLemmas = 0; } +bool QModelBuilder::isQuantifierActive( Node f ) { + return !f.hasAttribute(QRewriteRuleAttribute()); +} + bool QModelBuilder::optUseModel() { return options::fmfModelBasedInst(); @@ -355,7 +359,8 @@ QModelBuilderIG::Statistics::~Statistics(){ } bool QModelBuilderIG::isQuantifierActive( Node f ){ - return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end(); + return !f.hasAttribute(QRewriteRuleAttribute()) && + ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end(); } bool QModelBuilderIG::isTermActive( Node n ){ |