Clausify context-dependent simplifications in ext theory (#2711)

diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp
index 589ec45c0b8fb56cc98207c5e2ecccef6f9d75ab..c1e7c971f30b26b2ca767f56abfb84425e10ac69 100644 (file)
--- 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))
             {