From 904ac98847d99e54223a41b24ff83eeea139bfac Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Mon, 18 May 2020 23:11:16 -0300 Subject: adding cnf rules and their checkers --- src/expr/proof_rule.cpp | 24 +++ src/expr/proof_rule.h | 135 ++++++++++++++++ src/theory/booleans/proof_checker.cpp | 291 ++++++++++++++++++++++++++++++++++ 3 files changed, 450 insertions(+) diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index c2b5d31b1..438ed8056 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -54,6 +54,30 @@ const char* toString(PfRule id) 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"; + //================================================= 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"; //================================================= Equality rules case PfRule::REFL: return "REFL"; case PfRule::SYMM: return "SYMM"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index f45ff3544..af5a8f6d9 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -290,6 +290,141 @@ enum class PfRule : uint32_t // Conclusion: (or C (not F2)) NOT_ITE_ELIM2, + //================================================= 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, + //================================================= Equality rules // ======== Reflexive // Children: none diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 48ea256a5..8d0e4c849 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -38,6 +38,28 @@ void BoolProofRuleChecker::registerTo(ProofChecker* pc) 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(CNF_AND_POS, this); + pc->registerChecker(CNF_AND_NEG, this); + pc->registerChecker(CNF_OR_POS, this); + pc->registerChecker(CNF_OR_NEG, this); + pc->registerChecker(CNF_IMPLIES_POS, this); + pc->registerChecker(CNF_IMPLIES_NEG1G1, this); + pc->registerChecker(CNF_IMPLIES_NEG2G2, this); + pc->registerChecker(CNF_EQUIV_POS1, this); + pc->registerChecker(CNF_EQUIV_POS2, this); + pc->registerChecker(CNF_EQUIV_NEG1, this); + pc->registerChecker(CNF_EQUIV_NEG2, this); + pc->registerChecker(CNF_XOR_POS1, this); + pc->registerChecker(CNF_XOR_POS2, this); + pc->registerChecker(CNF_XOR_NEG1, this); + pc->registerChecker(CNF_XOR_NEG2, this); + pc->registerChecker(CNF_ITE_POS1, this); + pc->registerChecker(CNF_ITE_POS2, this); + pc->registerChecker(CNF_ITE_POS3, this); + pc->registerChecker(CNF_ITE_NEG1, this); + pc->registerChecker(CNF_ITE_NEG2, this); + pc->registerChecker(CNF_ITE_NEG3, this); } Node BoolProofRuleChecker::checkInternal(PfRule id, @@ -51,6 +73,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, return NodeManager::currentNM()->mkNode( kind::OR, args[0], args[0].notNode()); } + // natural deduction rules if (id == PfRule::AND_ELIM) { Assert(children.size() == 1); @@ -253,6 +276,274 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, 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 || !getIndex(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); + uint32_t i; + 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 || !getIndex(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(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0].notNode(), args[0][0].notNode(), args[0][1]}); + } + if (id == PfRule::CNF_IMPLIES_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode(kind::OR, {args[0], args[0][0]}); + } + if (id == PfRule::CNF_IMPLIES_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::IMPLIES) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode(kind::OR, + {args[0], args[0][1].notNode()}); + } + if (id == PfRule::CNF_EQUIV_POS1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0].notNode(), args[0][0].notNode(), args[0][1]}); + } + if (id == PfRule::CNF_EQUIV_POS2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0].notNode(), args[0][0], args[0][1].notNode()}); + } + if (id == PfRule::CNF_EQUIV_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode(kind::OR, + {args[0], args[0][0], args[0][1]}); + } + if (id == PfRule::CNF_EQUIV_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::EQUAL) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0], args[0][0].notNode(), args[0][1].notNode()}); + } + if (id == PfRule::CNF_XOR_POS1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0].notNode(), args[0][0], args[0][1]}); + } + if (id == PfRule::CNF_XOR_POS2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, + {args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()}); + } + if (id == PfRule::CNF_XOR_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0], args[0][0].notNode(), args[0][1]}); + } + if (id == PfRule::CNF_XOR_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::XOR) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0], args[0][0], args[0][1].notNode()}); + } + if (id == PfRule::CNF_ITE_POS1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0].notNode(), args[0][0].notNode(), args[0][1]}); + } + if (id == PfRule::CNF_ITE_POS2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0].notNode(), args[0][0], args[0][2]}); + } + if (id == PfRule::CNF_ITE_POS3) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0].notNode(), args[0][1], args[0][2]}); + } + if (id == PfRule::CNF_ITE_NEG1) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0], args[0][0].notNode(), args[0][1].notNode()}); + } + if (id == PfRule::CNF_ITE_NEG2) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0], args[0][0], args[0][2].notNode()}); + } + if (id == PfRule::CNF_ITE_NEG3) + { + Assert(children.empty()); + Assert(args.size() == 1); + if (args[0].getKind() != kind::ITE) + { + return Node::null(); + } + return NodeManager::currentNM()->mkNode( + kind::OR, {args[0], args[0][1].notNode(), args[0][2].notNode()}); + } // no rule return Node::null(); } -- cgit v1.2.3