From 77dfb2623f3cb8ce8e9795f319d6ae574012debf Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 26 Oct 2021 16:42:14 -0300 Subject: [PATCH] [proofs] Fix and simplify CHAIN_RESOLUTION checker (#7492) Fixes cvc5/cvc5-projects#319 --- src/smt/proof_post_processor.cpp | 5 + src/theory/booleans/proof_checker.cpp | 136 ++++++++++-------- test/regress/CMakeLists.txt | 1 + .../proofs/qgu-fuzz-3-chainres-checking.smt2 | 7 + 4 files changed, 86 insertions(+), 63 deletions(-) create mode 100644 test/regress/regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index a519ca6b5..a6b5b832e 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -683,6 +683,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // literals, which could themselves add crowding literals. if (chainConclusion == args[0]) { + Trace("smt-proof-pp-debug") << "..same conclusion, DONE.\n"; cdp->addStep( chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs); return chainConclusion; @@ -716,6 +717,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // chain. if (chainConclusionLitsSet != conclusionLitsSet) { + Trace("smt-proof-pp-debug") << "..need to eliminate crowding lits.\n"; chainConclusion = eliminateCrowdingLits( chainConclusionLits, conclusionLits, children, args, cdp); // update vector of lits. Note that the set is no longer used, so we don't @@ -739,6 +741,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, } else { + Trace("smt-proof-pp-debug") << "..add chainRes step directly.\n"; cdp->addStep( chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs); } @@ -751,6 +754,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // factoring if (chainConclusionLits.size() != conclusionLits.size()) { + Trace("smt-proof-pp-debug") << "..add factoring step.\n"; // We build it rather than taking conclusionLits because the order may be // different std::vector factoredLits; @@ -777,6 +781,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id, // reordering if (n != args[0]) { + Trace("smt-proof-pp-debug") << "..add reordering step.\n"; cdp->addStep(args[0], PfRule::REORDERING, {n}, {args[0]}); } return args[0]; diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index eea179ad3..a7fefd47a 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -196,79 +196,89 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, NodeManager* nm = NodeManager::currentNM(); 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) + // The lhs and rhs clauses in a binary resolution step, respectively. Since + // children correspond to the premises in the resolution chain, the first + // lhs clause is the first premise, the first rhs clause is the second + // premise. Each subsequent lhs clause will be the result of the previous + // binary resolution step in the chain, while each subsequent rhs clause + // will be respectively the second, third etc premises. + std::vector lhsClause, rhsClause; + // The pivots to be eliminated to the lhs clause and rhs clause in a binary + // resolution step, respectively + Node lhsElim, rhsElim; + // Get lhsClause of first resolution. + // + // 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 + // first child equal to the first pivot (which is args[1] or + // args[1].notNote() depending on the polarity). + if (children[0].getKind() != kind::OR + || (args[0] == trueNode && children[0] == args[1]) + || (args[0] == falseNode && children[0] == args[1].notNode())) + { + lhsClause.push_back(children[0]); + } + else { - // Literals to be removed from the current clause, according to this - // clause being in the lhs or the rhs of a resolution. The first clause - // has no rhsElim and the last clause has no lhsElim. The literal to be - // eliminated depends ond the pivot and the polarity stored in the - // arguments. - Node lhsElim = Node::null(); - Node rhsElim = Node::null(); - if (i < childrenSize - 1) + 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 = args.size(); i < argsSize; i = i + 2) + { + // Polarity determines how the pivot occurs in lhs and rhs + if (args[i] == trueNode) { - std::size_t index = 2 * i; - lhsElim = args[index] == trueNode ? args[index + 1] - : args[index + 1].notNode(); - Trace("bool-pfcheck") << i << ": lhsElim: " << lhsElim << "\n"; + lhsElim = args[i + 1]; + rhsElim = args[i + 1].notNode(); } - if (i > 0) + else { - std::size_t index = 2 * (i - 1); - rhsElim = args[index] == trueNode ? args[index + 1].notNode() - : args[index + 1]; - Trace("bool-pfcheck") << i << ": rhsElim: " << rhsElim << "\n"; + Assert(args[i] == falseNode); + lhsElim = args[i + 1].notNode(); + rhsElim = args[i + 1]; } - // The current set of literals is what we had before plus those in the - // current child. - // - // 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 equal to the lhsElim or to the rhsElim (which means that the - // negation of the child is in lhsElim). - std::vector lits{clauseNodes}; - if (children[i].getKind() == kind::OR && children[i] != lhsElim - && children[i] != rhsElim) + // The index of the child corresponding to the current rhs clause + size_t childIndex = i / 2 + 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"; - // We now compute the set of literals minus those to be eliminated in this - // step - std::vector curr; - for (std::size_t j = 0, size = lits.size(); j < size; ++j) - { - if (lits[j] == lhsElim) - { - lhsElim = Node::null(); - Trace("bool-pfcheck") << "\t removed lit: " << lits[j] << "\n"; - continue; - } - if (lits[j] == rhsElim) - { - rhsElim = Node::null(); - Trace("bool-pfcheck") << "\t removed lit: " << lits[j] << "\n"; - continue; - } - curr.push_back(lits[j]); - } - Trace("bool-pfcheck") << "\n"; - clauseNodes.clear(); - clauseNodes.insert(clauseNodes.end(), curr.begin(), curr.end()); - } - Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop; - return nm->mkOr(clauseNodes); + Trace("bool-pfcheck") << i / 2 << "-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 lhsElim from lhsClause + // - remove rhsElim from rhsClause and add the lits to lhsClause + auto itlhs = std::find(lhsClause.begin(), lhsClause.end(), lhsElim); + AlwaysAssert(itlhs != lhsClause.end()); + lhsClause.erase(itlhs); + Trace("bool-pfcheck") << "\t.. after lhsClause: " << lhsClause << "\n"; + auto itrhs = std::find(rhsClause.begin(), rhsClause.end(), rhsElim); + 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"; + rhsClause.clear(); + } + Trace("bool-pfcheck") << "\n resulting clause: " << lhsClause << "\n" + << pop; + return nm->mkOr(lhsClause); } if (id == PfRule::MACRO_RESOLUTION_TRUST) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 299261284..34ef1a9f7 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -859,6 +859,7 @@ set(regress_0_tests regress0/proofs/open-pf-rederivation.smt2 regress0/proofs/qgu-fuzz-1-bool-sat.smt2 regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 + regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 regress0/proofs/scope.smt2 regress0/proofs/trust-subs-eq-open.smt2 regress0/push-pop/boolean/fuzz_12.smt2 diff --git a/test/regress/regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 b/test/regress/regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 new file mode 100644 index 000000000..27836734b --- /dev/null +++ b/test/regress/regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 @@ -0,0 +1,7 @@ +; EXPECT: unsat +(set-logic ALL) +(declare-fun a () Bool) +(declare-fun c () Bool) +(declare-fun d () Bool) +(assert (and (= a (ite (or c d) d a)) (not (ite d a false)) (ite c a d))) +(check-sat) \ No newline at end of file -- 2.30.2