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.

diff --git a/src/omt/bitvector_optimizer.cpp b/src/omt/bitvector_optimizer.cpp
index bfbf1cef376b7ea1bca65d96931cc5ff049095d5..ab5af03f79c7735aacd96e3502f407f2d2c9fae2 100644 (file)
--- 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,

diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
index 386f5b8f8df1799ebfaf5322afc3d4bef579735e..f94f37a19c1d57a722db2013fa1863d10f1ae149 100644 (file)
--- a/test/unit/theory/theory_bv_opt_white.cpp
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -151,5 +151,30 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max)
             << std::endl;
 }
 
+TEST_F(TestTheoryWhiteBVOpt, min_boundary)
+{
+  Node x = d_nodeManager->mkVar(*d_BV32Type);
+  Node y = d_nodeManager->mkVar(*d_BV32Type);
+
+  // x <= 18
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(
+      kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
+  // this perturbs the solver to trigger some boundary bug
+  // that existed previously
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
+
+  d_optslv->activateObj(x, ObjectiveType::OBJECTIVE_MINIMIZE, false);
+
+  OptResult r = d_optslv->checkOpt();
+
+  ASSERT_EQ(r, OptResult::OPT_OPTIMAL);
+
+  // expect the maximum x = 18
+  ASSERT_EQ(d_optslv->objectiveGetValue(),
+            d_nodeManager->mkConst(BitVector(32u, 18u)));
+  std::cout << "Optimized value is: " << d_optslv->objectiveGetValue()
+            << std::endl;
+}
+
 }  // namespace test
 }  // namespace cvc5