Cleaning and documenting cnf stream (#5134)

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

1 files changed, 172 insertions, 162 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;
   }