From: Guy <katz911@gmail.com>
Date: Wed, 27 Jul 2016 19:54:29 +0000 (-0700)
Subject: Added an option for a more aggressive weakest implicant optimization
X-Git-Tag: cvc5-1.0.0~6040^2~23
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6e5f92fe7c71fdbd11f28a11071bd3d37e429c82;p=cvc5.git

Added an option for a more aggressive weakest implicant optimization
---

diff --git a/src/options/proof_options b/src/options/proof_options
index a99d858bc..8a496bda6 100644
--- a/src/options/proof_options
+++ b/src/options/proof_options
@@ -8,4 +8,7 @@ module PROOF "options/proof_options.h" Proof
 option lfscLetification --lfsc-letification bool :default true
  turns on global letification in LFSC proofs
 
+option aggressiveCoreMin --aggressive-core-min bool :default false
+ turns on aggressive unsat core minimization (experimental)
+
 endmodule
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 0e683b084..a0b25fab1 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -348,7 +348,8 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
   Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off");
   Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" );
 
-  if (lemma.getKind() != kind::AND)
+  // If we're doing aggressive minimization, work on all lemmas, not just conjunctions.
+  if (!options::aggressiveCoreMin() && (lemma.getKind() != kind::AND))
     return lemma;
 
   constructSatProof();
@@ -377,15 +378,18 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) {
       for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) {
         builder << *lemmaIt;
 
-        // Sanity check: make sure that each conjunct really appears in the original lemma
-        bool found = false;
-        for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
-          if (lemma[i] == *lemmaIt)
-            found = true;
+        // Unless in aggressive mode, check that each conjunct appears in the original
+        // lemma.
+        if (!options::aggressiveCoreMin()) {
+          bool found = false;
+          for (unsigned i = 0; i < lemma.getNumChildren(); ++i) {
+            if (lemma[i] == *lemmaIt)
+              found = true;
+          }
+
+          if (!found)
+            return lemma;
         }
-
-        if (!found)
-          return lemma;
       }
     }
   }