From b8a5b453e3a4f6d2ae15ac727358540b191c186e Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 16 Dec 2021 17:04:31 -0300 Subject: [PATCH] [proofs] Simplifying and adding new utils to SAT proof manager and Proof Cnf Stream (#7826) These will be necessary for upcoming changes to the SAT proof manager and Proof Cnf Stream to handle incremental proofs when optimizing the level of SAT clauses. --- src/prop/proof_cnf_stream.cpp | 47 ++++++++++++++++++++++++++-------- src/prop/proof_cnf_stream.h | 13 +++++++++- src/prop/sat_proof_manager.cpp | 33 ++++++++---------------- src/prop/sat_proof_manager.h | 3 --- 4 files changed, 60 insertions(+), 36 deletions(-) diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp index b5542ab35..8aaa68b9a 100644 --- a/src/prop/proof_cnf_stream.cpp +++ b/src/prop/proof_cnf_stream.cpp @@ -20,8 +20,6 @@ #include "theory/builtin/proof_checker.h" #include "util/rational.h" -using namespace cvc5::kind; - namespace cvc5 { namespace prop { @@ -58,7 +56,7 @@ bool ProofCnfStream::hasProofFor(Node f) std::string ProofCnfStream::identify() const { return "ProofCnfStream"; } -void ProofCnfStream::normalizeAndRegister(TNode clauseNode) +Node ProofCnfStream::normalizeAndRegister(TNode clauseNode) { Node normClauseNode = d_psb.factorReorderElimDoubleNeg(clauseNode); if (Trace.isOn("cnf") && normClauseNode != clauseNode) @@ -69,6 +67,7 @@ void ProofCnfStream::normalizeAndRegister(TNode clauseNode) << pop; } d_satPM->registerSatAssumptions({normClauseNode}); + return normClauseNode; } void ProofCnfStream::convertAndAssert(TNode node, @@ -104,7 +103,8 @@ void ProofCnfStream::convertAndAssert(TNode node, void ProofCnfStream::convertAndAssert(TNode node, bool negated) { Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node - << ", negated = " << (negated ? "true" : "false") << ")\n"; + << ", negated = " << (negated ? "true" : "false") << ")\n" + << push; switch (node.getKind()) { case kind::AND: convertAndAssertAnd(node, negated); break; @@ -159,12 +159,14 @@ void ProofCnfStream::convertAndAssert(TNode node, bool negated) } } } + Trace("cnf") << pop; } void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated) { Trace("cnf") << "ProofCnfStream::convertAndAssertAnd(" << node - << ", negated = " << (negated ? "true" : "false") << ")\n"; + << ", negated = " << (negated ? "true" : "false") << ")\n" + << push; Assert(node.getKind() == kind::AND); if (!negated) { @@ -205,12 +207,14 @@ void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated) normalizeAndRegister(clauseNode); } } + Trace("cnf") << pop; } void ProofCnfStream::convertAndAssertOr(TNode node, bool negated) { Trace("cnf") << "ProofCnfStream::convertAndAssertOr(" << node - << ", negated = " << (negated ? "true" : "false") << ")\n"; + << ", negated = " << (negated ? "true" : "false") << ")\n" + << push; Assert(node.getKind() == kind::OR); if (!negated) { @@ -240,12 +244,14 @@ void ProofCnfStream::convertAndAssertOr(TNode node, bool negated) convertAndAssert(node[i], true); } } + Trace("cnf") << pop; } void ProofCnfStream::convertAndAssertXor(TNode node, bool negated) { Trace("cnf") << "ProofCnfStream::convertAndAssertXor(" << node - << ", negated = " << (negated ? "true" : "false") << ")\n"; + << ", negated = " << (negated ? "true" : "false") << ")\n" + << push; if (!negated) { // p XOR q @@ -317,12 +323,14 @@ void ProofCnfStream::convertAndAssertXor(TNode node, bool negated) normalizeAndRegister(clauseNode); } } + Trace("cnf") << pop; } void ProofCnfStream::convertAndAssertIff(TNode node, bool negated) { Trace("cnf") << "ProofCnfStream::convertAndAssertIff(" << node - << ", negated = " << (negated ? "true" : "false") << ")\n"; + << ", negated = " << (negated ? "true" : "false") << ")\n" + << push; if (!negated) { // p <=> q @@ -400,12 +408,14 @@ void ProofCnfStream::convertAndAssertIff(TNode node, bool negated) normalizeAndRegister(clauseNode); } } + Trace("cnf") << pop; } void ProofCnfStream::convertAndAssertImplies(TNode node, bool negated) { Trace("cnf") << "ProofCnfStream::convertAndAssertImplies(" << node - << ", negated = " << (negated ? "true" : "false") << ")\n"; + << ", negated = " << (negated ? "true" : "false") << ")\n" + << push; if (!negated) { // ~p v q @@ -444,12 +454,14 @@ void ProofCnfStream::convertAndAssertImplies(TNode node, bool negated) << "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM2 added " << node[1].notNode() << "\n"; } + Trace("cnf") << pop; } void ProofCnfStream::convertAndAssertIte(TNode node, bool negated) { Trace("cnf") << "ProofCnfStream::convertAndAssertIte(" << node - << ", negated = " << (negated ? "true" : "false") << ")\n"; + << ", negated = " << (negated ? "true" : "false") << ")\n" + << push; // ITE(p, q, r) SatLiteral p = toCNF(node[0], false); SatLiteral q = toCNF(node[1], negated); @@ -515,6 +527,7 @@ void ProofCnfStream::convertAndAssertIte(TNode node, bool negated) normalizeAndRegister(clauseNode); } } + Trace("cnf") << pop; } void ProofCnfStream::convertPropagation(TrustNode trn) @@ -590,6 +603,20 @@ void ProofCnfStream::convertPropagation(TrustNode trn) } } + +Node ProofCnfStream::getClauseNode(const SatClause& clause) +{ + std::vector clauseNodes; + for (size_t i = 0, size = clause.size(); i < size; ++i) + { + SatLiteral satLit = clause[i]; + clauseNodes.push_back(d_cnfStream.getNode(satLit)); + } + // order children by node id + std::sort(clauseNodes.begin(), clauseNodes.end()); + return NodeManager::currentNM()->mkNode(kind::OR, clauseNodes); +} + void ProofCnfStream::ensureLiteral(TNode n) { Trace("cnf") << "ProofCnfStream::ensureLiteral(" << n << ")\n"; diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h index af131c2c3..b79b3098f 100644 --- a/src/prop/proof_cnf_stream.h +++ b/src/prop/proof_cnf_stream.h @@ -148,8 +148,19 @@ class ProofCnfStream : public ProofGenerator * resulting clauses of the clausification process are synchronized with the * clauses used in the underlying SAT solver, which automatically performs the * above normalizations on all added clauses. + * + * @param clauseNode The clause node to be normalized. + * @return The normalized clause node. + */ + Node normalizeAndRegister(TNode clauseNode); + + /** Gets node equivalent to SAT clause. + * + * To avoid generating different nodes for the same clause, modulo ordering, + * an invariant assumed throughout this class, the OR node generated by this + * method always has its children ordered. */ - void normalizeAndRegister(TNode clauseNode); + Node getClauseNode(const SatClause& clause); /** Reference to the underlying cnf stream. */ CnfStream& d_cnfStream; diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index fb37b1d01..fd57fb13c 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -42,33 +42,20 @@ SatProofManager::SatProofManager(Minisat::Solver* solver, void SatProofManager::printClause(const Minisat::Clause& clause) { - for (unsigned i = 0, size = clause.size(); i < size; ++i) + for (size_t i = 0, size = clause.size(); i < size; ++i) { SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]); Trace("sat-proof") << satLit << " "; } } -Node SatProofManager::getClauseNode(SatLiteral satLit) -{ - Assert(d_cnfStream->getNodeCache().find(satLit) - != d_cnfStream->getNodeCache().end()) - << "SatProofManager::getClauseNode: literal " << satLit - << " undefined.\n"; - return d_cnfStream->getNodeCache()[satLit]; -} - Node SatProofManager::getClauseNode(const Minisat::Clause& clause) { std::vector clauseNodes; - for (unsigned i = 0, size = clause.size(); i < size; ++i) + for (size_t i = 0, size = clause.size(); i < size; ++i) { SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]); - Assert(d_cnfStream->getNodeCache().find(satLit) - != d_cnfStream->getNodeCache().end()) - << "SatProofManager::getClauseNode: literal " << satLit - << " undefined\n"; - clauseNodes.push_back(d_cnfStream->getNodeCache()[satLit]); + clauseNodes.push_back(d_cnfStream->getNode(satLit)); } // order children by node id std::sort(clauseNodes.begin(), clauseNodes.end()); @@ -140,7 +127,7 @@ void SatProofManager::endResChain(Minisat::Lit lit) SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit); Trace("sat-proof") << "SatProofManager::endResChain: chain_res for " << satLit; - endResChain(getClauseNode(satLit), {satLit}); + endResChain(d_cnfStream->getNode(satLit), {satLit}); } void SatProofManager::endResChain(const Minisat::Clause& clause) @@ -346,7 +333,7 @@ void SatProofManager::explainLit(SatLiteral lit, std::unordered_set& premises) { Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit; - Node litNode = getClauseNode(lit); + Node litNode = d_cnfStream->getNode(lit); Trace("sat-proof") << " [" << litNode << "]\n"; // We don't need to explain nodes who are inputs. Note that it's *necessary* // to avoid attempting such explanations because they can introduce cycles at @@ -723,7 +710,7 @@ void SatProofManager::finalizeProof() Trace("sat-proof") << "SatProofManager::finalizeProof: conflicting (lazy) satLit: " << d_conflictLit << "\n"; - finalizeProof(getClauseNode(d_conflictLit), {d_conflictLit}); + finalizeProof(d_cnfStream->getNode(d_conflictLit), {d_conflictLit}); // reset since if in incremental mode this may be used again d_conflictLit = undefSatVariable; } @@ -733,7 +720,7 @@ void SatProofManager::finalizeProof(Minisat::Lit inConflict, bool adding) SatLiteral satLit = MinisatSatSolver::toSatLiteral(inConflict); Trace("sat-proof") << "SatProofManager::finalizeProof: conflicting satLit: " << satLit << "\n"; - Node clauseNode = getClauseNode(satLit); + Node clauseNode = d_cnfStream->getNode(satLit); if (adding) { registerSatAssumptions({clauseNode}); @@ -777,9 +764,11 @@ std::shared_ptr SatProofManager::getProof() void SatProofManager::registerSatLitAssumption(Minisat::Lit lit) { Trace("sat-proof") << "SatProofManager::registerSatLitAssumption: - " - << getClauseNode(MinisatSatSolver::toSatLiteral(lit)) + << d_cnfStream->getNode( + MinisatSatSolver::toSatLiteral(lit)) << "\n"; - d_assumptions.insert(getClauseNode(MinisatSatSolver::toSatLiteral(lit))); + d_assumptions.insert( + d_cnfStream->getNode(MinisatSatSolver::toSatLiteral(lit))); } void SatProofManager::registerSatAssumptions(const std::vector& assumps) diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index a224f3a28..98d125591 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -568,14 +568,11 @@ class SatProofManager /** All clauses added to the SAT solver, kept in a context-dependent manner. */ context::CDHashSet d_assumptions; - /** * A placeholder that may be used to store the literal with the final * conflict. */ SatLiteral d_conflictLit; - /** Gets node equivalent to literal */ - Node getClauseNode(SatLiteral satLit); /** Gets node equivalent to clause. * * To avoid generating different nodes for the same clause, modulo ordering, -- 2.30.2