diff options
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)) { |