From 2bd04431e38dbbaad843a8f92ba730a6a7a86e53 Mon Sep 17 00:00:00 2001
From: Guy <katz911@gmail.com>
Date: Thu, 28 Jul 2016 13:40:36 -0700
Subject: [PATCH] The "aggressive" optimizer for lemma L now returns the
 conjunction of all lemmas L' that originated from L and were used in the
 unsat core

---
 src/proof/proof_manager.cpp | 54 ++++++++++++++++++++++++++-----------
 1 file changed, 38 insertions(+), 16 deletions(-)

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 3249ed19d..42319153f 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -380,24 +380,23 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
   IdToSatClause::const_iterator it;
   std::set<Node>::iterator lemmaIt;
 
-  for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) {
-    std::set<Node> currentLemma = satClauseToNodeSet(it->second);
-
-    // 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(currentLemma))
-      continue;
+  if (!options::aggressiveCoreMin()) {
+    for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) {
+      std::set<Node> currentLemma = satClauseToNodeSet(it->second);
+
+      // 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(currentLemma))
+        continue;
 
-    recipe = getCnfProof()->getProofRecipe(currentLemma);
-    if (recipe.getOriginalLemma() == lemma) {
-      for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) {
-        builder << *lemmaIt;
+      recipe = getCnfProof()->getProofRecipe(currentLemma);
+      if (recipe.getOriginalLemma() == lemma) {
+        for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) {
+          builder << *lemmaIt;
 
-        // Unless in aggressive mode, check that each conjunct appears in the original
-        // lemma.
-        if (!options::aggressiveCoreMin()) {
+          // Check that each conjunct appears in the original lemma.
           bool found = false;
           for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
             if (lemma[i] == *lemmaIt)
@@ -409,6 +408,29 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
         }
       }
     }
+  } else {
+    // Aggressive mode
+    for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) {
+      std::set<Node> currentLemma = satClauseToNodeSet(it->second);
+
+      // 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(currentLemma))
+        continue;
+
+      recipe = getCnfProof()->getProofRecipe(currentLemma);
+      if (recipe.getOriginalLemma() == lemma) {
+        NodeBuilder<> disjunction(kind::OR);
+        for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) {
+          disjunction << *lemmaIt;
+        }
+
+        Node conjunct = (disjunction.getNumChildren() == 1) ? disjunction[0] : disjunction;
+        builder << conjunct;
+      }
+    }
   }
 
   AlwaysAssert(builder.getNumChildren() != 0);
-- 
2.30.2