Fixed a performance issue with unconstrained simplifier

3 files changed, 82 insertions, 28 deletions

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index b7ad1d174..f56dd47b6 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -103,25 +103,27 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache)
   return substitutionCache[t];
 }
 
-void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) {
+void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache, bool backSub, bool forwardSub) {
   Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl;
   Assert(d_substitutions.find(x) == d_substitutions.end());
 
-  // Temporary substitution cache
-  NodeCache tempCache;
-  tempCache[x] = t;
+  if (backSub) {
+    // Temporary substitution cache
+    NodeCache tempCache;
+    tempCache[x] = t;
 
-  // Put in the new substitutions into the old ones
-  NodeMap::iterator it = d_substitutions.begin();
-  NodeMap::iterator it_end = d_substitutions.end();
-  for(; it != it_end; ++ it) {
-    d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
+    // Put in the new substitutions into the old ones
+    NodeMap::iterator it = d_substitutions.begin();
+    NodeMap::iterator it_end = d_substitutions.end();
+    for(; it != it_end; ++ it) {
+      d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache);
+    }
   }
 
-  // Put the new substitution in, but apply existing substitutions to rhs first
-  d_substitutions[x] = apply(t);
+  // Put the new substitution in
+  d_substitutions[x] = forwardSub ? apply(t) : Node(t);
 
-  // Also invalidate the cache
+  // Also invalidate the cache if necessary
   if (invalidateCache) {
     d_cacheInvalidated = true;
   }
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 711ff9b72..c32dee635 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -102,9 +102,17 @@ public:
   }
 
   /**
-   * Adds a substitution from x to t
+   * Adds a substitution from x to t.  Typically you also want to apply this
+   * substitution to the existing set (backSub), but you do not need to
+   * apply the existing set to the new substitution (forwardSub).  However,
+   * the method allows you to do either.  Probably you should not do both,
+   * as it will be very difficult to maintain the invariant that no
+   * left-hand side appears on any right-hand side.
    */
-  void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
+  void addSubstitution(TNode x, TNode t,
+                       bool invalidateCache = true,
+                       bool backSub = true,
+                       bool forwardSub = false);
 
   /**
    * Returns true iff x is in the substitution map
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index b1a944597..43377cf37 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -121,18 +121,21 @@ void UnconstrainedSimplifier::processUnconstrained()
   for ( ; it != iend; ++it) {
     workList.push_back(*it);
   }
-  TNode current = workList.back();
   Node currentSub;
-  workList.pop_back();
+  TNode parent;
+  bool swap;
+  bool isSigned;
+  bool strict;
+  vector<TNode> delayQueueLeft;
+  vector<TNode> delayQueueRight;
 
+  TNode current = workList.back();
+  workList.pop_back();
   for (;;) {
-    TNodeMap::iterator itNodeMap;
     Assert(d_visitedOnce.find(current) != d_visitedOnce.end());
-    TNode parent = d_visitedOnce[current];
-    bool swap = false;
-    bool isSigned = false;
-    bool strict = false;
+    parent = d_visitedOnce[current];
     if (!parent.isNull()) {
+      swap = isSigned = strict = false;
       switch (parent.getKind()) {
 
         // If-then-else operator - any two unconstrained children makes the parent unconstrained
@@ -146,12 +149,30 @@ void UnconstrainedSimplifier::processUnconstrained()
                 !d_substitutions.hasSubstitution(parent)) {
               removeExpr(parent);
               if (uThen) {
-                if (parent[1] != current || currentSub.isNull()) {
-                  currentSub = parent[1];
+                if (parent[1] != current) {
+                  if (parent[1].isVar()) {
+                    currentSub = parent[1];
+                  }
+                  else {
+                    Assert(d_substitutions.hasSubstitution(parent[1]));
+                    currentSub = d_substitutions.apply(parent[1]);
+                  }
+                }
+                else if (currentSub.isNull()) {
+                  currentSub = current;
+                }
+              }
+              else if (parent[2] != current) {
+                if (parent[2].isVar()) {
+                  currentSub = parent[2];
+                }
+                else {
+                  Assert(d_substitutions.hasSubstitution(parent[2]));
+                  currentSub = d_substitutions.apply(parent[2]);
                 }
               }
-              else if (parent[2] != current || currentSub.isNull()) {
-                currentSub = parent[2];
+              else if (currentSub.isNull()) {
+                currentSub = current;
               }
               current = parent;
             }
@@ -520,8 +541,12 @@ void UnconstrainedSimplifier::processUnconstrained()
             if (d_unconstrained.find(parent) == d_unconstrained.end() &&
                 !d_substitutions.hasSubstitution(parent)) {
               removeExpr(parent);
-              if (parent[0] != current || currentSub.isNull()) {
-                currentSub = parent[0];
+              if (parent[0] != current) {
+                Assert(d_substitutions.hasSubstitution(parent[0]));
+                currentSub = d_substitutions.apply(parent[0]);
+              }
+              else if (currentSub.isNull()) {
+                currentSub = current;
               }
               current = parent;
             }
@@ -603,6 +628,10 @@ void UnconstrainedSimplifier::processUnconstrained()
             else {
               currentSub = currentSub.orNode(test);
             }
+            // Delay adding this substitution - see comment at end of function
+            delayQueueLeft.push_back(current);
+            delayQueueRight.push_back(currentSub);
+            currentSub = Node();
             parent = TNode();
           }
           break;
@@ -627,7 +656,8 @@ void UnconstrainedSimplifier::processUnconstrained()
       }
     }
     if (!currentSub.isNull()) {
-      d_substitutions.addSubstitution(current, currentSub);
+      Assert(currentSub.isVar());
+      d_substitutions.addSubstitution(current, currentSub, false, false, false);
     }
     if (workList.empty()) {
       break;
@@ -636,6 +666,20 @@ void UnconstrainedSimplifier::processUnconstrained()
     currentSub = Node();
     workList.pop_back();
   }
+  TNode left;
+  Node right;
+  // All substitutions except those arising from bitvector comparisons are
+  // substitutions t -> x where x is a variable.  This allows us to build the
+  // substitution very quickly (never invalidating the substitution cache).
+  // Bitvector comparisons are more complicated and may require
+  // back-substitution and cache-invalidation.  So we do these last.
+  while (!delayQueueLeft.empty()) {
+    left = delayQueueLeft.back();
+    right = d_substitutions.apply(delayQueueRight.back());
+    d_substitutions.addSubstitution(delayQueueLeft.back(), right, true, true, false);
+    delayQueueLeft.pop_back();
+    delayQueueRight.pop_back();
+  }
 }