diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-05 19:48:30 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-05 19:48:30 +0000 |
commit | f5ce374d107882e4385f8b0deed3ef1129f49c79 (patch) | |
tree | 293f9fd11581677561e743322bd0743b9d0c4c23 /src/theory/unconstrained_simplifier.cpp | |
parent | dd0ca308c3299155bfab89ade6cfd0a70b9abda5 (diff) |
Fixed a performance issue with unconstrained simplifier
Diffstat (limited to 'src/theory/unconstrained_simplifier.cpp')
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 72 |
1 files changed, 58 insertions, 14 deletions
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<TNode> delayQueueLeft; + vector<TNode> 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(); + } } |