diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/options/proof_options | 3 | ||||
| -rw-r--r-- | src/proof/proof_manager.cpp | 22 |
2 files changed, 16 insertions, 9 deletions
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; } } } |