From 741ee9aae3bd68c92a7c569f069b7f7361c34c70 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 31 Jul 2026 15:44:59 -0700
Subject: [PATCH] more

---
 src/ir/constraint.cpp     | 12 ++++++++
 test/gtest/constraint.cpp | 65 +++++++++++++++++++++++++++++++++++++--
 2 files changed, 75 insertions(+), 2 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index afe76703a91..b2b018500d3 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -265,11 +265,17 @@ std::optional<Constraint> approximateOrTermEqualPair(const Abstract::Op aOp,
   if (aOp == Eq && bOp == GtS) {
     return Constraint{GeS, term};
   }
+  if (aOp == Eq && bOp == GtU) {
+    return Constraint{GeU, term};
+  }
 
   // x > C || x >= C  ===  x >= C
   if (aOp == GtS && bOp == GeS) {
     return Constraint{GeS, term};
   }
+  if (aOp == GtU && bOp == GeU) {
+    return Constraint{GeU, term};
+  }
 
   // TODO: all the rest
 
@@ -286,11 +292,17 @@ std::optional<Constraint> approximateOrAdjacentConstantPair(
   if (aOp == Eq && bOp == GeS && !aConstant.isSignedMax()) {
     return Constraint{GeS, {aConstant}};
   }
+  if (aOp == Eq && bOp == GeU && !aConstant.isUnsignedMax()) {
+    return Constraint{GeU, {aConstant}};
+  }
 
   // x > C || x >= C+1  ===  x > C, if C+1 does not overflow.
   if (aOp == GtS && bOp == GeS && !aConstant.isSignedMax()) {
     return Constraint{GtS, {aConstant}};
   }
+  if (aOp == GtU && bOp == GeU && !aConstant.isUnsignedMax()) {
+    return Constraint{GtU, {aConstant}};
+  }
 
   // TODO: all the rest
 
diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index da1f05f2f66..0b534d12efb 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -348,10 +348,12 @@ TEST(ConstraintTest, TestOrLoop) {
   checkOr(leftNe, right, empty);
 
   // Change the GtS on the right to GtU:
-  // { x == 5 } || { x >U 5 && x <= 42 }   ==>   { x <= 42 }
+  // { x == 5 } || { x >U 5 && x <= 42 }   ==>   { x >=U 5 && x <= 42 }
   AndedConstraintSet rightGtU(
     {{GtU, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}});
-  checkOr(left, rightGtU, rightOnly42);
+  AndedConstraintSet resultMixed(
+    {{GeU, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}});
+  checkOr(left, rightGtU, resultMixed);
 
   // Change the LeS on the right to LeU:
   // { x == 5 } || { x > 5 && x <=U 42 }   ==>   { x >= 5 && x <=U 42 }
@@ -373,6 +375,65 @@ TEST(ConstraintTest, TestOrLoop) {
   checkOr(left, rightAdded, resultAdded);
 }
 
+TEST(ConstraintTest, TestOrLoopUnsigned) {
+  // As above, but unsigned.
+
+  // { x == 5 } || { x > 5 && x <= 42 }   ==>   { x >= 5 && x <= 42 }
+  AndedConstraintSet left{{Eq, {Literal(int32_t(5))}}};
+  AndedConstraintSet right(
+    {{GtU, {Literal(int32_t(5))}}, {LeU, {Literal(int32_t(42))}}});
+  AndedConstraintSet result(
+    {{GeU, {Literal(int32_t(5))}}, {LeU, {Literal(int32_t(42))}}});
+  checkOr(left, right, result);
+
+  // Changes to constants:
+
+  // Change 5 on the left to 7:
+  // { x == 7 } || { x > 5 && x <= 42 }   ==>   { x > 5 && x <= 42}
+  AndedConstraintSet left7{{Eq, {Literal(int32_t(7))}}};
+  checkOr(left7, right, right);
+
+  // Change 5 on the left to 99:
+  // { x == 99 } || { x > 5 && x <= 42 }   ==>   { x > 5 }
+  // TODO: we could emit a range (5, 99]
+  AndedConstraintSet left99{{Eq, {Literal(int32_t(99))}}};
+  AndedConstraintSet rightOnly5{{GtU, {Literal(int32_t(5))}}};
+  checkOr(left99, right, rightOnly5);
+
+  // Change 5 on the left to 4:
+  // { x == 4 } || { x > 5 && x <= 42 }   ==>   { x <= 42 }
+  // TODO: we could emit a range [4, 42]
+  AndedConstraintSet left4{{Eq, {Literal(int32_t(4))}}};
+  AndedConstraintSet rightOnly42({{LeU, {Literal(int32_t(42))}}});
+  checkOr(left4, right, rightOnly42);
+
+  // Change 5 on the right to 6:
+  // { x == 5 } || { x > 6 && x <= 42 }   ==>   { x <= 42 }
+  AndedConstraintSet right6(
+    {{GtU, {Literal(int32_t(6))}}, {LeU, {Literal(int32_t(42))}}});
+  checkOr(left, right6, rightOnly42);
+
+  // Changes to operations:
+
+  // Change the Eq on the left to Ne. We fail to find anything for the OR.
+  // { x != 5 } || { x > 5 && x <= 42 }   ==>   {}
+  // TODO: we could emit x != 5
+  AndedConstraintSet leftNe{{Ne, {Literal(int32_t(5))}}};
+  auto empty = AndedConstraintSet::makeProvesNothing();
+  checkOr(leftNe, right, empty);
+
+  // Add an operation on the right, x != 21:
+  // { x == 5 } || { x >  5 && x <= 42 && x != 21 }   ==>
+  //               { x >= 5 && x <= 42 && x != 21 }
+  AndedConstraintSet rightAdded({{GtU, {Literal(int32_t(5))}},
+                                 {LeU, {Literal(int32_t(42))}},
+                                 {Ne, {Literal(int32_t(21))}}});
+  AndedConstraintSet resultAdded({{GeU, {Literal(int32_t(5))}},
+                                  {LeU, {Literal(int32_t(42))}},
+                                  {Ne, {Literal(int32_t(21))}}});
+  checkOr(left, rightAdded, resultAdded);
+}
+
 static void checkAnd(const AndedConstraintSet& a,
                      const AndedConstraintSet& b,
                      const AndedConstraintSet& result) {