diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-27 17:47:56 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-27 15:47:56 -0700 |
commit | 3af2dfea22aae0d527fcfa93600c451b323c15b7 (patch) | |
tree | 046c84f5f05ca2900d1e8484a45fbf1cba7b91cb /src/theory/uf | |
parent | 24936010e7d0dc644bd2bf1f533ac0abee678f6b (diff) |
Fix collect model info for higher-order (#3409)
This ensures we add lemmas when collect model info fails for the higher order extension of UF. This fixes #3405 (that benchmark now answers unknown).
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/ho_extension.cpp | 10 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 2 |
2 files changed, 12 insertions, 0 deletions
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp index 88b2ba8d2..0ca9b151f 100644 --- a/src/theory/uf/ho_extension.cpp +++ b/src/theory/uf/ho_extension.cpp @@ -186,6 +186,7 @@ Node HoExtension::getApplyUfForHoApply(Node node) unsigned HoExtension::checkExtensionality(TheoryModel* m) { eq::EqualityEngine* ee = d_parent.getEqualityEngine(); + NodeManager* nm = NodeManager::currentNM(); unsigned num_lemmas = 0; bool isCollectModel = (m != nullptr); Trace("uf-ho") << "HoExtension::checkExtensionality, collectModel=" @@ -243,6 +244,11 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m) << "Add extensionality deq to model : " << edeq << std::endl; if (!m->assertEquality(edeq[0][0], edeq[0][1], false)) { + Node eq = edeq[0][0].eqNode(edeq[0][1]); + Node lem = nm->mkNode(OR, deq.negate(), eq); + Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem + << std::endl; + d_parent.getOutputChannel().lemma(lem); return 1; } } @@ -423,6 +429,10 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m) Node hn = TheoryUfRewriter::getHoApplyForApplyUf(n); if (!m->assertEquality(n, hn, true)) { + Node eq = n.eqNode(hn); + Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq + << std::endl; + d_parent.getOutputChannel().lemma(eq); return false; } } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 6284ae31e..76e6e08bc 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -324,6 +324,7 @@ bool TheoryUF::collectModelInfo(TheoryModel* m) if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) { + Trace("uf") << "Collect model info fail UF" << std::endl; return false; } @@ -332,6 +333,7 @@ bool TheoryUF::collectModelInfo(TheoryModel* m) // function equivalence classes. if (!d_ho->collectModelInfoHo(termSet, m)) { + Trace("uf") << "Collect model info fail HO" << std::endl; return false; } } |