diff options
-rw-r--r-- | NEWS | 1 | ||||
-rw-r--r-- | src/options/smt_options.toml | 8 | ||||
-rw-r--r-- | src/smt/set_defaults.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 71 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 7 | ||||
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/minimal_unsat_core.smt2 | 12 |
7 files changed, 100 insertions, 2 deletions
@@ -23,6 +23,7 @@ New Features: * Support for `str.indexof_re(s, r, n)`, which returns the index of the first occurrence of a regular expression `r` in a string `s` after index `n` or -1 if `r` does not match a substring after `n`. +* A new option to compute minimal unsat cores (`--minimal-unsat-cores`). Improvements: * New API: Added functions to retrieve the heap/nil term when using separation diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 9b5a93486..a97fe572f 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -195,6 +195,14 @@ name = "SMT Layer" help = "Produce unsat cores using solving under assumptions and preprocessing proofs." [[option]] + name = "minimalUnsatCores" + category = "regular" + long = "minimal-unsat-cores" + type = "bool" + default = "false" + help = "if an unsat core is produced, it is reduced to a minimal unsat core" + +[[option]] name = "checkUnsatCores" category = "regular" long = "check-unsat-cores" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index bb104e98d..d5b3b7929 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -69,7 +69,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.driver.dumpUnsatCores = true; } if (options::checkUnsatCores() || options::dumpUnsatCores() - || options::unsatAssumptions() + || options::unsatAssumptions() || options::minimalUnsatCores() || options::unsatCoresMode() != options::UnsatCoresMode::OFF) { opts.smt.unsatCores = true; 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"; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3128257e6..02e5c6b06 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -1,6 +1,6 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew Reynolds, Morgan Deters, Aina Niemetz + * * This file is part of the cvc5 project. * @@ -368,6 +368,11 @@ class CVC5_EXPORT SmtEngine Result assertFormula(const Node& formula, bool inUnsatCore = true); /** + * Reduce an unsatisfiable core to make it minimal. + */ + std::vector<Node> reduceUnsatCore(const std::vector<Node>& core); + + /** * Check if a given (set of) expression(s) is entailed with respect to the * current set of assertions. We check this by asserting the negation of * the (big AND over the) given (set of) expression(s). diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index db6a7ae48..6ebb91f9e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1649,6 +1649,7 @@ set(regress_1_tests regress1/issue5739-rtf-processed.smt2 regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2 regress1/lemmas/pursuit-safety-8.smtv1.smt2 + regress1/minimal_unsat_core.smt2 regress1/model-blocker-simple.smt2 regress1/model-blocker-values.smt2 regress1/nl/approx-sqrt.smt2 diff --git a/test/regress/regress1/minimal_unsat_core.smt2 b/test/regress/regress1/minimal_unsat_core.smt2 new file mode 100644 index 000000000..ef1d3ceef --- /dev/null +++ b/test/regress/regress1/minimal_unsat_core.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --minimal-unsat-cores +(set-logic QF_NIA) +(set-info :status unsat) +(declare-fun n () Int) + +(assert (= n 0)) +(assert (= (div (div n n) n) + (div (div (div n n) n) n))) +(assert (distinct (div (div n n) n) + (div (div (div (div (div n n) n) n) n) n))) + +(check-sat) |