diff options
Diffstat (limited to 'src/theory/substitutions.cpp')
-rw-r--r-- | src/theory/substitutions.cpp | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index b7ad1d174..f56dd47b6 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -103,25 +103,27 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache) return substitutionCache[t]; } -void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) { +void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache, bool backSub, bool forwardSub) { Debug("substitution") << "SubstitutionMap::addSubstitution(" << x << ", " << t << ")" << std::endl; Assert(d_substitutions.find(x) == d_substitutions.end()); - // Temporary substitution cache - NodeCache tempCache; - tempCache[x] = t; + if (backSub) { + // Temporary substitution cache + NodeCache tempCache; + tempCache[x] = t; - // Put in the new substitutions into the old ones - NodeMap::iterator it = d_substitutions.begin(); - NodeMap::iterator it_end = d_substitutions.end(); - for(; it != it_end; ++ it) { - d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache); + // Put in the new substitutions into the old ones + NodeMap::iterator it = d_substitutions.begin(); + NodeMap::iterator it_end = d_substitutions.end(); + for(; it != it_end; ++ it) { + d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache); + } } - // Put the new substitution in, but apply existing substitutions to rhs first - d_substitutions[x] = apply(t); + // Put the new substitution in + d_substitutions[x] = forwardSub ? apply(t) : Node(t); - // Also invalidate the cache + // Also invalidate the cache if necessary if (invalidateCache) { d_cacheInvalidated = true; } |