diff options
| -rw-r--r-- | src/prop/sat_proof_manager.cpp | 177 | ||||
| -rw-r--r-- | src/prop/sat_proof_manager.h | 16 | ||||
| -rw-r--r-- | src/theory/booleans/proof_checker.cpp | 2 |
3 files changed, 105 insertions, 90 deletions
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 985763c84..aae11ae51 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -81,20 +81,26 @@ void SatProofManager::startResChain(const Minisat::Clause& start) printClause(start); Trace("sat-proof") << "\n"; } - d_resLinks.push_back( - std::pair<Node, Node>(getClauseNode(start), Node::null())); + d_resLinks.emplace_back(getClauseNode(start), Node::null(), true); } void SatProofManager::addResolutionStep(Minisat::Lit lit, bool redundant) { SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit); + Node litNode = d_cnfStream->getNodeCache()[satLit]; + bool negated = satLit.isNegated(); + Assert(!negated || litNode.getKind() == kind::NOT); if (!redundant) { - Trace("sat-proof") << "SatProofManager::addResolutionStep: [" << satLit - << "] " << ~satLit << "\n"; - d_resLinks.push_back( - std::pair<Node, Node>(d_cnfStream->getNodeCache()[~satLit], - d_cnfStream->getNodeCache()[satLit])); + Trace("sat-proof") << "SatProofManager::addResolutionStep: {" + << satLit.isNegated() << "} [" << satLit << "] " + << ~satLit << "\n"; + // if lit is negated then the chain resolution construction will use it as a + // pivot occurring as is in the second clause and the node under the + // negation in the first clause + d_resLinks.emplace_back(d_cnfStream->getNodeCache()[~satLit], + negated ? litNode[0] : litNode, + !satLit.isNegated()); } else { @@ -107,17 +113,20 @@ void SatProofManager::addResolutionStep(Minisat::Lit lit, bool redundant) void SatProofManager::addResolutionStep(const Minisat::Clause& clause, Minisat::Lit lit) { - // the given clause is supposed to be the second in a resolution, with the - // given literal as the pivot occurring positive in the first and negatively - // in the second clause. Thus, we store its negation - SatLiteral satLit = MinisatSatSolver::toSatLiteral(~lit); + SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit); + Node litNode = d_cnfStream->getNodeCache()[satLit]; + bool negated = satLit.isNegated(); + Assert(!negated || litNode.getKind() == kind::NOT); Node clauseNode = getClauseNode(clause); - d_resLinks.push_back( - std::pair<Node, Node>(clauseNode, d_cnfStream->getNodeCache()[satLit])); + // if lit is negative then the chain resolution construction will use it as a + // pivot occurring as is in the second clause and the node under the + // negation in the first clause, which means that the third argument of the + // tuple must be false + d_resLinks.emplace_back(clauseNode, negated ? litNode[0] : litNode, negated); if (Trace.isOn("sat-proof")) { - Trace("sat-proof") << "SatProofManager::addResolutionStep: [" << satLit - << "] "; + Trace("sat-proof") << "SatProofManager::addResolutionStep: {" + << satLit.isNegated() << "} [" << ~satLit << "] "; printClause(clause); Trace("sat-proof") << "\nSatProofManager::addResolutionStep:\t" << clauseNode << "\n"; @@ -160,31 +169,32 @@ void SatProofManager::endResChain(Node conclusion, } d_redundantLits.clear(); // build resolution chain - std::vector<Node> children, args; + NodeManager* nm = NodeManager::currentNM(); + // the conclusion is stored already in the arguments because of the + // possibility of reordering + std::vector<Node> children, args{conclusion}; for (unsigned i = 0, size = d_resLinks.size(); i < size; ++i) { - children.push_back(d_resLinks[i].first); + Node clause, pivot; + bool posFirst; + std::tie(clause, pivot, posFirst) = d_resLinks[i]; + children.push_back(clause); Trace("sat-proof") << "SatProofManager::endResChain: "; if (i > 0) { - Trace("sat-proof") - << "[" << d_cnfStream->getTranslationCache()[d_resLinks[i].second] - << "] "; + Trace("sat-proof") << "{" << posFirst << "} [" + << d_cnfStream->getTranslationCache()[pivot] << "] "; } // special case for clause (or l1 ... ln) being a single literal // corresponding itself to a clause, which is indicated by the pivot being // of the form (not (or l1 ... ln)) - if (d_resLinks[i].first.getKind() == kind::OR - && !(d_resLinks[i].second.getKind() == kind::NOT - && d_resLinks[i].second[0].getKind() == kind::OR - && d_resLinks[i].second[0] == d_resLinks[i].first)) + if (clause.getKind() == kind::OR + && !(pivot.getKind() == kind::NOT && pivot[0].getKind() == kind::OR + && pivot[0] == clause)) { - for (unsigned j = 0, sizeJ = d_resLinks[i].first.getNumChildren(); - j < sizeJ; - ++j) + for (unsigned j = 0, sizeJ = clause.getNumChildren(); j < sizeJ; ++j) { - Trace("sat-proof") - << d_cnfStream->getTranslationCache()[d_resLinks[i].first[j]]; + Trace("sat-proof") << d_cnfStream->getTranslationCache()[clause[j]]; if (j < sizeJ - 1) { Trace("sat-proof") << ", "; @@ -193,21 +203,20 @@ void SatProofManager::endResChain(Node conclusion, } else { - Assert(d_cnfStream->getTranslationCache().find(d_resLinks[i].first) + Assert(d_cnfStream->getTranslationCache().find(clause) != d_cnfStream->getTranslationCache().end()) - << "clause node " << d_resLinks[i].first - << " treated as unit has no literal. Pivot is " - << d_resLinks[i].second << "\n"; - Trace("sat-proof") - << d_cnfStream->getTranslationCache()[d_resLinks[i].first]; + << "clause node " << clause + << " treated as unit has no literal. Pivot is " << pivot << "\n"; + Trace("sat-proof") << d_cnfStream->getTranslationCache()[clause]; } Trace("sat-proof") << " : "; if (i > 0) { - args.push_back(d_resLinks[i].second); - Trace("sat-proof") << "[" << d_resLinks[i].second << "] "; + args.push_back(nm->mkConst(posFirst)); + args.push_back(pivot); + Trace("sat-proof") << "{" << posFirst << "} [" << pivot << "] "; } - Trace("sat-proof") << d_resLinks[i].first << "\n"; + Trace("sat-proof") << clause << "\n"; } // clearing d_resLinks.clear(); @@ -225,40 +234,15 @@ void SatProofManager::endResChain(Node conclusion, << conclusion << "\n"; } // since the conclusion can be both reordered and without duplicates and the - // SAT solver does not record this information, we must recompute it here so - // the proper CHAIN_RESOLUTION step can be created - // compute chain resolution conclusion - Node chainConclusion = d_pnm->getChecker()->checkDebug( - PfRule::CHAIN_RESOLUTION, children, args, Node::null(), ""); - Trace("sat-proof") - << "SatProofManager::endResChain: creating step for computed conclusion " - << chainConclusion << "\n"; - // buffer steps - theory::TheoryProofStepBuffer psb; - psb.addStep(PfRule::CHAIN_RESOLUTION, children, args, chainConclusion); - if (chainConclusion != conclusion) - { - // if this happens that chainConclusion needs to be factored and/or - // reordered, which in either case can be done only if it's not a unit - // clause. - CVC4_UNUSED Node reducedChainConclusion = - psb.factorReorderElimDoubleNeg(chainConclusion); - Assert(reducedChainConclusion == conclusion) - << "original conclusion " << conclusion - << "\nis different from computed conclusion " << chainConclusion - << "\nafter factorReorderElimDoubleNeg " << reducedChainConclusion; - } - // buffer the steps in the resolution chain proof generator - const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps(); - for (const std::pair<Node, ProofStep>& step : steps) - { - Trace("sat-proof") << "SatProofManager::endResChain: adding for " - << step.first << " step " << step.second << "\n"; - d_resChainPg.addStep(step.first, step.second); - // the premises of this resolution may not have been justified yet, so we do - // not pass assumptions to check closedness - d_resChains.addLazyStep(step.first, &d_resChainPg); - } + // SAT solver does not record this information, we use a MACRO_RESOLUTION + // step, which bypasses these. Note that we could generate a chain resolution + // rule here by explicitly computing the detailed steps, but leave this for + // post-processing. + ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); + d_resChainPg.addStep(conclusion, ps); + // the premises of this resolution may not have been justified yet, so we do + // not pass assumptions to check closedness + d_resChains.addLazyStep(conclusion, &d_resChainPg); } void SatProofManager::processRedundantLit( @@ -283,9 +267,14 @@ void SatProofManager::processRedundantLit( << "\n" << pop; visited.insert(lit); - d_resLinks.insert(d_resLinks.begin() + pos, - std::pair<Node, Node>(d_cnfStream->getNodeCache()[~lit], - d_cnfStream->getNodeCache()[lit])); + Node litNode = d_cnfStream->getNodeCache()[lit]; + bool negated = lit.isNegated(); + Assert(!negated || litNode.getKind() == kind::NOT); + + d_resLinks.emplace(d_resLinks.begin() + pos, + d_cnfStream->getNodeCache()[~lit], + negated ? litNode[0] : litNode, + !negated); return; } Assert(reasonRef >= 0 && reasonRef < d_solver->ca.size()) @@ -319,9 +308,13 @@ void SatProofManager::processRedundantLit( // assumption that the redundant literal is removed via the resolution with // the explanation of its negation Node clauseNode = getClauseNode(reason); - d_resLinks.insert( - d_resLinks.begin() + pos, - std::pair<Node, Node>(clauseNode, d_cnfStream->getNodeCache()[lit])); + Node litNode = d_cnfStream->getNodeCache()[lit]; + bool negated = lit.isNegated(); + Assert(!negated || litNode.getKind() == kind::NOT); + d_resLinks.emplace(d_resLinks.begin() + pos, + clauseNode, + negated ? litNode[0] : litNode, + !negated); } void SatProofManager::explainLit( @@ -359,6 +352,7 @@ void SatProofManager::explainLit( std::vector<Node> children{getClauseNode(reason)}, args; // save in the premises premises.insert(children.back()); + NodeManager* nm = NodeManager::currentNM(); Trace("sat-proof") << push; for (unsigned i = 0; i < size; ++i) { @@ -374,7 +368,14 @@ void SatProofManager::explainLit( Assert(d_cnfStream->getNodeCache().find(curr_lit) != d_cnfStream->getNodeCache().end()); children.push_back(d_cnfStream->getNodeCache()[~curr_lit]); - args.push_back(d_cnfStream->getNodeCache()[curr_lit]); + Node currLitNode = d_cnfStream->getNodeCache()[curr_lit]; + bool negated = curr_lit.isNegated(); + Assert(!negated || currLitNode.getKind() == kind::NOT); + // note this is the opposite of what is done in addResolutionStep. This is + // because here the clause, which contains the literal being analyzed, is + // the first clause rather than the second + args.push_back(nm->mkConst(!negated)); + args.push_back(negated ? currLitNode[0] : currLitNode); // add child premises and the child itself premises.insert(childPremises.begin(), childPremises.end()); premises.insert(d_cnfStream->getNodeCache()[~curr_lit]); @@ -404,7 +405,8 @@ void SatProofManager::explainLit( } Trace("sat-proof") << pop; // create step - ProofStep ps(PfRule::CHAIN_RESOLUTION, children, args); + args.insert(args.begin(), litNode); + ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); d_resChainPg.addStep(litNode, ps); // the premises in the limit of the justification may correspond to other // links in the chain which have, themselves, literals yet to be justified. So @@ -465,7 +467,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, // get resolution Node cur = link.first; std::shared_ptr<ProofNode> pfn = link.second; - while (pfn->getRule() != PfRule::CHAIN_RESOLUTION) + while (pfn->getRule() != PfRule::MACRO_RESOLUTION) { Assert(pfn->getChildren().size() == 1 && pfn->getChildren()[0]->getRule() == PfRule::ASSUME) @@ -514,6 +516,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, // arguments for the resolution step to conclude false. std::vector<Node> children{inConflictNode}, args; std::unordered_set<TNode, TNodeHashFunction> premises; + NodeManager* nm = NodeManager::currentNM(); for (unsigned i = 0, size = inConflict.size(); i < size; ++i) { Assert(d_cnfStream->getNodeCache().find(inConflict[i]) @@ -523,7 +526,14 @@ void SatProofManager::finalizeProof(Node inConflictNode, Node negatedLitNode = d_cnfStream->getNodeCache()[~inConflict[i]]; // save to resolution chain premises / arguments children.push_back(negatedLitNode); - args.push_back(d_cnfStream->getNodeCache()[inConflict[i]]); + Node litNode = d_cnfStream->getNodeCache()[inConflict[i]]; + bool negated = inConflict[i].isNegated(); + Assert(!negated || litNode.getKind() == kind::NOT); + // note this is the opposite of what is done in addResolutionStep. This is + // because here the clause, which contains the literal being analyzed, is + // the first clause rather than the second + args.push_back(nm->mkConst(!negated)); + args.push_back(negated ? litNode[0] : litNode); // add child premises and the child itself premises.insert(childPremises.begin(), childPremises.end()); premises.insert(negatedLitNode); @@ -544,7 +554,8 @@ void SatProofManager::finalizeProof(Node inConflictNode, } } // create step - ProofStep ps(PfRule::CHAIN_RESOLUTION, children, args); + args.insert(args.begin(), d_false); + ProofStep ps(PfRule::MACRO_RESOLUTION, children, args); d_resChainPg.addStep(d_false, ps); // not yet ready to check closedness because maybe only now we will justify // literals used in resolutions diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 79dc09549..9dd162e48 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -296,7 +296,8 @@ class SatProofManager * level, and the literal, at the node level, as the pivot. * * @param clause the clause being resolved against - * @param lit the pivot of the resolution step + * @param lit the literal occurring in clause to be the pivot of the + * resolution step */ void addResolutionStep(const Minisat::Clause& clause, Minisat::Lit lit); /** Adds a resolution step with a unit clause @@ -529,13 +530,16 @@ class SatProofManager ProofNodeManager* d_pnm; /** Resolution steps (links) accumulator for chain resolution. * - * Each pair has a clause and the pivot for the resolution step it is involved - * on. The pivot occurs positively in the clause yielded by the resolution up - * to the previous link and negatively in this link. The first link has a null - * pivot. Links are kept at the node level. + * Each tuple has a clause and the pivot for the resolution step it is + * involved on, as well as whether the pivot occurs positively/negatively or + * negatively/positively in the clauses being resolved. If the third argument + * is true (resp. false), the pivot occurs positively (negatively) in the + * clause yielded by the resolution up to the previous link and negatively + * (positively) in this link. The first link has a null pivot. Links are kept + * at the node level. * * This accumulator is reset after each chain resolution. */ - std::vector<std::pair<Node, Node>> d_resLinks; + std::vector<std::tuple<Node, Node, bool>> d_resLinks; /** Redundant literals removed from the resolution chain's conclusion. * diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 2cbf6a2e8..83662a50f 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -353,7 +353,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, // child is in lhsElim or is equal to rhsElim (which means that the // negation of the child is in lhsElim). std::vector<Node> lits; - if (children[i].getKind() == kind::OR && elim.count(children[i]) == 0) + if (children[i].getKind() == kind::OR && !elim.count(children[i])) { lits.insert(lits.end(), children[i].begin(), children[i].end()); } |