diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-10-04 16:15:47 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-10-04 16:15:47 +0000 |
commit | 7094d127b0cd69b4926203c05dd2d60cb4d27292 (patch) | |
tree | b913b13274593a841387a4d07840f6ef79da3a01 /src/theory/substitutions.h | |
parent | 7961e06fdca05678d27653a0fbe6cec730664a3f (diff) |
fixes to context-dependent caching substitutions
Diffstat (limited to 'src/theory/substitutions.h')
-rw-r--r-- | src/theory/substitutions.h | 38 |
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. */ |