diff options
author | Peter Collingbourne <pcc@google.com> | 2014-03-16 22:00:39 -0700 |
---|---|---|
committer | Peter Collingbourne <pcc@google.com> | 2014-03-16 22:36:30 -0700 |
commit | e1ac093478ef409707833ebe59be944536605c71 (patch) | |
tree | 1f1259de8c9aba3bcd48edeb282a8cc3cdacbf4b /src/theory/unconstrained_simplifier.cpp | |
parent | 52514303081e78c98e504980a50b76a04f4b8762 (diff) |
Fix for ite of >=64bit wide bitvectors with unconstrained condition.
Diffstat (limited to 'src/theory/unconstrained_simplifier.cpp')
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 35 |
1 files changed, 19 insertions, 16 deletions
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index a6e885f97..115788639 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -163,23 +163,26 @@ void UnconstrainedSimplifier::processUnconstrained() currentSub = Node(); } } - else if (uCond && parent.getType().getCardinality().isFinite() && parent.getType().getCardinality().getFiniteCardinality() == 2) { - // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result - // is unconstrained - Node test; - if (parent.getType().isBoolean()) { - test = Rewriter::rewrite(parent[1].iffNode(parent[2])); - } - else { - test = Rewriter::rewrite(parent[1].eqNode(parent[2])); - } - if (test == NodeManager::currentNM()->mkConst<bool>(false)) { - ++d_numUnconstrainedElim; - if (currentSub.isNull()) { - currentSub = current; + else if (uCond) { + Cardinality card = parent.getType().getCardinality(); + if (card.isFinite() && !card.isLargeFinite() && card.getFiniteCardinality() == 2) { + // Special case: condition is unconstrained, then and else are different, and total cardinality of the type is 2, then the result + // is unconstrained + Node test; + if (parent.getType().isBoolean()) { + test = Rewriter::rewrite(parent[1].iffNode(parent[2])); + } + else { + test = Rewriter::rewrite(parent[1].eqNode(parent[2])); + } + if (test == NodeManager::currentNM()->mkConst<bool>(false)) { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; } - currentSub = newUnconstrainedVar(parent.getType(), currentSub); - current = parent; } } break; |