[proof-new] Adds a proof-producing CNF converter (#5137)

A proof generator that wraps the original CNF stream, to be used when the prop engine is proof producing. It tracks in a lazy cdproof both the concrete clausification steps and the proof generators of the formulas being clausified (in particular, theory lemmas).

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 587f845d3f958bdc6727a3c6074c8a164a82fbf1..fc251e0ec0566278ceef20653fb0b4757130e37c 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -165,6 +165,8 @@ libcvc4_add_sources(
   prop/cryptominisat.h
   prop/kissat.cpp
   prop/kissat.h
+  prop/proof_cnf_stream.cpp
+  prop/proof_cnf_stream.h
   prop/minisat/core/Dimacs.h
   prop/minisat/core/Solver.cc
   prop/minisat/core/Solver.h

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 5e68b7a82d395406f5df9229fc01e4a21d8f7da2..dd7fbc15ff5ac539a226aec09276458470e56c5b 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -29,6 +29,7 @@
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "proof/proof_manager.h"
+#include "prop/proof_cnf_stream.h"
 #include "prop/registrar.h"
 #include "prop/theory_proxy.h"
 
@@ -38,6 +39,8 @@ class OutputManager;
 
 namespace prop {
 
+class ProofCnfStream;
+
 /**
  * Implements the following recursive algorithm
  * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
@@ -48,6 +51,9 @@ namespace prop {
  * substitute the new literal for the formula, and so on, recursively.
  */
 class CnfStream {
+  friend PropEngine;
+  friend ProofCnfStream;
+
  public:
   /** Cache of what nodes have been registered to a literal. */
   typedef context::CDInsertHashMap<SatLiteral, TNode, SatLiteralHashFunction>

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
new file mode 100644 (file)
index 0000000..92212de
--- /dev/null
+++ b/src/prop/proof_cnf_stream.cpp
@@ -0,0 +1,979 @@
+/*********************                                                        */
+/*! \file proof_cnf_stream.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 Implementation of the proof-producing CNF stream
+ **/
+
+#include "prop/proof_cnf_stream.h"
+
+#include "options/smt_options.h"
+#include "prop/minisat/minisat.h"
+#include "theory/builtin/proof_checker.h"
+
+namespace CVC4 {
+namespace prop {
+
+ProofCnfStream::ProofCnfStream(context::UserContext* u,
+                               CnfStream& cnfStream,
+                               SatProofManager* satPM,
+                               ProofNodeManager* pnm)
+    : d_cnfStream(cnfStream),
+      d_satPM(satPM),
+      d_proof(pnm, nullptr, u, "ProofCnfStream::LazyCDProof"),
+      d_blocked(u)
+{
+}
+
+void ProofCnfStream::addBlocked(std::shared_ptr<ProofNode> pfn)
+{
+  d_blocked.insert(pfn);
+}
+
+bool ProofCnfStream::isBlocked(std::shared_ptr<ProofNode> pfn)
+{
+  return d_blocked.contains(pfn);
+}
+
+std::shared_ptr<ProofNode> ProofCnfStream::getProofFor(Node f)
+{
+  return d_proof.getProofFor(f);
+}
+
+bool ProofCnfStream::hasProofFor(Node f)
+{
+  return d_proof.hasStep(f) || d_proof.hasGenerator(f);
+}
+
+std::string ProofCnfStream::identify() const { return "ProofCnfStream"; }
+
+void ProofCnfStream::normalizeAndRegister(TNode clauseNode)
+{
+  Node normClauseNode = d_psb.factorReorderElimDoubleNeg(clauseNode);
+  if (Trace.isOn("cnf") && normClauseNode != clauseNode)
+  {
+    Trace("cnf") << push
+                 << "ProofCnfStream::normalizeAndRegister: steps to normalized "
+                 << normClauseNode << "\n"
+                 << pop;
+  }
+  d_satPM->registerSatAssumptions({normClauseNode});
+}
+
+void ProofCnfStream::convertAndAssert(TNode node,
+                                      bool negated,
+                                      bool removable,
+                                      ProofGenerator* pg)
+{
+  Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
+               << ", negated = " << (negated ? "true" : "false")
+               << ", removable = " << (removable ? "true" : "false") << ")\n";
+  d_removable = removable;
+  if (pg)
+  {
+    Trace("cnf") << "ProofCnfStream::convertAndAssert: pg: " << pg->identify()
+                 << "\n";
+    Node toJustify = negated ? node.notNode() : static_cast<Node>(node);
+    d_proof.addLazyStep(
+        toJustify, pg, true, "ProofCnfStream::convertAndAssert:cnf");
+  }
+  convertAndAssert(node, negated);
+  // process saved steps in buffer
+  const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps();
+  for (const std::pair<Node, ProofStep>& step : steps)
+  {
+    d_proof.addStep(step.first, step.second);
+  }
+  d_psb.clear();
+}
+
+void ProofCnfStream::convertAndAssert(TNode node, bool negated)
+{
+  Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
+  switch (node.getKind())
+  {
+    case kind::AND: convertAndAssertAnd(node, negated); break;
+    case kind::OR: convertAndAssertOr(node, negated); break;
+    case kind::XOR: convertAndAssertXor(node, negated); break;
+    case kind::IMPLIES: convertAndAssertImplies(node, negated); break;
+    case kind::ITE: convertAndAssertIte(node, negated); break;
+    case kind::NOT:
+    {
+      // track double negation elimination
+      if (negated)
+      {
+        d_proof.addStep(node[0],
+                        PfRule::MACRO_SR_PRED_TRANSFORM,
+                        {node.notNode()},
+                        {node[0]});
+        Trace("cnf") << "ProofCnfStream::convertAndAssert: "
+                        "MACRO_SR_PRED_TRANSFORM added norm "
+                     << node[0] << "\n";
+      }
+      convertAndAssert(node[0], !negated);
+      break;
+    }
+    case kind::EQUAL:
+      if (node[0].getType().isBoolean())
+      {
+        convertAndAssertIff(node, negated);
+        break;
+      }
+      CVC4_FALLTHROUGH;
+    default:
+    {
+      // negate
+      Node nnode = negated ? node.negate() : static_cast<Node>(node);
+      // Atoms
+      SatLiteral lit = toCNF(node, negated);
+      bool added = d_cnfStream.assertClause(nnode, lit);
+      if (negated && added && nnode != node.notNode())
+      {
+        // track double negation elimination
+        //    (not (not n))
+        //   -------------- MACRO_SR_PRED_TRANSFORM
+        //        n
+        d_proof.addStep(
+            nnode, PfRule::MACRO_SR_PRED_TRANSFORM, {node.notNode()}, {nnode});
+        Trace("cnf") << "ProofCnfStream::convertAndAssert: "
+                        "MACRO_SR_PRED_TRANSFORM added norm "
+                     << nnode << "\n";
+      }
+      if (added)
+      {
+        // note that we do not need to do the normalization here since this is
+        // not a clause and double negation is tracked in a dedicated manner
+        // above
+        d_satPM->registerSatAssumptions({nnode});
+      }
+    }
+  }
+}
+
+void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated)
+{
+  Trace("cnf") << "ProofCnfStream::convertAndAssertAnd(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
+  Assert(node.getKind() == kind::AND);
+  if (!negated)
+  {
+    // If the node is a conjunction, we handle each conjunct separately
+    NodeManager* nm = NodeManager::currentNM();
+    for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
+    {
+      // Create a proof step for each n_i
+      Node iNode = nm->mkConst<Rational>(i);
+      d_proof.addStep(node[i], PfRule::AND_ELIM, {node}, {iNode});
+      Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: AND_ELIM " << i
+                   << " added norm " << node[i] << "\n";
+      convertAndAssert(node[i], false);
+    }
+  }
+  else
+  {
+    // If the node is a disjunction, we construct a clause and assert it
+    unsigned i, size = node.getNumChildren();
+    SatClause clause(size);
+    for (i = 0; i < size; ++i)
+    {
+      clause[i] = toCNF(node[i], true);
+    }
+    bool added = d_cnfStream.assertClause(node.negate(), clause);
+    // register proof step
+    if (added)
+    {
+      std::vector<Node> disjuncts;
+      for (i = 0; i < size; ++i)
+      {
+        disjuncts.push_back(node[i].notNode());
+      }
+      Node clauseNode = NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
+      d_proof.addStep(clauseNode, PfRule::NOT_AND, {node.notNode()}, {});
+      Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: NOT_AND added "
+                   << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+  }
+}
+
+void ProofCnfStream::convertAndAssertOr(TNode node, bool negated)
+{
+  Trace("cnf") << "ProofCnfStream::convertAndAssertOr(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
+  Assert(node.getKind() == kind::OR);
+  if (!negated)
+  {
+    // If the node is a disjunction, we construct a clause and assert it
+    unsigned size = node.getNumChildren();
+    SatClause clause(size);
+    for (unsigned i = 0; i < size; ++i)
+    {
+      clause[i] = toCNF(node[i], false);
+    }
+    normalizeAndRegister(node);
+    d_cnfStream.assertClause(node, clause);
+  }
+  else
+  {
+    // If the node is a negated disjunction, we handle it as a conjunction of
+    // the negated arguments
+    NodeManager* nm = NodeManager::currentNM();
+    for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
+    {
+      // Create a proof step for each (not n_i)
+      Node iNode = nm->mkConst<Rational>(i);
+      d_proof.addStep(
+          node[i].notNode(), PfRule::NOT_OR_ELIM, {node.notNode()}, {iNode});
+      Trace("cnf") << "ProofCnfStream::convertAndAssertOr: NOT_OR_ELIM " << i
+                   << " added norm  " << node[i].notNode() << "\n";
+      convertAndAssert(node[i], true);
+    }
+  }
+}
+
+void ProofCnfStream::convertAndAssertXor(TNode node, bool negated)
+{
+  Trace("cnf") << "ProofCnfStream::convertAndAssertXor(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
+  if (!negated)
+  {
+    // p XOR q
+    SatLiteral p = toCNF(node[0], false);
+    SatLiteral q = toCNF(node[1], false);
+    bool added;
+    NodeManager* nm = NodeManager::currentNM();
+    // Construct the clause (~p v ~q)
+    SatClause clause1(2);
+    clause1[0] = ~p;
+    clause1[1] = ~q;
+    added = d_cnfStream.assertClause(node, clause1);
+    if (added)
+    {
+      Node clauseNode =
+          nm->mkNode(kind::OR, node[0].notNode(), node[1].notNode());
+      d_proof.addStep(clauseNode, PfRule::XOR_ELIM2, {node}, {});
+      Trace("cnf") << "ProofCnfStream::convertAndAssertXor: XOR_ELIM2 added "
+                   << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+    // Construct the clause (p v q)
+    SatClause clause2(2);
+    clause2[0] = p;
+    clause2[1] = q;
+    added = d_cnfStream.assertClause(node, clause2);
+    if (added)
+    {
+      Node clauseNode = nm->mkNode(kind::OR, node[0], node[1]);
+      d_proof.addStep(clauseNode, PfRule::XOR_ELIM1, {node}, {});
+      Trace("cnf") << "ProofCnfStream::convertAndAssertXor: XOR_ELIM1 added "
+                   << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+  }
+  else
+  {
+    // ~(p XOR q) is the same as p <=> q
+    SatLiteral p = toCNF(node[0], false);
+    SatLiteral q = toCNF(node[1], false);
+    bool added;
+    NodeManager* nm = NodeManager::currentNM();
+    // Construct the clause ~p v q
+    SatClause clause1(2);
+    clause1[0] = ~p;
+    clause1[1] = q;
+    added = d_cnfStream.assertClause(node.negate(), clause1);
+    if (added)
+    {
+      Node clauseNode = nm->mkNode(kind::OR, node[0].notNode(), node[1]);
+      d_proof.addStep(clauseNode, PfRule::NOT_XOR_ELIM2, {node.notNode()}, {});
+      Trace("cnf")
+          << "ProofCnfStream::convertAndAssertXor: NOT_XOR_ELIM2 added "
+          << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+    // Construct the clause ~q v p
+    SatClause clause2(2);
+    clause2[0] = p;
+    clause2[1] = ~q;
+    added = d_cnfStream.assertClause(node.negate(), clause2);
+    if (added)
+    {
+      Node clauseNode = nm->mkNode(kind::OR, node[0], node[1].notNode());
+      d_proof.addStep(clauseNode, PfRule::NOT_XOR_ELIM1, {node.notNode()}, {});
+      Trace("cnf")
+          << "ProofCnfStream::convertAndAssertXor: NOT_XOR_ELIM1 added "
+          << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+  }
+}
+
+void ProofCnfStream::convertAndAssertIff(TNode node, bool negated)
+{
+  Trace("cnf") << "ProofCnfStream::convertAndAssertIff(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
+  if (!negated)
+  {
+    // p <=> q
+    Trace("cnf") << push;
+    SatLiteral p = toCNF(node[0], false);
+    SatLiteral q = toCNF(node[1], false);
+    Trace("cnf") << pop;
+    bool added;
+    NodeManager* nm = NodeManager::currentNM();
+    // Construct the clauses ~p v q
+    SatClause clause1(2);
+    clause1[0] = ~p;
+    clause1[1] = q;
+    added = d_cnfStream.assertClause(node, clause1);
+    if (added)
+    {
+      Node clauseNode = nm->mkNode(kind::OR, node[0].notNode(), node[1]);
+      d_proof.addStep(clauseNode, PfRule::EQUIV_ELIM1, {node}, {});
+      Trace("cnf") << "ProofCnfStream::convertAndAssertIff: EQUIV_ELIM1 added "
+                   << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+    // Construct the clauses ~q v p
+    SatClause clause2(2);
+    clause2[0] = p;
+    clause2[1] = ~q;
+    added = d_cnfStream.assertClause(node, clause2);
+    if (added)
+    {
+      Node clauseNode = nm->mkNode(kind::OR, node[0], node[1].notNode());
+      d_proof.addStep(clauseNode, PfRule::EQUIV_ELIM2, {node}, {});
+      Trace("cnf") << "ProofCnfStream::convertAndAssertIff: EQUIV_ELIM2 added "
+                   << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+  }
+  else
+  {
+    // ~(p <=> q) is the same as p XOR q
+    Trace("cnf") << push;
+    SatLiteral p = toCNF(node[0], false);
+    SatLiteral q = toCNF(node[1], false);
+    Trace("cnf") << pop;
+    bool added;
+    NodeManager* nm = NodeManager::currentNM();
+    // Construct the clauses ~p v ~q
+    SatClause clause1(2);
+    clause1[0] = ~p;
+    clause1[1] = ~q;
+    added = d_cnfStream.assertClause(node.negate(), clause1);
+    if (added)
+    {
+      Node clauseNode =
+          nm->mkNode(kind::OR, node[0].notNode(), node[1].notNode());
+      d_proof.addStep(
+          clauseNode, PfRule::NOT_EQUIV_ELIM2, {node.notNode()}, {});
+      Trace("cnf")
+          << "ProofCnfStream::convertAndAssertIff: NOT_EQUIV_ELIM2 added "
+          << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+    // Construct the clauses q v p
+    SatClause clause2(2);
+    clause2[0] = p;
+    clause2[1] = q;
+    added = d_cnfStream.assertClause(node.negate(), clause2);
+    if (added)
+    {
+      Node clauseNode = nm->mkNode(kind::OR, node[0], node[1]);
+      d_proof.addStep(
+          clauseNode, PfRule::NOT_EQUIV_ELIM1, {node.notNode()}, {});
+      Trace("cnf")
+          << "ProofCnfStream::convertAndAssertIff: NOT_EQUIV_ELIM1 added "
+          << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+  }
+}
+
+void ProofCnfStream::convertAndAssertImplies(TNode node, bool negated)
+{
+  Trace("cnf") << "ProofCnfStream::convertAndAssertImplies(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
+  if (!negated)
+  {
+    // ~p v q
+    SatLiteral p = toCNF(node[0], false);
+    SatLiteral q = toCNF(node[1], false);
+    // Construct the clause ~p || q
+    SatClause clause(2);
+    clause[0] = ~p;
+    clause[1] = q;
+    bool added = d_cnfStream.assertClause(node, clause);
+    if (added)
+    {
+      Node clauseNode = NodeManager::currentNM()->mkNode(
+          kind::OR, node[0].notNode(), node[1]);
+      d_proof.addStep(clauseNode, PfRule::IMPLIES_ELIM, {node}, {});
+      Trace("cnf")
+          << "ProofCnfStream::convertAndAssertImplies: IMPLIES_ELIM added "
+          << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+  }
+  else
+  {
+    // ~(p => q) is the same as p ^ ~q
+    // process p
+    convertAndAssert(node[0], false);
+    d_proof.addStep(node[0], PfRule::NOT_IMPLIES_ELIM1, {node.notNode()}, {});
+    Trace("cnf")
+        << "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM1 added "
+        << node[0] << "\n";
+    // process ~q
+    convertAndAssert(node[1], true);
+    d_proof.addStep(
+        node[1].notNode(), PfRule::NOT_IMPLIES_ELIM2, {node.notNode()}, {});
+    Trace("cnf")
+        << "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM2 added "
+        << node[1].notNode() << "\n";
+  }
+}
+
+void ProofCnfStream::convertAndAssertIte(TNode node, bool negated)
+{
+  Trace("cnf") << "ProofCnfStream::convertAndAssertIte(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
+  // ITE(p, q, r)
+  SatLiteral p = toCNF(node[0], false);
+  SatLiteral q = toCNF(node[1], negated);
+  SatLiteral r = toCNF(node[2], negated);
+  bool added;
+  NodeManager* nm = NodeManager::currentNM();
+  // Construct the clauses:
+  // (~p v q) and (p v r)
+  //
+  // Note that below q and r can be used directly because whether they are
+  // negated has been push to the literal definitions above
+  Node nnode = negated ? node.negate() : static_cast<Node>(node);
+  // (~p v q)
+  SatClause clause1(2);
+  clause1[0] = ~p;
+  clause1[1] = q;
+  added = d_cnfStream.assertClause(nnode, clause1);
+  if (added)
+  {
+    // redo the negation here to avoid silent double negation elimination
+    if (!negated)
+    {
+      Node clauseNode = nm->mkNode(kind::OR, node[0].notNode(), node[1]);
+      d_proof.addStep(clauseNode, PfRule::ITE_ELIM1, {node}, {});
+      Trace("cnf") << "ProofCnfStream::convertAndAssertIte: ITE_ELIM1 added "
+                   << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+    else
+    {
+      Node clauseNode =
+          nm->mkNode(kind::OR, node[0].notNode(), node[1].notNode());
+      d_proof.addStep(clauseNode, PfRule::NOT_ITE_ELIM1, {node.notNode()}, {});
+      Trace("cnf")
+          << "ProofCnfStream::convertAndAssertIte: NOT_ITE_ELIM1 added "
+          << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+  }
+  // (p v r)
+  SatClause clause2(2);
+  clause2[0] = p;
+  clause2[1] = r;
+  added = d_cnfStream.assertClause(nnode, clause2);
+  if (added)
+  {
+    // redo the negation here to avoid silent double negation elimination
+    if (!negated)
+    {
+      Node clauseNode = nm->mkNode(kind::OR, node[0], node[2]);
+      d_proof.addStep(clauseNode, PfRule::ITE_ELIM2, {node}, {});
+      Trace("cnf") << "ProofCnfStream::convertAndAssertIte: ITE_ELIM2 added "
+                   << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+    else
+    {
+      Node clauseNode = nm->mkNode(kind::OR, node[0], node[2].notNode());
+      d_proof.addStep(clauseNode, PfRule::NOT_ITE_ELIM2, {node.notNode()}, {});
+      Trace("cnf")
+          << "ProofCnfStream::convertAndAssertIte: NOT_ITE_ELIM2 added "
+          << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+  }
+}
+
+void ProofCnfStream::convertPropagation(theory::TrustNode trn)
+{
+  Node proven = trn.getProven();
+  Trace("cnf") << "ProofCnfStream::convertPropagation: proven explanation"
+               << proven << "\n";
+  Assert(trn.getGenerator());
+  Assert(trn.getGenerator()->getProofFor(proven)->isClosed());
+  Trace("cnf-steps") << proven << " by explainPropagation "
+                     << trn.identifyGenerator() << std::endl;
+  d_proof.addLazyStep(
+      proven, trn.getGenerator(), true, "ProofCnfStream::convertPropagation");
+  // since the propagation is added directly to the SAT solver via theoryProxy,
+  // do the transformation of the lemma E1 ^ ... ^ En => P into CNF here
+  NodeManager* nm = NodeManager::currentNM();
+  Node clauseImpliesElim = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]);
+  Trace("cnf") << "ProofCnfStream::convertPropagation: adding "
+               << PfRule::IMPLIES_ELIM << " rule to conclude "
+               << clauseImpliesElim << "\n";
+  d_proof.addStep(clauseImpliesElim, PfRule::IMPLIES_ELIM, {proven}, {});
+  Node clauseExp;
+  // need to eliminate AND
+  if (proven[0].getKind() == kind::AND)
+  {
+    std::vector<Node> disjunctsAndNeg{proven[0]};
+    std::vector<Node> disjunctsRes;
+    for (unsigned i = 0, size = proven[0].getNumChildren(); i < size; ++i)
+    {
+      disjunctsAndNeg.push_back(proven[0][i].notNode());
+      disjunctsRes.push_back(proven[0][i].notNode());
+    }
+    disjunctsRes.push_back(proven[1]);
+    Node clauseAndNeg = nm->mkNode(kind::OR, disjunctsAndNeg);
+    // add proof steps to convert into clause
+    d_proof.addStep(clauseAndNeg, PfRule::CNF_AND_NEG, {}, {proven[0]});
+    clauseExp = nm->mkNode(kind::OR, disjunctsRes);
+    d_proof.addStep(clauseExp,
+                    PfRule::RESOLUTION,
+                    {clauseAndNeg, clauseImpliesElim},
+                    {proven[0]});
+  }
+  else
+  {
+    clauseExp = clauseImpliesElim;
+  }
+  normalizeAndRegister(clauseExp);
+  // consume steps
+  const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps();
+  for (const std::pair<Node, ProofStep>& step : steps)
+  {
+    d_proof.addStep(step.first, step.second);
+  }
+  d_psb.clear();
+}
+
+SatLiteral ProofCnfStream::toCNF(TNode node, bool negated)
+{
+  Trace("cnf") << "toCNF(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
+  SatLiteral lit;
+  // If the node has already has a literal, return it (maybe negated)
+  if (d_cnfStream.hasLiteral(node))
+  {
+    Trace("cnf") << "toCNF(): already translated\n";
+    lit = d_cnfStream.getLiteral(node);
+    // Return the (maybe negated) literal
+    return !negated ? lit : ~lit;
+  }
+
+  // Handle each Boolean operator case
+  switch (node.getKind())
+  {
+    case kind::AND: lit = handleAnd(node); break;
+    case kind::OR: lit = handleOr(node); break;
+    case kind::XOR: lit = handleXor(node); break;
+    case kind::IMPLIES: lit = handleImplies(node); break;
+    case kind::ITE: lit = handleIte(node); break;
+    case kind::NOT: lit = ~toCNF(node[0]); break;
+    case kind::EQUAL:
+      lit = node[0].getType().isBoolean() ? handleIff(node)
+                                          : d_cnfStream.convertAtom(node);
+      break;
+    default: { lit = d_cnfStream.convertAtom(node);
+    }
+    break;
+  }
+  // Return the (maybe negated) literal
+  return !negated ? lit : ~lit;
+}
+
+SatLiteral ProofCnfStream::handleAnd(TNode node)
+{
+  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
+  Assert(node.getKind() == kind::AND) << "Expecting an AND expression!";
+  Assert(node.getNumChildren() > 1) << "Expecting more than 1 child!";
+  Assert(!d_removable) << "Removable clauses cannot contain Boolean structure";
+  Trace("cnf") << "ProofCnfStream::handleAnd(" << node << ")\n";
+  // Number of children
+  unsigned size = node.getNumChildren();
+  // Transform all the children first (remembering the negation)
+  SatClause clause(size + 1);
+  for (unsigned i = 0; i < size; ++i)
+  {
+    Trace("cnf") << push;
+    clause[i] = ~toCNF(node[i]);
+    Trace("cnf") << pop;
+  }
+  // Create literal for the node
+  SatLiteral lit = d_cnfStream.newLiteral(node);
+  bool added;
+  NodeManager* nm = NodeManager::currentNM();
+  // lit -> (a_1 & a_2 & a_3 & ... & a_n)
+  // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
+  // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
+  for (unsigned i = 0; i < size; ++i)
+  {
+    Trace("cnf") << push;
+    added = d_cnfStream.assertClause(node.negate(), ~lit, ~clause[i]);
+    Trace("cnf") << pop;
+    if (added)
+    {
+      Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[i]);
+      Node iNode = nm->mkConst<Rational>(i);
+      d_proof.addStep(clauseNode, PfRule::CNF_AND_POS, {}, {node, iNode});
+      Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_POS " << i
+                   << " added " << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+  }
+  // lit <- (a_1 & a_2 & a_3 & ... a_n)
+  // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
+  // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
+  clause[size] = lit;
+  // This needs to go last, as the clause might get modified by the SAT solver
+  Trace("cnf") << push;
+  added = d_cnfStream.assertClause(node, clause);
+  Trace("cnf") << pop;
+  if (added)
+  {
+    std::vector<Node> disjuncts{node};
+    for (unsigned i = 0; i < size; ++i)
+    {
+      disjuncts.push_back(node[i].notNode());
+    }
+    Node clauseNode = nm->mkNode(kind::OR, disjuncts);
+    d_proof.addStep(clauseNode, PfRule::CNF_AND_NEG, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_NEG added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  return lit;
+}
+
+SatLiteral ProofCnfStream::handleOr(TNode node)
+{
+  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
+  Assert(node.getKind() == kind::OR) << "Expecting an OR expression!";
+  Assert(node.getNumChildren() > 1) << "Expecting more then 1 child!";
+  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Trace("cnf") << "ProofCnfStream::handleOr(" << node << ")\n";
+  // Number of children
+  unsigned size = node.getNumChildren();
+  // Transform all the children first
+  SatClause clause(size + 1);
+  for (unsigned i = 0; i < size; ++i)
+  {
+    clause[i] = toCNF(node[i]);
+  }
+  // Create literal for the node
+  SatLiteral lit = d_cnfStream.newLiteral(node);
+  bool added;
+  NodeManager* nm = NodeManager::currentNM();
+  // lit <- (a_1 | a_2 | a_3 | ... | a_n)
+  // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
+  // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
+  for (unsigned i = 0; i < size; ++i)
+  {
+    added = d_cnfStream.assertClause(node, lit, ~clause[i]);
+    if (added)
+    {
+      Node clauseNode = nm->mkNode(kind::OR, node, node[i].notNode());
+      Node iNode = nm->mkConst<Rational>(i);
+      d_proof.addStep(clauseNode, PfRule::CNF_OR_NEG, {}, {node, iNode});
+      Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_NEG " << i << " added "
+                   << clauseNode << "\n";
+      normalizeAndRegister(clauseNode);
+    }
+  }
+  // lit -> (a_1 | a_2 | a_3 | ... | a_n)
+  // ~lit | a_1 | a_2 | a_3 | ... | a_n
+  clause[size] = ~lit;
+  // This needs to go last, as the clause might get modified by the SAT solver
+  added = d_cnfStream.assertClause(node.negate(), clause);
+  if (added)
+  {
+    std::vector<Node> disjuncts{node.notNode()};
+    for (unsigned i = 0; i < size; ++i)
+    {
+      disjuncts.push_back(node[i]);
+    }
+    Node clauseNode = nm->mkNode(kind::OR, disjuncts);
+    d_proof.addStep(clauseNode, PfRule::CNF_OR_POS, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_POS added " << clauseNode
+                 << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  return lit;
+}
+
+SatLiteral ProofCnfStream::handleXor(TNode node)
+{
+  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
+  Assert(node.getKind() == kind::XOR) << "Expecting an XOR expression!";
+  Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
+  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Trace("cnf") << "ProofCnfStream::handleXor(" << node << ")\n";
+  SatLiteral a = toCNF(node[0]);
+  SatLiteral b = toCNF(node[1]);
+  SatLiteral lit = d_cnfStream.newLiteral(node);
+  bool added;
+  added = d_cnfStream.assertClause(node.negate(), a, b, ~lit);
+  if (added)
+  {
+    Node clauseNode = NodeManager::currentNM()->mkNode(
+        kind::OR, node.notNode(), node[0], node[1]);
+    d_proof.addStep(clauseNode, PfRule::CNF_XOR_POS1, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_POS1 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  added = d_cnfStream.assertClause(node.negate(), ~a, ~b, ~lit);
+  if (added)
+  {
+    Node clauseNode = NodeManager::currentNM()->mkNode(
+        kind::OR, node.notNode(), node[0].notNode(), node[1].notNode());
+    d_proof.addStep(clauseNode, PfRule::CNF_XOR_POS2, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_POS2 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  added = d_cnfStream.assertClause(node, a, ~b, lit);
+  if (added)
+  {
+    Node clauseNode = NodeManager::currentNM()->mkNode(
+        kind::OR, node, node[0], node[1].notNode());
+    d_proof.addStep(clauseNode, PfRule::CNF_XOR_NEG2, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_NEG2 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  added = d_cnfStream.assertClause(node, ~a, b, lit);
+  if (added)
+  {
+    Node clauseNode = NodeManager::currentNM()->mkNode(
+        kind::OR, node, node[0].notNode(), node[1]);
+    d_proof.addStep(clauseNode, PfRule::CNF_XOR_NEG1, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_NEG1 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  return lit;
+}
+
+SatLiteral ProofCnfStream::handleIff(TNode node)
+{
+  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
+  Assert(node.getKind() == kind::EQUAL) << "Expecting an EQUAL expression!";
+  Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
+  Trace("cnf") << "handleIff(" << node << ")\n";
+  // Convert the children to CNF
+  SatLiteral a = toCNF(node[0]);
+  SatLiteral b = toCNF(node[1]);
+  // Create literal for the node
+  SatLiteral lit = d_cnfStream.newLiteral(node);
+  bool added;
+  NodeManager* nm = NodeManager::currentNM();
+  // lit -> ((a-> b) & (b->a))
+  // ~lit | ((~a | b) & (~b | a))
+  // (~a | b | ~lit) & (~b | a | ~lit)
+  added = d_cnfStream.assertClause(node.negate(), ~a, b, ~lit);
+  if (added)
+  {
+    Node clauseNode =
+        nm->mkNode(kind::OR, node.notNode(), node[0].notNode(), node[1]);
+    d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_POS1, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_POS1 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  added = d_cnfStream.assertClause(node.negate(), a, ~b, ~lit);
+  if (added)
+  {
+    Node clauseNode =
+        nm->mkNode(kind::OR, node.notNode(), node[0], node[1].notNode());
+    d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_POS2, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_POS2 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  // (a<->b) -> lit
+  // ~((a & b) | (~a & ~b)) | lit
+  // (~(a & b)) & (~(~a & ~b)) | lit
+  // ((~a | ~b) & (a | b)) | lit
+  // (~a | ~b | lit) & (a | b | lit)
+  added = d_cnfStream.assertClause(node, ~a, ~b, lit);
+  if (added)
+  {
+    Node clauseNode =
+        nm->mkNode(kind::OR, node, node[0].notNode(), node[1].notNode());
+    d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_NEG2, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_NEG2 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  added = d_cnfStream.assertClause(node, a, b, lit);
+  if (added)
+  {
+    Node clauseNode = nm->mkNode(kind::OR, node, node[0], node[1]);
+    d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_NEG1, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_NEG1 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  return lit;
+}
+
+SatLiteral ProofCnfStream::handleImplies(TNode node)
+{
+  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
+  Assert(node.getKind() == kind::IMPLIES) << "Expecting an IMPLIES expression!";
+  Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
+  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Trace("cnf") << "ProofCnfStream::handleImplies(" << node << ")\n";
+  // Convert the children to cnf
+  SatLiteral a = toCNF(node[0]);
+  SatLiteral b = toCNF(node[1]);
+  SatLiteral lit = d_cnfStream.newLiteral(node);
+  bool added;
+  NodeManager* nm = NodeManager::currentNM();
+  // lit -> (a->b)
+  // ~lit | ~ a | b
+  added = d_cnfStream.assertClause(node.negate(), ~lit, ~a, b);
+  if (added)
+  {
+    Node clauseNode =
+        nm->mkNode(kind::OR, node.notNode(), node[0].notNode(), node[1]);
+    d_proof.addStep(clauseNode, PfRule::CNF_IMPLIES_POS, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_POS added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  // (a->b) -> lit
+  // ~(~a | b) | lit
+  // (a | l) & (~b | l)
+  added = d_cnfStream.assertClause(node, a, lit);
+  if (added)
+  {
+    Node clauseNode = nm->mkNode(kind::OR, node, node[0]);
+    d_proof.addStep(clauseNode, PfRule::CNF_IMPLIES_NEG1, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_NEG1 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  added = d_cnfStream.assertClause(node, ~b, lit);
+  if (added)
+  {
+    Node clauseNode = nm->mkNode(kind::OR, node, node[1].notNode());
+    d_proof.addStep(clauseNode, PfRule::CNF_IMPLIES_NEG2, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_NEG2 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  return lit;
+}
+
+SatLiteral ProofCnfStream::handleIte(TNode node)
+{
+  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
+  Assert(node.getKind() == kind::ITE);
+  Assert(node.getNumChildren() == 3);
+  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Trace("cnf") << "handleIte(" << node[0] << " " << node[1] << " " << node[2]
+               << ")\n";
+  SatLiteral condLit = toCNF(node[0]);
+  SatLiteral thenLit = toCNF(node[1]);
+  SatLiteral elseLit = toCNF(node[2]);
+  // create literal to the node
+  SatLiteral lit = d_cnfStream.newLiteral(node);
+  bool added;
+  NodeManager* nm = NodeManager::currentNM();
+  // If ITE is true then one of the branches is true and the condition
+  // implies which one
+  // lit -> (ite b t e)
+  // lit -> (t | e) & (b -> t) & (!b -> e)
+  // lit -> (t | e) & (!b | t) & (b | e)
+  // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
+  added = d_cnfStream.assertClause(node.negate(), ~lit, thenLit, elseLit);
+  if (added)
+  {
+    Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[1], node[2]);
+    d_proof.addStep(clauseNode, PfRule::CNF_ITE_POS3, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS3 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  added = d_cnfStream.assertClause(node.negate(), ~lit, ~condLit, thenLit);
+  if (added)
+  {
+    Node clauseNode =
+        nm->mkNode(kind::OR, node.notNode(), node[0].notNode(), node[1]);
+    d_proof.addStep(clauseNode, PfRule::CNF_ITE_POS1, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS1 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  added = d_cnfStream.assertClause(node.negate(), ~lit, condLit, elseLit);
+  if (added)
+  {
+    Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[0], node[2]);
+    d_proof.addStep(clauseNode, PfRule::CNF_ITE_POS2, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS2 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  // If ITE is false then one of the branches is false and the condition
+  // implies which one
+  // !lit -> !(ite b t e)
+  // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
+  // !lit -> (!t | !e) & (!b | !t) & (b | !e)
+  // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
+  added = d_cnfStream.assertClause(node, lit, ~thenLit, ~elseLit);
+  if (added)
+  {
+    Node clauseNode =
+        nm->mkNode(kind::OR, node, node[1].notNode(), node[2].notNode());
+    d_proof.addStep(clauseNode, PfRule::CNF_ITE_NEG3, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG3 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  added = d_cnfStream.assertClause(node, lit, ~condLit, ~thenLit);
+  if (added)
+  {
+    Node clauseNode =
+        nm->mkNode(kind::OR, node, node[0].notNode(), node[1].notNode());
+    d_proof.addStep(clauseNode, PfRule::CNF_ITE_NEG1, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG1 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  added = d_cnfStream.assertClause(node, lit, condLit, ~elseLit);
+  if (added)
+  {
+    Node clauseNode = nm->mkNode(kind::OR, node, node[0], node[2].notNode());
+    d_proof.addStep(clauseNode, PfRule::CNF_ITE_NEG2, {}, {node});
+    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG2 added "
+                 << clauseNode << "\n";
+    normalizeAndRegister(clauseNode);
+  }
+  return lit;
+}
+
+}  // namespace prop
+}  // namespace CVC4

diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
new file mode 100644 (file)
index 0000000..80be072
--- /dev/null
+++ b/src/prop/proof_cnf_stream.h
@@ -0,0 +1,174 @@
+/*********************                                                        */
+/*! \file proof_cnf_stream.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 The proof-producing CNF stream
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PROP__PROOF_CNF_STREAM_H
+#define CVC4__PROP__PROOF_CNF_STREAM_H
+
+#include "context/cdhashmap.h"
+#include "expr/lazy_proof.h"
+#include "expr/node.h"
+#include "expr/proof_node.h"
+#include "expr/proof_node_manager.h"
+#include "prop/cnf_stream.h"
+#include "prop/sat_proof_manager.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/theory_proof_step_buffer.h"
+
+namespace CVC4 {
+namespace prop {
+
+class SatProofManager;
+
+/**
+ * A proof generator for CNF transformation. It is a layer on top of CNF stream,
+ * tracking the justifications for clauses added into the underlying SAT solver
+ * in a user-context dependent manner in a lazy context-dependent (LazyCDProof)
+ * object. The proof is lazy because formulas asserted to this class may also
+ * take proof generators (which is the case, for example, for theory lemmas), so
+ * that getting the proof of a clausified formula will also extend to its
+ * registered proof generator.
+ */
+class ProofCnfStream : public ProofGenerator
+{
+ public:
+  ProofCnfStream(context::UserContext* u,
+                 CnfStream& cnfStream,
+                 SatProofManager* satPM,
+                 ProofNodeManager* pnm);
+
+  /** Invokes getProofFor of the underlying LazyCDProof */
+  std::shared_ptr<ProofNode> getProofFor(Node f) override;
+  /** Whether there is a concrete step or a generator associated with f in the
+   * underlying LazyCDProof. */
+  bool hasProofFor(Node f) override;
+  /** identify */
+  std::string identify() const override;
+  /**
+   * Converts a formula into CNF into CNF and asserts the generated clauses into
+   * the underlying SAT solver of d_cnfStream. Every transformation the formula
+   * goes through is saved as a concrete step in d_proof.
+   *
+   * The given formula has arbitrary Boolean structure via kinds AND, OR, EQUAL,
+   * XOR, IMPLIES. ITE and NOT. The conversion is done polynomially via Tseitin
+   * transformation, with the children of non-conjunctive kinds being abstracted
+   * as new literals, which are clausified with the respective "handle" methods
+   * below.
+
+   * @param node formula to convert and assert
+   * @param negated whether we are asserting the node negated
+   * @param removable whether the SAT solver can choose to remove the clauses
+   * @param pg a proof generator for node
+   */
+  void convertAndAssert(TNode node,
+                        bool negated,
+                        bool removable,
+                        ProofGenerator* pg);
+
+  /**
+   * Clausifies the given propagation lemma *without* registering the
+   * resoluting clause in the SAT solver, as this is handled internally by the
+   * SAT solver. The clausification steps and the generator within the trust
+   * node are saved in d_proof. */
+  void convertPropagation(theory::TrustNode ttn);
+
+  /**
+   * Blocks a proof, so that it is not further updated by a post processor of
+   * this class's proof. */
+  void addBlocked(std::shared_ptr<ProofNode> pfn);
+
+  /**
+   * Whether a given proof is blocked for further updates.  An example of a
+   * blocked proof node is one integrated into this class via an external proof
+   * generator. */
+  bool isBlocked(std::shared_ptr<ProofNode> pfn);
+
+ private:
+  /**
+   * Same as above, except that uses the saved d_removable flag. It calls the
+   * dedicated converter for the possible formula kinds.
+   */
+  void convertAndAssert(TNode node, bool negated);
+  /** Specific converters for each formula kind. */
+  void convertAndAssertAnd(TNode node, bool negated);
+  void convertAndAssertOr(TNode node, bool negated);
+  void convertAndAssertXor(TNode node, bool negated);
+  void convertAndAssertIff(TNode node, bool negated);
+  void convertAndAssertImplies(TNode node, bool negated);
+  void convertAndAssertIte(TNode node, bool negated);
+  /**
+   * Transforms the node into CNF recursively and yields a literal
+   * definitionally equal to it.
+   *
+   * This method also populates caches, kept in d_cnfStream, between formulas
+   * and literals to avoid redundant work and to retrieve formulas from literals
+   * and vice-versa.
+   *
+   * @param node the formula to transform
+   * @param negated whether the literal is negated
+   * @return the literal representing the root of the formula
+   */
+  SatLiteral toCNF(TNode node, bool negated = false);
+  /**
+   * Specific clausifiers, based on the formula kinds, that clausify a formula,
+   * by calling toCNF into each of the formula's children under the respective
+   * kind, and introduce a literal definitionally equal to it. */
+  SatLiteral handleNot(TNode node);
+  SatLiteral handleXor(TNode node);
+  SatLiteral handleImplies(TNode node);
+  SatLiteral handleIff(TNode node);
+  SatLiteral handleIte(TNode node);
+  SatLiteral handleAnd(TNode node);
+  SatLiteral handleOr(TNode node);
+
+  /** Normalizes a clause node and registers it in the SAT proof manager.
+   *
+   * Normalization (factoring, reordering, double negation elimination) is done
+   * via the TheoryProofStepBuffer of this class, which will register the
+   * respective steps, if any. This normalization is necessary so that the
+   * resulting clauses of the clausification process are synchronized with the
+   * clauses used in the underlying SAT solver, which automatically performs the
+   * above normalizations on all added clauses.
+   */
+  void normalizeAndRegister(TNode clauseNode);
+  /**
+   * Are we asserting a removable clause (true) or a permanent clause (false).
+   * This is set at the beginning of convertAndAssert so that it doesn't need to
+   * be passed on over the stack. Only pure clauses can be asserted as
+   * removable.
+   */
+  bool d_removable;
+  /** Reference to the underlying cnf stream. */
+  CnfStream& d_cnfStream;
+  /** The proof manager of underlying SAT solver associated with this stream. */
+  SatProofManager* d_satPM;
+  /** The proof node manager. */
+  ProofNodeManager* d_pnm;
+  /** The user-context-dependent proof object. */
+  LazyCDProof d_proof;
+  /** An accumulator of steps that may be applied to normalize the clauses
+   * generated during clausification. */
+  theory::TheoryProofStepBuffer d_psb;
+  /** Blocked proofs.
+   *
+   * These are proof nodes added to this class by external generators. */
+  context::CDHashSet<std::shared_ptr<ProofNode>, ProofNodeHashFunction>
+      d_blocked;
+};
+
+}  // namespace prop
+}  // namespace CVC4
+
+#endif