Revert Clark's last commit, at his request; there are some bugs.

This reverts commit 9775bced75843c6f01e9524c2d0e7021535e3ec0.

7 files changed, 128 insertions, 130 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a5effc1e8..91eae8915 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -307,6 +307,23 @@ private:
   /** The top level substitutions */
   SubstitutionMap d_topLevelSubstitutions;
 
+  /**
+   * d_lastSubstitutionPos points to the last
+   * substitution that was added to d_topLevelSubstitutions.
+   * If d_lastSubstitutionPos == d_topLevelSubstitutions.end(), there
+   * are no substitutions.
+   */
+  context::CDO<SubstitutionMap::iterator> d_lastSubstitutionPos;
+  /**
+   * In incremental settings, substitutions cannot be performed
+   * "backward," only forward.  So we need to keep all substitutions
+   * around as assertions.  This iterator remembers the last
+   * substitution at the time processAssertions was called.  All
+   * substitutions added since then need to be included in the set of
+   * assertions in incremental mode.
+   */
+  context::CDO<SubstitutionMap::iterator> d_lastSubstitutionPosAtEntryToProcessAssertions;
+
   static const bool d_doConstantProp = true;
 
   /**
@@ -390,7 +407,9 @@ public:
     d_modZero(),
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
-    d_topLevelSubstitutions(smt.d_userContext, true, true)
+    d_topLevelSubstitutions(smt.d_userContext),
+    d_lastSubstitutionPos(smt.d_userContext, d_topLevelSubstitutions.end()),
+    d_lastSubstitutionPosAtEntryToProcessAssertions(smt.d_userContext, d_topLevelSubstitutions.end())
   {
     d_smt.d_nodeManager->subscribeEvents(this);
   }
@@ -1726,15 +1745,12 @@ bool SmtEnginePrivate::nonClausalSimplify() {
 
   // No, conflict, go through the literals and solve them
   SubstitutionMap constantPropagations(d_smt.d_context);
-  SubstitutionMap newSubstitutions(d_smt.d_context, true, true);
-  SubstitutionMap::iterator pos;
   unsigned j = 0;
   for(unsigned i = 0, i_end = d_nonClausalLearnedLiterals.size(); i < i_end; ++ i) {
     // Simplify the literal we learned wrt previous substitutions
     Node learnedLiteral = d_nonClausalLearnedLiterals[i];
     Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
-    Assert(d_topLevelSubstitutions.apply(learnedLiteral) == learnedLiteral);
-    Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral);
+    Node learnedLiteralNew = d_topLevelSubstitutions.apply(learnedLiteral);
     if (learnedLiteral != learnedLiteralNew) {
       learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
     }
@@ -1763,20 +1779,41 @@ bool SmtEnginePrivate::nonClausalSimplify() {
       }
     }
 
+    SubstitutionMap::iterator pos = d_lastSubstitutionPos;
+#ifdef CVC4_ASSERTIONS
+    // Check that d_lastSubstitutionPos really points to the last substitution
+    if (pos != d_topLevelSubstitutions.end()) {
+      ++pos;
+      Assert(pos == d_topLevelSubstitutions.end());
+      pos = d_lastSubstitutionPos;
+    }
+#endif
+
     // Solve it with the corresponding theory, possibly adding new
-    // substitutions to newSubstitutions
+    // substitutions to d_topLevelSubstitutions
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                       << "solving " << learnedLiteral << endl;
-
     Theory::PPAssertStatus solveStatus =
-      d_smt.d_theoryEngine->solve(learnedLiteral, newSubstitutions);
+      d_smt.d_theoryEngine->solve(learnedLiteral, d_topLevelSubstitutions);
 
     switch (solveStatus) {
       case Theory::PP_ASSERT_STATUS_SOLVED: {
+        // Update d_lastSubstitutionPos
+        if (pos == d_topLevelSubstitutions.end()) {
+          pos = d_topLevelSubstitutions.begin();
+        }
+        SubstitutionMap::iterator next = pos;
+        ++next;
+        while (next != d_topLevelSubstitutions.end()) {
+          pos = next;
+          ++next;
+        }
+        d_lastSubstitutionPos = pos;
+
         // The literal should rewrite to true
         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                           << "solved " << learnedLiteral << endl;
-        Assert(Rewriter::rewrite(newSubstitutions.apply(learnedLiteral)).isConst());
+        Assert(Rewriter::rewrite(d_topLevelSubstitutions.apply(learnedLiteral)).isConst());
         //        vector<pair<Node, Node> > equations;
         //        constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true);
         //        if (equations.empty()) {
@@ -1811,7 +1848,6 @@ bool SmtEnginePrivate::nonClausalSimplify() {
           Assert(!t.isConst());
           Assert(constantPropagations.apply(t) == t);
           Assert(d_topLevelSubstitutions.apply(t) == t);
-          Assert(newSubstitutions.apply(t) == t);
           constantPropagations.addSubstitution(t, c);
           // vector<pair<Node,Node> > equations;a
           // constantPropagations.simplifyLHS(t, c, equations, true);
@@ -1837,11 +1873,10 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a
     //    constant propagation too
     // 4. each lhs of constantPropagations is different from each rhs
-    for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
+    pos = d_topLevelSubstitutions.begin();
+    for (; pos != d_topLevelSubstitutions.end(); ++pos) {
       Assert((*pos).first.isVar());
-      Assert(d_topLevelSubstitutions.apply((*pos).first) == (*pos).first);
-      Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
-      Assert(newSubstitutions.apply(newSubstitutions.apply((*pos).second)) == newSubstitutions.apply((*pos).second));
+      //      Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
     }
     for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
       Assert((*pos).second.isConst());
@@ -1865,17 +1900,14 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   // Resize the learnt
   d_nonClausalLearnedLiterals.resize(j);
 
-  // If not in incremental mode, must add substitutions to model
-  if( !options::incrementalSolving() &&
-      !options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL ) {
-    TheoryModel* m = d_smt.d_theoryEngine->getModel();
-    if(m != NULL) {
-      for(pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
-        Node n = (*pos).first;
-        Node v = newSubstitutions.apply((*pos).second);
-        Trace("model") << "Add substitution : " << n << " " << v << endl;
-        m->addSubstitution( n, v );
-      }
+  //must add substitutions to model
+  TheoryModel* m = d_smt.d_theoryEngine->getModel();
+  if(m != NULL) {
+    for( SubstitutionMap::iterator pos = d_topLevelSubstitutions.begin(); pos != d_topLevelSubstitutions.end(); ++pos) {
+      Node n = (*pos).first;
+      Node v = (*pos).second;
+      Trace("model") << "Add substitution : " << n << " " << v << endl;
+      m->addSubstitution( n, v );
     }
   }
 
@@ -1883,7 +1915,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   Trace("debugging") << "NonClausal simplify pre-preprocess\n";
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
     Node assertion = d_assertionsToPreprocess[i];
-    Node assertionNew = newSubstitutions.apply(assertion);
+    Node assertionNew = d_topLevelSubstitutions.apply(assertion);
     Trace("debugging") << "assertion = " << assertion << endl;
     Trace("debugging") << "assertionNew = " << assertionNew << endl;
     if (assertion != assertionNew) {
@@ -1914,23 +1946,29 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   Assert(d_realAssertionsEnd <= d_assertionsToCheck.size());
   learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd - 1];
 
-  // If in incremental mode, add substitutions to the list of assertions
   if( options::incrementalSolving() ||
       options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL ) {
-    pos = newSubstitutions.begin();
-    for (; pos != newSubstitutions.end(); ++pos) {
+    // Keep substitutions
+    SubstitutionMap::iterator pos = d_lastSubstitutionPosAtEntryToProcessAssertions;
+    if(pos == d_topLevelSubstitutions.end()) {
+      pos = d_topLevelSubstitutions.begin();
+    } else {
+      ++pos;
+    }
+
+    while(pos != d_topLevelSubstitutions.end()) {
       // Add back this substitution as an assertion
-      TNode lhs = (*pos).first, rhs = newSubstitutions.apply((*pos).second);
+      TNode lhs = (*pos).first, rhs = d_topLevelSubstitutions.apply((*pos).second);
       Node n = NodeManager::currentNM()->mkNode(lhs.getType().isBoolean() ? kind::IFF : kind::EQUAL, lhs, rhs);
       learnedBuilder << n;
       Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
+      ++pos;
     }
   }
 
   for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
     Node learned = d_nonClausalLearnedLiterals[i];
-    Assert(d_topLevelSubstitutions.apply(learned) == learned);
-    Node learnedNew = newSubstitutions.apply(learned);
+    Node learnedNew = d_topLevelSubstitutions.apply(learned);
     if (learned != learnedNew) {
       learned = Rewriter::rewrite(learnedNew);
     }
@@ -1954,11 +1992,10 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   }
   d_nonClausalLearnedLiterals.clear();
 
-  
-  for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
+  SubstitutionMap::iterator pos = constantPropagations.begin();
+  for (; pos != constantPropagations.end(); ++pos) {
     Node cProp = (*pos).first.eqNode((*pos).second);
-    Assert(d_topLevelSubstitutions.apply(cProp) == cProp);
-    Node cPropNew = newSubstitutions.apply(cProp);
+    Node cPropNew = d_topLevelSubstitutions.apply(cProp);
     if (cProp != cPropNew) {
       cProp = Rewriter::rewrite(cPropNew);
       Assert(Rewriter::rewrite(cProp) == cProp);
@@ -1973,11 +2010,6 @@ bool SmtEnginePrivate::nonClausalSimplify() {
                       << cProp << endl;
   }
 
-  // Add new substitutions to topLevelSubstitutions
-  // Note that we don't have to keep rhs's in full solved form
-  // because SubstitutionMap::apply does a fixed-point iteration when substituting
-  d_topLevelSubstitutions.addSubstitutions(newSubstitutions);
-
   if(learnedBuilder.getNumChildren() > 1) {
     d_assertionsToCheck[d_realAssertionsEnd - 1] =
       Rewriter::rewrite(Node(learnedBuilder));
@@ -2807,6 +2839,8 @@ void SmtEnginePrivate::processAssertions() {
 
   dumpAssertions("pre-substitution", d_assertionsToPreprocess);
 
+  // Record current last substitution
+  d_lastSubstitutionPosAtEntryToProcessAssertions = d_lastSubstitutionPos.get();
   // Apply the substitutions we already have, and normalize
   Chat() << "applying substitutions..." << endl;
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index 87aadf3f0..3e75dd258 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -17,7 +17,6 @@
 #include "theory/theory.h"
 #include "theory/booleans/theory_bool.h"
 #include "theory/booleans/circuit_propagator.h"
-#include "theory/substitutions.h"
 #include "theory/valuation.h"
 #include "util/boolean_simplification.h"
 
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index c4f06e396..c12129d01 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -29,7 +29,7 @@ struct substitution_stack_element {
   : node(node), children_added(false) {}
 };/* struct substitution_stack_element */
 
-Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
+Node SubstitutionMap::internalSubstitute(TNode t) {
 
   Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << endl;
 
@@ -50,8 +50,8 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
     Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl;
 
     // If node already in the cache we're done, pop from the stack
-    NodeCache::iterator find = cache.find(current);
-    if (find != cache.end()) {
+    NodeCache::iterator find = d_substitutionCache.find(current);
+    if (find != d_substitutionCache.end()) {
       toVisit.pop_back();
       continue;
     }
@@ -59,7 +59,7 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
     if (!d_substituteUnderQuantifiers &&
         (current.getKind() == kind::FORALL || current.getKind() == kind::EXISTS)) {
       Debug("substitution::internal") << "--not substituting under quantifier" << endl;
-      cache[current] = current;
+      d_substitutionCache[current] = current;
       toVisit.pop_back();
       continue;
     }
@@ -68,9 +68,9 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
     if (find2 != d_substitutions.end()) {
       Node rhs = (*find2).second;
       Assert(rhs != current);
-      internalSubstitute(rhs, cache);
-      d_substitutions[current] = cache[rhs];
-      cache[current] = cache[rhs];
+      internalSubstitute(rhs);
+      d_substitutions[current] = d_substitutionCache[rhs];
+      d_substitutionCache[current] = d_substitutionCache[rhs];
       toVisit.pop_back();
       continue;
     }
@@ -80,17 +80,17 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
       // Children have been processed, so substitute
       NodeBuilder<> builder(current.getKind());
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        builder << Node(cache[current.getOperator()]);
+        builder << Node(d_substitutionCache[current.getOperator()]);
       }
       for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
-        Assert(cache.find(current[i]) != cache.end());
-        builder << Node(cache[current[i]]);
+        Assert(d_substitutionCache.find(current[i]) != d_substitutionCache.end());
+        builder << Node(d_substitutionCache[current[i]]);
       }
       // Mark the substitution and continue
       Node result = builder;
       if (result != current) {
-        find = cache.find(result);
-        if (find != cache.end()) {
+        find = d_substitutionCache.find(result);
+        if (find != d_substitutionCache.end()) {
           result = find->second;
         }
         else {
@@ -98,15 +98,15 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
           if (find2 != d_substitutions.end()) {
             Node rhs = (*find2).second;
             Assert(rhs != result);
-            internalSubstitute(rhs, cache);
-            d_substitutions[result] = cache[rhs];
-            cache[result] = cache[rhs];
-            result = cache[rhs];
+            internalSubstitute(rhs);
+            d_substitutions[result] = d_substitutionCache[rhs];
+            d_substitutionCache[result] = d_substitutionCache[rhs];
+            result = d_substitutionCache[rhs];
           }
         }
       }
       Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl;
-      cache[current] = result;
+      d_substitutionCache[current] = result;
       toVisit.pop_back();
     } else {
       // Mark that we have added the children if any
@@ -115,33 +115,34 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) {
         // We need to add the operator, if any
         if(current.getMetaKind() == kind::metakind::PARAMETERIZED) {
           TNode opNode = current.getOperator();
-          NodeCache::iterator opFind = cache.find(opNode);
-          if (opFind == cache.end()) {
+          NodeCache::iterator opFind = d_substitutionCache.find(opNode);
+          if (opFind == d_substitutionCache.end()) {
             toVisit.push_back(opNode);
           }
         }
         // We need to add the children
         for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
           TNode childNode = *child_it;
-          NodeCache::iterator childFind = cache.find(childNode);
-          if (childFind == cache.end()) {
+          NodeCache::iterator childFind = d_substitutionCache.find(childNode);
+          if (childFind == d_substitutionCache.end()) {
             toVisit.push_back(childNode);
           }
         }
       } else {
         // No children, so we're done
         Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << endl;
-        cache[current] = current;
+        d_substitutionCache[current] = current;
         toVisit.pop_back();
       }
     }
   }
 
   // Return the substituted version
