fixes to context-dependent caching substitutions

1 files changed, 21 insertions, 4 deletions

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index cdcf33f6a..f235e16a4 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -30,7 +30,7 @@ struct substitution_stack_element {
   : node(node), children_added(false) {}
 };
 
-Node SubstitutionMap::internalSubstitute(TNode t, NodeMap& substitutionCache) {
+Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache) {
 
   Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << std::endl;
 
@@ -52,7 +52,7 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeMap& substitutionCache) {
     Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << std::endl;
 
     // If node already in the cache we're done, pop from the stack
-    NodeMap::iterator find = substitutionCache.find(current);
+    NodeCache::iterator find = substitutionCache.find(current);
     if (find != substitutionCache.end()) {
       toVisit.pop_back();
       continue;
@@ -81,7 +81,7 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeMap& substitutionCache) {
         // We need to add the children
         for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
           TNode childNode = *child_it;
-          NodeMap::iterator childFind = substitutionCache.find(childNode);
+          NodeCache::iterator childFind = substitutionCache.find(childNode);
           if (childFind == substitutionCache.end()) {
             toVisit.push_back(childNode);
           }
@@ -104,7 +104,7 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) {
   Assert(d_substitutions.find(x) == d_substitutions.end());
 
   // Temporary substitution cache
-  NodeMap tempCache(d_context);
+  NodeCache tempCache;
   tempCache[x] = t;
 
   // Put in the new substitutions into the old ones
@@ -127,11 +127,15 @@ static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC
 static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) {
   SubstitutionMap::NodeMap::const_iterator it = substitutions.begin();
   SubstitutionMap::NodeMap::const_iterator it_end = substitutions.end();
+  Debug("substitution") << "checking " << node << std::endl;
   for (; it != it_end; ++ it) {
+    Debug("substitution") << "-- hasSubterm( " << (*it).first << " ) ?" << std::endl;
     if (node.hasSubterm((*it).first)) {
+      Debug("substitution") << "-- FAIL" << std::endl;
       return false;
     }
   }
+  Debug("substitution") << "-- SUCCEED" << std::endl;
   return true;
 }
 
@@ -148,6 +152,19 @@ Node SubstitutionMap::apply(TNode t) {
       d_substitutionCache[(*it).first] = (*it).second;
     }
     d_cacheInvalidated = false;
+    Debug("substitution") << "-- reset the cache" << std::endl;
+  }
+
+  SubstitutionMap::NodeMap::const_iterator it = d_substitutions.begin();
+  SubstitutionMap::NodeMap::const_iterator it_end = d_substitutions.end();
+  for (; it != it_end; ++ it) {
+    Debug("substitution") << "substs has ( " << (*it).first << " => " << (*it).second << " )" << std::endl;
+  }
+
+  SubstitutionMap::NodeCache::const_iterator iit = d_substitutionCache.begin();
+  SubstitutionMap::NodeCache::const_iterator iit_end = d_substitutionCache.end();
+  for (; iit != iit_end; ++ iit) {
+    Debug("substitution") << "CACHE has ( " << (*iit).first << " => " << (*iit).second << " )" << std::endl;
   }
 
   // Perform the substitution