diff options
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 ){ |