-  return cache[t];
+  return d_substitutionCache[t];
 }/* SubstitutionMap::internalSubstitute() */
 
 
+  /*
 void SubstitutionMap::simplifyRHS(const SubstitutionMap& subMap)
 {
   // Put the new substitutions into the old ones
@@ -159,10 +160,10 @@ void SubstitutionMap::simplifyRHS(TNode x, TNode t) {
   tempCache[x] = t;
 
   // Put the new substitution into the old ones
-  NodeMap::iterator it = d_substitutions.begin();
-  NodeMap::iterator it_end = d_substitutions.end();
+  NodeMap::iterator it = d_substitutionsOld.begin();
+  NodeMap::iterator it_end = d_substitutionsOld.end();
   for(; it != it_end; ++ it) {
-    d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
+    d_substitutionsOld[(*it).first] = internalSubstituteOld((*it).second, tempCache);
   }  
   // it = d_substitutionsLazy.begin();
   // it_end = d_substitutionsLazy.end();
@@ -170,7 +171,7 @@ void SubstitutionMap::simplifyRHS(TNode x, TNode t) {
   //   d_substitutionsLazy[(*it).first] = internalSubstitute((*it).second, tempCache);
   // }  
 }
-
+*/
 
 /* We use subMap to simplify the left-hand sides of the current substitution map.  If rewrite is true,
  * we also apply the rewriter to the result.
@@ -282,24 +283,6 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
   }
 }
 
-
-void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateCache)
-{
-  SubstitutionMap::NodeMap::const_iterator it = subMap.begin();
-  SubstitutionMap::NodeMap::const_iterator it_end = subMap.end();
-  for (; it != it_end; ++ it) {
-    Assert(d_substitutions.find((*it).first) == d_substitutions.end());
-    d_substitutions[(*it).first] = (*it).second;
-    if (!invalidateCache) {
-      d_substitutionCache[(*it).first] = d_substitutions[(*it).first];
-    }
-  }
-  if (invalidateCache) {
-    d_cacheInvalidated = true;
-  }
-}
-
-
 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED;
 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
   SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
@@ -328,7 +311,7 @@ Node SubstitutionMap::apply(TNode t) {
   }
 
   // Perform the substitution
-  Node result = internalSubstitute(t, d_substitutionCache);
+  Node result = internalSubstitute(t);
   Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl;
 
   //  Assert(check(result, d_substitutions));
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 5a478a250..bde7dfdbc 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -68,11 +68,8 @@ private:
   /** Has the cache been invalidated? */
   bool d_cacheInvalidated;
 
