Cleaning and documenting cnf stream (#5134)

Moreover changes assertClause to return a bool, which is gonna be used by the proof cnf stream.

6 files changed, 331 insertions, 375 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 62e4eee29..8936fb584 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -38,9 +38,6 @@
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
 
-using namespace std;
-using namespace CVC4::kind;
-
 namespace CVC4 {
 namespace prop {
 
@@ -48,6 +45,7 @@ CnfStream::CnfStream(SatSolver* satSolver,
                      Registrar* registrar,
                      context::Context* context,
                      OutputManager* outMgr,
+                     ResourceManager* rm,
                      bool fullLitToNodeMap,
                      std::string name)
     : d_satSolver(satSolver),
@@ -59,24 +57,15 @@ CnfStream::CnfStream(SatSolver* satSolver,
       d_convertAndAssertCounter(0),
       d_registrar(registrar),
       d_name(name),
-      d_cnfProof(NULL),
-      d_removable(false)
+      d_cnfProof(nullptr),
+      d_removable(false),
+      d_resourceManager(rm)
 {
 }
 
-TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver,
-                                   Registrar* registrar,
-                                   context::Context* context,
-                                   OutputManager* outMgr,
-                                   ResourceManager* rm,
-                                   bool fullLitToNodeMap,
-                                   std::string name)
-    : CnfStream(satSolver, registrar, context, outMgr, fullLitToNodeMap, name),
-      d_resourceManager(rm)
-{}
-
-void CnfStream::assertClause(TNode node, SatClause& c) {
-  Debug("cnf") << "Inserting into stream " << c << " node = " << node << endl;
+bool CnfStream::assertClause(TNode node, SatClause& c)
+{
+  Trace("cnf") << "Inserting into stream " << c << " node = " << node << "\n";
   if (Dump.isOn("clauses") && d_outMgr != nullptr)
   {
     const Printer& printer = d_outMgr->getPrinter();
@@ -98,34 +87,40 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
     }
   }
 
-  ClauseId clause_id = d_satSolver->addClause(c, d_removable);
-  if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added)
+  ClauseId clauseId = d_satSolver->addClause(c, d_removable);
 
-  if (d_cnfProof && clause_id != ClauseIdError)
+  if (d_cnfProof && clauseId != ClauseIdUndef)
   {
-    d_cnfProof->registerConvertedClause(clause_id);
+    d_cnfProof->registerConvertedClause(clauseId);
   }
+  return clauseId != ClauseIdUndef;
 }
 
-void CnfStream::assertClause(TNode node, SatLiteral a) {
+bool CnfStream::assertClause(TNode node, SatLiteral a)
+{
   SatClause clause(1);
   clause[0] = a;
-  assertClause(node, clause);
+  return assertClause(node, clause);
 }
 
-void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) {
+bool CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b)
+{
   SatClause clause(2);
   clause[0] = a;
   clause[1] = b;
-  assertClause(node, clause);
+  return assertClause(node, clause);
 }
 
-void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) {
+bool CnfStream::assertClause(TNode node,
+                             SatLiteral a,
+                             SatLiteral b,
+                             SatLiteral c)
+{
   SatClause clause(3);
   clause[0] = a;
   clause[1] = b;
   clause[2] = c;
-  assertClause(node, clause);
+  return assertClause(node, clause);
 }
 
 bool CnfStream::hasLiteral(TNode n) const {
@@ -133,11 +128,12 @@ bool CnfStream::hasLiteral(TNode n) const {
   return find != d_nodeToLiteralMap.end();
 }
 
-void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
+void CnfStream::ensureLiteral(TNode n, bool noPreregistration)
+{
   // These are not removable and have no proof ID
   d_removable = false;
 
-  Debug("cnf") << "ensureLiteral(" << n << ")" << endl;
+  Trace("cnf") << "ensureLiteral(" << n << ")\n";
   if(hasLiteral(n)) {
     SatLiteral lit = getLiteral(n);
     if(!d_literalToNodeMap.contains(lit)){
@@ -203,20 +199,25 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
 }
 
 SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister, bool canEliminate) {
-  Debug("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom << ")" << endl;
+  Trace("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom
+               << ")\n"
+               << push;
   Assert(node.getKind() != kind::NOT);
 
   // Get the literal for this node
   SatLiteral lit;
   if (!hasLiteral(node)) {
+    Trace("cnf") << d_name << "::newLiteral: node already registered\n";
     // If no literal, we'll make one
     if (node.getKind() == kind::CONST_BOOLEAN) {
+      Trace("cnf") << d_name << "::newLiteral: boolean const\n";
       if (node.getConst<bool>()) {
         lit = SatLiteral(d_satSolver->trueVar());
       } else {
         lit = SatLiteral(d_satSolver->falseVar());
       }
     } else {
+      Trace("cnf") << d_name << "::newLiteral: new var\n";
       lit = SatLiteral(d_satSolver->newVar(isTheoryAtom, preRegister, canEliminate));
     }
     d_nodeToLiteralMap.insert(node, lit);
@@ -239,19 +240,28 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister
     d_registrar->preRegister(node);
     d_removable = backupRemovable;
   }
-
   // Here, you can have it
-  Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl;
-
+  Trace("cnf") << "newLiteral(" << node << ") => " << lit << "\n" << pop;
   return lit;
 }
 
 TNode CnfStream::getNode(const SatLiteral& literal) {
-  Debug("cnf") << "getNode(" << literal << ")" << endl;
-  Debug("cnf") << "getNode(" << literal << ") => " << d_literalToNodeMap[literal] << endl;
+  Trace("cnf") << "getNode(" << literal << ")\n";
+  Trace("cnf") << "getNode(" << literal << ") => "
+               << d_literalToNodeMap[literal] << "\n";
   return d_literalToNodeMap[literal];
 }
 
+const CnfStream::NodeToLiteralMap& CnfStream::getTranslationCache() const
+{
+  return d_nodeToLiteralMap;
+}
+
+const CnfStream::LiteralToNodeMap& CnfStream::getNodeCache() const
+{
+  return d_literalToNodeMap;
+}
+
 void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
   context::CDList<TNode>::const_iterator it, it_end;
   for (it = d_booleanVariables.begin(); it != d_booleanVariables.end(); ++ it) {
@@ -265,7 +275,7 @@ void CnfStream::setProof(CnfProof* proof) {
 }
 
 SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
-  Debug("cnf") << "convertAtom(" << node << ")" << endl;
+  Trace("cnf") << "convertAtom(" << node << ")\n";
 
   Assert(!hasLiteral(node)) << "atom already mapped!";
 
@@ -274,9 +284,12 @@ SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
   bool preRegister = false;
 
   // Is this a variable add it to the list
-  if (node.isVar() && node.getKind()!=BOOLEAN_TERM_VARIABLE) {
+  if (node.isVar() && node.getKind() != kind::BOOLEAN_TERM_VARIABLE)
+  {
     d_booleanVariables.push_back(node);
-  } else {
+  }
+  else
+  {
     theoryLiteral = true;
     canEliminate = false;
     preRegister = !noPreregistration;
@@ -295,15 +308,18 @@ SatLiteral CnfStream::getLiteral(TNode node) {
       << "Literal not in the CNF Cache: " << node << "\n";
 
   SatLiteral literal = d_nodeToLiteralMap[node];
-  Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
+  Trace("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal
+               << "\n";
   return literal;
 }
 
-SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
+SatLiteral CnfStream::handleXor(TNode xorNode)
+{
   Assert(!hasLiteral(xorNode)) << "Atom already mapped!";
-  Assert(xorNode.getKind() == XOR) << "Expecting an XOR expression!";
+  Assert(xorNode.getKind() == kind::XOR) << "Expecting an XOR expression!";
   Assert(xorNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
   Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Trace("cnf") << "CnfStream::handleXor(" << xorNode << ")\n";
 
   SatLiteral a = toCNF(xorNode[0]);
   SatLiteral b = toCNF(xorNode[1]);
@@ -318,11 +334,13 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
   return xorLit;
 }
 
-SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
+SatLiteral CnfStream::handleOr(TNode orNode)
+{
   Assert(!hasLiteral(orNode)) << "Atom already mapped!";
-  Assert(orNode.getKind() == OR) << "Expecting an OR expression!";
+  Assert(orNode.getKind() == kind::OR) << "Expecting an OR expression!";
   Assert(orNode.getNumChildren() > 1) << "Expecting more then 1 child!";
   Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Trace("cnf") << "CnfStream::handleOr(" << orNode << ")\n";
 
   // Number of children
   unsigned n_children = orNode.getNumChildren();
@@ -355,11 +373,13 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
   return orLit;
 }
 
-SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
+SatLiteral CnfStream::handleAnd(TNode andNode)
+{
   Assert(!hasLiteral(andNode)) << "Atom already mapped!";
-  Assert(andNode.getKind() == AND) << "Expecting an AND expression!";
+  Assert(andNode.getKind() == kind::AND) << "Expecting an AND expression!";
   Assert(andNode.getNumChildren() > 1) << "Expecting more than 1 child!";
   Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Trace("cnf") << "handleAnd(" << andNode << ")\n";
 
   // Number of children
   unsigned n_children = andNode.getNumChildren();
@@ -392,12 +412,14 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
   return andLit;
 }
 
-SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
+SatLiteral CnfStream::handleImplies(TNode impliesNode)
+{
   Assert(!hasLiteral(impliesNode)) << "Atom already mapped!";
-  Assert(impliesNode.getKind() == IMPLIES)
+  Assert(impliesNode.getKind() == kind::IMPLIES)
       << "Expecting an IMPLIES expression!";
   Assert(impliesNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
   Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Trace("cnf") << "handleImplies(" << impliesNode << ")\n";
 
   // Convert the children to cnf
   SatLiteral a = toCNF(impliesNode[0]);
@@ -418,13 +440,13 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
   return impliesLit;
 }
 
-
-SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
+SatLiteral CnfStream::handleIff(TNode iffNode)
+{
   Assert(!hasLiteral(iffNode)) << "Atom already mapped!";
-  Assert(iffNode.getKind() == EQUAL) << "Expecting an EQUAL expression!";
+  Assert(iffNode.getKind() == kind::EQUAL) << "Expecting an EQUAL expression!";
   Assert(iffNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
-
-  Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
+  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
+  Trace("cnf") << "handleIff(" << iffNode << ")\n";
 
   // Convert the children to CNF
   SatLiteral a = toCNF(iffNode[0]);
@@ -450,23 +472,14 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
   return iffLit;
 }
 
-
-SatLiteral TseitinCnfStream::handleNot(TNode notNode) {
-  Assert(!hasLiteral(notNode)) << "Atom already mapped!";
-  Assert(notNode.getKind() == NOT) << "Expecting a NOT expression!";
-  Assert(notNode.getNumChildren() == 1) << "Expecting exactly 1 child!";
-
-  SatLiteral notLit = ~toCNF(notNode[0]);
-
-  return notLit;
-}
-
-SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
-  Assert(iteNode.getKind() == ITE);
+SatLiteral CnfStream::handleIte(TNode iteNode)
+{
+  Assert(!hasLiteral(iteNode)) << "Atom already mapped!";
+  Assert(iteNode.getKind() == kind::ITE);
   Assert(iteNode.getNumChildren() == 3);
   Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
-
-  Debug("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl;
+  Trace("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " "
+               << iteNode[2] << ")\n";
 
   SatLiteral condLit = toCNF(iteNode[0]);
   SatLiteral thenLit = toCNF(iteNode[1]);
@@ -497,64 +510,48 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   return iteLit;
 }
 
-
-SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
-  Debug("cnf") << "toCNF(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
-
+SatLiteral CnfStream::toCNF(TNode node, bool negated)
+{
+  Trace("cnf") << "toCNF(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
   SatLiteral nodeLit;
   Node negatedNode = node.notNode();
 
   // If the non-negated node has already been translated, get the translation
   if(hasLiteral(node)) {
-    Debug("cnf") << "toCNF(): already translated" << endl;
+    Trace("cnf") << "toCNF(): already translated\n";
     nodeLit = getLiteral(node);
-  } else {
-    // Handle each Boolean operator case
-    switch(node.getKind()) {
-    case NOT:
-      nodeLit = handleNot(node);
-      break;
-    case XOR:
-      nodeLit = handleXor(node);
-      break;
-    case ITE:
-      nodeLit = handleIte(node);
-      break;
-    case IMPLIES:
-      nodeLit = handleImplies(node);
-      break;
-    case OR:
-      nodeLit = handleOr(node);
-      break;
-    case AND:
-      nodeLit = handleAnd(node);
-      break;
-    case EQUAL:
-      if(node[0].getType().isBoolean()) {
-        nodeLit = handleIff(node);
-      } else {
-        nodeLit = convertAtom(node);
-      }
+    // Return the (maybe negated) literal
+    return !negated ? nodeLit : ~nodeLit;
+  }
+  // Handle each Boolean operator case
+  switch (node.getKind())
+  {
+    case kind::NOT: nodeLit = ~toCNF(node[0]); break;
+    case kind::XOR: nodeLit = handleXor(node); break;
+    case kind::ITE: nodeLit = handleIte(node); break;
+    case kind::IMPLIES: nodeLit = handleImplies(node); break;
+    case kind::OR: nodeLit = handleOr(node); break;
+    case kind::AND: nodeLit = handleAnd(node); break;
+    case kind::EQUAL:
+      nodeLit =
+          node[0].getType().isBoolean() ? handleIff(node) : convertAtom(node);
       break;
     default:
-      {
-        //TODO make sure this does not contain any boolean substructure
-        nodeLit = convertAtom(node);
-        //Unreachable();
-        //Node atomic = handleNonAtomicNode(node);
-        //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic);
-      }
-      break;
+    {
+      nodeLit = convertAtom(node);
     }
+    break;
   }
-
-  // Return the appropriate (negated) literal
-  if (!negated) return nodeLit;
-  else return ~nodeLit;
+  // Return the (maybe negated) literal
+  return !negated ? nodeLit : ~nodeLit;
 }
 
-void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
-  Assert(node.getKind() == AND);
+void CnfStream::convertAndAssertAnd(TNode node, bool negated)
+{
+  Assert(node.getKind() == kind::AND);
+  Trace("cnf") << "CnfStream::convertAndAssertAnd(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
   if (!negated) {
     // If the node is a conjunction, we handle each conjunct separately
     for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
@@ -575,8 +572,11 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
   }
 }
 
-void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
-  Assert(node.getKind() == OR);
+void CnfStream::convertAndAssertOr(TNode node, bool negated)
+{
+  Assert(node.getKind() == kind::OR);
+  Trace("cnf") << "CnfStream::convertAndAssertOr(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
   if (!negated) {
     // If the node is a disjunction, we construct a clause and assert it
     int nChildren = node.getNumChildren();
@@ -597,7 +597,11 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
   }
 }
 
-void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
+void CnfStream::convertAndAssertXor(TNode node, bool negated)
+{
+  Assert(node.getKind() == kind::XOR);
+  Trace("cnf") << "CnfStream::convertAndAssertXor(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
   if (!negated) {
     // p XOR q
     SatLiteral p = toCNF(node[0], false);
@@ -627,7 +631,11 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
   }
 }
 
-void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
+void CnfStream::convertAndAssertIff(TNode node, bool negated)
+{
+  Assert(node.getKind() == kind::EQUAL);
+  Trace("cnf") << "CnfStream::convertAndAssertIff(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
   if (!negated) {
     // p <=> q
     SatLiteral p = toCNF(node[0], false);
@@ -657,7 +665,11 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
   }
 }
 
-void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
+void CnfStream::convertAndAssertImplies(TNode node, bool negated)
+{
+  Assert(node.getKind() == kind::IMPLIES);
+  Trace("cnf") << "CnfStream::convertAndAssertImplies(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
   if (!negated) {
     // p => q
     SatLiteral p = toCNF(node[0], false);
@@ -674,13 +686,20 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
   }
 }
 
-void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
+void CnfStream::convertAndAssertIte(TNode node, bool negated)
+{
+  Assert(node.getKind() == kind::ITE);
+  Trace("cnf") << "CnfStream::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);
   // Construct the clauses:
   // (p => q) and (!p => 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 = node;
   if( negated ){
     nnode = node.negate();
@@ -698,14 +717,14 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
 // At the top level we must ensure that all clauses that are asserted are
 // not unit, except for the direct assertions. This allows us to remove the
 // clauses later when they are not needed anymore (lemmas for example).
-void TseitinCnfStream::convertAndAssert(TNode node,
-                                        bool removable,
-                                        bool negated,
-                                        bool input)
+void CnfStream::convertAndAssert(TNode node,
+                                 bool removable,
+                                 bool negated,
+                                 bool input)
 {
-  Debug("cnf") << "convertAndAssert(" << node
-               << ", removable = " << (removable ? "true" : "false")
-               << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+  Trace("cnf") << "convertAndAssert(" << node
+               << ", negated = " << (negated ? "true" : "false")
+               << ", removable = " << (removable ? "true" : "false") << ")\n";
   d_removable = removable;
 
   if (d_cnfProof)
@@ -720,9 +739,10 @@ void TseitinCnfStream::convertAndAssert(TNode node,
   }
 }
 
-void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
-  Debug("cnf") << "convertAndAssert(" << node
-               << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+void CnfStream::convertAndAssert(TNode node, bool negated)
+{
+  Trace("cnf") << "convertAndAssert(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")\n";
 
   if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
     d_resourceManager->spendResource(ResourceManager::Resource::CnfStep);
@@ -731,38 +751,28 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   ++d_convertAndAssertCounter;
 
   switch(node.getKind()) {
-  case AND:
-    convertAndAssertAnd(node, negated);
-    break;
-  case OR:
-    convertAndAssertOr(node, negated);
-    break;
-  case XOR:
-    convertAndAssertXor(node, negated);
-    break;
-  case IMPLIES:
-    convertAndAssertImplies(node, negated);
-    break;
-  case ITE:
-    convertAndAssertIte(node, negated);
-    break;
-  case NOT:
-    convertAndAssert(node[0], !negated);
-    break;
-  case EQUAL:
-    if( node[0].getType().isBoolean() ){
-      convertAndAssertIff(node, negated);
-      break;
-    }
-    CVC4_FALLTHROUGH;
-  default:
-  {
-    Node nnode = node;
-    if( negated ){
-      nnode = node.negate();
-    }
-    // Atoms
-    assertClause(nnode, toCNF(node, negated));
+    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: convertAndAssert(node[0], !negated); break;
+    case kind::EQUAL:
+      if (node[0].getType().isBoolean())
+      {
+        convertAndAssertIff(node, negated);
+        break;
+      }
+      CVC4_FALLTHROUGH;
+    default:
+    {
+      Node nnode = node;
+      if (negated)
+      {
+        nnode = node.negate();
+      }
+      // Atoms
+      assertClause(nnode, toCNF(node, negated));
   }
     break;
   }
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index ea64ccf13..3f40bfbbd 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -41,8 +41,13 @@ namespace prop {
 class PropEngine;
 
 /**
- * Comments for the behavior of the whole class... [??? -Chris]
- * @author Tim King <taking@cs.nyu.edu>
+ * Implements the following recursive algorithm
+ * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
+ * in a single pass.
+ *
+ * The general idea is to introduce a new literal that will be equivalent to
+ * each subexpression in the constructed equi-satisfiable formula, then
+ * substitute the new literal for the formula, and so on, recursively.
  */
 class CnfStream {
  public:
@@ -54,7 +59,123 @@ class CnfStream {
   typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction>
       NodeToLiteralMap;
 
+  /**
+   * Constructs a CnfStream that performs equisatisfiable CNF transformations
+   * and sends the generated clauses and to the given SAT solver. This does not
+   * take ownership of satSolver, registrar, or context.
+   *
+   * @param satSolver the sat solver to use.
+   * @param registrar the entity that takes care of preregistration of Nodes.
+   * @param context the context that the CNF should respect.
+   * @param outMgr Reference to the output manager of the smt engine. Assertions
+   * will not be dumped if outMgr == nullptr.
+   * @param rm the resource manager of the CNF stream
+   * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping.
+   * @param name string identifier to distinguish between different instances
+   * even for non-theory literals.
+   */
+  CnfStream(SatSolver* satSolver,
+            Registrar* registrar,
+            context::Context* context,
+            OutputManager* outMgr,
+            ResourceManager* rm,
+            bool fullLitToNodeMap = false,
+            std::string name = "");
+  /**
+   * Convert a given formula to CNF and assert it to the SAT solver.
+   *
+   * @param node node to convert and assert
+   * @param removable whether the sat solver can choose to remove the clauses
+   * @param negated whether we are asserting the node negated
+   * @param input whether it is an input assertion (rather than a lemma). This
+   * information is only relevant for unsat core tracking.
+   */
+  void convertAndAssert(TNode node,
+                        bool removable,
+                        bool negated,
+                        bool input = false);
+  /**
+   * Get the node that is represented by the given SatLiteral.
+   * @param literal the literal from the sat solver
+   * @return the actual node
+   */
+  TNode getNode(const SatLiteral& literal);
+
+  /**
+   * Returns true iff the node has an assigned literal (it might not be
+   * translated).
+   * @param node the node
+   */
+  bool hasLiteral(TNode node) const;
+
+  /**
+   * Ensure that the given node will have a designated SAT literal that is
+   * definitionally equal to it.  The result of this function is that the Node
+   * can be queried via getSatValue(). Essentially, this is like a "convert-but-
+   * don't-assert" version of convertAndAssert().
+   */
+  void ensureLiteral(TNode n, bool noPreregistration = false);
+
+  /**
+   * Returns the literal that represents the given node in the SAT CNF
+   * representation.
+   * @param node [Presumably there are some constraints on the kind of
+   * node? E.g., it needs to be a boolean? -Chris]
+   */
+  SatLiteral getLiteral(TNode node);
+
+  /**
+   * Returns the Boolean variables from the input problem.
+   */
+  void getBooleanVariables(std::vector<TNode>& outputVariables) const;
+
+  /** Retrieves map from nodes to literals. */
+  const CnfStream::NodeToLiteralMap& getTranslationCache() const;
+
+  /** Retrieves map from literals to nodes. */
+  const CnfStream::LiteralToNodeMap& getNodeCache() const;
+
+  void setProof(CnfProof* proof);
+
  protected:
+  /**
+   * 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);
+
   /** The SAT solver we will be using */
   SatSolver* d_satSolver;
 
@@ -92,14 +213,6 @@ class CnfStream {
   /** Pointer to the proof corresponding to this CnfStream */
   CnfProof* d_cnfProof;
 
-  /** Remove nots from the node */
-  TNode stripNot(TNode node) {
-    while (node.getKind() == kind::NOT) {
-      node = node[0];
-    }
-    return node;
-  }
-
   /**
    * 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
@@ -112,23 +225,26 @@ class CnfStream {
    * Asserts the given clause to the sat solver.
    * @param node the node giving rise to this clause
    * @param clause the clause to assert
+   * @return whether the clause was asserted in the SAT solver.
    */
-  void assertClause(TNode node, SatClause& clause);
+  bool assertClause(TNode node, SatClause& clause);
 
   /**
    * Asserts the unit clause to the sat solver.
    * @param node the node giving rise to this clause
    * @param a the unit literal of the clause
+   * @return whether the clause was asserted in the SAT solver.
    */
-  void assertClause(TNode node, SatLiteral a);
+  bool assertClause(TNode node, SatLiteral a);
 
   /**
    * Asserts the binary clause to the sat solver.
    * @param node the node giving rise to this clause
    * @param a the first literal in the clause
    * @param b the second literal in the clause
+   * @return whether the clause was asserted in the SAT solver.
    */
-  void assertClause(TNode node, SatLiteral a, SatLiteral b);
+  bool assertClause(TNode node, SatLiteral a, SatLiteral b);
 
   /**
    * Asserts the ternary clause to the sat solver.
@@ -136,8 +252,9 @@ class CnfStream {
    * @param a the first literal in the clause
    * @param b the second literal in the clause
    * @param c the thirs literal in the clause
+   * @return whether the clause was asserted in the SAT solver.
    */
-  void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
+  bool assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
 
   /**
    * Acquires a new variable from the SAT solver to represent the node
@@ -163,182 +280,11 @@ class CnfStream {
    */
   SatLiteral convertAtom(TNode node, bool noPreprocessing = false);
 
- public:
-  /**
-   * Constructs a CnfStream that sends constructs an equi-satisfiable
-   * set of clauses and sends them to the given sat solver. This does not take
-   * ownership of satSolver, registrar, or context.
-   * @param satSolver the sat solver to use.
-   * @param registrar the entity that takes care of preregistration of Nodes.
-   * @param context the context that the CNF should respect.
-   * @param outMgr Reference to the output manager of the smt engine. Assertions
-   * will not be dumped if outMgr == nullptr.
-   * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping.
-   * @param name string identifier to distinguish between different instances
-   * even for non-theory literals.
-   */
-  CnfStream(SatSolver* satSolver,
-            Registrar* registrar,
-            context::Context* context,
-            OutputManager* outMgr = nullptr,
-            bool fullLitToNodeMap = false,
-            std::string name = "");
-
-  /**
-   * Destructs a CnfStream.  This implementation does nothing, but we
-   * need a virtual destructor for safety in case subclasses have a
-   * destructor.
-   */
-  virtual ~CnfStream() {}
-
-  /**
-   * Converts and asserts a formula.
-   * @param node node to convert and assert
-   * @param removable whether the sat solver can choose to remove the clauses
-   * @param negated whether we are asserting the node negated
-   * @param input whether it is an input assertion (rather than a lemma). This
-   * information is only relevant for unsat core tracking.
-   */
-  virtual void convertAndAssert(TNode node,
-                                bool removable,
-                                bool negated,
-                                bool input = false) = 0;
-
-  /**
-   * Get the node that is represented by the given SatLiteral.
-   * @param literal the literal from the sat solver
-   * @return the actual node
-   */
-  TNode getNode(const SatLiteral& literal);
-
-  /**
-   * Returns true iff the node has an assigned literal (it might not be
-   * translated).
-   * @param node the node
-   */
-  bool hasLiteral(TNode node) const;
-
-  /**
-   * Ensure that the given node will have a designated SAT literal that is
-   * definitionally equal to it.  The result of this function is that the Node
-   * can be queried via getSatValue(). Essentially, this is like a "convert-but-
-   * don't-assert" version of convertAndAssert().
-   */
-  virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0;
-
-  /**
-   * Returns the literal that represents the given node in the SAT CNF
-   * representation.
-   * @param node [Presumably there are some constraints on the kind of
-   * node? E.g., it needs to be a boolean? -Chris]
-   */
-  SatLiteral getLiteral(TNode node);
-
-  /**
-   * Returns the Boolean variables from the input problem.
-   */
-  void getBooleanVariables(std::vector<TNode>& outputVariables) const;
-
-  const NodeToLiteralMap& getTranslationCache() const {
-    return d_nodeToLiteralMap;
-  }
-
-  const LiteralToNodeMap& getNodeCache() const { return d_literalToNodeMap; }
-
-  void setProof(CnfProof* proof);
-}; /* class CnfStream */
-
-/**
- * TseitinCnfStream is based on the following recursive algorithm
- * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
- * The general idea is to introduce a new literal that
- * will be equivalent to each subexpression in the constructed equi-satisfiable
- * formula, then substitute the new literal for the formula, and so on,
- * recursively.
- *
- * This implementation does this in a single recursive pass. [??? -Chris]
- */
-class TseitinCnfStream : public CnfStream {
- public:
-  /**
-   * Constructs the stream to use the given sat solver.  This does not take
-   * ownership of satSolver, registrar, or context.
-   * @param satSolver the sat solver to use
-   * @param registrar the entity that takes care of pre-registration of Nodes
-   * @param context the context that the CNF should respect.
-   * @param outMgr reference to the output manager of the smt engine. Assertions
-   * will not be dumped if outMgr == nullptr.
-   * @param rm the resource manager of the CNF stream
-   * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
-   * even for non-theory literals
-   */
-  TseitinCnfStream(SatSolver* satSolver,
-                   Registrar* registrar,
-                   context::Context* context,
-                   OutputManager* outMgr,
-                   ResourceManager* rm,
-                   bool fullLitToNodeMap = false,
-                   std::string name = "");
-
-  /**
-   * Convert a given formula to CNF and assert it to the SAT solver.
-   * @param node the formula to assert
-   * @param removable is this something that can be erased
-   * @param negated true if negated
-   * @param input whether it is an input assertion (rather than a lemma). This
-   * information is only relevant for unsat core tracking.
-   */
-  void convertAndAssert(TNode node,
-                        bool removable,
-                        bool negated,
-                        bool input = false) override;
-
- private:
-  /**
-   * Same as above, except that removable is remembered.
-   */
-  void convertAndAssert(TNode node, bool negated);
-
-  // Each of these formulas handles takes care of a Node of each Kind.
-  //
-  // Each handleX(Node &n) is responsible for:
-  //   - constructing a new literal, l (if necessary)
-  //   - calling registerNode(n,l)
-  //   - adding clauses assure that l is equivalent to the Node
-  //   - calling toCNF on its children (if necessary)
-  //   - returning l
-  //
-  // handleX( n ) can assume that n is not in d_translationCache
-  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);
-
-  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.
-   * @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);
-
-  void ensureLiteral(TNode n, bool noPreregistration = false) override;
-
   /** Pointer to resource manager for associated SmtEngine */
   ResourceManager* d_resourceManager;
-}; /* class TseitinCnfStream */
+}; /* class CnfStream */
 
-} /* CVC4::prop namespace */
-} /* CVC4 namespace */
+}  // namespace prop
+}  // namespace CVC4
 
 #endif /* CVC4__PROP__CNF_STREAM_H */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index e3f00d489..4596972e9 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -91,7 +91,7 @@ PropEngine::PropEngine(TheoryEngine* te,
   d_satSolver = SatSolverFactory::createDPLLMinisat(smtStatisticsRegistry());
 
   d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
-  d_cnfStream = new CVC4::prop::TseitinCnfStream(
+  d_cnfStream = new CVC4::prop::CnfStream(
       d_satSolver, d_registrar, userContext, &d_outMgr, rm, true);
 
   d_theoryProxy = new TheoryProxy(
diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index c48e20224..046ad4b1b 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -69,13 +69,13 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
   }
   d_satSolver.reset(solver);
   ResourceManager* rm = smt::currentResourceManager();
-  d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
-                                               d_bitblastingRegistrar.get(),
-                                               d_nullContext.get(),
-                                               nullptr,
-                                               rm,
-                                               false,
-                                               "EagerBitblaster"));
+  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
+                                        d_bitblastingRegistrar.get(),
+                                        d_nullContext.get(),
+                                        nullptr,
+                                        rm,
+                                        false,
+                                        "EagerBitblaster"));
 }
 
 EagerBitblaster::~EagerBitblaster() {}
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.cpp b/src/theory/bv/bitblast/lazy_bitblaster.cpp
index c6590db81..95d78c69b 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.cpp
+++ b/src/theory/bv/bitblast/lazy_bitblaster.cpp
@@ -80,13 +80,13 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c,
       prop::SatSolverFactory::createMinisat(c, smtStatisticsRegistry(), name));
 
   ResourceManager* rm = smt::currentResourceManager();
-  d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
-                                               d_nullRegistrar.get(),
-                                               d_nullContext.get(),
-                                               nullptr,
-                                               rm,
-                                               false,
-                                               "LazyBitblaster"));
+  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
+                                        d_nullRegistrar.get(),
+                                        d_nullContext.get(),
+                                        nullptr,
+                                        rm,
+                                        false,
+                                        "LazyBitblaster"));
 
   d_satSolverNotify.reset(
       d_emptyNotify
@@ -575,11 +575,11 @@ void TLazyBitblaster::clearSolver() {
   d_satSolver.reset(
       prop::SatSolverFactory::createMinisat(d_ctx, smtStatisticsRegistry()));
   ResourceManager* rm = smt::currentResourceManager();
-  d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
-                                               d_nullRegistrar.get(),
-                                               d_nullContext.get(),
-                                               nullptr,
-                                               rm));
+  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
+                                        d_nullRegistrar.get(),
+                                        d_nullContext.get(),
+                                        nullptr,
+                                        rm));
   d_satSolverNotify.reset(
       d_emptyNotify
           ? (prop::BVSatSolverNotify*)new MinisatEmptyNotify()
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index d64749d6b..ae79e1517 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -146,11 +146,11 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     d_cnfContext = new context::Context();
     d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine);
     ResourceManager* rm = d_smt->getResourceManager();
-    d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver,
-                                                   d_cnfRegistrar,
-                                                   d_cnfContext,
-                                                   &d_smt->getOutputManager(),
-                                                   rm);
+    d_cnfStream = new CVC4::prop::CnfStream(d_satSolver,
+                                            d_cnfRegistrar,
+                                            d_cnfContext,
+                                            &d_smt->getOutputManager(),
+                                            rm);
   }
 
   void tearDown() override