diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-07-28 14:11:55 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-07-28 14:11:55 -0700 |
commit | 1377cede4b223a5b6a68d7d9194b7e3346a2d51a (patch) | |
tree | face9b6f6b46f663a38115c6ca11fb7415acbd10 /src/smt/smt_engine.cpp | |
parent | 5067dee413caf5f5bda4e666d877841f936d74b0 (diff) | |
parent | e6747735d2074fc2651c5edc11fa8170fc13663e (diff) |
Merge branch 'master' into docsLinkdocsLink
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 79 |
1 files changed, 76 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 9056e7c94..bbd65c24f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -27,6 +27,8 @@ #include "options/language.h" #include "options/main_options.h" #include "options/option_exception.h" +#include "options/options_public.h" +#include "options/parser_options.h" #include "options/printer_options.h" #include "options/proof_options.h" #include "options/smt_options.h" @@ -549,7 +551,7 @@ std::string SmtEngine::getInfo(const std::string& key) const } Assert(key == "all-options"); // get the options, like all-statistics - return toSExpr(Options::current().getOptions()); + return toSExpr(options::getAll(getOptions())); } void SmtEngine::debugCheckFormals(const std::vector<Node>& formals, Node func) @@ -1400,9 +1402,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"; @@ -1907,7 +1980,7 @@ void SmtEngine::setOption(const std::string& key, const std::string& value) } std::string optionarg = value; - getOptions().setOption(key, optionarg); + options::set(getOptions(), key, optionarg); } void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; } @@ -1972,7 +2045,7 @@ std::string SmtEngine::getOption(const std::string& key) const return nm->mkNode(Kind::SEXPR, result).toString(); } - std::string atom = getOptions().getOption(key); + std::string atom = options::get(getOptions(), key); if (atom != "true" && atom != "false") { |