-  /** Whether to keep substitutions in solved form */
-  bool d_solvedForm;
-
   /** Internal method that performs substitution */
-  Node internalSubstitute(TNode t, NodeCache& cache);
+  Node internalSubstitute(TNode t);
 
   /** Helper class to invalidate cache on user pop */
   class CacheInvalidator : public context::ContextNotifyObj {
@@ -101,15 +98,13 @@ private:
 
 public:
 
-  SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true, bool solvedForm = false) :
+  SubstitutionMap(context::Context* context, bool substituteUnderQuantifiers = true) :
     d_context(context),
     d_substitutions(context),
     d_substitutionCache(),
     d_substituteUnderQuantifiers(substituteUnderQuantifiers),
     d_cacheInvalidated(false),
-    d_solvedForm(solvedForm),
-    d_cacheInvalidator(context, d_cacheInvalidated)
-    {
+    d_cacheInvalidator(context, d_cacheInvalidated) {
   }
 
   /**
@@ -118,11 +113,6 @@ public:
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
 
   /**
-   * Merge subMap into current set of substitutions
-   */
-  void addSubstitutions(SubstitutionMap& subMap, bool invalidateCache = true);
-
-  /**
    * Returns true iff x is in the substitution map
    */
   bool hasSubstitution(TNode x) const {
@@ -180,13 +170,13 @@ public:
   // should best interact with cache invalidation on context
   // pops.
 
+  /*
   // Simplify right-hand sides of current map using the given substitutions
   void simplifyRHS(const SubstitutionMap& subMap);
 
   // Simplify right-hand sides of current map with lhs -> rhs
   void simplifyRHS(TNode lhs, TNode rhs);
 
-  /*
   // Simplify left-hand sides of current map using the given substitutions
   void simplifyLHS(const SubstitutionMap& subMap,
                    std::vector<std::pair<Node,Node> >& equalities,
@@ -198,8 +188,6 @@ public:
                    bool rewrite = true);
   */
 
-  bool isSolvedForm() const { return d_solvedForm; }
-
   /**
    * Print to the output stream
    */
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 9a23d5518..a1a835170 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -17,7 +17,6 @@
 #include "theory/theory.h"
 #include "util/cvc4_assert.h"
 #include "theory/quantifiers_engine.h"
-#include "theory/substitutions.h"
 
 #include <vector>
 
@@ -207,27 +206,5 @@ void Theory::computeRelevantTerms(set<Node>& termSet)
 }
 
 
-Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstitutions)
-{
-  if (in.getKind() == kind::EQUAL) {
-    if (in[0].isVar() && !in[1].hasSubterm(in[0])) {
-      outSubstitutions.addSubstitution(in[0], in[1]);
-      return PP_ASSERT_STATUS_SOLVED;
-    }
-    if (in[1].isVar() && !in[0].hasSubterm(in[1])) {
-      outSubstitutions.addSubstitution(in[1], in[0]);
-      return PP_ASSERT_STATUS_SOLVED;
-    }
-    if (in[0].isConst() && in[1].isConst()) {
-      if (in[0] != in[1]) {
-        return PP_ASSERT_STATUS_CONFLICT;
-      }
-    }
-  }
-
-  return PP_ASSERT_STATUS_UNSOLVED;
-}
-
-
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 94afdb1d0..d1734674d 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -23,6 +23,7 @@
 #include "expr/attribute.h"
 #include "expr/command.h"
 #include "theory/valuation.h"
