diff options
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; |