diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-14 19:37:31 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-14 19:37:31 +0000 |
commit | b849eeef09465da1100cd6a94beacc893849fb25 (patch) | |
tree | 569562d3de4aa31268a52dc14edec4e0dece7a4a /src/theory/unconstrained_simplifier.cpp | |
parent | 2581001b96a64e1d11d826cf554d378ac522bbe2 (diff) |
New substitutions implementation - fixes performance issue seen in nonclausal
simplification for some benchmarks
Diffstat (limited to 'src/theory/unconstrained_simplifier.cpp')
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 1c507eb71..7e06297fb 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -653,7 +653,7 @@ void UnconstrainedSimplifier::processUnconstrained() } if (!currentSub.isNull()) { Assert(currentSub.isVar()); - d_substitutions.addSubstitution(current, currentSub, false, false, false); + d_substitutions.addSubstitution(current, currentSub, false); } if (workList.empty()) { break; @@ -673,7 +673,7 @@ void UnconstrainedSimplifier::processUnconstrained() left = delayQueueLeft.back(); if (!d_substitutions.hasSubstitution(left)) { right = d_substitutions.apply(delayQueueRight.back()); - d_substitutions.addSubstitution(delayQueueLeft.back(), right, true, true, false); + d_substitutions.addSubstitution(delayQueueLeft.back(), right); } delayQueueLeft.pop_back(); delayQueueRight.pop_back(); |