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.cpp | |
parent | 7961e06fdca05678d27653a0fbe6cec730664a3f (diff) |
fixes to context-dependent caching substitutions
Diffstat (limited to 'src/theory/substitutions.cpp')
-rw-r--r-- | src/theory/substitutions.cpp | 25 |
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 |