diff options
Diffstat (limited to 'src/theory/quantifiers/fmf/model_builder.cpp')
| -rw-r--r-- | src/theory/quantifiers/fmf/model_builder.cpp | 30 |
1 files changed, 11 insertions, 19 deletions
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 5ae05f2a7..a3dc50dd1 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -47,7 +47,8 @@ bool QModelBuilder::preProcessBuildModel(TheoryModel* m) { bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { d_addedLemmas = 0; d_triedLemmas = 0; - if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){ + if (options::fmfFunWellDefinedRelevant()) + { FirstOrderModel * fm = (FirstOrderModel*)m; //traverse equality engine std::map< TypeNode, bool > eqc_usort; @@ -63,28 +64,19 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) { Node q = fm->getAssertedQuantifier( i, true ); if( fm->isQuantifierActive( q ) ){ //check if any of these quantified formulas can be set inactive - if( options::fmfEmptySorts() ){ - for (const Node& var : q[0]) + if (q[0].getNumChildren() == 1) + { + TypeNode tn = q[0][0].getType(); + if (tn.getAttribute(AbsTypeFunDefAttribute())) { - TypeNode tn = var.getType(); - //we are allowed to assume the type is empty - if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){ - Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl; + // we are allowed to assume the introduced type is empty + if (eqc_usort.find(tn) == eqc_usort.end()) + { + Trace("model-engine-debug") + << "Irrelevant function definition : " << q << std::endl; fm->setQuantifierActive( q, false ); } } - }else if( options::fmfFunWellDefinedRelevant() ){ - if( q[0].getNumChildren()==1 ){ - TypeNode tn = q[0][0].getType(); - if( tn.getAttribute(AbsTypeFunDefAttribute()) ){ - //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl; - //we are allowed to assume the introduced type is empty - if( eqc_usort.find( tn )==eqc_usort.end() ){ - Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl; - fm->setQuantifierActive( q, false ); - } - } - } } } } |