diff options
-rw-r--r-- | src/expr/proof_rule.h | 8 | ||||
-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 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 16 | ||||
-rw-r--r-- | src/theory/booleans/proof_checker.cpp | 6 |
9 files changed, 169 insertions, 27 deletions
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 88e344b8a..432ff1f89 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -247,6 +247,14 @@ enum class PfRule : uint32_t // where F is an equality (= t t') that holds by a form of substitution that // could not be determined by the TrustSubstitutionMap. TRUST_SUBS_MAP, + // ========= SAT Refutation for assumption-based unsat cores + // Children: (P1, ..., Pn) + // Arguments: none + // --------------------- + // Conclusion: false + // Note: P1, ..., Pn correspond to the unsat core determined by the SAT + // solver. + SAT_REFUTATION, //================================================= Boolean rules // ======== Resolution 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8e8a1e062..09b3d64ab 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1419,9 +1419,19 @@ UnsatCore SmtEngine::getUnsatCoreInternal() // generate with new proofs PropEngine* pe = getPropEngine(); Assert(pe != nullptr); - Assert(pe->getProof() != nullptr); - std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof( - pe->getProof(), *d_asserts, *d_definedFunctions); + + std::shared_ptr<ProofNode> pepf; + if (options::unsatCoresMode() == options::UnsatCoresMode::ASSUMPTIONS) + { + pepf = pe->getRefutation(); + } + else + { + pepf = pe->getProof(); + } + Assert(pepf != nullptr); + std::shared_ptr<ProofNode> pfn = + d_pfManager->getFinalProof(pepf, *d_asserts, *d_definedFunctions); std::vector<Node> core; d_ucManager->getUnsatCore(pfn, *d_asserts, core); return UnsatCore(core); diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 256ccedce..8b2967fe6 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -74,6 +74,7 @@ void BoolProofRuleChecker::registerTo(ProofChecker* pc) pc->registerChecker(PfRule::CNF_ITE_NEG1, this); pc->registerChecker(PfRule::CNF_ITE_NEG2, this); pc->registerChecker(PfRule::CNF_ITE_NEG3, this); + pc->registerTrustedChecker(PfRule::SAT_REFUTATION, this, 1); } Node BoolProofRuleChecker::checkInternal(PfRule id, @@ -950,6 +951,11 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, args[0], args[0][1].notNode(), args[0][2].notNode()}; return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); } + if (id == PfRule::SAT_REFUTATION) + { + Assert(args.empty()); + return NodeManager::currentNM()->mkConst(false); + } // no rule return Node::null(); } |