diff options
author | Guy <katz911@gmail.com> | 2016-07-27 12:54:29 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-27 12:54:29 -0700 |
commit | 6e5f92fe7c71fdbd11f28a11071bd3d37e429c82 (patch) | |
tree | a001eedf0b3035ffa3cf652ea70b9f39799ff340 /src/proof/proof_manager.cpp | |
parent | 9dd9a6f7cff50d6877a81675073a322730afad91 (diff) |
Added an option for a more aggressive weakest implicant optimization
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 22 |
1 files changed, 13 insertions, 9 deletions
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; } } } |