diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-22 00:50:02 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-22 07:50:02 +0000 |
commit | d3af203110d575a89a119c4f2c3956a4f6ce69f5 (patch) | |
tree | 865ff8ba65e9ea03008680a493091d0ba4a441b6 /src/smt/smt_engine.cpp | |
parent | b839049634d97025ac57ba9a342fd8ab70737a33 (diff) |
Add support for minimal unsat cores (#4605)
This commit adds support for computing minimal unsat cores. The
algorithm implemented in this commit is just a trivial deletion-based
algorithm that tries to remove each assertion in the unsat core
individually.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 71 |
1 files changed, 71 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9056e7c94..b09fdb4d7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1400,9 +1400,80 @@ UnsatCore SmtEngine::getUnsatCoreInternal() std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(pepf, *d_asserts); std::vector<Node> core; d_ucManager->getUnsatCore(pfn, *d_asserts, core); + if (options::minimalUnsatCores()) + { + core = reduceUnsatCore(core); + } return UnsatCore(core); } +std::vector<Node> SmtEngine::reduceUnsatCore(const std::vector<Node>& core) +{ + Assert(options::unsatCores()) + << "cannot reduce unsat core if unsat cores are turned off"; + + Notice() << "SmtEngine::reduceUnsatCore(): reducing unsat core" << endl; + std::unordered_set<Node> removed; + for (const Node& skip : core) + { + std::unique_ptr<SmtEngine> coreChecker; + initializeSubsolver(coreChecker); + coreChecker->setLogic(getLogicInfo()); + coreChecker->getOptions().smt.checkUnsatCores = false; + // disable all proof options + coreChecker->getOptions().smt.produceProofs = false; + coreChecker->getOptions().smt.checkProofs = false; + coreChecker->getOptions().proof.proofEagerChecking = false; + + for (const Node& ucAssertion : core) + { + if (ucAssertion != skip && removed.find(ucAssertion) == removed.end()) + { + Node assertionAfterExpansion = expandDefinitions(ucAssertion); + coreChecker->assertFormula(assertionAfterExpansion); + } + } + Result r; + try + { + r = coreChecker->checkSat(); + } + catch (...) + { + throw; + } + + if (r.asSatisfiabilityResult().isSat() == Result::UNSAT) + { + removed.insert(skip); + } + else if (r.asSatisfiabilityResult().isUnknown()) + { + Warning() << "SmtEngine::reduceUnsatCore(): could not reduce unsat core " + "due to " + "unknown result."; + } + } + + if (removed.empty()) + { + return core; + } + else + { + std::vector<Node> newUcAssertions; + for (const Node& n : core) + { + if (removed.find(n) == removed.end()) + { + newUcAssertions.push_back(n); + } + } + + return newUcAssertions; + } +} + void SmtEngine::checkUnsatCore() { Assert(d_env->getOptions().smt.unsatCores) << "cannot check unsat core if unsat cores are turned off"; |