From 52cecd9300327e7680228279acb19ec5224441b7 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 20 Aug 2024 14:53:53 -0300 Subject: [PATCH] [proof checker] Fixes for MACRO_RESOLUTION (#11121) The previous checker was buggy and not exactly following the expected semantics. This fixes it. --- src/theory/booleans/proof_checker.cpp | 136 ++++++++++++++------------ 1 file changed, 75 insertions(+), 61 deletions(-) diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 94bb73feb04..cdf5a8b7c71 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -283,7 +283,14 @@ Node BoolProofRuleChecker::checkInternal(ProofRule id, AlwaysAssert(itrhs != rhsClause.end()); lhsClause.insert(lhsClause.end(), rhsClause.begin(), itrhs); lhsClause.insert(lhsClause.end(), itrhs + 1, rhsClause.end()); - Trace("bool-pfcheck") << "\t.. after rhsClause: " << lhsClause << "\n"; + if (TraceIsOn("bool-pfcheck")) + { + std::vector updatedRhsClause{rhsClause.begin(), itrhs}; + updatedRhsClause.insert( + updatedRhsClause.end(), itrhs + 1, rhsClause.end()); + Trace("bool-pfcheck") + << "\t.. after rhsClause: " << updatedRhsClause << "\n"; + } rhsClause.clear(); } Trace("bool-pfcheck") << "\n resulting clause: " << lhsClause << "\n" @@ -304,79 +311,87 @@ Node BoolProofRuleChecker::checkInternal(ProofRule id, NodeManager* nm = nodeManager(); Node trueNode = nm->mkConst(true); Node falseNode = nm->mkConst(false); - std::vector clauseNodes; - for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize; - ++i) + std::vector lhsClause, rhsClause; + Node lhsElim, rhsElim; + std::vector pols, lits; + for (size_t i = 1, nargs = args.size(); i < nargs; i = i + 2) + { + pols.push_back(args[i]); + lits.push_back(args[i + 1]); + } + + if (children[0].getKind() != Kind::OR + || (pols[0] == trueNode && children[0] == lits[0]) + || (pols[0] == falseNode && children[0] == lits[0].notNode())) { - std::unordered_set elim; - // literals to be removed from "first" clause - if (i < childrenSize - 1) + lhsClause.push_back(children[0]); + } + else + { + lhsClause.insert(lhsClause.end(), children[0].begin(), children[0].end()); + } + // Traverse the links, which amounts to for each pair of args removing a + // literal from the lhs and a literal from the lhs. + for (size_t i = 0, argsSize = pols.size(); i < argsSize; i++) + { + // Polarity determines how the pivot occurs in lhs and rhs + if (pols[i] == trueNode) { - for (std::size_t j = (2 * i) + 1, argsSize = args.size(); j < argsSize; - j = j + 2) - { - // whether pivot should occur as is or negated depends on the polarity - // of each step in the macro - if (args[j] == trueNode) - { - elim.insert(args[j + 1]); - } - else - { - Assert(args[j] == falseNode); - elim.insert(args[j + 1].notNode()); - } - } + lhsElim = lits[i]; + rhsElim = lits[i].notNode(); } - // literal to be removed from "second" clause. They will be negated - if (i > 0) + else { - std::size_t index = 2 * (i - 1) + 1; - Node pivot = args[index] == trueNode ? args[index + 1].notNode() - : args[index + 1]; - elim.insert(pivot); + Assert(pols[i] == falseNode); + lhsElim = lits[i].notNode(); + rhsElim = lits[i]; } - Trace("bool-pfcheck") << i << ": elimination set: " << elim << "\n"; - // only add to conclusion nodes that are not in elimination set. First get - // the nodes. - // - // Since a Node cannot hold an OR with a single child we need to - // disambiguate singleton clauses that are OR nodes from non-singleton - // clauses (i.e. unit clauses in the SAT solver). - // - // If the child is not an OR, it is a singleton clause and we take the - // child itself as the clause. Otherwise the child can only be a singleton - // clause if the child itself is used as a resolution literal, i.e. if the - // child is in lhsElim or is equal to rhsElim (which means that the - // negation of the child is in lhsElim). - std::vector lits; - if (children[i].getKind() == Kind::OR && !elim.count(children[i])) + // The index of the child corresponding to the current rhs clause + size_t childIndex = i + 1; + // Get rhs clause. It's a singleton if not an OR node or if equal to + // rhsElim + if (children[childIndex].getKind() != Kind::OR + || children[childIndex] == rhsElim) { - lits.insert(lits.end(), children[i].begin(), children[i].end()); + rhsClause.push_back(children[childIndex]); } else { - lits.push_back(children[i]); + rhsClause = {children[childIndex].begin(), children[childIndex].end()}; } - Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n"; - std::vector added; - for (std::size_t j = 0, size = lits.size(); j < size; ++j) + Trace("bool-pfcheck") << i << "-th res link:\n"; + Trace("bool-pfcheck") << "\t - lhsClause: " << lhsClause << "\n"; + Trace("bool-pfcheck") << "\t\t - lhsElim: " << lhsElim << "\n"; + Trace("bool-pfcheck") << "\t - rhsClause: " << rhsClause << "\n"; + Trace("bool-pfcheck") << "\t\t - rhsElim: " << rhsElim << "\n"; + // Compute the resulting clause, which will be the next lhsClause, as + // follows: + // - remove all lhsElim from lhsClause + // - remove all rhsElim from rhsClause and add the lits to lhsClause + // + // Note that to remove the elements from lhsClaus we use the + // "erase-remove" idiom in C++: the std::remove call shuffles the elements + // different from lhsElim to the beginning of the container, returning an + // iterator to the beginning of the "rest" of the container (with + // occurrences of lhsElim). Then the call to erase removes the range from + // there to the end. Once C++ 20 is allowed in the cvc5 code base, this + // could be done with a single call to std::erase. + lhsClause.erase(std::remove(lhsClause.begin(), lhsClause.end(), lhsElim), + lhsClause.end()); + for (const Node& l : rhsClause) { // only add if literal does not occur in elimination set - if (elim.count(lits[j]) == 0) + if (rhsElim != l) { - clauseNodes.push_back(lits[j]); - added.push_back(lits[j]); - // eliminate duplicates - elim.insert(lits[j]); + lhsClause.push_back(l); } } - Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n"; + rhsClause.clear(); } - Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n"; + + Trace("bool-pfcheck") << "clause: " << lhsClause << "\n"; // check that set representation is the same as of the given conclusion - std::unordered_set clauseComputed{clauseNodes.begin(), - clauseNodes.end()}; + std::unordered_set clauseComputed{lhsClause.begin(), lhsClause.end()}; Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop; if (clauseComputed.empty()) { @@ -396,10 +411,9 @@ Node BoolProofRuleChecker::checkInternal(ProofRule id, } return args[0]; } - // At this point, should amount to them differing only on order. So the - // original result can't be a singleton clause - if (args[0].getKind() != Kind::OR - || clauseComputed.size() != args[0].getNumChildren()) + // At this point, should amount to them differing only on order or in + // repetitions. So the original result can't be a singleton clause. + if (args[0].getKind() != Kind::OR) { return Node::null(); }