summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/minisat/core/Solver.cc46
-rw-r--r--src/prop/minisat/core/Solver.h7
-rw-r--r--src/prop/minisat/minisat.cpp36
-rw-r--r--src/prop/minisat/minisat.h10
-rw-r--r--src/prop/prop_engine.cpp54
-rw-r--r--src/prop/prop_engine.h13
6 files changed, 142 insertions, 24 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 40274489b..19f1bff97 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -484,8 +484,8 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
// If a literal is false at 0 level (both sat and user level) we also
// ignore it, unless we are tracking the SAT solver's reasoning
if (value(ps[i]) == l_False) {
- if (!options::unsatCores() && !isProofEnabled()
- && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0)
+ if (!options::unsatCores() && !needProof() && level(var(ps[i])) == 0
+ && user_level(var(ps[i])) == 0)
{
continue;
}
@@ -527,7 +527,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
// If all false, we're in conflict
if (ps.size() == falseLiteralsCount) {
- if (options::unsatCores() || isProofEnabled())
+ if (options::unsatCores() || needProof())
{
// Take care of false units here; otherwise, we need to
// construct the clause below to give to the proof manager
@@ -549,7 +549,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
ProofManager::getSatProof()->finalizeProof(
cvc5::Minisat::CRef_Lazy);
}
- if (isProofEnabled())
+ if (needProof())
{
d_pfManager->finalizeProof(ps[0], true);
}
@@ -574,7 +574,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
clauses_persistent.push(cr);
attachClause(cr);
- if (options::unsatCores() || isProofEnabled())
+ if (options::unsatCores() || needProof())
{
if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF)
{
@@ -596,7 +596,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
{
ProofManager::getSatProof()->finalizeProof(cr);
}
- if (isProofEnabled())
+ if (needProof())
{
d_pfManager->finalizeProof(ca[cr], true);
}
@@ -633,7 +633,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
// already been registered, as the ProofCnfStream will not register
// them and as they are not the result of propagation will be left
// hanging in assumptions accumulator
- if (isProofEnabled())
+ if (needProof())
{
d_pfManager->registerSatLitAssumption(ps[0]);
}
@@ -654,7 +654,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
ProofManager::getSatProof()->finalizeProof(confl);
}
}
- if (isProofEnabled())
+ if (needProof())
{
if (ca[confl].size() == 1)
{
@@ -755,7 +755,7 @@ void Solver::removeClause(CRef cr) {
// Solver::reason, if it appears in a resolution chain built lazily we
// will be unable to do so after the step below. Thus we eagerly justify
// this propagation here.
- if (isProofEnabled())
+ if (needProof())
{
Trace("pf::sat")
<< "Solver::removeClause: eagerly compute propagation of " << c[0]
@@ -1001,7 +1001,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
{
ProofManager::getSatProof()->startResChain(confl);
}
- if (isProofEnabled())
+ if (needProof())
{
d_pfManager->startResChain(ca[confl]);
}
@@ -1066,7 +1066,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
{
ProofManager::getSatProof()->resolveOutUnit(q);
}
- if (isProofEnabled())
+ if (needProof())
{
d_pfManager->addResolutionStep(q);
}
@@ -1088,7 +1088,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
{
ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p));
}
- if (isProofEnabled())
+ if (needProof())
{
d_pfManager->addResolutionStep(ca[confl], p);
}
@@ -1129,7 +1129,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
{
ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]);
}
- if (isProofEnabled())
+ if (needProof())
{
Debug("newproof::sat")
<< "Solver::analyze: redundant lit "
@@ -1677,7 +1677,7 @@ lbool Solver::search(int nof_conflicts)
{
ProofManager::getSatProof()->finalizeProof(confl);
}
- if (isProofEnabled())
+ if (needProof())
{
if (confl == CRef_Lazy)
{
@@ -1704,7 +1704,7 @@ lbool Solver::search(int nof_conflicts)
{
ProofManager::getSatProof()->endResChain(learnt_clause[0]);
}
- if (isProofEnabled())
+ if (needProof())
{
d_pfManager->endResChain(learnt_clause[0]);
}
@@ -1723,7 +1723,7 @@ lbool Solver::search(int nof_conflicts)
ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
ProofManager::getSatProof()->endResChain(id);
}
- if (isProofEnabled())
+ if (needProof())
{
d_pfManager->endResChain(ca[cr]);
}
@@ -2219,7 +2219,7 @@ CRef Solver::updateLemmas() {
// If it's an empty lemma, we have a conflict at zero level
if (lemma.size() == 0) {
- Assert(!options::unsatCores() && !isProofEnabled());
+ Assert(!options::unsatCores() && !needProof());
conflict = CRef_Lazy;
backtrackLevel = 0;
Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
@@ -2249,7 +2249,7 @@ CRef Solver::updateLemmas() {
// Last index in the trail
int backtrack_index = trail.size();
- Assert(!options::unsatCores() || isProofEnabled()
+ Assert(!options::unsatCores() || needProof()
|| lemmas.size() == (int)lemmas_cnf_assertion.size());
// Attach all the clauses and enqueue all the propagations
@@ -2320,7 +2320,7 @@ CRef Solver::updateLemmas() {
{
ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT);
}
- if (isProofEnabled())
+ if (needProof())
{
d_pfManager->storeUnitConflict(lemma[0]);
}
@@ -2334,7 +2334,7 @@ CRef Solver::updateLemmas() {
}
}
- Assert(!options::unsatCores() || isProofEnabled()
+ Assert(!options::unsatCores() || needProof()
|| lemmas.size() == (int)lemmas_cnf_assertion.size());
// Clear the lemmas
lemmas.clear();
@@ -2400,5 +2400,11 @@ std::shared_ptr<ProofNode> Solver::getProof()
bool Solver::isProofEnabled() const { return d_pfManager != nullptr; }
+bool Solver::needProof() const
+{
+ return isProofEnabled()
+ && options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS;
+}
+
} // namespace Minisat
} // namespace cvc5
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index cd3f38c9e..a9ee25c11 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -160,6 +160,13 @@ public:
/** Is proof enabled? */
bool isProofEnabled() const;
+ /**
+ * Checks whether we need a proof.
+ *
+ * SAT proofs are not required for assumption-based unsat cores.
+ */
+ bool needProof() const;
+
// Less than for literals in a lemma
struct lemma_lt
{
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 813292a21..611416dbc 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -32,7 +32,7 @@ namespace prop {
//// DPllMinisatSatSolver
MinisatSatSolver::MinisatSatSolver(StatisticsRegistry& registry)
- : d_minisat(NULL), d_context(NULL), d_statistics(registry)
+ : d_minisat(NULL), d_context(NULL), d_assumptions(), d_statistics(registry)
{}
MinisatSatSolver::~MinisatSatSolver()
@@ -193,6 +193,40 @@ SatValue MinisatSatSolver::solve() {
return result;
}
+SatValue MinisatSatSolver::solve(const std::vector<SatLiteral>& assumptions)
+{
+ setupOptions();
+ d_minisat->budgetOff();
+
+ d_assumptions.clear();
+ Minisat::vec<Minisat::Lit> assumps;
+
+ for (const SatLiteral& lit : assumptions)
+ {
+ Minisat::Lit mlit = toMinisatLit(lit);
+ assumps.push(mlit);
+ d_assumptions.emplace(lit);
+ }
+
+ SatValue result = toSatLiteralValue(d_minisat->solve(assumps));
+ d_minisat->clearInterrupt();
+ return result;
+}
+
+void MinisatSatSolver::getUnsatAssumptions(
+ std::vector<SatLiteral>& unsat_assumptions)
+{
+ for (size_t i = 0, size = d_minisat->d_conflict.size(); i < size; ++i)
+ {
+ Minisat::Lit mlit = d_minisat->d_conflict[i];
+ SatLiteral lit = ~toSatLiteral(mlit);
+ if (d_assumptions.find(lit) != d_assumptions.end())
+ {
+ unsat_assumptions.push_back(lit);
+ }
+ }
+}
+
bool MinisatSatSolver::ok() const {
return d_minisat->okay();
}
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 42588080d..74b7ab749 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -58,6 +58,8 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
SatValue solve() override;
SatValue solve(long unsigned int&) override;
+ SatValue solve(const std::vector<SatLiteral>& assumptions) override;
+ void getUnsatAssumptions(std::vector<SatLiteral>& unsat_assumptions) override;
bool ok() const override;
@@ -100,6 +102,14 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
/** Context we will be using to synchronize the sat solver */
context::Context* d_context;
+ /**
+ * Stores assumptions passed via last solve() call.
+ *
+ * It is used in getUnsatAssumptions() to determine which of the literals in
+ * the final conflict clause are assumptions.
+ */
+ std::unordered_set<SatLiteral, SatLiteralHashFunction> d_assumptions;
+
void setupOptions();
class Statistics {
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c4d929d35..23377cb0c 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -82,7 +82,8 @@ PropEngine::PropEngine(TheoryEngine* te,
d_ppm(nullptr),
d_interrupted(false),
d_resourceManager(rm),
- d_outMgr(outMgr)
+ d_outMgr(outMgr),
+ d_assumptions(userContext)
{
Debug("prop") << "Constructing the PropEngine" << std::endl;
@@ -262,7 +263,18 @@ void PropEngine::assertInternal(
// Assert as (possibly) removable
if (isProofEnabled())
{
- d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
+ if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS
+ && input)
+ {
+ Assert(!negated);
+ d_pfCnfStream->ensureLiteral(node);
+ d_assumptions.push_back(node);
+ }
+ else
+ {
+ d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
+ }
+
// if input, register the assertion
if (input)
{
@@ -274,6 +286,7 @@ void PropEngine::assertInternal(
d_cnfStream->convertAndAssert(node, removable, negated, input);
}
}
+
void PropEngine::assertLemmasInternal(
theory::TrustNode trn,
const std::vector<theory::TrustNode>& ppLemmas,
@@ -358,7 +371,20 @@ Result PropEngine::checkSat() {
d_interrupted = false;
// Check the problem
- SatValue result = d_satSolver->solve();
+ SatValue result;
+ if (d_assumptions.size() == 0)
+ {
+ result = d_satSolver->solve();
+ }
+ else
+ {
+ std::vector<SatLiteral> assumptions;
+ for (const Node& node : d_assumptions)
+ {
+ assumptions.push_back(d_cnfStream->getLiteral(node));
+ }
+ result = d_satSolver->solve(assumptions);
+ }
if( result == SAT_VALUE_UNKNOWN ) {
@@ -628,5 +654,27 @@ std::shared_ptr<ProofNode> PropEngine::getProof()
bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; }
+void PropEngine::getUnsatCore(std::vector<Node>& core)
+{
+ Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS);
+ std::vector<SatLiteral> unsat_assumptions;
+ d_satSolver->getUnsatAssumptions(unsat_assumptions);
+ for (const SatLiteral& lit : unsat_assumptions)
+ {
+ core.push_back(d_cnfStream->getNode(lit));
+ }
+}
+
+std::shared_ptr<ProofNode> PropEngine::getRefutation()
+{
+ Assert(options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS);
+ std::vector<Node> core;
+ getUnsatCore(core);
+ CDProof cdp(d_pnm);
+ Node fnode = NodeManager::currentNM()->mkConst(false);
+ cdp.addStep(fnode, PfRule::SAT_REFUTATION, core, {});
+ return cdp.getProofFor(fnode);
+}
+
} // namespace prop
} // namespace cvc5
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index a0496a525..6812a6549 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -286,6 +286,13 @@ class PropEngine
/** Is proof enabled? */
bool isProofEnabled() const;
+
+ /** Retrieve unsat core from SAT solver for assumption-based unsat cores. */
+ void getUnsatCore(std::vector<Node>& core);
+
+ /** Return the prop engine proof for assumption-based unsat cores. */
+ std::shared_ptr<ProofNode> getRefutation();
+
private:
/** Dump out the satisfying assignment (after SAT result) */
void printSatisfyingAssignment();
@@ -370,6 +377,12 @@ class PropEngine
/** Reference to the output manager of the smt engine */
OutputManager& d_outMgr;
+
+ /**
+ * Stores assumptions added via assertInternal() if assumption-based unsat
+ * cores are enabled.
+ */
+ context::CDList<Node> d_assumptions;
};
} // namespace prop
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback