Fixed a performance issue with unconstrained simplifier

1 files changed, 58 insertions, 14 deletions

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();
+  }
 }