From d3af203110d575a89a119c4f2c3956a4f6ce69f5 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 22 Jul 2021 00:50:02 -0700 Subject: [PATCH] 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. --- NEWS | 1 + src/options/smt_options.toml | 8 +++ src/smt/set_defaults.cpp | 2 +- src/smt/smt_engine.cpp | 71 +++++++++++++++++++ src/smt/smt_engine.h | 7 +- test/regress/CMakeLists.txt | 1 + test/regress/regress1/minimal_unsat_core.smt2 | 12 ++++ 7 files changed, 100 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/minimal_unsat_core.smt2 diff --git a/NEWS b/NEWS index 74ee86165..f01643643 100644 --- a/NEWS +++ b/NEWS @@ -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 @@ -194,6 +194,14 @@ name = "SMT Layer" name = "assumptions" 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" 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 pfn = d_pfManager->getFinalProof(pepf, *d_asserts); std::vector core; d_ucManager->getUnsatCore(pfn, *d_asserts, core); + if (options::minimalUnsatCores()) + { + core = reduceUnsatCore(core); + } return UnsatCore(core); } +std::vector SmtEngine::reduceUnsatCore(const std::vector& core) +{ + Assert(options::unsatCores()) + << "cannot reduce unsat core if unsat cores are turned off"; + + Notice() << "SmtEngine::reduceUnsatCore(): reducing unsat core" << endl; + std::unordered_set removed; + for (const Node& skip : core) + { + std::unique_ptr 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 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. * @@ -367,6 +367,11 @@ class CVC5_EXPORT SmtEngine */ Result assertFormula(const Node& formula, bool inUnsatCore = true); + /** + * Reduce an unsatisfiable core to make it minimal. + */ + std::vector reduceUnsatCore(const std::vector& 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 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) -- 2.30.2