From: Haniel Barbosa Date: Wed, 3 Jun 2020 21:54:47 +0000 (-0300) Subject: (proof-new) Adding rules and proof checker for Boolean reasoning (#4560) X-Git-Tag: cvc5-1.0.0~3263 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b19d246d75be92a0189b9aaacc71426395b8c098;p=cvc5.git (proof-new) Adding rules and proof checker for Boolean reasoning (#4560) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4fb1606bc..97c352d5d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -355,6 +355,8 @@ libcvc4_add_sources( theory/atom_requests.h theory/booleans/circuit_propagator.cpp theory/booleans/circuit_propagator.h + theory/booleans/proof_checker.cpp + theory/booleans/proof_checker.h theory/booleans/theory_bool.cpp theory/booleans/theory_bool.h theory/booleans/theory_bool_rewriter.cpp diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 09ffc82bf..0e73d8c10 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -32,6 +32,51 @@ const char* toString(PfRule id) case PfRule::MACRO_SR_PRED_ELIM: return "MACRO_SR_PRED_ELIM"; case PfRule::MACRO_SR_PRED_TRANSFORM: return "MACRO_SR_PRED_TRANSFORM"; + //================================================= Boolean rules + case PfRule::SPLIT: return "SPLIT"; + case PfRule::AND_ELIM: return "AND_ELIM"; + case PfRule::AND_INTRO: return "AND_INTRO"; + case PfRule::NOT_OR_ELIM: return "NOT_OR_ELIM"; + case PfRule::IMPLIES_ELIM: return "IMPLIES_ELIM"; + case PfRule::NOT_IMPLIES_ELIM1: return "NOT_IMPLIES_ELIM1"; + case PfRule::NOT_IMPLIES_ELIM2: return "NOT_IMPLIES_ELIM2"; + case PfRule::EQUIV_ELIM1: return "EQUIV_ELIM1"; + case PfRule::EQUIV_ELIM2: return "EQUIV_ELIM2"; + case PfRule::NOT_EQUIV_ELIM1: return "NOT_EQUIV_ELIM1"; + case PfRule::NOT_EQUIV_ELIM2: return "NOT_EQUIV_ELIM2"; + case PfRule::XOR_ELIM1: return "XOR_ELIM1"; + case PfRule::XOR_ELIM2: return "XOR_ELIM2"; + case PfRule::NOT_XOR_ELIM1: return "NOT_XOR_ELIM1"; + case PfRule::NOT_XOR_ELIM2: return "NOT_XOR_ELIM2"; + case PfRule::ITE_ELIM1: return "ITE_ELIM1"; + case PfRule::ITE_ELIM2: return "ITE_ELIM2"; + case PfRule::NOT_ITE_ELIM1: return "NOT_ITE_ELIM1"; + case PfRule::NOT_ITE_ELIM2: return "NOT_ITE_ELIM2"; + case PfRule::CONTRA: return "CONTRA"; + //================================================= De Morgan rules + case PfRule::NOT_AND: return "NOT_AND"; + //================================================= CNF rules + case PfRule::CNF_AND_POS: return "CNF_AND_POS"; + case PfRule::CNF_AND_NEG: return "CNF_AND_NEG"; + case PfRule::CNF_OR_POS: return "CNF_OR_POS"; + case PfRule::CNF_OR_NEG: return "CNF_OR_NEG"; + case PfRule::CNF_IMPLIES_POS: return "CNF_IMPLIES_POS"; + case PfRule::CNF_IMPLIES_NEG1: return "CNF_IMPLIES_NEG1"; + case PfRule::CNF_IMPLIES_NEG2: return "CNF_IMPLIES_NEG2"; + case PfRule::CNF_EQUIV_POS1: return "CNF_EQUIV_POS1"; + case PfRule::CNF_EQUIV_POS2: return "CNF_EQUIV_POS2"; + case PfRule::CNF_EQUIV_NEG1: return "CNF_EQUIV_NEG1"; + case PfRule::CNF_EQUIV_NEG2: return "CNF_EQUIV_NEG2"; + case PfRule::CNF_XOR_POS1: return "CNF_XOR_POS1"; + case PfRule::CNF_XOR_POS2: return "CNF_XOR_POS2"; + case PfRule::CNF_XOR_NEG1: return "CNF_XOR_NEG1"; + case PfRule::CNF_XOR_NEG2: return "CNF_XOR_NEG2"; + case PfRule::CNF_ITE_POS1: return "CNF_ITE_POS1"; + case PfRule::CNF_ITE_POS2: return "CNF_ITE_POS2"; + case PfRule::CNF_ITE_POS3: return "CNF_ITE_POS3"; + case PfRule::CNF_ITE_NEG1: return "CNF_ITE_NEG1"; + case PfRule::CNF_ITE_NEG2: return "CNF_ITE_NEG2"; + case PfRule::CNF_ITE_NEG3: return "CNF_ITE_NEG3"; //================================================= Unknown rule case PfRule::UNKNOWN: return "UNKNOWN"; default: return "?"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index e0a626b69..9dc1d017f 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -71,6 +71,262 @@ enum class PfRule : uint32_t // has the conclusion (=> F F) and has no free assumptions. More generally, a // proof with no free assumptions always concludes a valid formula. SCOPE, + //================================================= Boolean rules + // ======== Split + // Children: none + // Arguments: (F) + // --------------------- + // Conclusion: (or F (not F)) + SPLIT, + // ======== And elimination + // Children: (P:(and F1 ... Fn)) + // Arguments: (i) + // --------------------- + // Conclusion: (Fi) + AND_ELIM, + // ======== And introduction + // Children: (P1:F1 ... Pn:Fn)) + // Arguments: () + // --------------------- + // Conclusion: (and P1 ... Pn) + AND_INTRO, + // ======== Not Or elimination + // Children: (P:(not (or F1 ... Fn))) + // Arguments: (i) + // --------------------- + // Conclusion: (not Fi) + NOT_OR_ELIM, + // ======== Implication elimination + // Children: (P:(=> F1 F2)) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) F2) + IMPLIES_ELIM, + // ======== Not Implication elimination version 1 + // Children: (P:(not (=> F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (F1) + NOT_IMPLIES_ELIM1, + // ======== Not Implication elimination version 2 + // Children: (P:(not (=> F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (not F2) + NOT_IMPLIES_ELIM2, + // ======== Equivalence elimination version 1 + // Children: (P:(= F1 F2)) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) F2) + EQUIV_ELIM1, + // ======== Equivalence elimination version 2 + // Children: (P:(= F1 F2)) + // Arguments: () + // --------------------- + // Conclusion: (or F1 (not F2)) + EQUIV_ELIM2, + // ======== Not Equivalence elimination version 1 + // Children: (P:(not (= F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or F1 F2) + NOT_EQUIV_ELIM1, + // ======== Not Equivalence elimination version 2 + // Children: (P:(not (= F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) (not F2)) + NOT_EQUIV_ELIM2, + // ======== XOR elimination version 1 + // Children: (P:(xor F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or F1 F2) + XOR_ELIM1, + // ======== XOR elimination version 2 + // Children: (P:(xor F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) (not F2)) + XOR_ELIM2, + // ======== Not XOR elimination version 1 + // Children: (P:(not (xor F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or F1 (not F2)) + NOT_XOR_ELIM1, + // ======== Not XOR elimination version 2 + // Children: (P:(not (xor F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) F2) + NOT_XOR_ELIM2, + // ======== ITE elimination version 1 + // Children: (P:(ite C F1 F2)) + // Arguments: () + // --------------------- + // Conclusion: (or (not C) F1) + ITE_ELIM1, + // ======== ITE elimination version 2 + // Children: (P:(ite C F1 F2)) + // Arguments: () + // --------------------- + // Conclusion: (or C F2) + ITE_ELIM2, + // ======== Not ITE elimination version 1 + // Children: (P:(not (ite C F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or (not C) (not F1)) + NOT_ITE_ELIM1, + // ======== Not ITE elimination version 1 + // Children: (P:(not (ite C F1 F2))) + // Arguments: () + // --------------------- + // Conclusion: (or C (not F2)) + NOT_ITE_ELIM2, + // ======== Not ITE elimination version 1 + // Children: (P1:P P2:(not P)) + // Arguments: () + // --------------------- + // Conclusion: (false) + CONTRA, + + //================================================= De Morgan rules + // ======== Not And + // Children: (P:(not (and F1 ... Fn)) + // Arguments: () + // --------------------- + // Conclusion: (or (not F1) ... (not Fn)) + NOT_AND, + //================================================= CNF rules + // ======== CNF And Pos + // Children: () + // Arguments: ((and F1 ... Fn), i) + // --------------------- + // Conclusion: (or (not (and F1 ... Fn)) Fi) + CNF_AND_POS, + // ======== CNF And Neg + // Children: () + // Arguments: ((and F1 ... Fn)) + // --------------------- + // Conclusion: (or (and F1 ... Fn) (not F1) ... (not Fn)) + CNF_AND_NEG, + // ======== CNF Or Pos + // Children: () + // Arguments: ((or F1 ... Fn)) + // --------------------- + // Conclusion: (or (not (or F1 ... Fn)) F1 ... Fn) + CNF_OR_POS, + // ======== CNF Or Neg + // Children: () + // Arguments: ((or F1 ... Fn), i) + // --------------------- + // Conclusion: (or (or F1 ... Fn) (not Fi)) + CNF_OR_NEG, + // ======== CNF Implies Pos + // Children: () + // Arguments: ((implies F1 F2)) + // --------------------- + // Conclusion: (or (not (implies F1 F2)) (not F1) F2) + CNF_IMPLIES_POS, + // ======== CNF Implies Neg version 1 + // Children: () + // Arguments: ((implies F1 F2)) + // --------------------- + // Conclusion: (or (implies F1 F2) F1) + CNF_IMPLIES_NEG1, + // ======== CNF Implies Neg version 2 + // Children: () + // Arguments: ((implies F1 F2)) + // --------------------- + // Conclusion: (or (implies F1 F2) (not F2)) + CNF_IMPLIES_NEG2, + // ======== CNF Equiv Pos version 1 + // Children: () + // Arguments: ((= F1 F2)) + // --------------------- + // Conclusion: (or (not (= F1 F2)) (not F1) F2) + CNF_EQUIV_POS1, + // ======== CNF Equiv Pos version 2 + // Children: () + // Arguments: ((= F1 F2)) + // --------------------- + // Conclusion: (or (not (= F1 F2)) F1 (not F2)) + CNF_EQUIV_POS2, + // ======== CNF Equiv Neg version 1 + // Children: () + // Arguments: ((= F1 F2)) + // --------------------- + // Conclusion: (or (= F1 F2) F1 F2) + CNF_EQUIV_NEG1, + // ======== CNF Equiv Neg version 2 + // Children: () + // Arguments: ((= F1 F2)) + // --------------------- + // Conclusion: (or (= F1 F2) (not F1) (not F2)) + CNF_EQUIV_NEG2, + // ======== CNF Xor Pos version 1 + // Children: () + // Arguments: ((xor F1 F2)) + // --------------------- + // Conclusion: (or (not (xor F1 F2)) F1 F2) + CNF_XOR_POS1, + // ======== CNF Xor Pos version 2 + // Children: () + // Arguments: ((xor F1 F2)) + // --------------------- + // Conclusion: (or (not (xor F1 F2)) (not F1) (not F2)) + CNF_XOR_POS2, + // ======== CNF Xor Neg version 1 + // Children: () + // Arguments: ((xor F1 F2)) + // --------------------- + // Conclusion: (or (xor F1 F2) (not F1) F2) + CNF_XOR_NEG1, + // ======== CNF Xor Neg version 2 + // Children: () + // Arguments: ((xor F1 F2)) + // --------------------- + // Conclusion: (or (xor F1 F2) F1 (not F2)) + CNF_XOR_NEG2, + // ======== CNF ITE Pos version 1 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (not (ite C F1 F2)) (not C) F1) + CNF_ITE_POS1, + // ======== CNF ITE Pos version 2 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (not (ite C F1 F2)) C F2) + CNF_ITE_POS2, + // ======== CNF ITE Pos version 3 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (not (ite C F1 F2)) F1 F2) + CNF_ITE_POS3, + // ======== CNF ITE Neg version 1 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (ite C F1 F2) (not C) (not F1)) + CNF_ITE_NEG1, + // ======== CNF ITE Neg version 2 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (ite C F1 F2) C (not F2)) + CNF_ITE_NEG2, + // ======== CNF ITE Neg version 3 + // Children: () + // Arguments: ((ite C F1 F2)) + // --------------------- + // Conclusion: (or (ite C F1 F2) (not F1) (not F2)) + CNF_ITE_NEG3, //======================== Builtin theory (common node operations) // ======== Substitution @@ -101,7 +357,7 @@ enum class PfRule : uint32_t // --------------------------------------------------------------- // Conclusion: (= t t') // where - // t' is + // t' is // toWitness(Rewriter{idr}(toSkolem(t)*sigma{ids}(Fn)*...*sigma{ids}(F1))) // toSkolem(...) converts terms from witness form to Skolem form, // toWitness(...) converts terms from Skolem form to witness form. @@ -167,7 +423,7 @@ enum class PfRule : uint32_t // Notice that we apply rewriting on the witness form of F and G, similar to // MACRO_SR_PRED_INTRO. MACRO_SR_PRED_TRANSFORM, - + //================================================= Unknown rule UNKNOWN, }; diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp new file mode 100644 index 000000000..8fdbe9f6b --- /dev/null +++ b/src/theory/booleans/proof_checker.cpp @@ -0,0 +1,568 @@ +/********************* */ +/*! \file proof_checker.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of equality proof checker + **/ + +#include "theory/booleans/proof_checker.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +void BoolProofRuleChecker::registerTo(ProofChecker* pc) +{ + pc->registerChecker(PfRule::SPLIT, this); + pc->registerChecker(PfRule::AND_ELIM, this); + pc->registerChecker(PfRule::AND_INTRO, this); + pc->registerChecker(PfRule::NOT_OR_ELIM, this); + pc->registerChecker(PfRule::IMPLIES_ELIM, this); + pc->registerChecker(PfRule::NOT_IMPLIES_ELIM1, this); + pc->registerChecker(PfRule::NOT_IMPLIES_ELIM2, this); + pc->registerChecker(PfRule::EQUIV_ELIM1, this); + pc->registerChecker(PfRule::EQUIV_ELIM2, this); + pc->registerChecker(PfRule::NOT_EQUIV_ELIM1, this); + pc->registerChecker(PfRule::NOT_EQUIV_ELIM2, this); + pc->registerChecker(PfRule::XOR_ELIM1, this); + pc->registerChecker(PfRule::XOR_ELIM2, this); + pc->registerChecker(PfRule::NOT_XOR_ELIM1, this); + pc->registerChecker(PfRule::NOT_XOR_ELIM2, this); + pc->registerChecker(PfRule::ITE_ELIM1, this); + pc->registerChecker(PfRule::ITE_ELIM2, this); + pc->registerChecker(PfRule::NOT_ITE_ELIM1, this); + pc->registerChecker(PfRule::NOT_ITE_ELIM2, this); + pc->registerChecker(PfRule::NOT_AND, this); + pc->registerChecker(PfRule::CNF_AND_POS, this); + pc->registerChecker(PfRule::CNF_AND_NEG, this); + pc->registerChecker(PfRule::CNF_OR_POS, this); + pc->registerChecker(PfRule::CNF_OR_NEG, this); + pc->registerChecker(PfRule::CNF_IMPLIES_POS, this); + pc->registerChecker(PfRule::CNF_IMPLIES_NEG1, this); + pc->registerChecker(PfRule::CNF_IMPLIES_NEG2, this); + pc->registerChecker(PfRule::CNF_EQUIV_POS1, this); + pc->registerChecker(PfRule::CNF_EQUIV_POS2, this); + pc->registerChecker(PfRule::CNF_EQUIV_NEG1, this); + pc->registerChecker(PfRule::CNF_EQUIV_NEG2, this); + pc->registerChecker(PfRule::CNF_XOR_POS1, this); + pc->registerChecker(PfRule::CNF_XOR_POS2, this); + pc->registerChecker(PfRule::CNF_XOR_NEG1, this); + pc->registerChecker(PfRule::CNF_XOR_NEG2, this); + pc->registerChecker(PfRule::CNF_ITE_POS1, this); + pc->registerChecker(PfRule::CNF_ITE_POS2, this); + pc->registerChecker(PfRule::CNF_ITE_POS3, this); + pc->registerChecker(PfRule::CNF_ITE_NEG1, this); + pc->registerChecker(PfRule::CNF_ITE_NEG2, this); + pc->registerChecker(PfRule::CNF_ITE_NEG3, this); +} + +Node BoolProofRuleChecker::checkInternal(PfRule id, + const std::vector& children, + const std::vector& args) +{ + if (id == PfRule::SPLIT) + { + Assert(children.empty()); + Assert(args.size() == 1); + return NodeManager::currentNM()->mkNode( + kind::OR, args[0], args[0].notNode()); + } + // natural deduction rules + if (id == PfRule::AND_ELIM) + { + Assert(children.size() == 1); + Assert(args.size() == 1); + uint32_t i; + if (children[0].getKind() != kind::AND || !getUInt32(args[0], i)) + { + return Node::null(); + } + if (i >= children[0].getNumChildren()) + { + return Node::null(); + } + return children[0][i]; + } + if (id == PfRule::AND_INTRO) + { + Assert(children.size() >= 1); + return children.size() == 1 + ? children[0] + : NodeManager::currentNM()->mkNode(kind::AND, children); + } + if (id == PfRule::NOT_OR_ELIM) + { + Assert(children.size() == 1); + Assert(args.size() == 1); + uint32_t i; + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::OR || !getUInt32(args[0], i)) + { + return Node::null(); + } + if (i >= children[0][0].getNumChildren()) + { + return Node::null(); + } + return children[0][0][i].notNode(); + } + if (id == PfRule::IMPLIES_ELIM) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0].notNode(), children[0][1]); + } + if (id == PfRule::NOT_IMPLIES_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + return children[0][0][0]; + } + if (id == PfRule::NOT_IMPLIES_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + return children[0][0][1].notNode(); + } + if (id == PfRule::EQUIV_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0].notNode(), children[0][1]); + } + if (id == PfRule::EQUIV_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0], children[0][1].notNode()); + } + if (id == PfRule::NOT_EQUIV_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0], children[0][0][1]); + } + if (id == PfRule::NOT_EQUIV_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode()); + } + if (id == PfRule::XOR_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0], children[0][1]); + } + if (id == PfRule::XOR_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0].notNode(), children[0][1].notNode()); + } + if (id == PfRule::NOT_XOR_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0], children[0][0][1].notNode()); + } + if (id == PfRule::NOT_XOR_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0].notNode(), children[0][0][1]); + } + if (id == PfRule::ITE_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0].notNode(), children[0][1]); + } + if (id == PfRule::ITE_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0], children[0][2]); + } + if (id == PfRule::NOT_ITE_ELIM1) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode()); + } + if (id == PfRule::NOT_ITE_ELIM2) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, children[0][0][0], children[0][0][2].notNode()); + } + // De Morgan + if (id == PfRule::NOT_AND) + { + Assert(children.size() == 1); + Assert(args.empty()); + if (children[0].getKind() != kind::NOT + || children[0][0].getKind() != kind::AND) + { + return Node::null(); + } + std::vector disjuncts; + for (unsigned i = 0, size = children[0][0].getNumChildren(); i < size; ++i) + { + disjuncts.push_back(children[0][0][i].notNode()); + } + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + // valid clauses rules for Tseitin CNF transformation + if (id == PfRule::CNF_AND_POS) + { + Assert(children.empty()); + Assert(args.size() == 2); + uint32_t i; + if (args[0].getKind() != kind::AND || !getUInt32(args[1], i)) + { + return Node::null(); + } + if (i >= args[0].getNumChildren()) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, args[0].notNode(), args[0][i]); + } + if (id == PfRule::CNF_AND_NEG) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::AND) + { + return Node::null(); + } + std::vector disjuncts{args[0]}; + for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i) + { + disjuncts.push_back(args[0][i].notNode()); + } + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_OR_POS) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::OR) + { + return Node::null(); + } + std::vector disjuncts{args[0].notNode()}; + for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i) + { + disjuncts.push_back(args[0][i]); + } + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_OR_NEG) + { + Assert(children.empty()); + Assert(args.size() == 2); + uint32_t i; + if (args[0].getKind() != kind::OR || !getUInt32(args[1], i)) + { + return Node::null(); + } + if (i >= args[0].getNumChildren()) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, args[0], args[0][i].notNode()); + } + if (id == PfRule::CNF_IMPLIES_POS) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + std::vector disjuncts{ + args[0].notNode(), args[0][0].notNode(), args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_IMPLIES_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + std::vector disjuncts{args[0], args[0][0]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_IMPLIES_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + std::vector disjuncts{args[0], args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_EQUIV_POS1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + std::vector disjuncts{ + args[0].notNode(), args[0][0].notNode(), args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_EQUIV_POS2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + std::vector disjuncts{ + args[0].notNode(), args[0][0], args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_EQUIV_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + std::vector disjuncts{args[0], args[0][0], args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_EQUIV_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + std::vector disjuncts{ + args[0], args[0][0].notNode(), args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_XOR_POS1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + std::vector disjuncts{args[0].notNode(), args[0][0], args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_XOR_POS2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + std::vector disjuncts{ + args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_XOR_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + std::vector disjuncts{args[0], args[0][0].notNode(), args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_XOR_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + std::vector disjuncts{args[0], args[0][0], args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_POS1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector disjuncts{ + args[0].notNode(), args[0][0].notNode(), args[0][1]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_POS2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector disjuncts{args[0].notNode(), args[0][0], args[0][2]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_POS3) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector disjuncts{args[0].notNode(), args[0][1], args[0][2]}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector disjuncts{ + args[0], args[0][0].notNode(), args[0][1].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector disjuncts{args[0], args[0][0], args[0][2].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + if (id == PfRule::CNF_ITE_NEG3) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + std::vector disjuncts{ + args[0], args[0][1].notNode(), args[0][2].notNode()}; + return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); + } + // no rule + return Node::null(); +} + +} // namespace booleans +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/booleans/proof_checker.h b/src/theory/booleans/proof_checker.h new file mode 100644 index 000000000..56414ff91 --- /dev/null +++ b/src/theory/booleans/proof_checker.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file proof_checker.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Boolean proof checker utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H +#define CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H + +#include "expr/node.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" + +namespace CVC4 { +namespace theory { +namespace booleans { + +/** A checker for boolean reasoning in proofs */ +class BoolProofRuleChecker : public ProofRuleChecker +{ + public: + BoolProofRuleChecker() {} + ~BoolProofRuleChecker() {} + + /** Register all rules owned by this rule checker into pc. */ + void registerTo(ProofChecker* pc) override; + + protected: + /** Return the conclusion of the given proof step, or null if it is invalid */ + Node checkInternal(PfRule id, + const std::vector& children, + const std::vector& args) override; +}; + +} // namespace booleans +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H */