From: Guy <katz911@gmail.com>
Date: Thu, 28 Jul 2016 16:01:52 +0000 (-0700)
Subject: Add the negative conjunction case
X-Git-Tag: cvc5-1.0.0~6040^2~19
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b539fb0692680c16247e3aa6e150457dd265f834;p=cvc5.git

Add the negative conjunction case
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e4b4756bf..bd0b467f2 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -112,9 +112,17 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori
   switch (lemma.getKind()) {
 
   case kind::AND:
-    Assert(!negated); // TODO
-    for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
-      registerLemmaRecipe(lemma[i], originalLemma, false, theoryId);
+    if (!negated) {
+      for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
+        registerLemmaRecipe(lemma[i], originalLemma, false, theoryId);
+    } else {
+      NodeBuilder<> builder(kind::OR);
+      for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
+        builder << lemma[i].negate();
+
+      Node disjunction = (builder.getNumChildren() == 1) ? builder[0] : builder;
+      registerLemmaRecipe(disjunction, originalLemma, false, theoryId);
+    }
     break;
 
   case kind::IFF: