Partial merge from kind-backend branch, including Minisat and CNF work to

support incrementality.

Some clean-up work will likely follow, but the CNF/Minisat stuff should be
left pretty much untouched.

Expected performance change negligible; slightly better on memory:
  http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5
Note that there are crashes, but that these are exhibited in the nightly
regression run too!

1 files changed, 66 insertions, 9 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 9f49d81a2..396454fac 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -50,9 +50,19 @@ CnfStream::CnfStream(SatSolverInterface *satSolver, Registrar* registrar, bool f
   d_registrar(registrar) {
 }
 
-void CnfStream::recordTranslation(TNode node) {
+void CnfStream::recordTranslation(TNode node, bool alwaysRecord) {
+  Debug("cnf") << "recordTranslation(" << alwaysRecord << "," << d_removable << "): " << node << std::endl;
   if (!d_removable) {
-    d_translationTrail.push_back(stripNot(node));
+    node = stripNot(node);
+    if(d_translationCache.find(node)->second.recorded) {
+      Debug("cnf") << "--> Already recorded, not recording again." << std::endl;
+    } else {
+      Debug("cnf") << "--> Recorded at position " << d_translationTrail.size() << ". (level " << d_translationCache.find(node)->second.level << ")" << std::endl;
+      Assert(d_translationTrail.empty() || d_translationCache.find(node)->second.level >= d_translationCache.find(d_translationTrail.back())->second.level, "levels on the translation trail should be monotonically increasing ?!");
+      d_translationTrail.push_back(node);
+      d_translationCache.find(node)->second.recorded = true;
+      d_translationCache.find(node.notNode())->second.recorded = true;
+    }
   }
 }
 
@@ -112,7 +122,8 @@ bool CnfStream::hasLiteral(TNode n) const {
 void TseitinCnfStream::ensureLiteral(TNode n) {
   if(hasLiteral(n)) {
     // Already a literal!
-    SatLiteral lit = getLiteral(n);
+    // newLiteral() may be necessary to renew a previously-extant literal
+    SatLiteral lit = isTranslated(n) ? getLiteral(n) : newLiteral(n, true);
     NodeCache::iterator i = d_nodeCache.find(lit);
     if(i == d_nodeCache.end()) {
       // Store backward-mappings
@@ -158,11 +169,12 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
 
 SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   Debug("cnf") << "newLiteral(" << node << ", " << theoryLiteral << ")" << endl;
+  Assert(node.getKind() != kind::NOT);
 
   // Get the literal for this node
   SatLiteral lit;
   if (!hasLiteral(node)) {
-    // If no literal, well make one
+    // If no literal, we'll make one
     lit = SatLiteral(d_satSolver->newVar(theoryLiteral));
     d_translationCache[node].literal = lit;
     d_translationCache[node.notNode()].literal = ~lit;
@@ -174,13 +186,15 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
 
   // We will translate clauses, so remember the level
   int level = d_satSolver->getAssertionLevel();
+  d_translationCache[node].recorded = false;
+  d_translationCache[node.notNode()].recorded = false;
   d_translationCache[node].level = level;
   d_translationCache[node.notNode()].level = level;
 
   // If it's a theory literal, need to store it for back queries
   if ( theoryLiteral || d_fullLitToNodeMap ||
        ( CVC4_USE_REPLAY && Options::current()->replayLog != NULL ) ||
-       Dump.isOn("clauses") ) {
+       (Dump.isOn("clauses")) ) {
     d_nodeCache[lit] = node;
     d_nodeCache[~lit] = node.notNode();
   }
@@ -223,6 +237,11 @@ SatLiteral CnfStream::convertAtom(TNode node) {
     }
   }
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(node, true);
+
   return lit;
 }
 
@@ -250,6 +269,11 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
   assertClause(xorNode, a, ~b, xorLit);
   assertClause(xorNode, ~a, b, xorLit);
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(xorNode, true);
+
   return xorLit;
 }
 
@@ -285,6 +309,11 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
   // This needs to go last, as the clause might get modified by the SAT solver
   assertClause(orNode, clause);
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(orNode, true);
+
   // Return the literal
   return orLit;
 }
@@ -321,6 +350,12 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
   clause[n_children] = andLit;
   // This needs to go last, as the clause might get modified by the SAT solver
   assertClause(andNode, clause);
+
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(andNode, true);
+
   return andLit;
 }
 
@@ -345,6 +380,11 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
   assertClause(impliesNode, a, impliesLit);
   assertClause(impliesNode, ~b, impliesLit);
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(impliesNode, true);
+
   return impliesLit;
 }
 
@@ -377,6 +417,11 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
   assertClause(iffNode, ~a, ~b, iffLit);
   assertClause(iffNode, a, b, iffLit);
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(iffNode, true);
+
   return iffLit;
 }
 
@@ -423,6 +468,11 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   assertClause(iteNode, iteLit, ~condLit, ~thenLit);
   assertClause(iteNode, iteLit, condLit, ~elseLit);
 
+  // We have a literal, so it has to be recorded.  The definitional clauses
+  // go away on user-pop, so this literal will have to be re-vivified if it's
+  // used subsequently.
+  recordTranslation(iteNode, true);
+
   return iteLit;
 }
 
@@ -435,6 +485,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
 
   // If the non-negated node has already been translated, get the translation
   if(isTranslated(node)) {
+    Debug("cnf") << "toCNF(): already translated" << endl;
     nodeLit = getLiteral(node);
   } else {
     // Handle each Boolean operator case
@@ -690,15 +741,19 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
 
 void CnfStream::removeClausesAboveLevel(int level) {
   while (d_translationTrail.size() > 0) {
+    Debug("cnf") << "Considering translation trail position " << d_translationTrail.size() << std::endl;
     TNode node = d_translationTrail.back();
+    // Get the translation information
+    TranslationInfo& infoPos = d_translationCache.find(node)->second;
+    // If the level of the node is less or equal to given we are done
+    if (infoPos.level >= 0 && infoPos.level <= level) {
+      Debug("cnf") << "Node is " << node << " level " << infoPos.level << ", we're done." << std::endl;
+      break;
+    }
     Debug("cnf") << "Removing node " << node << " from CNF translation" << endl;
     d_translationTrail.pop_back();
-    // Get the translation informations
-    TranslationInfo& infoPos = d_translationCache.find(node)->second;
     // If already untranslated, we're done
     if (infoPos.level == -1) continue;
-    // If the level of the node is less or equal to given we are done
-    if (infoPos.level <= level) break;
     // Otherwise we have to undo the translation
     undoTranslate(node, level);
   }
@@ -734,6 +789,7 @@ void CnfStream::undoTranslate(TNode node, int level) {
 
   // Untranslate
   infoPos.level = -1;
+  infoPos.recorded = false;
 
   // Untranslate the negation node
   // If not a not node, unregister it from sat and untranslate the negation
@@ -747,6 +803,7 @@ void CnfStream::undoTranslate(TNode node, int level) {
     Assert(it != d_translationCache.end());
     TranslationInfo& infoNeg = (*it).second;
     infoNeg.level = -1;
+    infoNeg.recorded = false;
   }
 
   // undoTranslate the children