fixes to context-dependent caching substitutions

1 files changed, 31 insertions, 7 deletions

diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h
index 253507645..c03baa1ac 100644
--- 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.
    */