From f58e7e32d99b9fda841ebfd0c29016c41a109bfe Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Wed, 16 Sep 2020 00:05:10 -0300 Subject: [PATCH] [proof-new] Resolution rules and checkers (#5070) --- src/expr/proof_rule.cpp | 4 + src/expr/proof_rule.h | 39 ++++++++ src/theory/booleans/proof_checker.cpp | 137 ++++++++++++++++++++++++++ 3 files changed, 180 insertions(+) diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 1d46b183f..57dd3e0bd 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -42,6 +42,10 @@ const char* toString(PfRule id) case PfRule::THEORY_PREPROCESS_LEMMA: return "THEORY_PREPROCESS_LEMMA"; case PfRule::WITNESS_AXIOM: return "WITNESS_AXIOM"; //================================================= Boolean rules + case PfRule::RESOLUTION: return "RESOLUTION"; + case PfRule::CHAIN_RESOLUTION: return "CHAIN_RESOLUTION"; + case PfRule::FACTORING: return "FACTORING"; + case PfRule::REORDERING: return "REORDERING"; case PfRule::SPLIT: return "SPLIT"; case PfRule::EQ_RESOLVE: return "EQ_RESOLVE"; case PfRule::AND_ELIM: return "AND_ELIM"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 825503d5d..c02292dab 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -226,6 +226,45 @@ enum class PfRule : uint32_t WITNESS_AXIOM, //================================================= Boolean rules + // ======== Resolution + // Children: + // (P1:(or F_1 ... F_i-1 F_i F_i+1 ... F_n), + // P2:(or G_1 ... G_j-1 G_j G_j+1 ... G_m)) + // + // Arguments: (F_i) + // --------------------- + // Conclusion: (or F_1 ... F_i-1 F_i+1 ... F_n G_1 ... G_j-1 G_j+1 ... G_m) + // where + // G_j = (not F_i) + RESOLUTION, + // ======== Chain Resolution + // Children: (P1:(or F_{1,1} ... F_{1,n1}), ..., Pm:(or F_{m,1} ... F_{m,nm})) + // Arguments: (L_1, ..., L_{m-1}) + // --------------------- + // Conclusion: C_m' + // where + // let "C_1 <>_l C_2" represent the resolution of C_1 with C_2 with pivot l, + // let C_1' = C_1 (from P_1), + // for each i > 1, C_i' = C_i <>_L_i C_{i-1}' + CHAIN_RESOLUTION, + // ======== Factoring + // Children: (P:C1) + // Arguments: () + // --------------------- + // Conclusion: C2 + // where + // Set representations of C1 and C2 is the same and the number of literals in + // C2 is smaller than that of C1 + FACTORING, + // ======== Reordering + // Children: (P:C1) + // Arguments: (C2) + // --------------------- + // Conclusion: C2 + // where + // Set representations of C1 and C2 is the same but the number of literals in + // C2 is the same of that of C1 + REORDERING, // ======== Split // Children: none // Arguments: (F) diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 6a8244ce0..e9dafdad6 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -21,6 +21,10 @@ namespace booleans { void BoolProofRuleChecker::registerTo(ProofChecker* pc) { pc->registerChecker(PfRule::SPLIT, this); + pc->registerChecker(PfRule::RESOLUTION, this); + pc->registerChecker(PfRule::CHAIN_RESOLUTION, this); + pc->registerChecker(PfRule::FACTORING, this); + pc->registerChecker(PfRule::REORDERING, this); pc->registerChecker(PfRule::EQ_RESOLVE, this); pc->registerChecker(PfRule::AND_ELIM, this); pc->registerChecker(PfRule::AND_INTRO, this); @@ -68,6 +72,139 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, const std::vector& children, const std::vector& args) { + if (id == PfRule::RESOLUTION) + { + Assert(children.size() == 2); + Assert(args.size() == 1); + std::vector disjuncts; + for (unsigned i = 0; i < 2; ++i) + { + // if first clause, eliminate pivot, otherwise its negation + Node elim = i == 0 ? args[0] : args[0].notNode(); + for (unsigned j = 0, size = children[i].getNumChildren(); j < size; ++j) + { + if (elim != children[i][j]) + { + disjuncts.push_back(children[i][j]); + } + } + } + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::FACTORING) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::OR) + { + return Node::null(); + } + // remove duplicates while keeping the order of children + std::unordered_set clauseSet; + std::vector disjuncts; + unsigned size = children[0].getNumChildren(); + for (unsigned i = 0; i < size; ++i) + { + if (clauseSet.count(children[0][i])) + { + continue; + } + disjuncts.push_back(children[0][i]); + clauseSet.insert(children[0][i]); + } + if (disjuncts.size() == size) + { + return Node::null(); + } + NodeManager* nm = NodeManager::currentNM(); + return disjuncts.empty() + ? nm->mkConst(false) + : disjuncts.size() == 1 ? disjuncts[0] + : nm->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::REORDERING) + { + Assert(children.size() == 1); + Assert(args.size() == 1); + std::unordered_set clauseSet1, clauseSet2; + if (children[0].getKind() == kind::OR) + { + clauseSet1.insert(children[0].begin(), children[0].end()); + } + else + { + clauseSet1.insert(children[0]); + } + if (args[0].getKind() == kind::OR) + { + clauseSet2.insert(args[0].begin(), args[0].end()); + } + else + { + clauseSet2.insert(args[0]); + } + if (clauseSet1 != clauseSet2) + { + Trace("bool-pfcheck") << id << ": clause set1: " << clauseSet1 << "\n" + << id << ": clause set2: " << clauseSet2 << "\n"; + return Node::null(); + } + return args[0]; + } + if (id == PfRule::CHAIN_RESOLUTION) + { + Assert(children.size() > 1); + Assert(args.size() == children.size() - 1); + Trace("bool-pfcheck") << "chain_res:\n" << push; + std::vector clauseNodes; + for (unsigned i = 0, childrenSize = children.size(); i < childrenSize; ++i) + { + std::unordered_set elim; + // literals to be removed from "first" clause + if (i < childrenSize - 1) + { + elim.insert(args.begin() + i, args.end()); + } + // literal to be removed from "second" clause. They will be negated + if (i > 0) + { + elim.insert(args[i - 1].negate()); + } + Trace("bool-pfcheck") << i << ": elimination set: " << elim << "\n"; + // only add to conclusion nodes that are not in elimination set. First get + // the nodes. + // + // Since unit clauses can also be OR nodes, we rely on the invariant that + // non-unit clauses will not occur themselves in their elimination sets. + // If they do then they must be unit. + std::vector lits; + if (children[i].getKind() == kind::OR && elim.count(children[i]) == 0) + { + lits.insert(lits.end(), children[i].begin(), children[i].end()); + } + else + { + lits.push_back(children[i]); + } + Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n"; + std::vector added; + for (unsigned j = 0, size = lits.size(); j < size; ++j) + { + if (elim.count(lits[j]) == 0) + { + clauseNodes.push_back(lits[j]); + added.push_back(lits[j]); + } + } + Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n"; + } + Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop; + NodeManager* nm = NodeManager::currentNM(); + return clauseNodes.empty() + ? nm->mkConst(false) + : clauseNodes.size() == 1 ? clauseNodes[0] + : nm->mkNode(kind::OR, clauseNodes); + } if (id == PfRule::SPLIT) { Assert(children.empty()); -- 2.30.2