summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/proof_rule.cpp24
-rw-r--r--src/expr/proof_rule.h135
-rw-r--r--src/theory/booleans/proof_checker.cpp297
3 files changed, 456 insertions, 0 deletions
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..37f8d209d 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(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,
@@ -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,280 @@ 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<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 || !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<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 || !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();
+ }
+ 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();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback