Added an option for a more aggressive weakest implicant optimization

diff --git a/src/options/proof_options b/src/options/proof_options
index a99d858bcd2c680139744e90ed01c40c56ba0287..8a496bda6d9a2aa77a50ccd8943d4b01af404c77 100644 (file)
--- 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 0e683b0848b5ac90b3faf1d93c473a8c51afe37a..a0b25fab11d0babc25f5bd9075439a3449134747 100644 (file)
--- 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;
       }
     }
   }