Fix BV Optimization Boundary Condition when lower bound = upper bound + 1 (#6452)

If lb = ub + 1 then (lb+ub)/2 =pivot == lb since it's rounding to -infinity.
and lb <= x < pivot will always be UNSAT.
We need to handle this differently.
And this only happens in minimization.

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,