diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-06-01 09:39:16 +0200 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-06-01 00:39:16 -0700 |
commit | 9b6985b4427aff888f07ecc84079452c11113cb6 (patch) | |
tree | e693faec20af263356c78ee7daa7bb5340b307f7 /src/theory/quantifiers/term_database.cpp | |
parent | 9d93595783e350969ad428ab277614a3250e59a0 (diff) |
Require that FMF model basis terms are variables (#3031)
The commit fixes an issue where FMF could theoretically chose interpreted function applications as "model basis terms". This triggered an incorrect model (caught by an AlwaysAssert) when the interpreted function later did not appear in a model and was chosen by FMF to be equal to a wrong value.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 19 |
1 files changed, 13 insertions, 6 deletions
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) |