(proof-new) Adding rules and proof checker for Boolean reasoning (#4560)

5 files changed, 922 insertions, 2 deletions

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<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
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<Node>& children,
+                     const std::vector<Node>& args) override;
+};
+
+}  // namespace booleans
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__BOOLEANS__PROOF_CHECKER_H */