diff options
author | Tim King <taking@google.com> | 2016-09-25 21:34:40 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-09-26 00:19:40 -0700 |
commit | f5ccf00833045487f75d2e241ea6b428f7da5dc2 (patch) | |
tree | 1dc7f2c009854bc195d0abd751193a14c44b6703 /src | |
parent | 6e809b29753727e3097e592780dd23ec68a534dc (diff) |
Simplifying control flow to avoid goto's in unconstrained_simplifier.cpp.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/unconstrained_simplifier.cpp | 78 |
1 files changed, 47 insertions, 31 deletions
diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index 393a7c559..32bbc662e 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -107,7 +107,6 @@ void UnconstrainedSimplifier::processUnconstrained() workList.push_back(*it); } Node currentSub; - TNode parent; bool swap; bool isSigned; bool strict; @@ -118,7 +117,7 @@ void UnconstrainedSimplifier::processUnconstrained() workList.pop_back(); for (;;) { Assert(d_visitedOnce.find(current) != d_visitedOnce.end()); - parent = d_visitedOnce[current]; + const TNode parent = d_visitedOnce[current]; if (!parent.isNull()) { swap = isSigned = strict = false; switch (parent.getKind()) { @@ -563,39 +562,56 @@ void UnconstrainedSimplifier::processUnconstrained() } break; - // Bit-vector comparisons: replace with new Boolean variable, but have to also conjoin with a side condition - // as there is always one case when the comparison is forced to be false + // Bit-vector comparisons: replace with new Boolean variable, but have + // to also conjoin with a side condition as there is always one case + // when the comparison is forced to be false case kind::BITVECTOR_ULT: - strict = true; case kind::BITVECTOR_UGE: - goto bvineq; - case kind::BITVECTOR_UGT: - strict = true; case kind::BITVECTOR_ULE: - swap = true; - goto bvineq; - case kind::BITVECTOR_SLT: - strict = true; case kind::BITVECTOR_SGE: - isSigned = true; - goto bvineq; - case kind::BITVECTOR_SGT: - strict = true; - case kind::BITVECTOR_SLE: - isSigned = true; - swap = true; - - bvineq: { + case kind::BITVECTOR_SLE: { + // Tuples over (signed, swap, strict). + switch (parent.getKind()) { + case kind::BITVECTOR_UGE: + break; + case kind::BITVECTOR_ULT: + strict = true; + break; + case kind::BITVECTOR_ULE: + swap = true; + break; + case kind::BITVECTOR_UGT: + swap = true; + strict = true; + break; + case kind::BITVECTOR_SGE: + isSigned = true; + break; + case kind::BITVECTOR_SLT: + isSigned = true; + strict = true; + break; + case kind::BITVECTOR_SLE: + isSigned = true; + swap = true; + break; + case kind::BITVECTOR_SGT: + isSigned = true; + swap = true; + strict = true; + break; + default: + Unreachable(); + } TNode other; bool left = false; if (parent[0] == current) { other = parent[1]; left = true; - } - else { + } else { Assert(parent[1] == current); other = parent[0]; } @@ -608,14 +624,14 @@ void UnconstrainedSimplifier::processUnconstrained() } currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; - } - else { + } else { currentSub = Node(); } - } - else { + } else { unsigned size = current.getType().getBitVectorSize(); - BitVector bv = isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) : BitVector(size, unsigned(0)); + BitVector bv = + isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) + : BitVector(size, unsigned(0)); if (swap == left) { bv = ~bv; } @@ -625,14 +641,14 @@ void UnconstrainedSimplifier::processUnconstrained() currentSub = newUnconstrainedVar(parent.getType(), currentSub); current = parent; NodeManager* nm = NodeManager::currentNM(); - Node test = Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv))); + Node test = + Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv))); if (test == nm->mkConst<bool>(false)) { break; } if (strict) { currentSub = currentSub.andNode(test.notNode()); - } - else { + } else { currentSub = currentSub.orNode(test); } // Delay adding this substitution - see comment at end of function |