fixes to incremental simplification, cnf routines, other stuff in preparation of user push/pop in SAT solver

3 files changed, 20 insertions, 8 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 5b8e4c3f3..4e557d416 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -103,17 +103,22 @@ bool CnfStream::isTranslated(TNode n) const {
   return find != d_translationCache.end() && find->second.level >= 0;
 }
 
-bool CnfStream::hasLiteral(TNode n) const {
+bool CnfStream::hasEverHadLiteral(TNode n) const {
   TranslationCache::const_iterator find = d_translationCache.find(n);
   return find != d_translationCache.end();
 }
 
+bool CnfStream::currentlyHasLiteral(TNode n) const {
+  TranslationCache::const_iterator find = d_translationCache.find(n);
+  return find != d_translationCache.end() && (*find).second.level != -1;
+}
+
 SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl;
 
   // Get the literal for this node
   SatLiteral lit;
-  if (!hasLiteral(node)) {
+  if (!hasEverHadLiteral(node)) {
     // If no literal, well make one
     lit = variableToLiteral(d_satSolver->newVar(theoryLiteral));
     d_translationCache[node].literal = lit;
@@ -599,13 +604,16 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated
 void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
   Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
-  if(hasLiteral(node)) {
+  /*
+  if(currentlyHasLiteral(node)) {
     Debug("cnf") << "==> fortunate literal detected!" << endl;
     ++d_fortunateLiterals;
     SatLiteral lit = getLiteral(node);
     //d_satSolver->renewVar(lit);
     assertClause(node, negated ? ~lit : lit);
+    return;
   }
+  */
 
   switch(node.getKind()) {
   case AND:
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index ecb0fd2fb..3ef636811 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -215,12 +215,16 @@ public:
   TNode getNode(const SatLiteral& literal);
 
   /**
-   * Returns true if the node has an assigned literal (it might not be translated).
-   * Caches the pair of the node and the literal corresponding to the
-   * translation.
+   * Returns true iff the node has an assigned literal (it might not be translated).
    * @param node the node
    */
-  bool hasLiteral(TNode node) const;
+  bool hasEverHadLiteral(TNode node) const;
+
+  /**
+   * Returns true iff the node has an assigned literal and it's translated.
+   * @param node the node
+   */
+  bool currentlyHasLiteral(TNode node) const;
 
   /**
    * Returns the literal that represents the given node in the SAT CNF
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index c8e4083b1..7b4155bde 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -167,7 +167,7 @@ Node PropEngine::getValue(TNode node) {
 }
 
 bool PropEngine::isSatLiteral(TNode node) {
-  return d_cnfStream->hasLiteral(node);
+  return d_cnfStream->hasEverHadLiteral(node);
 }
 
 bool PropEngine::hasValue(TNode node, bool& value) {