diff options
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/set_defaults.cpp | 14 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 79 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 7 | ||||
-rw-r--r-- | src/smt/unsat_core_manager.cpp | 5 |
4 files changed, 99 insertions, 6 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index bb104e98d..e12d3eb1d 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; @@ -968,6 +968,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) Trace("smt") << "setting decision mode to " << opts.decision.decisionMode << std::endl; } + + // set up of central equality engine + if (opts.arith.arithEqSolver) + { + if (!opts.arith.arithCongManWasSetByUser) + { + // if we are using the arithmetic equality solver, do not use the + // arithmetic congruence manager by default + opts.arith.arithCongMan = false; + } + } + if (options::incrementalSolving()) { // disable modes not supported by incremental 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") { 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/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index ba2c07326..22304f9e8 100644 --- a/src/smt/unsat_core_manager.cpp +++ b/src/smt/unsat_core_manager.cpp @@ -80,7 +80,10 @@ void UnsatCoreManager::getRelevantInstantiations( const std::vector<Node>& instTerms = cur->getArguments(); Assert(cs.size() == 1); Node q = cs[0]->getResult(); - insts[q].push_back({instTerms.begin(), instTerms.end()}); + // the instantiation is a prefix of the arguments up to the number of + // variables + insts[q].push_back( + {instTerms.begin(), instTerms.begin() + q[0].getNumChildren()}); } for (const std::shared_ptr<ProofNode>& cp : cs) { |