From d442be84a2e47ccc6b3b91dbcf5ae2c1b891049b Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 22 Oct 2021 19:08:27 -0300 Subject: [PATCH] [proof] Fixing CHAIN_RESOLUTION checker (#7465) Previously the checker was doing things in a smart way that could lead to issues when a clause coincided with a singleton clause as a literal of another clause within the chain. Fixes cvc5/cvc5-projects#310 --- src/smt/proof_post_processor.cpp | 10 ++- src/theory/booleans/proof_checker.cpp | 88 +++++++------------ test/regress/CMakeLists.txt | 3 +- .../qgu-fuzz-2-bool-chainres-checking.smt2 | 10 +++ 4 files changed, 49 insertions(+), 62 deletions(-) create mode 100644 test/regress/regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index 04a36c1c0..a519ca6b5 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -318,8 +318,8 @@ Node ProofPostprocessCallback::eliminateCrowdingLits( size_t start = lastElim + 1; size_t end = nextGuardedElimPos - 1; Trace("smt-proof-pp-debug2") - << "res with:\n\tlastClause: " << lastClause << "\n\tstart: " << start - << "\n\tend: " << end << "\n"; + << "res with:\n\t\tlastClause: " << lastClause + << "\n\t\tstart: " << start << "\n\t\tend: " << end << "\n"; childrenRes.push_back(lastClause); // note that the interval of insert is exclusive in the end, so we add 1 childrenRes.insert(childrenRes.end(), @@ -328,8 +328,8 @@ Node ProofPostprocessCallback::eliminateCrowdingLits( childrenResArgs.insert(childrenResArgs.end(), args.begin() + (2 * start) - 1, args.begin() + (2 * end) + 1); - Trace("smt-proof-pp-debug2") << "res children: " << childrenRes << "\n"; - Trace("smt-proof-pp-debug2") << "res args: " << childrenResArgs << "\n"; + Trace("smt-proof-pp-debug2") << "\tres children: " << childrenRes << "\n"; + Trace("smt-proof-pp-debug2") << "\tres args: " << childrenResArgs << "\n"; resPlaceHolder = d_pnm->getChecker()->checkDebug(PfRule::CHAIN_RESOLUTION, childrenRes, childrenResArgs, @@ -337,6 +337,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits( ""); Trace("smt-proof-pp-debug2") << "resPlaceHorder: " << resPlaceHolder << "\n"; + Trace("smt-proof-pp-debug2") << "-------\n"; cdp->addStep( resPlaceHolder, PfRule::CHAIN_RESOLUTION, childrenRes, childrenResArgs); // I need to add factoring if end < children.size(). Otherwise, this is @@ -348,6 +349,7 @@ Node ProofPostprocessCallback::eliminateCrowdingLits( if (!lastClause.isNull()) { cdp->addStep(lastClause, PfRule::FACTORING, {resPlaceHolder}, {}); + Trace("smt-proof-pp-debug2") << "Apply factoring.\n"; } else { diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index d0461248c..eea179ad3 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -197,55 +197,32 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, Node trueNode = nm->mkConst(true); Node falseNode = nm->mkConst(false); std::vector clauseNodes; - // literals to be removed from the virtual lhs clause of the resolution - std::unordered_map lhsElim; - for (std::size_t i = 0, argsSize = args.size(); i < argsSize; i = i + 2) - { - // whether pivot should occur as is or negated depends on the polarity of - // each step in the chain - if (args[i] == trueNode) - { - lhsElim[args[i + 1]]++; - } - else - { - Assert(args[i] == falseNode); - lhsElim[args[i + 1].notNode()]++; - } - } - if (Trace.isOn("bool-pfcheck")) - { - Trace("bool-pfcheck") - << "Original elimination multiset for lhs clause:\n"; - for (const auto& pair : lhsElim) - { - Trace("bool-pfcheck") - << "\t- " << pair.first << " {" << pair.second << "}\n"; - } - } for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize; ++i) { - // literal to be removed from rhs clause. They will be negated + // 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 (Trace.isOn("bool-pfcheck")) + if (i < childrenSize - 1) { - Trace("bool-pfcheck") << i << ": current lhsElim:\n"; - for (const auto& pair : lhsElim) - { - Trace("bool-pfcheck") - << "\t- " << pair.first << " {" << pair.second << "}\n"; - } + std::size_t index = 2 * i; + lhsElim = args[index] == trueNode ? args[index + 1] + : args[index + 1].notNode(); + Trace("bool-pfcheck") << i << ": lhsElim: " << lhsElim << "\n"; } if (i > 0) { std::size_t index = 2 * (i - 1); rhsElim = args[index] == trueNode ? args[index + 1].notNode() : args[index + 1]; - Trace("bool-pfcheck") << i << ": rhs elim: " << rhsElim << "\n"; + Trace("bool-pfcheck") << i << ": rhsElim: " << rhsElim << "\n"; } - // Only add to conclusion nodes that are not in elimination set. First get - // the nodes. + // 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 @@ -254,10 +231,10 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, // 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 + // child equal to the lhsElim or to the rhsElim (which means that the // negation of the child is in lhsElim). - std::vector lits; - if (children[i].getKind() == kind::OR && lhsElim.count(children[i]) == 0 + std::vector lits{clauseNodes}; + if (children[i].getKind() == kind::OR && children[i] != lhsElim && children[i] != rhsElim) { lits.insert(lits.end(), children[i].begin(), children[i].end()); @@ -267,31 +244,28 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, lits.push_back(children[i]); } Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n"; - std::vector added; + // 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] == rhsElim) + if (lits[j] == lhsElim) { - rhsElim = Node::null(); + lhsElim = Node::null(); + Trace("bool-pfcheck") << "\t removed lit: " << lits[j] << "\n"; continue; } - auto it = lhsElim.find(lits[j]); - if (it == lhsElim.end()) - { - clauseNodes.push_back(lits[j]); - added.push_back(lits[j]); - } - else + if (lits[j] == rhsElim) { - // remove occurrence - it->second--; - if (it->second == 0) - { - lhsElim.erase(it); - } + rhsElim = Node::null(); + Trace("bool-pfcheck") << "\t removed lit: " << lits[j] << "\n"; + continue; } + curr.push_back(lits[j]); } - Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n"; + 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); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ab449dc13..5dd456b9f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -857,6 +857,7 @@ set(regress_0_tests regress0/proofs/open-pf-if-unordered-iff.smt2 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/scope.smt2 regress0/proofs/trust-subs-eq-open.smt2 regress0/push-pop/boolean/fuzz_12.smt2 @@ -2235,7 +2236,7 @@ set(regress_1_tests regress1/strings/issue6142-repl-inv-rew.smt2 regress1/strings/issue6180-proxy-vars.smt2 regress1/strings/issue6180-2-proxy-vars.smt2 - regress1/strings/issue6184-unsat-core.smt2 + regress1/strings/issue6184-unsat-core.smt2 regress1/strings/issue6191-replace-all.smt2 regress1/strings/issue6203-1-substr-ctn-strip.smt2 regress1/strings/issue6203-2-re-ccache.smt2 diff --git a/test/regress/regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 b/test/regress/regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 new file mode 100644 index 000000000..867f986da --- /dev/null +++ b/test/regress/regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 @@ -0,0 +1,10 @@ +; EXPECT: unsat +(set-logic ALL) +(declare-fun a () Bool) +(declare-fun b () Bool) +(declare-fun c () Bool) +(declare-fun d () Bool) +(assert +(and (ite a c (ite b d c)) (= d (ite a b c)) (not (= a (ite b c d))) (ite a c (ite b d a)) (ite c (ite b a d) c) (ite a c (ite c d a))) +) +(check-sat) \ No newline at end of file -- 2.30.2