// 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
// ---------------------------------------------------------------
// 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.
// 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,
};
--- /dev/null
+/********************* */
+/*! \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<Node>& children,
+ const std::vector<Node>& 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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
projects / cvc5.git / commitdiff