diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-04 09:32:31 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-11-04 09:32:31 -0500 |
commit | 84812843d121006218ab3d63fd651f6d7cd4c72e (patch) | |
tree | 1c74ee94271ea92cf9ee2fc0d001c8ff28b8ee6c /src/theory/uf/ho_extension.cpp | |
parent | b3d9ba15441dd2c46d7a25f97cf0f488d83b964f (diff) | |
parent | a517a9127e0ef70424364d093bb21be64891dd0d (diff) |
Merge branch 'master' into privateGetprivateGet
Diffstat (limited to 'src/theory/uf/ho_extension.cpp')
-rw-r--r-- | src/theory/uf/ho_extension.cpp | 20 |
1 files changed, 17 insertions, 3 deletions
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index fd7cd467e..e23262746 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -200,7 +200,11 @@ Node HoExtension::getApplyUfForHoApply(Node node) unsigned HoExtension::checkExtensionality(TheoryModel* m) { - eq::EqualityEngine* ee = d_state.getEqualityEngine(); + // if we are in collect model info, we require looking at the model's + // equality engine, so that we only consider "relevant" (see + // Theory::computeRelevantTerms) function terms. + eq::EqualityEngine* ee = + m != nullptr ? m->getEqualityEngine() : d_state.getEqualityEngine(); NodeManager* nm = NodeManager::currentNM(); unsigned num_lemmas = 0; bool isCollectModel = (m != nullptr); @@ -247,8 +251,13 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) for (unsigned k = (j + 1), sizek = itf->second.size(); k < sizek; k++) { // if these equivalence classes are not explicitly disequal, do - // extensionality to ensure distinctness - if (!ee->areDisequal(itf->second[j], itf->second[k], false)) + // extensionality to ensure distinctness. Notice that we always use + // the (local) equality engine for this check via the state, since the + // model's equality engine does not store any disequalities. This is + // an optimization to introduce fewer equalities during model + // construction, since we know such disequalities have already been + // witness via assertions. + if (!d_state.areDisequal(itf->second[j], itf->second[k])) { Node deq = Rewriter::rewrite(itf->second[j].eqNode(itf->second[k]).negate()); @@ -450,6 +459,11 @@ bool HoExtension::collectModelInfoHo(TheoryModel* m, return false; } } + // We apply an explicit extensionality technique for asserting + // disequalities to the model to ensure that function values are distinct + // in the curried HO_APPLY version of model construction. This is a + // non-standard alternative to using a type enumerator over function + // values to assign unique values. int addedLemmas = checkExtensionality(m); return addedLemmas == 0; } |