diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-19 19:18:38 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-11-19 19:18:38 -0600 |
commit | 2afbc4bbcccf9f91439809ee0026027a432a3061 (patch) | |
tree | 0f70972d260f46e772761661cf7bd86189c6daea /src/theory/ext_theory.cpp | |
parent | d7f5a6f2fa4b82b729e8ea76ef580c2bdb804e4e (diff) |
Clausify context-dependent simplifications in ext theory (#2711)
Diffstat (limited to 'src/theory/ext_theory.cpp')
-rw-r--r-- | src/theory/ext_theory.cpp | 24 |
1 files changed, 17 insertions, 7 deletions
diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp index 589ec45c0..c1e7c971f 100644 --- a/src/theory/ext_theory.cpp +++ b/src/theory/ext_theory.cpp @@ -233,6 +233,7 @@ bool ExtTheory::doInferencesInternal(int effort, std::vector<std::vector<Node> > exp; getSubstitutedTerms(effort, terms, sterms, exp); std::map<Node, unsigned> sterm_index; + NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = terms.size(); i < size; i++) { bool processed = false; @@ -245,15 +246,24 @@ bool ExtTheory::doInferencesInternal(int effort, { processed = true; markReduced(terms[i]); + // We have exp[i] => terms[i] = sr, convert this to a clause. + // This ensures the proof infrastructure can process this as a + // normal theory lemma. Node eq = terms[i].eqNode(sr); - Node expn = - exp[i].size() > 1 - ? NodeManager::currentNM()->mkNode(kind::AND, exp[i]) - : (exp[i].size() == 1 ? exp[i][0] : d_true); + Node lem = eq; + if (!exp[i].empty()) + { + std::vector<Node> eei; + for (const Node& e : exp[i]) + { + eei.push_back(e.negate()); + } + eei.push_back(eq); + lem = nm->mkNode(kind::OR, eei); + } + Trace("extt-debug") << "ExtTheory::doInferences : infer : " << eq - << " by " << expn << std::endl; - Node lem = - NodeManager::currentNM()->mkNode(kind::IMPLIES, expn, eq); + << " by " << exp[i] << std::endl; Trace("extt-debug") << "...send lemma " << lem << std::endl; if (sendLemma(lem)) { |