summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/set_defaults.cpp14
-rw-r--r--src/smt/smt_engine.cpp79
-rw-r--r--src/smt/smt_engine.h7
-rw-r--r--src/smt/unsat_core_manager.cpp5
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)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback