From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 21 Oct 2020 23:19:24 +0000 (+0200)
Subject: (proof-new) Make circuit propagator proof producing (#5318)
X-Git-Tag: cvc5-1.0.0~2672
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a99f5aaa46702a4894aaddeed3a7ff5cbf69bdfd;p=cvc5.git

(proof-new) Make circuit propagator proof producing (#5318)

This PR uses the proofs from #5301 to actually produce proofs from the circuit propagator.
---

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index a3650c988..2b788098a 100644
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -93,7 +93,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   }
 
   Trace("non-clausal-simplify") << "propagating" << std::endl;
-  if (propagator->propagate())
+  TrustNode conf = propagator->propagate();
+  if (!conf.isNull())
   {
     // If in conflict, just return false
     Trace("non-clausal-simplify")
@@ -122,11 +123,11 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   SubstitutionMap& newSubstitutions = tnewSubstituions.get();
   SubstitutionMap::iterator pos;
   size_t j = 0;
-  std::vector<Node>& learned_literals = propagator->getLearnedLiterals();
+  std::vector<TrustNode>& learned_literals = propagator->getLearnedLiterals();
   for (size_t i = 0, size = learned_literals.size(); i < size; ++i)
   {
     // Simplify the literal we learned wrt previous substitutions
-    Node learnedLiteral = learned_literals[i];
+    Node learnedLiteral = learned_literals[i].getNode();
     Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
     Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral);
     Trace("non-clausal-simplify")
@@ -164,7 +165,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
       {
         // If the learned literal simplifies to false, we're in conflict
         Trace("non-clausal-simplify")
-            << "conflict with " << learned_literals[i] << std::endl;
+            << "conflict with " << learned_literals[i].getNode() << std::endl;
         Assert(!options::unsatCores());
         assertionsToPreprocess->clear();
         Node n = NodeManager::currentNM()->mkConst<bool>(false);
@@ -385,7 +386,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
 
   for (size_t i = 0; i < learned_literals.size(); ++i)
   {
-    Node learned = learned_literals[i];
+    Node learned = learned_literals[i].getNode();
     Assert(top_level_substs.apply(learned) == learned);
     Node learnedNew = newSubstitutions.apply(learned);
     if (learned != learnedNew)
@@ -452,7 +453,6 @@ PreprocessingPassResult NonClausalSimp::applyInternal(
   return PreprocessingPassResult::NO_CONFLICT;
 }  // namespace passes
 
-
 /* -------------------------------------------------------------------------- */
 
 }  // namespace passes
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index f49c41346..270c0b9a9 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -16,11 +16,12 @@
 
 #include "theory/booleans/circuit_propagator.h"
 
+#include <algorithm>
 #include <stack>
 #include <vector>
-#include <algorithm>
 
 #include "expr/node_algorithm.h"
+#include "theory/booleans/proof_circuit_propagator.h"
 #include "util/utility.h"
 
 using namespace std;
@@ -29,29 +30,167 @@ namespace CVC4 {
 namespace theory {
 namespace booleans {
 
+CircuitPropagator::CircuitPropagator(bool enableForward, bool enableBackward)
+    : d_context(),
+      d_propagationQueue(),
+      d_propagationQueueClearer(&d_context, d_propagationQueue),
+      d_conflict(&d_context, TrustNode()),
+      d_learnedLiterals(),
+      d_learnedLiteralClearer(&d_context, d_learnedLiterals),
+      d_backEdges(),
+      d_backEdgesClearer(&d_context, d_backEdges),
+      d_seen(&d_context),
+      d_state(&d_context),
+      d_forwardPropagation(enableForward),
+      d_backwardPropagation(enableBackward),
+      d_needsFinish(false),
+      d_pnm(nullptr),
+      d_epg(nullptr),
+      d_proofInternal(nullptr),
+      d_proofExternal(nullptr)
+{
+}
+
+void CircuitPropagator::finish()
+{
+  Trace("circuit-prop") << "FINISH" << std::endl;
+  d_context.pop();
+}
+
 void CircuitPropagator::assertTrue(TNode assertion)
 {
-  if (assertion.getKind() == kind::AND) {
-    for (unsigned i = 0; i < assertion.getNumChildren(); ++ i) {
-      assertTrue(assertion[i]);
+  Trace("circuit-prop") << "TRUE: " << assertion << std::endl;
+  if (assertion.getKind() == kind::CONST_BOOLEAN && !assertion.getConst<bool>())
+  {
+    makeConflict(assertion);
+  }
+  else if (assertion.getKind() == kind::AND)
+  {
+    ProofCircuitPropagatorBackward prover{d_pnm, assertion, true};
+    if (isProofEnabled())
+    {
+      addProof(assertion, prover.assume(assertion));
+    }
+    for (auto it = assertion.begin(); it != assertion.end(); ++it)
+    {
+      addProof(*it, prover.andTrue(it));
+      assertTrue(*it);
     }
-  } else {
+  }
+  else
+  {
     // Analyze the assertion for back-edges and all that
     computeBackEdges(assertion);
     // Assign the given assertion to true
-    assignAndEnqueue(assertion, true);
+    if (isProofEnabled())
+    {
+      assignAndEnqueue(assertion, true, d_pnm->mkAssume(assertion));
+    }
+    else
+    {
+      assignAndEnqueue(assertion, true, nullptr);
+    }
   }
 }
 
-void CircuitPropagator::computeBackEdges(TNode node) {
+void CircuitPropagator::assignAndEnqueue(TNode n,
+                                         bool value,
+                                         std::shared_ptr<ProofNode> proof)
+{
+  Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", "
+                        << (value ? "true" : "false") << ")" << std::endl;
+
+  if (n.getKind() == kind::CONST_BOOLEAN)
+  {
+    // Assigning a constant to the opposite value is dumb
+    if (value != n.getConst<bool>())
+    {
+      makeConflict(n);
+      return;
+    }
+  }
 
-  Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")" << endl;
+  if (isProofEnabled())
+  {
+    if (proof == nullptr)
+    {
+      Warning() << "CircuitPropagator: Proof is missing for " << n << std::endl;
+      Assert(false);
+    }
+    else
+    {
+      Assert(!proof->getResult().isNull());
+      Node expected = value ? Node(n) : n.negate();
+      if (proof->getResult() != expected)
+      {
+        Warning() << "CircuitPropagator: Incorrect proof: " << expected
+                  << " vs. " << proof->getResult() << std::endl
+                  << *proof << std::endl;
+      }
+      addProof(expected, std::move(proof));
+    }
+  }
+
+  // Get the current assignment
+  AssignmentStatus state = d_state[n];
+
+  if (state != UNASSIGNED)
+  {
+    // If the node is already assigned we might have a conflict
+    if (value != (state == ASSIGNED_TO_TRUE))
+    {
+      makeConflict(n);
+    }
+  }
+  else
+  {
+    // If unassigned, mark it as assigned
+    d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
+    // Add for further propagation
+    d_propagationQueue.push_back(n);
+  }
+}
+
+void CircuitPropagator::makeConflict(Node n)
+{
+  auto bfalse = NodeManager::currentNM()->mkConst(false);
+  ProofGenerator* g = nullptr;
+  if (isProofEnabled())
+  {
+    if (d_epg->hasProofFor(bfalse))
+    {
+      return;
+    }
+    ProofCircuitPropagator pcp(d_pnm);
+    if (n == bfalse)
+    {
+      d_epg->setProofFor(bfalse, pcp.assume(bfalse));
+    }
+    else
+    {
+      d_epg->setProofFor(bfalse,
+                         pcp.conflict(pcp.assume(n), pcp.assume(n.negate())));
+    }
+    g = d_proofInternal.get();
+    Trace("circuit-prop") << "Added conflict " << *d_epg->getProofFor(bfalse)
+                          << std::endl;
+    Trace("circuit-prop") << "\texpanded " << *g->getProofFor(bfalse)
+                          << std::endl;
+  }
+  d_conflict = TrustNode::mkTrustLemma(bfalse, g);
+}
+
+void CircuitPropagator::computeBackEdges(TNode node)
+{
+  Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")"
+                        << endl;
 
   // Vector of nodes to visit
   vector<TNode> toVisit;
 
   // Start with the top node
-  if (d_seen.find(node) == d_seen.end()) {
+  if (d_seen.find(node) == d_seen.end())
+  {
     toVisit.push_back(node);
     d_seen.insert(node);
   }
@@ -60,20 +199,28 @@ void CircuitPropagator::computeBackEdges(TNode node) {
   d_backEdges[node];
 
   // Go through the visit list
-  for (unsigned i = 0; i < toVisit.size(); ++ i) {
+  for (unsigned i = 0; i < toVisit.size(); ++i)
+  {
     // Node we need to visit
     TNode current = toVisit[i];
-    Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(): processing " << current << endl;
+    Debug("circuit-prop")
+        << "CircuitPropagator::computeBackEdges(): processing " << current
+        << endl;
     Assert(d_seen.find(current) != d_seen.end());
 
     // If this not an atom visit all the children and compute the back edges
-    if (Theory::theoryOf(current) == THEORY_BOOL) {
-      for (unsigned child = 0, child_end = current.getNumChildren(); child < child_end; ++ child) {
+    if (Theory::theoryOf(current) == THEORY_BOOL)
+    {
+      for (unsigned child = 0, child_end = current.getNumChildren();
+           child < child_end;
+           ++child)
+      {
         TNode childNode = current[child];
         // Add the back edge
         d_backEdges[childNode].push_back(current);
         // Add to the queue if not seen yet
-        if (d_seen.find(childNode) == d_seen.end()) {
+        if (d_seen.find(childNode) == d_seen.end())
+        {
           toVisit.push_back(childNode);
           d_seen.insert(childNode);
         }
@@ -82,124 +229,204 @@ void CircuitPropagator::computeBackEdges(TNode node) {
   }
 }
 
-void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) {
-
-  Debug("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent << ", " << parentAssignment << ")" << endl;
+void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment)
+{
+  Debug("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent
+                        << ", " << parentAssignment << ")" << endl;
+  ProofCircuitPropagatorBackward prover{d_pnm, parent, parentAssignment};
 
   // backward rules
-  switch(parent.getKind()) {
-  case kind::AND:
-    if (parentAssignment) {
-      // AND = TRUE: forall children c, assign(c = TRUE)
-      for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) {
-        assignAndEnqueue(*i, true);
+  switch (parent.getKind())
+  {
+    case kind::AND:
+      if (parentAssignment)
+      {
+        // AND = TRUE: forall children c, assign(c = TRUE)
+        for (TNode::iterator i = parent.begin(), i_end = parent.end();
+             i != i_end;
+             ++i)
+        {
+          assignAndEnqueue(*i, true, prover.andTrue(i));
+        }
       }
-    } else {
-      // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE)
-      TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, true)));
-      if (holdout != parent.end()) {
-        assignAndEnqueue(*holdout, false);
+      else
+      {
+        // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE)
+        TNode::iterator holdout = find_if_unique(
+            parent.begin(), parent.end(), not1(IsAssignedTo(*this, true)));
+        if (holdout != parent.end())
+        {
+          assignAndEnqueue(*holdout, false, prover.andFalse(parent, holdout));
+        }
       }
-    }
-    break;
-  case kind::OR:
-    if (parentAssignment) {
-      // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE)
-      TNode::iterator holdout = find_if_unique(parent.begin(), parent.end(), not1(IsAssignedTo(*this, false)));
-      if (holdout != parent.end()) {
-        assignAndEnqueue(*holdout, true);
+      break;
+    case kind::OR:
+      if (parentAssignment)
+      {
+        // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE)
+        TNode::iterator holdout = find_if_unique(
+            parent.begin(), parent.end(), not1(IsAssignedTo(*this, false)));
+        if (holdout != parent.end())
+        {
+          assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout));
+        }
       }
-    } else {
-      // OR = FALSE: forall children c, assign(c = FALSE)
-      for(TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; ++i) {
-        assignAndEnqueue(*i, false);
+      else
+      {
+        // OR = FALSE: forall children c, assign(c = FALSE)
+        for (TNode::iterator i = parent.begin(), i_end = parent.end();
+             i != i_end;
+             ++i)
+        {
+          assignAndEnqueue(*i, false, prover.orFalse(i));
+        }
       }
-    }
-    break;
-  case kind::NOT:
-    // NOT = b: assign(c = !b)
-    assignAndEnqueue(parent[0], !parentAssignment);
-    break;
-  case kind::ITE:
-    if (isAssignedTo(parent[0], true)) {
-      // ITE c x y = v: if c is assigned and TRUE, assign(x = v)
-      assignAndEnqueue(parent[1], parentAssignment);
-    } else if (isAssignedTo(parent[0], false)) {
-      // ITE c x y = v: if c is assigned and FALSE, assign(y = v)
-      assignAndEnqueue(parent[2], parentAssignment);
-    } else if (isAssigned(parent[1]) && isAssigned(parent[2])) {
-      if (getAssignment(parent[1]) == parentAssignment && getAssignment(parent[2]) != parentAssignment) {
-        // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and y!=v, assign(c = TRUE)
-        assignAndEnqueue(parent[0], true);
-      } else if (getAssignment(parent[1]) != parentAssignment && getAssignment(parent[2]) == parentAssignment) {
-        // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and y==v, assign(c = FALSE)
-        assignAndEnqueue(parent[0], false);
+      break;
+    case kind::NOT:
+      // NOT = b: assign(c = !b)
+      assignAndEnqueue(
+          parent[0], !parentAssignment, prover.Not(!parentAssignment, parent));
+      break;
+    case kind::ITE:
+      if (isAssignedTo(parent[0], true))
+      {
+        // ITE c x y = v: if c is assigned and TRUE, assign(x = v)
+        assignAndEnqueue(parent[1], parentAssignment, prover.iteC(true));
       }
-    }
-    break;
-  case kind::EQUAL:
-    Assert(parent[0].getType().isBoolean());
-    if (parentAssignment) {
-      // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment])
-      if (isAssigned(parent[0])) {
-        assignAndEnqueue(parent[1], getAssignment(parent[0]));
-      } else if (isAssigned(parent[1])) {
-        assignAndEnqueue(parent[0], getAssignment(parent[1]));
+      else if (isAssignedTo(parent[0], false))
+      {
+        // ITE c x y = v: if c is assigned and FALSE, assign(y = v)
+        assignAndEnqueue(parent[2], parentAssignment, prover.iteC(false));
       }
-    } else {
-      // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment [resp x = !y.assignment])
-      if (isAssigned(parent[0])) {
-        assignAndEnqueue(parent[1], !getAssignment(parent[0]));
-      } else if (isAssigned(parent[1])) {
-        assignAndEnqueue(parent[0], !getAssignment(parent[1]));
+      else if (isAssigned(parent[1]) && isAssigned(parent[2]))
+      {
+        if (getAssignment(parent[1]) == parentAssignment
+            && getAssignment(parent[2]) != parentAssignment)
+        {
+          // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and
+          // y!=v, assign(c = TRUE)
+          assignAndEnqueue(parent[0], true, prover.iteIsCase(1));
+        }
+        else if (getAssignment(parent[1]) != parentAssignment
+                 && getAssignment(parent[2]) == parentAssignment)
+        {
+          // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and
+          // y==v, assign(c = FALSE)
+          assignAndEnqueue(parent[0], false, prover.iteIsCase(0));
+        }
       }
-    }
-    break;
-  case kind::IMPLIES:
-    if (parentAssignment) {
-      if (isAssignedTo(parent[0], true)) {
-        // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE)
-        assignAndEnqueue(parent[1], true);
+      break;
+    case kind::EQUAL:
+      Assert(parent[0].getType().isBoolean());
+      if (parentAssignment)
+      {
+        // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment
+        // [resp x = y.assignment])
+        if (isAssigned(parent[0]))
+        {
+          assignAndEnqueue(parent[1],
+                           getAssignment(parent[0]),
+                           prover.eqYFromX(getAssignment(parent[0]), parent));
+        }
+        else if (isAssigned(parent[1]))
+        {
+          assignAndEnqueue(parent[0],
+                           getAssignment(parent[1]),
+                           prover.eqXFromY(getAssignment(parent[1]), parent));
+        }
       }
-      if (isAssignedTo(parent[1], false)) {
-        // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE)
-        assignAndEnqueue(parent[0], false);
+      else
+      {
+        // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment
+        // [resp x = !y.assignment])
+        if (isAssigned(parent[0]))
+        {
+          assignAndEnqueue(parent[1],
+                           !getAssignment(parent[0]),
+                           prover.neqYFromX(getAssignment(parent[0]), parent));
+        }
+        else if (isAssigned(parent[1]))
+        {
+          assignAndEnqueue(parent[0],
+                           !getAssignment(parent[1]),
+                           prover.neqXFromY(getAssignment(parent[1]), parent));
+        }
       }
-    } else {
-      // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE)
-      assignAndEnqueue(parent[0], true);
-      assignAndEnqueue(parent[1], false);
-    }
-    break;
-  case kind::XOR:
-    if (parentAssignment) {
-      if (isAssigned(parent[0])) {
-        // XOR x y = TRUE, and x assigned, assign(y = !assignment(x))
-        assignAndEnqueue(parent[1], !getAssignment(parent[0]));
-      } else if (isAssigned(parent[1])) {
-        // XOR x y = TRUE, and y assigned, assign(x = !assignment(y))
-        assignAndEnqueue(parent[0], !getAssignment(parent[1]));
+      break;
+    case kind::IMPLIES:
+      if (parentAssignment)
+      {
+        if (isAssignedTo(parent[0], true))
+        {
+          // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE)
+          assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent));
+        }
+        if (isAssignedTo(parent[1], false))
+        {
+          // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE)
+          assignAndEnqueue(parent[0], false, prover.impliesXFromY(parent));
+        }
       }
-    } else {
-      if (isAssigned(parent[0])) {
-        // XOR x y = FALSE, and x assigned, assign(y = assignment(x))
-        assignAndEnqueue(parent[1], getAssignment(parent[0]));
-      } else if (isAssigned(parent[1])) {
-        // XOR x y = FALSE, and y assigned, assign(x = assignment(y))
-        assignAndEnqueue(parent[0], getAssignment(parent[1]));
+      else
+      {
+        // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE)
+        assignAndEnqueue(parent[0], true, prover.impliesNegX());
+        assignAndEnqueue(parent[1], false, prover.impliesNegY());
       }
-    }
-    break;
-  default:
-    Unhandled();
+      break;
+    case kind::XOR:
+      if (parentAssignment)
+      {
+        if (isAssigned(parent[0]))
+        {
+          // XOR x y = TRUE, and x assigned, assign(y = !assignment(x))
+          assignAndEnqueue(
+              parent[1],
+              !getAssignment(parent[0]),
+              prover.xorYFromX(
+                  !parentAssignment, getAssignment(parent[0]), parent));
+        }
+        else if (isAssigned(parent[1]))
+        {
+          // XOR x y = TRUE, and y assigned, assign(x = !assignment(y))
+          assignAndEnqueue(
+              parent[0],
+              !getAssignment(parent[1]),
+              prover.xorXFromY(
+                  !parentAssignment, getAssignment(parent[1]), parent));
+        }
+      }
+      else
+      {
+        if (isAssigned(parent[0]))
+        {
+          // XOR x y = FALSE, and x assigned, assign(y = assignment(x))
+          assignAndEnqueue(
+              parent[1],
+              getAssignment(parent[0]),
+              prover.xorYFromX(
+                  !parentAssignment, getAssignment(parent[0]), parent));
+        }
+        else if (isAssigned(parent[1]))
+        {
+          // XOR x y = FALSE, and y assigned, assign(x = assignment(y))
+          assignAndEnqueue(
+              parent[0],
+              getAssignment(parent[1]),
+              prover.xorXFromY(
+                  !parentAssignment, getAssignment(parent[1]), parent));
+        }
+      }
+      break;
+    default: Unhandled();
   }
 }
 
-
-void CircuitPropagator::propagateForward(TNode child, bool childAssignment) {
-
+void CircuitPropagator::propagateForward(TNode child, bool childAssignment)
+{
   // The assignment we have
-  Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child << ", " << childAssignment << ")" << endl;
+  Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child
+                        << ", " << childAssignment << ")" << endl;
 
   // Get the back any nodes where this is child
   const vector<Node>& parents = d_backEdges.find(child)->second;
@@ -207,165 +434,265 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) {
   // Go through the parents and see if there is anything to propagate
   vector<Node>::const_iterator parent_it = parents.begin();
   vector<Node>::const_iterator parent_it_end = parents.end();
-  for(; parent_it != parent_it_end && !d_conflict; ++ parent_it) {
+  for (; parent_it != parent_it_end && d_conflict.get().isNull(); ++parent_it)
+  {
     // The current parent of the child
     TNode parent = *parent_it;
+    Debug("circuit-prop") << "Parent: " << parent << endl;
     Assert(expr::hasSubterm(parent, child));
 
+    ProofCircuitPropagatorForward prover{d_pnm, child, childAssignment, parent};
+
     // Forward rules
-    switch(parent.getKind()) {
-    case kind::AND:
-      if (childAssignment) {
-        TNode::iterator holdout;
-        holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, true)));
-        if (holdout == parent.end()) { // all children are assigned TRUE
-          // AND ...(x=TRUE)...: if all children now assigned to TRUE, assign(AND = TRUE)
-          assignAndEnqueue(parent, true);
-        } else if (isAssignedTo(parent, false)) {// the AND is FALSE
-          // is the holdout unique ?
-          TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, true)));
-          if (other == parent.end()) { // the holdout is unique
-            // AND ...(x=TRUE)...: if all children BUT ONE now assigned to TRUE, and AND == FALSE, assign(last_holdout = FALSE)
-            assignAndEnqueue(*holdout, false);
+    switch (parent.getKind())
+    {
+      case kind::AND:
+        if (childAssignment)
+        {
+          TNode::iterator holdout;
+          holdout = find_if(
+              parent.begin(), parent.end(), not1(IsAssignedTo(*this, true)));
+          if (holdout == parent.end())
+          {  // all children are assigned TRUE
+            // AND ...(x=TRUE)...: if all children now assigned to TRUE,
+            // assign(AND = TRUE)
+            assignAndEnqueue(parent, true, prover.andAllTrue());
+          }
+          else if (isAssignedTo(parent, false))
+          {  // the AND is FALSE
+            // is the holdout unique ?
+            TNode::iterator other = find_if(
+                holdout + 1, parent.end(), not1(IsAssignedTo(*this, true)));
+            if (other == parent.end())
+            {  // the holdout is unique
+              // AND ...(x=TRUE)...: if all children BUT ONE now assigned to
+              // TRUE, and AND == FALSE, assign(last_holdout = FALSE)
+              assignAndEnqueue(
+                  *holdout, false, prover.andFalse(parent, holdout));
+            }
           }
         }
-      } else {
-        // AND ...(x=FALSE)...: assign(AND = FALSE)
-        assignAndEnqueue(parent, false);
-      }
-      break;
-    case kind::OR:
-      if (childAssignment) {
-        // OR ...(x=TRUE)...: assign(OR = TRUE)
-        assignAndEnqueue(parent, true);
-      } else {
-        TNode::iterator holdout;
-        holdout = find_if (parent.begin(), parent.end(), not1(IsAssignedTo(*this, false)));
-        if (holdout == parent.end()) { // all children are assigned FALSE
-          // OR ...(x=FALSE)...: if all children now assigned to FALSE, assign(OR = FALSE)
-          assignAndEnqueue(parent, false);
-        } else if (isAssignedTo(parent, true)) {// the OR is TRUE
-          // is the holdout unique ?
-          TNode::iterator other = find_if (holdout + 1, parent.end(), not1(IsAssignedTo(*this, false)));
-          if (other == parent.end()) { // the holdout is unique
-            // OR ...(x=FALSE)...: if all children BUT ONE now assigned to FALSE, and OR == TRUE, assign(last_holdout = TRUE)
-            assignAndEnqueue(*holdout, true);
+        else
+        {
+          // AND ...(x=FALSE)...: assign(AND = FALSE)
+          assignAndEnqueue(parent, false, prover.andOneFalse());
+        }
+        break;
+      case kind::OR:
+        if (childAssignment)
+        {
+          // OR ...(x=TRUE)...: assign(OR = TRUE)
+          assignAndEnqueue(parent, true, prover.orOneTrue());
+        }
+        else
+        {
+          TNode::iterator holdout;
+          holdout = find_if(
+              parent.begin(), parent.end(), not1(IsAssignedTo(*this, false)));
+          if (holdout == parent.end())
+          {  // all children are assigned FALSE
+            // OR ...(x=FALSE)...: if all children now assigned to FALSE,
+            // assign(OR = FALSE)
+            assignAndEnqueue(parent, false, prover.orFalse());
+          }
+          else if (isAssignedTo(parent, true))
+          {  // the OR is TRUE
+            // is the holdout unique ?
+            TNode::iterator other = find_if(
+                holdout + 1, parent.end(), not1(IsAssignedTo(*this, false)));
+            if (other == parent.end())
+            {  // the holdout is unique
+              // OR ...(x=FALSE)...: if all children BUT ONE now assigned to
+              // FALSE, and OR == TRUE, assign(last_holdout = TRUE)
+              assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout));
+            }
           }
         }
-      }
-      break;
-
-    case kind::NOT:
-      // NOT (x=b): assign(NOT = !b)
-      assignAndEnqueue(parent, !childAssignment);
-      break;
-
-    case kind::ITE:
-      if (child == parent[0]) {
-        if (childAssignment) {
-          if (isAssigned(parent[1])) {
-            // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment)
-            assignAndEnqueue(parent, getAssignment(parent[1]));
+        break;
+
+      case kind::NOT:
+        // NOT (x=b): assign(NOT = !b)
+        assignAndEnqueue(
+            parent, !childAssignment, prover.Not(childAssignment, parent));
+        break;
+
+      case kind::ITE:
+        if (child == parent[0])
+        {
+          if (childAssignment)
+          {
+            if (isAssigned(parent[1]))
+            {
+              // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment)
+              assignAndEnqueue(parent,
+                               getAssignment(parent[1]),
+                               prover.iteEvalThen(getAssignment(parent[1])));
+            }
           }
-        } else {
-          if (isAssigned(parent[2])) {
-            // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment)
-            assignAndEnqueue(parent, getAssignment(parent[2]));
+          else
+          {
+            if (isAssigned(parent[2]))
+            {
+              // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment)
+              assignAndEnqueue(parent,
+                               getAssignment(parent[2]),
+                               prover.iteEvalElse(getAssignment(parent[2])));
+            }
           }
         }
-      }
-      if (child == parent[1]) {
-        if (isAssignedTo(parent[0], true)) {
-          // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v)
-          assignAndEnqueue(parent, childAssignment);
+        if (child == parent[1])
+        {
+          if (isAssignedTo(parent[0], true))
+          {
+            // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v)
+            assignAndEnqueue(
+                parent, childAssignment, prover.iteEvalThen(childAssignment));
+          }
         }
-      }
-      if (child == parent[2]) {
-        Assert(child == parent[2]);
-        if (isAssignedTo(parent[0], false)) {
-          // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v)
-          assignAndEnqueue(parent, childAssignment);
+        if (child == parent[2])
+        {
+          Assert(child == parent[2]);
+          if (isAssignedTo(parent[0], false))
+          {
+            // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v)
+            assignAndEnqueue(
+                parent, childAssignment, prover.iteEvalElse(childAssignment));
+          }
         }
-      }
-      break;
-    case kind::EQUAL:
-      Assert(parent[0].getType().isBoolean());
-      if (isAssigned(parent[0]) && isAssigned(parent[1])) {
-        // IFF x y: if x or y is assigned, assign(IFF = (x.assignment <=> y.assignment))
-        assignAndEnqueue(parent, getAssignment(parent[0]) == getAssignment(parent[1]));
-      } else {
-        if (isAssigned(parent)) {
-          if (child == parent[0]) {
-            if (getAssignment(parent)) {
-              // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b)
-              assignAndEnqueue(parent[1], childAssignment);
-            } else {
-              // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b)
-              assignAndEnqueue(parent[1], !childAssignment);
+        break;
+      case kind::EQUAL:
+        Assert(parent[0].getType().isBoolean());
+        if (isAssigned(parent[0]) && isAssigned(parent[1]))
+        {
+          // IFF x y: if x and y is assigned, assign(IFF = (x.assignment <=>
+          // y.assignment))
+          assignAndEnqueue(parent,
+                           getAssignment(parent[0]) == getAssignment(parent[1]),
+                           prover.eqEval(getAssignment(parent[0]),
+                                         getAssignment(parent[1])));
+        }
+        else
+        {
+          if (isAssigned(parent))
+          {
+            if (child == parent[0])
+            {
+              if (getAssignment(parent))
+              {
+                // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b)
+                assignAndEnqueue(parent[1],
+                                 childAssignment,
+                                 prover.eqYFromX(childAssignment, parent));
+              }
+              else
+              {
+                // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b)
+                assignAndEnqueue(parent[1],
+                                 !childAssignment,
+                                 prover.neqYFromX(childAssignment, parent));
+              }
             }
-          } else {
-            Assert(child == parent[1]);
-            if (getAssignment(parent)) {
-              // IFF x y = b: if IFF is assigned to TRUE, assign(x = b)
-              assignAndEnqueue(parent[0], childAssignment);
-            } else {
-              // IFF x y = b y: if IFF is assigned to TRUE, assign(x = !b)
-              assignAndEnqueue(parent[0], !childAssignment);
+            else
+            {
+              Assert(child == parent[1]);
+              if (getAssignment(parent))
+              {
+                // IFF x y = b: if IFF is assigned to TRUE, assign(x = b)
+                assignAndEnqueue(parent[0],
+                                 childAssignment,
+                                 prover.eqXFromY(childAssignment, parent));
+              }
+              else
+              {
+                // IFF x y = b y: if IFF is assigned to FALSE, assign(x = !b)
+                assignAndEnqueue(parent[0],
+                                 !childAssignment,
+                                 prover.neqXFromY(childAssignment, parent));
+              }
             }
           }
         }
-      }
-      break;
-    case kind::IMPLIES:
-      if (isAssigned(parent[0]) && isAssigned(parent[1])) {
-        // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2))
-        assignAndEnqueue(parent, !getAssignment(parent[0]) || getAssignment(parent[1]));
-      } else {
-        if (child == parent[0] && childAssignment && isAssignedTo(parent, true)) {
-          // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE)
-          assignAndEnqueue(parent[1], true);
-        }
-        if (child == parent[1] && !childAssignment && isAssignedTo(parent, true)) {
-          // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE)
-          assignAndEnqueue(parent[0], false);
-        }
-        // Note that IMPLIES == FALSE doesn't need any cases here
-        // because if that assignment has been done, we've already
-        // propagated all the children (in back-propagation).
-      }
-      break;
-    case kind::XOR:
-      if (isAssigned(parent)) {
-        if (child == parent[0]) {
-          // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR)
-          assignAndEnqueue(parent[1], childAssignment != getAssignment(parent));
-        } else {
-          Assert(child == parent[1]);
-          // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR))
-          assignAndEnqueue(parent[0], childAssignment != getAssignment(parent));
+        break;
+      case kind::IMPLIES:
+        if (isAssigned(parent[0]) && isAssigned(parent[1]))
+        {
+          // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2))
+          assignAndEnqueue(
+              parent,
+              !getAssignment(parent[0]) || getAssignment(parent[1]),
+              prover.impliesEval(getAssignment(parent[0]),
+                                 getAssignment(parent[1])));
         }
-      }
-      if (isAssigned(parent[0]) && isAssigned(parent[1])) {
-        assignAndEnqueue(parent, getAssignment(parent[0]) != getAssignment(parent[1]));
-      }
-      break;
-    default:
-      Unhandled();
+        else
+        {
+          if (child == parent[0] && childAssignment
+              && isAssignedTo(parent, true))
+          {
+            // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE)
+            assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent));
+          }
+          if (child == parent[1] && !childAssignment
+              && isAssignedTo(parent, true))
+          {
+            // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE)
+            assignAndEnqueue(parent[0], false, prover.impliesXFromY(parent));
+          }
+          // Note that IMPLIES == FALSE doesn't need any cases here
+          // because if that assignment has been done, we've already
+          // propagated all the children (in back-propagation).
+        }
+        break;
+      case kind::XOR:
+        if (isAssigned(parent))
+        {
+          if (child == parent[0])
+          {
+            // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR)
+            assignAndEnqueue(
+                parent[1],
+                childAssignment != getAssignment(parent),
+                prover.xorYFromX(
+                    !getAssignment(parent), childAssignment, parent));
+          }
+          else
+          {
+            Assert(child == parent[1]);
+            // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR))
+            assignAndEnqueue(
+                parent[0],
+                childAssignment != getAssignment(parent),
+                prover.xorXFromY(
+                    !getAssignment(parent), childAssignment, parent));
+          }
+        }
+        if (isAssigned(parent[0]) && isAssigned(parent[1]))
+        {
+          assignAndEnqueue(parent,
+                           getAssignment(parent[0]) != getAssignment(parent[1]),
+                           prover.xorEval(getAssignment(parent[0]),
+                                          getAssignment(parent[1])));
+        }
+        break;
+      default: Unhandled();
     }
   }
 }
 
-bool CircuitPropagator::propagate() {
-
+TrustNode CircuitPropagator::propagate()
+{
   Debug("circuit-prop") << "CircuitPropagator::propagate()" << std::endl;
 
-  for(unsigned i = 0; i < d_propagationQueue.size() && !d_conflict; ++ i) {
-
+  for (unsigned i = 0;
+       i < d_propagationQueue.size() && d_conflict.get().isNull();
+       ++i)
+  {
     // The current node we are propagating
     TNode current = d_propagationQueue[i];
-    Debug("circuit-prop") << "CircuitPropagator::propagate(): processing " << current << std::endl;
+    Debug("circuit-prop") << "CircuitPropagator::propagate(): processing "
+                          << current << std::endl;
     bool assignment = getAssignment(current);
-    Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " << (assignment ? "true" : "false") << std::endl;
+    Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to "
+                          << (assignment ? "true" : "false") << std::endl;
 
     // Is this an atom
     bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar()
@@ -373,17 +700,52 @@ bool CircuitPropagator::propagate() {
                     && (current[0].isVar() && current[1].isVar()));
 
     // If an atom, add to the list for simplification
-    if (atom) {
-      Debug("circuit-prop") << "CircuitPropagator::propagate(): adding to learned: " << (assignment ? (Node)current : current.notNode()) << std::endl;
-      d_learnedLiterals.push_back(assignment ? (Node)current : current.notNode());
+    if (atom)
+    {
+      Debug("circuit-prop")
+          << "CircuitPropagator::propagate(): adding to learned: "
+          << (assignment ? (Node)current : current.notNode()) << std::endl;
+      Node lit = assignment ? Node(current) : current.notNode();
+
+      if (isProofEnabled())
+      {
+        if (d_epg->hasProofFor(lit))
+        {
+          // if we have a parent proof generator that provides proofs of the
+          // inputs to this class, we must use the lazy proof chain
+          ProofGenerator* pg = d_proofInternal.get();
+          if (d_proofExternal != nullptr)
+          {
+            d_proofExternal->addLazyStep(lit, pg);
+            pg = d_proofExternal.get();
+          }
+          TrustNode tlit = TrustNode::mkTrustLemma(lit, pg);
+          d_learnedLiterals.push_back(tlit);
+        }
+        else
+        {
+          Warning() << "CircuitPropagator: Proof is missing for " << lit
+                    << std::endl;
+          TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr);
+          d_learnedLiterals.push_back(tlit);
+        }
+      }
+      else
+      {
+        TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr);
+        d_learnedLiterals.push_back(tlit);
+      }
+      Trace("circuit-prop") << "Added proof for " << lit << std::endl;
     }
 
     // Propagate this value to the children (if not an atom or a constant)
-    if (d_backwardPropagation && !atom && !current.isConst()) {
+    if (d_backwardPropagation && !atom && !current.isConst())
+    {
       propagateBackward(current, assignment);
     }
     // Propagate this value to the parents
-    if (d_forwardPropagation) {
+    if (d_forwardPropagation)
+    {
       propagateForward(current, assignment);
     }
   }
@@ -392,6 +754,48 @@ bool CircuitPropagator::propagate() {
   return d_conflict;
 }
 
-}/* CVC4::theory::booleans namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+void CircuitPropagator::setProof(ProofNodeManager* pnm,
+                                 context::Context* ctx,
+                                 ProofGenerator* defParent)
+{
+  d_pnm = pnm;
+  d_epg.reset(new EagerProofGenerator(pnm, ctx));
+  d_proofInternal.reset(
+      new LazyCDProofChain(pnm, true, ctx, d_epg.get(), true));
+  if (defParent != nullptr)
+  {
+    // If we provide a parent proof generator (defParent), we want the ASSUME
+    // leafs of proofs provided by this class to call the getProofFor method on
+    // the parent. To do this, we use a LazyCDProofChain.
+    d_proofExternal.reset(
+        new LazyCDProofChain(pnm, true, ctx, defParent, false));
+  }
+}
+
+bool CircuitPropagator::isProofEnabled() const
+{
+  return d_proofInternal != nullptr;
+}
+
+void CircuitPropagator::addProof(TNode f, std::shared_ptr<ProofNode> pf)
+{
+  if (isProofEnabled())
+  {
+    if (!d_epg->hasProofFor(f))
+    {
+      Trace("circuit-prop") << "Adding proof for " << f << std::endl
+                            << "\t" << *pf << std::endl;
+      d_epg->setProofFor(f, std::move(pf));
+    }
+    else
+    {
+      auto prf = d_epg->getProofFor(f);
+      Trace("circuit-prop") << "Ignoring proof, we already have" << std::endl
+                            << "\t" << *prf << std::endl;
+    }
+  }
+}
+
+}  // namespace booleans
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 3d22b0015..4c7c2d124 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -20,6 +20,7 @@
 #define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
 
 #include <functional>
+#include <memory>
 #include <unordered_map>
 #include <vector>
 
@@ -27,8 +28,13 @@
 #include "context/cdhashset.h"
 #include "context/cdo.h"
 #include "context/context.h"
+#include "expr/lazy_proof_chain.h"
 #include "expr/node.h"
+#include "expr/proof_generator.h"
+#include "expr/proof_node.h"
+#include "theory/eager_proof_generator.h"
 #include "theory/theory.h"
+#include "theory/trust_node.h"
 #include "util/hash.h"
 
 namespace CVC4 {
@@ -63,22 +69,7 @@ class CircuitPropagator
   /**
    * Construct a new CircuitPropagator.
    */
-  CircuitPropagator(bool enableForward = true, bool enableBackward = true)
-      : d_context(),
-        d_propagationQueue(),
-        d_propagationQueueClearer(&d_context, d_propagationQueue),
-        d_conflict(&d_context, false),
-        d_learnedLiterals(),
-        d_learnedLiteralClearer(&d_context, d_learnedLiterals),
-        d_backEdges(),
-        d_backEdgesClearer(&d_context, d_backEdges),
-        d_seen(&d_context),
-        d_state(&d_context),
-        d_forwardPropagation(enableForward),
-        d_backwardPropagation(enableBackward),
-        d_needsFinish(false)
-  {
-  }
+  CircuitPropagator(bool enableForward = true, bool enableBackward = true);
 
   /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
   bool getAssignment(TNode n) const
@@ -95,9 +86,10 @@ class CircuitPropagator
 
   bool getNeedsFinish() { return d_needsFinish; }
 
-  std::vector<Node>& getLearnedLiterals() { return d_learnedLiterals; }
+  std::vector<TrustNode>& getLearnedLiterals() { return d_learnedLiterals; }
 
-  void finish() { d_context.pop(); }
+  /** Finish the computation and pop the internal context */
+  void finish();
 
   /** Assert for propagation */
   void assertTrue(TNode assertion);
@@ -107,9 +99,10 @@ class CircuitPropagator
    * discovered by the propagator are put in the substitutions vector used in
    * construction.
    *
-   * @return true iff conflict found
+   * @return a trust node encapsulating the proof for a conflict as a lemma that
+   * proves false, or the null trust node otherwise
    */
-  bool propagate() CVC4_WARN_UNUSED_RESULT;
+  TrustNode propagate() CVC4_WARN_UNUSED_RESULT;
 
   /**
    * Get the back edges of this circuit.
@@ -142,6 +135,15 @@ class CircuitPropagator
     if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
     return false;
   }
+  /**
+   * Set proof node manager, context and parent proof generator.
+   *
+   * If parent is non-null, then it is responsible for the proofs provided
+   * to this class.
+   */
+  void setProof(ProofNodeManager* pnm,
+                context::Context* ctx,
+                ProofGenerator* defParent);
 
  private:
   /** A context-notify object that clears out stale data. */
@@ -206,40 +208,15 @@ class CircuitPropagator
    * Assign Node in circuit with the value and add it to the queue; note
    * conflicts.
    */
-  void assignAndEnqueue(TNode n, bool value)
-  {
-    Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", "
-                          << (value ? "true" : "false") << ")" << std::endl;
-
-    if (n.getKind() == kind::CONST_BOOLEAN)
-    {
-      // Assigning a constant to the opposite value is dumb
-      if (value != n.getConst<bool>())
-      {
-        d_conflict = true;
-        return;
-      }
-    }
-
-    // Get the current assignment
-    AssignmentStatus state = d_state[n];
+  void assignAndEnqueue(TNode n,
+                        bool value,
+                        std::shared_ptr<ProofNode> proof = nullptr);
 
-    if (state != UNASSIGNED)
-    {
-      // If the node is already assigned we might have a conflict
-      if (value != (state == ASSIGNED_TO_TRUE))
-      {
-        d_conflict = true;
-      }
-    }
-    else
-    {
-      // If unassigned, mark it as assigned
-      d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
-      // Add for further propagation
-      d_propagationQueue.push_back(n);
-    }
-  }
+  /**
+   * Store a conflict for the case that we have derived both n and n.negate()
+   * to be true.
+   */
+  void makeConflict(Node n);
 
   /**
    * Compute the map from nodes to the nodes that use it.
@@ -258,6 +235,9 @@ class CircuitPropagator
    */
   void propagateBackward(TNode parent, bool assignment);
 
+  /** Are proofs enabled? */
+  bool isProofEnabled() const;
+
   context::Context d_context;
 
   /** The propagation queue */
@@ -269,18 +249,18 @@ class CircuitPropagator
    * but this keeps us safe in case there's still some rubbish around
    * on the queue.
    */
-  DataClearer<std::vector<TNode> > d_propagationQueueClearer;
+  DataClearer<std::vector<TNode>> d_propagationQueueClearer;
 
   /** Are we in conflict? */
-  context::CDO<bool> d_conflict;
+  context::CDO<TrustNode> d_conflict;
 
   /** Map of substitutions */
-  std::vector<Node> d_learnedLiterals;
+  std::vector<TrustNode> d_learnedLiterals;
 
   /**
    * Similar data clearer for learned literals.
    */
-  DataClearer<std::vector<Node>> d_learnedLiteralClearer;
+  DataClearer<std::vector<TrustNode>> d_learnedLiteralClearer;
 
   /**
    * Back edges from nodes to where they are used.
@@ -307,6 +287,17 @@ class CircuitPropagator
   /* Does the current state require a call to finish()? */
   bool d_needsFinish;
 
+  /** Adds a new proof for f, or drops it if we already have a proof */
+  void addProof(TNode f, std::shared_ptr<ProofNode> pf);
+
+  /** A pointer to the proof manager */
+  ProofNodeManager* d_pnm;
+  /** Eager proof generator that actually stores the proofs */
+  std::unique_ptr<EagerProofGenerator> d_epg;
+  /** Connects the proofs to subproofs internally */
+  std::unique_ptr<LazyCDProofChain> d_proofInternal;
+  /** Connects the proofs to assumptions externally */
+  std::unique_ptr<LazyCDProofChain> d_proofExternal;
 }; /* class CircuitPropagator */
 
 }  // namespace booleans