1 files changed, 21 insertions, 20 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 45f7ab398..9136a73c3 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -102,26 +102,10 @@ Node CnfStream::getNode(const SatLiteral& literal) {
   return node;
 }
 
-SatLiteral CnfStream::getLiteral(TNode node) {
-  TranslationCache::iterator find = d_translationCache.find(node);
-  Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
-  SatLiteral literal = find->second;
-  Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
-  return literal;
-}
-
-const CnfStream::NodeCache& CnfStream::getNodeCache() const {
-  return d_nodeCache;
-}
-
-const CnfStream::TranslationCache& CnfStream::getTranslationCache() const {
-  return d_translationCache;
-}
-
-SatLiteral TseitinCnfStream::handleAtom(TNode node) {
+SatLiteral CnfStream::convertAtom(TNode node) {
   Assert(!isCached(node), "atom already mapped!");
 
-  Debug("cnf") << "handleAtom(" << node << ")" << endl;
+  Debug("cnf") << "convertAtom(" << node << ")" << endl;
 
   bool theoryLiteral = node.getKind() != kind::VARIABLE;
   SatLiteral lit = newLiteral(node, theoryLiteral);
@@ -137,6 +121,23 @@ SatLiteral TseitinCnfStream::handleAtom(TNode node) {
   return lit;
 }
 
+SatLiteral CnfStream::getLiteral(TNode node, bool create /* = false */) {
+  TranslationCache::iterator find = d_translationCache.find(node);
+  SatLiteral literal;
+  if(create) {
+    if(find == d_translationCache.end()) {
+      literal = convertAtom(node);
+    } else {
+      literal = find->second;
+    }
+  } else {
+    Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
+    literal = find->second;
+  }
+  Debug("cnf") << "CnfStream::getLiteral(" << node << ", create = " << create << ") => " << literal << std::endl;
+  return literal;
+}
+
 SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
   Assert(!isCached(xorNode), "Atom already mapped!");
   Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!");
@@ -366,10 +367,10 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
     default:
       {
         //TODO make sure this does not contain any boolean substructure
-        nodeLit = handleAtom(node);
+        nodeLit = convertAtom(node);
         //Unreachable();
         //Node atomic = handleNonAtomicNode(node);
-        //return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic);
+        //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic);
       }
     }
   }