diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 46 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 7 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 36 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 10 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 54 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 13 |
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 |