diff options
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 19 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 9 |
3 files changed, 23 insertions, 11 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 5428d9f1a..8d29cb8e1 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -328,7 +328,11 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn) } else { - mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn); + // The model basis term cannot be an interpreted function, or else we + // may produce an inconsistent model by choosing an arbitrary + // equivalence class for it. Hence, we require that it be an existing or + // fresh variable. + mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn, true); } } ModelBasisAttribute mba; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index c4b10eb6f..989609a76 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -113,19 +113,26 @@ Node TermDb::getTypeGroundTerm(TypeNode tn, unsigned i) const } } -Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn) +Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar) { std::map<TypeNode, std::vector<Node> >::const_iterator it = d_type_map.find(tn); if (it != d_type_map.end()) { Assert(!it->second.empty()); - return it->second[0]; - } - else - { - return getOrMakeTypeFreshVariable(tn); + if (!reqVar) + { + return it->second[0]; + } + for (const Node& v : it->second) + { + if (v.isVar()) + { + return v; + } + } } + return getOrMakeTypeFreshVariable(tn); } Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index cd5c27f0d..d58d33673 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -108,10 +108,11 @@ class TermDb : public QuantifiersUtil { */ Node getTypeGroundTerm(TypeNode tn, unsigned i) const; /** get or make ground term - * Returns the first ground term of type tn, - * or makes one if none exist. - */ - Node getOrMakeTypeGroundTerm(TypeNode tn); + * + * Returns the first ground term of type tn, or makes one if none exist. If + * reqVar is true, then the ground term must be a variable. + */ + Node getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar = false); /** make fresh variable * Returns a fresh variable of type tn. * This will return only a single fresh |