fixes to context-dependent caching substitutions

diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp
index cdcf33f6a94a41f224e664d436ddc49f4d586f0b..f235e16a425bfc95694913817a2d4552b9b4170a 100644 (file)
--- 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

diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 2535076459b21da2e39ff8a7c98471f7a7515efa..c03baa1ac5f0e7ffde73050a77696344937c1588 100644 (file)
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -29,6 +29,7 @@
 #include "context/context.h"
 #include "context/cdo.h"
 #include "context/cdmap.h"
+#include "util/hash.h"
 
 namespace CVC4 {
 namespace theory {
@@ -49,6 +50,8 @@ public:
 
 private:
 
+  typedef std::hash_map<Node, Node, NodeHashFunction> NodeCache;
+
   /** The context within which this SubstitutionMap was constructed. */
   context::Context* d_context;
 
@@ -56,21 +59,43 @@ private:
   NodeMap d_substitutions;
 
   /** Cache of the already performed substitutions */
-  NodeMap d_substitutionCache;
+  NodeCache d_substitutionCache;
 
-  /** Has the cache been invalidated */
-  context::CDO<bool> d_cacheInvalidated;
+  /** Has the cache been invalidated? */
+  bool d_cacheInvalidated;
 
   /** Internal method that performs substitution */
-  Node internalSubstitute(TNode t, NodeMap& substitutionCache);
+  Node internalSubstitute(TNode t, NodeCache& substitutionCache);
+
+  /** Helper class to invalidate cache on user pop */
+  class CacheInvalidator : public context::ContextNotifyObj {
+    bool& d_cacheInvalidated;
+
+  public:
+    CacheInvalidator(context::Context* context, bool& cacheInvalidated) :
+      context::ContextNotifyObj(context),
+      d_cacheInvalidated(cacheInvalidated) {
+    }
+
+    void notify() {
+      d_cacheInvalidated = true;
+    }
+  };/* class SubstitutionMap::CacheInvalidator */
+
+  /**
+   * This object is notified on user pop and marks the SubstitutionMap's
+   * cache as invalidated.
+   */
+  CacheInvalidator d_cacheInvalidator;
 
 public:
 
   SubstitutionMap(context::Context* context) :
     d_context(context),
     d_substitutions(context),
-    d_substitutionCache(context),
-    d_cacheInvalidated(context) {
+    d_substitutionCache(),
+    d_cacheInvalidated(false),
+    d_cacheInvalidator(context, d_cacheInvalidated) {
   }
 
   /**
@@ -78,7 +103,6 @@ public:
    */
   void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
 
-
   /**
    * Apply the substitutions to the node.
    */

diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 86eeae902fc23b9c3c43b428a233eb4869699a57..1dd1dcfd5e08ddf85da5ab124da18f781577d177 100644 (file)
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -11,7 +11,8 @@ MAKEFLAGS = -k
 CVC_TESTS = \
        test.00.cvc \
        test.01.cvc \
-       units.cvc
+       units.cvc \
+       incremental-subst-bug.cvc
 
 TESTS =        $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)