(proof-new) Add proofs for circuit propagator (#5301)

This PR adds code to generate proofs for inferences within the (non-clausal) circuit propagator.
It consists of many small methods that each implement simple derivations about single Boolean connectives. It uses already existing proof rules, and thus no separate proof checker is required.
A second PR will use these rules within the circuit propagator class.

3 files changed, 802 insertions, 0 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 29f5a57d4..4d96fa0b3 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -444,6 +444,8 @@ libcvc4_add_sources(
   theory/bags/theory_bags_type_rules.h
   theory/booleans/circuit_propagator.cpp
   theory/booleans/circuit_propagator.h
+  theory/booleans/proof_circuit_propagator.cpp
+  theory/booleans/proof_circuit_propagator.h
   theory/booleans/proof_checker.cpp
   theory/booleans/proof_checker.h
   theory/booleans/theory_bool.cpp
diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
new file mode 100644
index 000000000..bc4e0c8ae
--- /dev/null
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -0,0 +1,587 @@
+/*********************                                                        */
+/*! \file proof_circuit_propagator.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Proofs for the non-clausal circuit propagator.
+ **
+ ** Proofs for the non-clausal circuit propagator.
+ **/
+
+#include "theory/booleans/proof_circuit_propagator.h"
+
+#include "expr/proof_node_manager.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+namespace {
+
+/** Shorthand to create a Node from a constant number */
+template <typename T>
+Node mkRat(T val)
+{
+  return NodeManager::currentNM()->mkConst<Rational>(val);
+}
+
+/**
+ * Collect all children from parent except for one particular child (the
+ * "holdout"). The holdout is given as iterator, and should be an iterator into
+ * the [parent.begin(),parent.end()] range.
+ */
+inline std::vector<Node> collectButHoldout(TNode parent,
+                                           TNode::iterator holdout)
+{
+  std::vector<Node> lits;
+  for (TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end;
+       ++i)
+  {
+    if (i != holdout)
+    {
+      lits.emplace_back(*i);
+    }
+  }
+  return lits;
+}
+
+}  // namespace
+
+ProofCircuitPropagator::ProofCircuitPropagator(ProofNodeManager* pnm)
+    : d_pnm(pnm)
+{
+}
+
+bool ProofCircuitPropagator::disabled() const { return d_pnm == nullptr; }
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::assume(Node n)
+{
+  return d_pnm->mkAssume(n);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::conflict(
+    const std::shared_ptr<ProofNode>& a, const std::shared_ptr<ProofNode>& b)
+{
+  if (a->getResult().notNode() == b->getResult())
+  {
+    return mkProof(PfRule::CONTRA, {a, b});
+  }
+  Assert(a->getResult() == b->getResult().notNode());
+  return mkProof(PfRule::CONTRA, {b, a});
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::andFalse(
+    Node parent, TNode::iterator holdout)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkNot(
+      mkCResolution(mkProof(PfRule::NOT_AND, {assume(parent.notNode())}),
+                    collectButHoldout(parent, holdout),
+                    false));
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::orTrue(
+    Node parent, TNode::iterator holdout)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkCResolution(
+      assume(parent), collectButHoldout(parent, holdout), true);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::Not(bool negate, Node parent)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkNot(assume(negate ? Node(parent[0]) : parent));
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesXFromY(Node parent)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkNot(mkResolution(
+      mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[1], true));
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesYFromX(Node parent)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkResolution(
+      mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[0], false);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::eqXFromY(bool y, Node parent)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  if (y)
+  {
+    return mkProof(
+        PfRule::EQ_RESOLVE,
+        {assume(parent[1]), mkProof(PfRule::SYMM, {assume(parent)})});
+  }
+  return mkNot(mkResolution(
+      mkProof(PfRule::EQUIV_ELIM1, {assume(parent)}), parent[1], true));
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::eqYFromX(bool x, Node parent)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  if (x)
+  {
+    return mkProof(PfRule::EQ_RESOLVE, {assume(parent[0]), assume(parent)});
+  }
+  return mkNot(mkResolution(
+      mkProof(PfRule::EQUIV_ELIM2, {assume(parent)}), parent[0], true));
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::neqXFromY(bool y,
+                                                             Node parent)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkResolution(
+      mkProof(y ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
+              {assume(parent.notNode())}),
+      parent[1],
+      !y);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x,
+                                                             Node parent)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkResolution(
+      mkProof(x ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
+              {assume(parent.notNode())}),
+      parent[0],
+      !x);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::xorXFromY(bool negated,
+                                                             bool y,
+                                                             Node parent)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  if (y)
+  {
+    return mkNot(mkResolution(
+        mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM2,
+                {assume(negated ? parent.notNode() : Node(parent))}),
+        parent[1],
+        false));
+  }
+  return mkResolution(
+      mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM1,
+              {assume(negated ? parent.notNode() : Node(parent))}),
+      parent[1],
+      true);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::xorYFromX(bool negated,
+                                                             bool x,
+                                                             Node parent)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  if (x)
+  {
+    return mkResolution(
+        mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM2,
+                {assume(negated ? parent.notNode() : Node(parent))}),
+        parent[0],
+        false);
+  }
+  return mkNot(
+      mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM1,
+                           {assume(negated ? parent.notNode() : Node(parent))}),
+                   parent[0],
+                   true));
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::mkProof(
+    PfRule rule,
+    const std::vector<std::shared_ptr<ProofNode>>& children,
+    const std::vector<Node>& args)
+{
+  if (Trace.isOn("circuit-prop"))
+  {
+    std::stringstream ss;
+    ss << "Constructing (" << rule;
+    for (const auto& c : children)
+    {
+      ss << " " << *c;
+    }
+    if (!args.empty())
+    {
+      ss << " :args";
+      for (const auto& a : args)
+      {
+        ss << " " << a;
+      }
+    }
+    ss << ")";
+    Trace("circuit-prop") << ss.str() << std::endl;
+  }
+  return d_pnm->mkNode(rule, children, args);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::mkCResolution(
+    const std::shared_ptr<ProofNode>& clause,
+    const std::vector<Node>& lits,
+    const std::vector<bool>& polarity)
+{
+  auto* nm = NodeManager::currentNM();
+  std::vector<std::shared_ptr<ProofNode>> children = {clause};
+  std::vector<Node> args;
+  Assert(lits.size() == polarity.size());
+  for (std::size_t i = 0, n = lits.size(); i < n; ++i)
+  {
+    bool pol = polarity[i];
+    Node lit = lits[i];
+    if (polarity[i])
+    {
+      if (lit.getKind() == Kind::NOT)
+      {
+        lit = lit[0];
+        pol = !pol;
+        children.emplace_back(assume(lit));
+      }
+      else
+      {
+        children.emplace_back(assume(lit.notNode()));
+      }
+    }
+    else
+    {
+      children.emplace_back(assume(lit));
+    }
+    args.emplace_back(nm->mkConst(pol));
+    args.emplace_back(lit);
+  }
+  return mkProof(PfRule::CHAIN_RESOLUTION, children, args);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::mkCResolution(
+    const std::shared_ptr<ProofNode>& clause,
+    const std::vector<Node>& lits,
+    bool polarity)
+{
+  return mkCResolution(clause, lits, std::vector<bool>(lits.size(), polarity));
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::mkResolution(
+    const std::shared_ptr<ProofNode>& clause, const Node& lit, bool polarity)
+{
+  auto* nm = NodeManager::currentNM();
+  if (polarity)
+  {
+    if (lit.getKind() == Kind::NOT)
+    {
+      return mkProof(PfRule::RESOLUTION,
+                     {clause, assume(lit[0])},
+                     {nm->mkConst(false), lit[0]});
+    }
+    return mkProof(PfRule::RESOLUTION,
+                   {clause, assume(lit.notNode())},
+                   {nm->mkConst(true), lit});
+  }
+  return mkProof(
+      PfRule::RESOLUTION, {clause, assume(lit)}, {nm->mkConst(false), lit});
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagator::mkNot(
+    const std::shared_ptr<ProofNode>& n)
+{
+  Node m = n->getResult();
+  if (m.getKind() == Kind::NOT && m[0].getKind() == Kind::NOT)
+  {
+    return mkProof(PfRule::NOT_NOT_ELIM, {n});
+  }
+  return n;
+}
+
+ProofCircuitPropagatorBackward::ProofCircuitPropagatorBackward(
+    ProofNodeManager* pnm, TNode parent, bool parentAssignment)
+    : ProofCircuitPropagator(pnm),
+      d_parent(parent),
+      d_parentAssignment(parentAssignment)
+{
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::andTrue(
+    TNode::iterator i)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkProof(
+      PfRule::AND_ELIM, {assume(d_parent)}, {mkRat(i - d_parent.begin())});
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::orFalse(
+    TNode::iterator i)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkNot(mkProof(PfRule::NOT_OR_ELIM,
+                       {assume(d_parent.notNode())},
+                       {mkRat(i - d_parent.begin())}));
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteC(bool c)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  if (d_parentAssignment)
+  {
+    return mkResolution(
+        mkProof(c ? PfRule::ITE_ELIM1 : PfRule::ITE_ELIM2, {assume(d_parent)}),
+        d_parent[0],
+        !c);
+  }
+  return mkResolution(mkProof(c ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2,
+                              {assume(d_parent.notNode())}),
+                      d_parent[0],
+                      !c);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  if (d_parentAssignment)
+  {
+    return mkResolution(
+        mkProof(PfRule::ITE_ELIM2, {assume(d_parent)}), d_parent[c + 1], false);
+  }
+  return mkResolution(
+      mkProof(PfRule::NOT_ITE_ELIM2, {assume(d_parent.notNode())}),
+      d_parent[c + 1],
+      false);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegX()
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkNot(
+      mkProof(PfRule::NOT_IMPLIES_ELIM1, {assume(d_parent.notNode())}));
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegY()
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkNot(
+      mkProof(PfRule::NOT_IMPLIES_ELIM2, {assume(d_parent.notNode())}));
+}
+
+ProofCircuitPropagatorForward::ProofCircuitPropagatorForward(
+    ProofNodeManager* pnm, Node child, bool childAssignment, Node parent)
+    : ProofCircuitPropagator{pnm},
+      d_child(child),
+      d_childAssignment(childAssignment),
+      d_parent(parent)
+{
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andAllTrue()
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  std::vector<std::shared_ptr<ProofNode>> children;
+  for (const auto& child : d_parent)
+  {
+    children.emplace_back(assume(child));
+  }
+  return mkProof(PfRule::AND_INTRO, children);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andOneFalse()
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  auto it = std::find(d_parent.begin(), d_parent.end(), d_child);
+  return mkResolution(
+      mkProof(
+          PfRule::CNF_AND_POS, {}, {d_parent, mkRat(it - d_parent.begin())}),
+      d_child,
+      true);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orOneTrue()
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  auto it = std::find(d_parent.begin(), d_parent.end(), d_child);
+  return mkNot(mkResolution(
+      mkProof(PfRule::CNF_OR_NEG, {}, {d_parent, mkRat(it - d_parent.begin())}),
+      d_child,
+      false));
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orFalse()
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  std::vector<Node> children(d_parent.begin(), d_parent.end());
+  return mkCResolution(
+      mkProof(PfRule::CNF_OR_POS, {}, {d_parent}), children, true);
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalThen(bool x)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkCResolution(
+      mkProof(x ? PfRule::CNF_ITE_NEG1 : PfRule::CNF_ITE_POS1, {}, {d_parent}),
+      {d_parent[0], d_parent[1]},
+      {false, !x});
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalElse(bool y)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  return mkCResolution(
+      mkProof(y ? PfRule::CNF_ITE_NEG2 : PfRule::CNF_ITE_POS2, {}, {d_parent}),
+      {d_parent[0], d_parent[2]},
+      {true, !y});
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::eqEval(bool x, bool y)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  if (x == y)
+  {
+    return mkCResolution(
+        mkProof(x ? PfRule::CNF_EQUIV_NEG2 : PfRule::CNF_EQUIV_NEG1,
+                {},
+                {d_parent}),
+        {d_parent[0], d_parent[1]},
+        {!x, !y});
+  }
+  return mkCResolution(
+      mkProof(
+          x ? PfRule::CNF_EQUIV_POS1 : PfRule::CNF_EQUIV_POS2, {}, {d_parent}),
+      {d_parent[0], d_parent[1]},
+      {!x, !y});
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::impliesEval(
+    bool premise, bool conclusion)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  if (!premise)
+  {
+    return mkResolution(
+        mkProof(PfRule::CNF_IMPLIES_NEG1, {}, {d_parent}), d_parent[0], true);
+  }
+  if (conclusion)
+  {
+    return mkResolution(
+        mkProof(PfRule::CNF_IMPLIES_NEG2, {}, {d_parent}), d_parent[1], false);
+  }
+  return mkCResolution(mkProof(PfRule::CNF_IMPLIES_POS, {}, {d_parent}),
+                       {d_parent[0], d_parent[1]},
+                       {false, true});
+}
+
+std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::xorEval(bool x,
+                                                                  bool y)
+{
+  if (disabled())
+  {
+    return nullptr;
+  }
+  if (x && y)
+  {
+    return mkCResolution(mkProof(PfRule::CNF_XOR_POS2, {}, {d_parent}),
+                         {d_parent[0], d_parent[1]},
+                         {false, false});
+  }
+  else if (x && !y)
+  {
+    return mkCResolution(mkProof(PfRule::CNF_XOR_NEG1, {}, {d_parent}),
+                         {d_parent[0], d_parent[1]},
+                         {false, true});
+  }
+  else if (!x && y)
+  {
+    return mkCResolution(mkProof(PfRule::CNF_XOR_NEG2, {}, {d_parent}),
+                         {d_parent[0], d_parent[1]},
+                         {true, false});
+  }
+  Assert(!x && !y);
+  return mkCResolution(mkProof(PfRule::CNF_XOR_POS1, {}, {d_parent}),
+                       {d_parent[0], d_parent[1]},
+                       {true, true});
+}
+
+}  // namespace booleans
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/booleans/proof_circuit_propagator.h b/src/theory/booleans/proof_circuit_propagator.h
new file mode 100644
index 000000000..cc0aaad36
--- /dev/null
+++ b/src/theory/booleans/proof_circuit_propagator.h
@@ -0,0 +1,213 @@
+/*********************                                                        */
+/*! \file proof_circuit_propagator.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Proofs for the non-clausal circuit propagator.
+ **
+ ** Proofs for the non-clausal circuit propagator.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
+#define CVC4__THEORY__BOOLEANS__PROOF_CIRCUIT_PROPAGATOR_H
+
+#include <memory>
+
+#include "expr/node.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace booleans {
+
+/**
+ * Base class for for CircuitPropagatorProofs.
+ * This class collects common functionality for proofs of backward and forward
+ * propagation.
+ */
+class ProofCircuitPropagator
+{
+ public:
+  ProofCircuitPropagator(ProofNodeManager* pnm);
+
+  /** Assuming the given node */
+  std::shared_ptr<ProofNode> assume(Node n);
+  /** Apply CONTRA rule. Takes care of switching a and b if necessary */
+  std::shared_ptr<ProofNode> conflict(const std::shared_ptr<ProofNode>& a,
+                                      const std::shared_ptr<ProofNode>& b);
+
+  /** (and true ... holdout true ...)  -->  holdout */
+  std::shared_ptr<ProofNode> andFalse(Node parent, TNode::iterator holdout);
+
+  /** (or false ... holdout false ...)  ->  holdout */
+  std::shared_ptr<ProofNode> orTrue(Node parent, TNode::iterator holdout);
+
+  /** (not x) is true  -->  x is false (and vice versa) */
+  std::shared_ptr<ProofNode> Not(bool negate, Node parent);
+
+  /** (=> X false)  -->  (not X) */
+  std::shared_ptr<ProofNode> impliesXFromY(Node parent);
+  /** (=> true Y)  -->  Y */
+  std::shared_ptr<ProofNode> impliesYFromX(Node parent);
+
+  /** Derive X from (= X Y) */
+  std::shared_ptr<ProofNode> eqXFromY(bool y, Node parent);
+  /** Derive Y from (= X Y) */
+  std::shared_ptr<ProofNode> eqYFromX(bool x, Node parent);
+  /** Derive X from (not (= X Y)) */
+  std::shared_ptr<ProofNode> neqXFromY(bool y, Node parent);
+  /** Derive Y from (not (= X Y)) */
+  std::shared_ptr<ProofNode> neqYFromX(bool x, Node parent);
+
+  /**
+   * Uses (xor X Y) to derive the value of X.
+   * (xor X false)  -->  X
+   * (xor X true)  -->  (not X)
+   * (not (xor X false))  -->  (not X)
+   * (not (xor X true))  -->  X
+   */
+  std::shared_ptr<ProofNode> xorXFromY(bool negated, bool y, Node parent);
+  /**
+   * Uses (xor X Y) to derive the value of Y.
+   * (xor false Y)  -->  Y
+   * (xor true Y)  -->  (not Y)
+   * (not (xor false Y))  -->  (not Y)
+   * (not (xor true Y))  -->  Y
+   */
+  std::shared_ptr<ProofNode> xorYFromX(bool negated, bool x, Node parent);
+
+ protected:
+  /** Shorthand to check whether proof generation is disabled */
+  bool disabled() const;
+
+  /** Construct proof using the given rule, children and args */
+  std::shared_ptr<ProofNode> mkProof(
+      PfRule rule,
+      const std::vector<std::shared_ptr<ProofNode>>& children,
+      const std::vector<Node>& args = {});
+  /**
+   * Apply CHAIN_RESOLUTION rule.
+   * Constructs the args from the given literals and polarities (called ids in
+   * the proof rule). Automatically adds the clauses to resolve with as
+   * assumptions, depending on their polarity.
+   */
+  std::shared_ptr<ProofNode> mkCResolution(
+      const std::shared_ptr<ProofNode>& clause,
+      const std::vector<Node>& lits,
+      const std::vector<bool>& polarity);
+  /** Shorthand for mkCResolution(clause, lits, {polarity, ...}) */
+  std::shared_ptr<ProofNode> mkCResolution(
+      const std::shared_ptr<ProofNode>& clause,
+      const std::vector<Node>& lits,
+      bool polarity);
+  /** Apply RESOLUTION rule */
+  std::shared_ptr<ProofNode> mkResolution(
+      const std::shared_ptr<ProofNode>& clause, const Node& lit, bool polarity);
+  /** Apply NOT_NOT_ELIM rule if n.getResult() is a nested negation */
+  std::shared_ptr<ProofNode> mkNot(const std::shared_ptr<ProofNode>& n);
+
+  /** The proof node manager */
+  ProofNodeManager* d_pnm;
+};
+
+/**
+ * Proof generator for backward propagation
+ * A backward propagation is triggered by the assignment of the parent node.
+ */
+class ProofCircuitPropagatorBackward : public ProofCircuitPropagator
+{
+ public:
+  ProofCircuitPropagatorBackward(ProofNodeManager* pnm,
+                                 TNode parent,
+                                 bool parentAssignment);
+
+  /** and true  -->  child is true */
+  std::shared_ptr<ProofNode> andTrue(TNode::iterator i);
+
+  /** or false  -->  child is false */
+  std::shared_ptr<ProofNode> orFalse(TNode::iterator i);
+
+  /**
+   * Propagate on ite with evaluate condition
+   * (ite true t e)  -->  t
+   * (not (ite true t e))  -->  (not t)
+   * (ite false t e)  -->  e
+   * (not (ite false t e))  -->  (not e)
+   */
+  std::shared_ptr<ProofNode> iteC(bool c);
+  /**
+   * For (ite c t e), we can derive the value for c
+   * c = 1: c = true
+   * c = 0: c = false
+   */
+  std::shared_ptr<ProofNode> iteIsCase(unsigned c);
+
+  /** (not (=> X Y))  -->  X */
+  std::shared_ptr<ProofNode> impliesNegX();
+  /** (not (=> X Y))  -->  (not Y) */
+  std::shared_ptr<ProofNode> impliesNegY();
+
+ private:
+  /** The parent node */
+  TNode d_parent;
+  /** The assignment of d_parent */
+  bool d_parentAssignment;
+};
+
+/**
+ * Proof generator for forward propagation
+ * A forward propagation is triggered by the assignment of a child node.
+ */
+class ProofCircuitPropagatorForward : public ProofCircuitPropagator
+{
+ public:
+  ProofCircuitPropagatorForward(ProofNodeManager* pnm,
+                                Node child,
+                                bool childAssignment,
+                                Node parent);
+
+  /** All children are true  -->  and is true */
+  std::shared_ptr<ProofNode> andAllTrue();
+  /** One child is false  -->  and is false */
+  std::shared_ptr<ProofNode> andOneFalse();
+
+  /** One child is true  -->  or is true */
+  std::shared_ptr<ProofNode> orOneTrue();
+  /** or false  -->  all children are false */
+  std::shared_ptr<ProofNode> orFalse();
+
+  /** Evaluate (ite true X _) from X */
+  std::shared_ptr<ProofNode> iteEvalThen(bool x);
+  /** Evaluate (ite false _ Y) from Y */
+  std::shared_ptr<ProofNode> iteEvalElse(bool y);
+
+  /** Evaluate (= X Y) from X,Y */
+  std::shared_ptr<ProofNode> eqEval(bool x, bool y);
+
+  /** Evaluate (=> X Y) from X,Y */
+  std::shared_ptr<ProofNode> impliesEval(bool premise, bool conclusion);
+  /** Evaluate (xor X Y) from X,Y */
+  std::shared_ptr<ProofNode> xorEval(bool x, bool y);
+
+ private:
+  /** The current child that triggered the propagations */
+  Node d_child;
+  /** The assignment of d_child */
+  bool d_childAssignment;
+  /** The parent node used for propagation */
+  Node d_parent;
+};
+
+}  // namespace booleans
+}  // namespace theory
+}  // namespace CVC4
+
+#endif