diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2013-09-24 16:56:06 -0700 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2013-09-24 16:56:06 -0700 |
commit | ccd1ca4c32e8a3eac8b18911a7b2d32b55203707 (patch) | |
tree | cf98ac89e90d4cbeae888886e54f9e833ee3b836 /src/theory/substitutions.cpp | |
parent | 6dc529e6b1d4816e37b106a539592452027e22ac (diff) |
Reduce compiler dependencies on substitutions.h,
Some new functionality in substitutions.h/cpp
Diffstat (limited to 'src/theory/substitutions.cpp')
-rw-r--r-- | src/theory/substitutions.cpp | 75 |
1 files changed, 46 insertions, 29 deletions
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index c12129d01..c4f06e396 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -29,7 +29,7 @@ struct substitution_stack_element { : node(node), children_added(false) {} };/* struct substitution_stack_element */ -Node SubstitutionMap::internalSubstitute(TNode t) { +Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& cache) { Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << ")" << endl; @@ -50,8 +50,8 @@ Node SubstitutionMap::internalSubstitute(TNode t) { Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): processing " << current << endl; // If node already in the cache we're done, pop from the stack - NodeCache::iterator find = d_substitutionCache.find(current); - if (find != d_substitutionCache.end()) { + NodeCache::iterator find = cache.find(current); + if (find != cache.end()) { toVisit.pop_back(); continue; } @@ -59,7 +59,7 @@ Node SubstitutionMap::internalSubstitute(TNode t) { if (!d_substituteUnderQuantifiers && (current.getKind() == kind::FORALL || current.getKind() == kind::EXISTS)) { Debug("substitution::internal") << "--not substituting under quantifier" << endl; - d_substitutionCache[current] = current; + cache[current] = current; toVisit.pop_back(); continue; } @@ -68,9 +68,9 @@ Node SubstitutionMap::internalSubstitute(TNode t) { if (find2 != d_substitutions.end()) { Node rhs = (*find2).second; Assert(rhs != current); - internalSubstitute(rhs); - d_substitutions[current] = d_substitutionCache[rhs]; - d_substitutionCache[current] = d_substitutionCache[rhs]; + internalSubstitute(rhs, cache); + d_substitutions[current] = cache[rhs]; + cache[current] = cache[rhs]; toVisit.pop_back(); continue; } @@ -80,17 +80,17 @@ Node SubstitutionMap::internalSubstitute(TNode t) { // Children have been processed, so substitute NodeBuilder<> builder(current.getKind()); if (current.getMetaKind() == kind::metakind::PARAMETERIZED) { - builder << Node(d_substitutionCache[current.getOperator()]); + builder << Node(cache[current.getOperator()]); } for (unsigned i = 0; i < current.getNumChildren(); ++ i) { - Assert(d_substitutionCache.find(current[i]) != d_substitutionCache.end()); - builder << Node(d_substitutionCache[current[i]]); + Assert(cache.find(current[i]) != cache.end()); + builder << Node(cache[current[i]]); } // Mark the substitution and continue Node result = builder; if (result != current) { - find = d_substitutionCache.find(result); - if (find != d_substitutionCache.end()) { + find = cache.find(result); + if (find != cache.end()) { result = find->second; } else { @@ -98,15 +98,15 @@ Node SubstitutionMap::internalSubstitute(TNode t) { if (find2 != d_substitutions.end()) { Node rhs = (*find2).second; Assert(rhs != result); - internalSubstitute(rhs); - d_substitutions[result] = d_substitutionCache[rhs]; - d_substitutionCache[result] = d_substitutionCache[rhs]; - result = d_substitutionCache[rhs]; + internalSubstitute(rhs, cache); + d_substitutions[result] = cache[rhs]; + cache[result] = cache[rhs]; + result = cache[rhs]; } } } Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << endl; - d_substitutionCache[current] = result; + cache[current] = result; toVisit.pop_back(); } else { // Mark that we have added the children if any @@ -115,34 +115,33 @@ Node SubstitutionMap::internalSubstitute(TNode t) { // We need to add the operator, if any if(current.getMetaKind() == kind::metakind::PARAMETERIZED) { TNode opNode = current.getOperator(); - NodeCache::iterator opFind = d_substitutionCache.find(opNode); - if (opFind == d_substitutionCache.end()) { + NodeCache::iterator opFind = cache.find(opNode); + if (opFind == cache.end()) { toVisit.push_back(opNode); } } // We need to add the children for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) { TNode childNode = *child_it; - NodeCache::iterator childFind = d_substitutionCache.find(childNode); - if (childFind == d_substitutionCache.end()) { + NodeCache::iterator childFind = cache.find(childNode); + if (childFind == cache.end()) { toVisit.push_back(childNode); } } } else { // No children, so we're done Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << current << endl; - d_substitutionCache[current] = current; + cache[current] = current; toVisit.pop_back(); } } } // Return the substituted version - return d_substitutionCache[t]; + return cache[t]; }/* SubstitutionMap::internalSubstitute() */ - /* void SubstitutionMap::simplifyRHS(const SubstitutionMap& subMap) { // Put the new substitutions into the old ones @@ -160,10 +159,10 @@ void SubstitutionMap::simplifyRHS(TNode x, TNode t) { tempCache[x] = t; // Put the new substitution into the old ones - NodeMap::iterator it = d_substitutionsOld.begin(); - NodeMap::iterator it_end = d_substitutionsOld.end(); + NodeMap::iterator it = d_substitutions.begin(); + NodeMap::iterator it_end = d_substitutions.end(); for(; it != it_end; ++ it) { - d_substitutionsOld[(*it).first] = internalSubstituteOld((*it).second, tempCache); + d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache); } // it = d_substitutionsLazy.begin(); // it_end = d_substitutionsLazy.end(); @@ -171,7 +170,7 @@ void SubstitutionMap::simplifyRHS(TNode x, TNode t) { // d_substitutionsLazy[(*it).first] = internalSubstitute((*it).second, tempCache); // } } -*/ + /* We use subMap to simplify the left-hand sides of the current substitution map. If rewrite is true, * we also apply the rewriter to the result. @@ -283,6 +282,24 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) } } + +void SubstitutionMap::addSubstitutions(SubstitutionMap& subMap, bool invalidateCache) +{ + SubstitutionMap::NodeMap::const_iterator it = subMap.begin(); + SubstitutionMap::NodeMap::const_iterator it_end = subMap.end(); + for (; it != it_end; ++ it) { + Assert(d_substitutions.find((*it).first) == d_substitutions.end()); + d_substitutions[(*it).first] = (*it).second; + if (!invalidateCache) { + d_substitutionCache[(*it).first] = d_substitutions[(*it).first]; + } + } + if (invalidateCache) { + d_cacheInvalidated = true; + } +} + + static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED; static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) { SubstitutionMap::NodeMap::const_iterator it = substitutions.begin(); @@ -311,7 +328,7 @@ Node SubstitutionMap::apply(TNode t) { } // Perform the substitution - Node result = internalSubstitute(t); + Node result = internalSubstitute(t, d_substitutionCache); Debug("substitution") << "SubstitutionMap::apply(" << t << ") => " << result << endl; // Assert(check(result, d_substitutions)); |