From: Guy <katz911@gmail.com>
Date: Thu, 28 Jul 2016 01:17:41 +0000 (-0700)
Subject: proper handling of ITEs
X-Git-Tag: cvc5-1.0.0~6040^2~21
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9242c63ff2564612f7ea719c3bd735be7c68bc00;p=cvc5.git

proper handling of ITEs
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index feed010e8..123b0bffc 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -103,12 +103,40 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori
 
   NodeManager* nm = NodeManager::currentNM();
 
-  if (lemma.getKind() == kind::AND) {
+  bool negated = (lemma.getKind() == kind::NOT);
+  if (negated)
+    lemma = lemma[0];
+
+  switch (lemma.getKind()) {
+
+  case kind::AND:
+    Assert(!negated); // TODO
     for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
       registerLemmaRecipe(lemma[i], originalLemma, theoryId);
-  } else if (lemma.getKind() == kind::IFF) {
-    registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1].negate()), originalLemma, theoryId);
-    registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, theoryId);
+    break;
+
+  case kind::IFF:
+    if (!negated) {
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1].negate()), originalLemma, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, theoryId);
+    } else {
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1]), originalLemma, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, theoryId);
+    }
+    break;
+
+  case kind::ITE:
+    if (!negated) {
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2]), originalLemma, theoryId);
+    } else {
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2].negate()), originalLemma, theoryId);
+    }
+    break;
+
+  default:
+    break;
   }
 
   // Theory lemmas have one step that proves the empty clause