From: Guy <katz911@gmail.com>
Date: Thu, 28 Jul 2016 18:24:07 +0000 (-0700)
Subject: Bug fix involving negated lemmas
X-Git-Tag: cvc5-1.0.0~6040^2~18
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fff97c76bc1ba86594114ea91ba6b23944964f55;p=cvc5.git

Bug fix involving negated lemmas
---

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index a86991963..3249ed19d 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -41,6 +41,15 @@
 
 namespace CVC4 {
 
+std::string nodeSetToString(const std::set<Node>& nodes) {
+  std::ostringstream os;
+  std::set<Node>::const_iterator it;
+  for (it = nodes.begin(); it != nodes.end(); ++it) {
+    os << *it << " ";
+  }
+  return os.str();
+}
+
 std::string append(const std::string& str, uint64_t num) {
   std::ostringstream os;
   os << str << num;
@@ -315,17 +324,23 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod
   IdToSatClause::const_iterator it;
   std::set<Node> seen;
 
+  Debug("pf::lemmasUnsatCore") << "Dumping all lemmas in unsat core" << std::endl;
   for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) {
     std::set<Node> lemma = satClauseToNodeSet(it->second);
+    Debug("pf::lemmasUnsatCore") << nodeSetToString(lemma);
 
     // TODO: we should be able to drop the "haveProofRecipe" check.
     // however, there are some rewrite issues with the arith solver, resulting
     // in non-registered recipes. For now we assume no one is requesting arith lemmas.
     LemmaProofRecipe recipe;
-    if (!getCnfProof()->haveProofRecipe(lemma))
+    if (!getCnfProof()->haveProofRecipe(lemma)) {
+      Debug("pf::lemmasUnsatCore") << "\t[no recipe]" << std::endl;
       continue;
+    }
 
     recipe = getCnfProof()->getProofRecipe(lemma);
+    Debug("pf::lemmasUnsatCore") << "\t[owner = " << recipe.getTheory()
+                                 << ", original = " << recipe.getOriginalLemma() << "]" << std::endl;
     if (recipe.simpleLemma() && recipe.getTheory() == theory && seen.find(recipe.getOriginalLemma()) == seen.end()) {
       lemmas.push_back(recipe.getOriginalLemma());
       seen.insert(recipe.getOriginalLemma());
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index bd0b467f2..94281156f 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -106,19 +106,18 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori
     lemma = d_engine->preprocess(lemma);
 
   bool negated = (lemma.getKind() == kind::NOT);
-  if (negated)
-    lemma = lemma[0];
+  Node nnLemma = negated ? lemma[0] : lemma;
 
-  switch (lemma.getKind()) {
+  switch (nnLemma.getKind()) {
 
   case kind::AND:
     if (!negated) {
-      for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
-        registerLemmaRecipe(lemma[i], originalLemma, false, theoryId);
+      for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i)
+        registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId);
     } else {
       NodeBuilder<> builder(kind::OR);
-      for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
-        builder << lemma[i].negate();
+      for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i)
+        builder << nnLemma[i].negate();
 
       Node disjunction = (builder.getNumChildren() == 1) ? builder[0] : builder;
       registerLemmaRecipe(disjunction, originalLemma, false, theoryId);
@@ -127,21 +126,21 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori
 
   case kind::IFF:
     if (!negated) {
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1].negate()), originalLemma, false, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId);
     } else {
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1]), originalLemma, false, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId);
     }
     break;
 
   case kind::ITE:
     if (!negated) {
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, false, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2]), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2]), originalLemma, false, theoryId);
     } else {
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, false, theoryId);
-      registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2].negate()), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId);
+      registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2].negate()), originalLemma, false, theoryId);
     }
     break;