diff options
Diffstat (limited to 'src/omt')
-rw-r--r-- | src/omt/bitvector_optimizer.cpp | 53 |
1 files changed, 22 insertions, 31 deletions
diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp index bfbf1cef3..ab5af03f7 100644 --- a/src/omt/bitvector_optimizer.cpp +++ b/src/omt/bitvector_optimizer.cpp @@ -35,18 +35,12 @@ BitVector OMTOptimizerBitVector::computeAverage(const BitVector& a, // average = (a / 2) + (b / 2) + (((a % 2) + (b % 2)) / 2) uint32_t aMod2 = static_cast<uint32_t>(a.isBitSet(0)); uint32_t bMod2 = static_cast<uint32_t>(b.isBitSet(0)); - BitVector aMod2PlusbMod2(a.getSize(), (aMod2 + bMod2) / 2); + BitVector aMod2PlusbMod2Div2(a.getSize(), (aMod2 + bMod2) / 2); BitVector bv1 = BitVector::mkOne(a.getSize()); - if (isSigned) - { - return (a.arithRightShift(bv1) + b.arithRightShift(bv1) - + aMod2PlusbMod2.arithRightShift(bv1)); - } - else - { - return (a.logicalRightShift(bv1) + b.logicalRightShift(bv1) - + aMod2PlusbMod2.logicalRightShift(bv1)); - } + return (isSigned) ? ((a.arithRightShift(bv1) + b.arithRightShift(bv1) + + aMod2PlusbMod2Div2)) + : ((a.logicalRightShift(bv1) + b.logicalRightShift(bv1) + + aMod2PlusbMod2Div2)); } std::pair<OptResult, Node> OMTOptimizerBitVector::minimize( @@ -92,23 +86,24 @@ std::pair<OptResult, Node> OMTOptimizerBitVector::minimize( // pivot = (lowerBound + upperBound) / 2 // rounded towards -infinity BitVector pivot; - while (true) + while ((d_isSigned && lowerBound.signedLessThan(upperBound)) + || (!d_isSigned && lowerBound.unsignedLessThan(upperBound))) { - if (d_isSigned) + pivot = computeAverage(lowerBound, upperBound, d_isSigned); + optChecker->push(); + if (lowerBound == pivot) { - if (!lowerBound.signedLessThan(upperBound)) break; + optChecker->assertFormula( + nm->mkNode(kind::EQUAL, target, nm->mkConst(lowerBound))); } else { - if (!lowerBound.unsignedLessThan(upperBound)) break; + // lowerBound <= target < pivot + optChecker->assertFormula( + nm->mkNode(kind::AND, + nm->mkNode(GEOperator, target, nm->mkConst(lowerBound)), + nm->mkNode(LTOperator, target, nm->mkConst(pivot)))); } - pivot = computeAverage(lowerBound, upperBound, d_isSigned); - optChecker->push(); - // lowerBound <= target < pivot - optChecker->assertFormula( - nm->mkNode(kind::AND, - nm->mkNode(GEOperator, target, nm->mkConst(lowerBound)), - nm->mkNode(LTOperator, target, nm->mkConst(pivot)))); intermediateSatResult = optChecker->checkSat(); if (intermediateSatResult.isUnknown() || intermediateSatResult.isNull()) { @@ -186,19 +181,15 @@ std::pair<OptResult, Node> OMTOptimizerBitVector::maximize( // pivot = (lowerBound + upperBound) / 2 // rounded towards -infinity BitVector pivot; - while (true) + while ((d_isSigned && lowerBound.signedLessThan(upperBound)) + || (!d_isSigned && lowerBound.unsignedLessThan(upperBound))) { - if (d_isSigned) - { - if (!lowerBound.signedLessThan(upperBound)) break; - } - else - { - if (!lowerBound.unsignedLessThan(upperBound)) break; - } pivot = computeAverage(lowerBound, upperBound, d_isSigned); optChecker->push(); + // notice that we don't have boundary condition here + // because lowerBound == pivot / lowerBound == upperBound + 1 is also + // covered // pivot < target <= upperBound optChecker->assertFormula( nm->mkNode(kind::AND, |