+#include "theory/substitutions.h"
 #include "theory/output_channel.h"
 #include "theory/logic_info.h"
 #include "theory/options.h"
@@ -48,7 +49,6 @@ class TheoryEngine;
 namespace theory {
 
 class QuantifiersEngine;
-class SubstitutionMap;
 class TheoryModel;
 
 namespace rrinst {
@@ -576,7 +576,25 @@ public:
    * Given a literal, add the solved substitutions to the map, if any.
    * The method should return true if the literal can be safely removed.
    */
-  virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
+  virtual PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
+    if (in.getKind() == kind::EQUAL) {
+      if (in[0].isVar() && !in[1].hasSubterm(in[0])) {
+        outSubstitutions.addSubstitution(in[0], in[1]);
+        return PP_ASSERT_STATUS_SOLVED;
+      }
+      if (in[1].isVar() && !in[0].hasSubterm(in[1])) {
+        outSubstitutions.addSubstitution(in[1], in[0]);
+        return PP_ASSERT_STATUS_SOLVED;
+      }
+      if (in[0].isConst() && in[1].isConst()) {
+        if (in[0] != in[1]) {
+          return PP_ASSERT_STATUS_CONFLICT;
+        }
+      }
+    }
+
+    return PP_ASSERT_STATUS_UNSOLVED;
+  }
 
   /**
    * Given an atom of the theory coming from the input formula, this
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index 40713fa41..94ab47d23 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -21,7 +21,6 @@
 #define __CVC4__THEORY__UF__THEORY_UF_REWRITER_H
 
 #include "theory/rewriter.h"
-#include "theory/substitutions.h"
 
 namespace CVC4 {
 namespace theory {