From f5ce374d107882e4385f8b0deed3ef1129f49c79 Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Tue, 5 Jun 2012 19:48:30 +0000 Subject: [PATCH] Fixed a performance issue with unconstrained simplifier --- src/theory/substitutions.cpp | 26 ++++----- src/theory/substitutions.h | 12 ++++- src/theory/unconstrained_simplifier.cpp | 72 ++++++++++++++++++++----- 3 files changed, 82 insertions(+), 28 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; } diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 711ff9b72..c32dee635 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -102,9 +102,17 @@ public: } /** - * Adds a substitution from x to t + * Adds a substitution from x to t. Typically you also want to apply this + * substitution to the existing set (backSub), but you do not need to + * apply the existing set to the new substitution (forwardSub). However, + * the method allows you to do either. Probably you should not do both, + * as it will be very difficult to maintain the invariant that no + * left-hand side appears on any right-hand side. */ - void addSubstitution(TNode x, TNode t, bool invalidateCache = true); + void addSubstitution(TNode x, TNode t, + bool invalidateCache = true, + bool backSub = true, + bool forwardSub = false); /** * Returns true iff x is in the substitution map diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index b1a944597..43377cf37 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -121,18 +121,21 @@ void UnconstrainedSimplifier::processUnconstrained() for ( ; it != iend; ++it) { workList.push_back(*it); } - TNode current = workList.back(); Node currentSub; - workList.pop_back(); + TNode parent; + bool swap; + bool isSigned; + bool strict; + vector delayQueueLeft; + vector delayQueueRight; + TNode current = workList.back(); + workList.pop_back(); for (;;) { - TNodeMap::iterator itNodeMap; Assert(d_visitedOnce.find(current) != d_visitedOnce.end()); - TNode parent = d_visitedOnce[current]; - bool swap = false; - bool isSigned = false; - bool strict = false; + parent = d_visitedOnce[current]; if (!parent.isNull()) { + swap = isSigned = strict = false; switch (parent.getKind()) { // If-then-else operator - any two unconstrained children makes the parent unconstrained @@ -146,12 +149,30 @@ void UnconstrainedSimplifier::processUnconstrained() !d_substitutions.hasSubstitution(parent)) { removeExpr(parent); if (uThen) { - if (parent[1] != current || currentSub.isNull()) { - currentSub = parent[1]; + if (parent[1] != current) { + if (parent[1].isVar()) { + currentSub = parent[1]; + } + else { + Assert(d_substitutions.hasSubstitution(parent[1])); + currentSub = d_substitutions.apply(parent[1]); + } + } + else if (currentSub.isNull()) { + currentSub = current; + } + } + else if (parent[2] != current) { + if (parent[2].isVar()) { + currentSub = parent[2]; + } + else { + Assert(d_substitutions.hasSubstitution(parent[2])); + currentSub = d_substitutions.apply(parent[2]); } } - else if (parent[2] != current || currentSub.isNull()) { - currentSub = parent[2]; + else if (currentSub.isNull()) { + currentSub = current; } current = parent; } @@ -520,8 +541,12 @@ void UnconstrainedSimplifier::processUnconstrained() if (d_unconstrained.find(parent) == d_unconstrained.end() && !d_substitutions.hasSubstitution(parent)) { removeExpr(parent); - if (parent[0] != current || currentSub.isNull()) { - currentSub = parent[0]; + if (parent[0] != current) { + Assert(d_substitutions.hasSubstitution(parent[0])); + currentSub = d_substitutions.apply(parent[0]); + } + else if (currentSub.isNull()) { + currentSub = current; } current = parent; } @@ -603,6 +628,10 @@ void UnconstrainedSimplifier::processUnconstrained() else { currentSub = currentSub.orNode(test); } + // Delay adding this substitution - see comment at end of function + delayQueueLeft.push_back(current); + delayQueueRight.push_back(currentSub); + currentSub = Node(); parent = TNode(); } break; @@ -627,7 +656,8 @@ void UnconstrainedSimplifier::processUnconstrained() } } if (!currentSub.isNull()) { - d_substitutions.addSubstitution(current, currentSub); + Assert(currentSub.isVar()); + d_substitutions.addSubstitution(current, currentSub, false, false, false); } if (workList.empty()) { break; @@ -636,6 +666,20 @@ void UnconstrainedSimplifier::processUnconstrained() currentSub = Node(); workList.pop_back(); } + TNode left; + Node right; + // All substitutions except those arising from bitvector comparisons are + // substitutions t -> x where x is a variable. This allows us to build the + // substitution very quickly (never invalidating the substitution cache). + // Bitvector comparisons are more complicated and may require + // back-substitution and cache-invalidation. So we do these last. + while (!delayQueueLeft.empty()) { + left = delayQueueLeft.back(); + right = d_substitutions.apply(delayQueueRight.back()); + d_substitutions.addSubstitution(delayQueueLeft.back(), right, true, true, false); + delayQueueLeft.pop_back(); + delayQueueRight.pop_back(); + } } -- 2.30.2