From 7094d127b0cd69b4926203c05dd2d60cb4d27292 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 4 Oct 2011 16:15:47 +0000 Subject: [PATCH] fixes to context-dependent caching substitutions --- src/theory/substitutions.cpp | 25 +++++++++++--- src/theory/substitutions.h | 38 ++++++++++++++++++---- test/regress/regress0/push-pop/Makefile.am | 3 +- 3 files changed, 54 insertions(+), 12 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 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 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 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 86eeae902..1dd1dcfd5 100644 --- 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) -- 2.30.2