New substitutions implementation - fixes performance issue seen in nonclausal

simplification for some benchmarks

4 files changed, 67 insertions, 50 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6771b8cd5..3da8e1b33 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1004,7 +1004,7 @@ void SmtEnginePrivate::nonClausalSimplify() {
           Assert(!t.isConst());
           Assert(constantPropagations.apply(t) == t);
           Assert(d_topLevelSubstitutions.apply(t) == t);
-          constantPropagations.addSubstitution(t, c, true, false, false);
+          constantPropagations.addSubstitution(t, c);
           // vector<pair<Node,Node> > equations;a
           // constantPropagations.simplifyLHS(t, c, equations, true);
           // if (!equations.empty()) {
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index 65c4524ee..b7c9278e1 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -31,12 +31,12 @@ struct substitution_stack_element {
   : node(node), children_added(false) {}
 };
 
-Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache) {
+
+Node SubstitutionMap::internalSubstitute(TNode t) {
 
   Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << std::endl;
 
-  // If nothing to substitute just return the node
-  if (substitutionCache.empty()) {
+  if (d_substitutions.empty()) {
     return t;
   }
 
@@ -53,8 +53,19 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache)
     Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << std::endl;
 
     // If node already in the cache we're done, pop from the stack
-    NodeCache::iterator find = substitutionCache.find(current);
-    if (find != substitutionCache.end()) {
+    NodeCache::iterator find = d_substitutionCache.find(current);
+    if (find != d_substitutionCache.end()) {
+      toVisit.pop_back();
+      continue;
+    }
+
+    NodeMap::iterator find2 = d_substitutions.find(current);
+    if (find2 != d_substitutions.end()) {
+      Node rhs = (*find2).second;
+      Assert(rhs != current);
+      internalSubstitute(rhs);
+      d_substitutions[current] = d_substitutionCache[rhs];
+      d_substitutionCache[current] = d_substitutionCache[rhs];
       toVisit.pop_back();
       continue;
     }
@@ -67,17 +78,30 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache)
         builder << current.getOperator();
       }
       for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
-        Assert(substitutionCache.find(current[i]) != substitutionCache.end());
-        builder << Node(substitutionCache[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;
-      find = substitutionCache.find(result);
-      if (find != substitutionCache.end()) {
-        result = find->second;
+      if (result != current) {
+        find = d_substitutionCache.find(result);
+        if (find != d_substitutionCache.end()) {
+          result = find->second;
+        }
+        else {
+          find2 = d_substitutions.find(result);
+          if (find2 != d_substitutions.end()) {
+            Node rhs = (*find2).second;
+            Assert(rhs != result);
+            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 << std::endl;
-      substitutionCache[current] = result;
+      d_substitutionCache[current] = result;
       toVisit.pop_back();
     } else {
       // Mark that we have added the children if any
@@ -86,25 +110,26 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache)
         // 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 = substitutionCache.find(childNode);
-          if (childFind == substitutionCache.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 << std::endl;
-        substitutionCache[current] = current;
+        d_substitutionCache[current] = current;
         toVisit.pop_back();
       }
     }
   }
 
   // Return the substituted version
-  return substitutionCache[t];
+  return d_substitutionCache[t];
 }
 
 
+  /*
 void SubstitutionMap::simplifyRHS(const SubstitutionMap& subMap)
 {
   // Put the new substitutions into the old ones
@@ -122,13 +147,18 @@ 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();
+  // for(; it != it_end; ++ it) {
+  //   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.
@@ -138,6 +168,7 @@ void SubstitutionMap::simplifyRHS(TNode x, TNode t) {
  *   (i) if l' is equal to some ll (in a rule ll -> rr), then if r != rr we add (r,rr) to the equation list
  *   (i) if l' is equalto some rr (in a rule ll -> rr), then if r != rr we add (r,rr) to the equation list
  */
+/*
 void SubstitutionMap::simplifyLHS(const SubstitutionMap& subMap, vector<pair<Node, Node> >& equalities, bool rewrite)
 {
   Assert(d_worklist.empty());
@@ -203,7 +234,7 @@ void SubstitutionMap::processWorklist(vector<pair<Node, Node> >& equalities, boo
         break;
       }
 
-      newLeft2 = internalSubstitute((*it).first, tempCache);
+      newLeft2 = internalSubstituteOld((*it).first, tempCache);
       if (newLeft2 != (*it).first) {
         if (rewrite) {
           newLeft2 = Rewriter::rewrite(newLeft2);
@@ -217,18 +248,14 @@ void SubstitutionMap::processWorklist(vector<pair<Node, Node> >& equalities, boo
     }
   }
 }
+*/
 
-
-void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache, bool backSub, bool forwardSub) {
+void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache)
+{
   Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl;
   Assert(d_substitutions.find(x) == d_substitutions.end());
 
-  if (backSub) {
-    simplifyRHS(x, t);
-  }
-
-  // Put the new substitution in
-  d_substitutions[x] = forwardSub ? apply(t) : Node(t);
+  d_substitutions[x] = t;
 
   // Also invalidate the cache if necessary
   if (invalidateCache) {
@@ -261,21 +288,16 @@ Node SubstitutionMap::apply(TNode t) {
 
   // Setup the cache
   if (d_cacheInvalidated) {
-    SubstitutionMap::NodeMap::const_iterator it = d_substitutions.begin();
-    SubstitutionMap::NodeMap::const_iterator it_end = d_substitutions.end();
     d_substitutionCache.clear();
-    for (; it != it_end; ++ it) {
-      d_substitutionCache[(*it).first] = (*it).second;
-    }
     d_cacheInvalidated = false;
     Debug("substitution") << "-- reset the cache" << std::endl;
   }
 
   // Perform the substitution
-  Node result = internalSubstitute(t, d_substitutionCache);
+  Node result = internalSubstitute(t);
   Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << std::endl;
 
-//  Assert(check(result, d_substitutions));
+  //  Assert(check(result, d_substitutions));
 
   return result;
 }
diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 32ed35074..cf751b69e 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -68,7 +68,7 @@ private:
   bool d_cacheInvalidated;
 
   /** Internal method that performs substitution */
-  Node internalSubstitute(TNode t, NodeCache& substitutionCache);
+  Node internalSubstitute(TNode t);
 
   /** Helper class to invalidate cache on user pop */
   class CacheInvalidator : public context::ContextNotifyObj {
@@ -92,8 +92,8 @@ private:
   CacheInvalidator d_cacheInvalidator;
 
   // Helper list and method for simplifyLHS methods
-  std::vector<std::pair<Node, Node> > d_worklist;
-  void processWorklist(std::vector<std::pair<Node, Node> >& equalities, bool rewrite);
+  // std::vector<std::pair<Node, Node> > d_worklist;
+  // void processWorklist(std::vector<std::pair<Node, Node> >& equalities, bool rewrite);
 
 public:
 
@@ -106,17 +106,10 @@ public:
   }
 
   /**
-   * 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.
+   * Adds a substitution from x to t.
    */
   void addSubstitution(TNode x, TNode t,
-                       bool invalidateCache = true,
-                       bool backSub = true,
-                       bool forwardSub = false);
+                       bool invalidateCache = true);
 
   /**
    * Returns true iff x is in the substitution map
@@ -162,6 +155,7 @@ 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);
 
@@ -177,6 +171,7 @@ public:
   void simplifyLHS(TNode lhs, TNode rhs,
                    std::vector<std::pair<Node,Node> >& equalities,
                    bool rewrite = true);
+  */
 
   /**
    * Print to the output stream
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 1c507eb71..7e06297fb 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -653,7 +653,7 @@ void UnconstrainedSimplifier::processUnconstrained()
     }
     if (!currentSub.isNull()) {
       Assert(currentSub.isVar());
-      d_substitutions.addSubstitution(current, currentSub, false, false, false);
+      d_substitutions.addSubstitution(current, currentSub, false);
     }
     if (workList.empty()) {
       break;
@@ -673,7 +673,7 @@ void UnconstrainedSimplifier::processUnconstrained()
     left = delayQueueLeft.back();
     if (!d_substitutions.hasSubstitution(left)) {
       right = d_substitutions.apply(delayQueueRight.back());
-      d_substitutions.addSubstitution(delayQueueLeft.back(), right, true, true, false);
+      d_substitutions.addSubstitution(delayQueueLeft.back(), right);
     }
     delayQueueLeft.pop_back();
     delayQueueRight.pop_back();