ConstraintAnalysis: Add more simple inequalities

src/ir/constraint.cpp

@@ -266,6 +266,32 @@ std::optional<Constraint> approximateOrTermEqualPair(const Abstract::Op aOp,
     return Constraint{GeS, term};
   }
 
+  // x > C || x >= C  ===  x >= C
+  if (aOp == GtS && bOp == GeS) {
+    return Constraint{GeS, term};
+  }
+
+  // TODO: all the rest
+
+  return {};
+}
+
+// Do an OR of a pair of constraints where the terms are adjacent constants: a
+// operates on C, and b on C+1.
+std::optional<Constraint> approximateOrAdjacentConstantPair(
+  const Abstract::Op aOp, const Literal& aConstant, const Abstract::Op bOp) {
+  using namespace Abstract;
+
+  // x == C || x >= C+1  ===  x >= C, if C+1 does not overflow.
+  if (aOp == Eq && bOp == GeS && !aConstant.isSignedMax()) {
+    return Constraint{GeS, {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}};
+  }
+
   // TODO: all the rest
 
   return {};
@@ -282,6 +308,18 @@ std::optional<Constraint> approximateOrPair(const Constraint& a,
     }
   }
 
+  // See if we operate on constants N, N+1.
+  if (auto* ac = std::get_if<Literal>(&a.term)) {
+    if (auto* bc = std::get_if<Literal>(&b.term)) {
+      if (ac->type == bc->type && ac->type.isInteger() &&
+          ac->add(Literal::makeFromInt32(1, ac->type)) == *bc) {
+        if (auto result = approximateOrAdjacentConstantPair(a.op, *ac, b.op)) {
+          return result;
+        }
+      }
+    }
+  }
+
   // If a proves b, e.g. x = 5 proves x >= 0 is true, then the OR is b.
   if (provesPair(a, b) == True) {
     return b;

test/gtest/constraint.cpp

@@ -265,6 +265,37 @@ TEST(ConstraintTest, TestOrInequality) {
 
   // x == 5 || x >= 5  =>  x >= 5
   checkOr(eq5, ges5, ges5);
+
+  // x == 5 || x >= 6  =>  x >= 5
+  AndedConstraintSet ges6{{GeS, {Literal(int32_t(6))}}};
+  checkOr(eq5, ges6, ges5);
+
+  // TODO: x == 5 || x >= 7  =>  x >= 5  TODO
+  AndedConstraintSet ges7{{GeS, {Literal(int32_t(7))}}};
+  auto empty = AndedConstraintSet::makeProvesNothing();
+  checkOr(eq5, ges7, empty);
+
+  // x > 5 || x >= 6  =>  x > 5
+  checkOr(gts5, ges6, gts5);
+
+  // x > 5 || x >= 5  =>  x >= 5
+  checkOr(gts5, ges5, ges5);
+
+  // Careful of overflow:
+  // x == signed_max || x >= (signed_max + 1 === signed_min) != x >= signed_max
+  AndedConstraintSet eqMax{
+    {Eq, {Literal(std::numeric_limits<int32_t>::max())}}};
+  AndedConstraintSet gesMin{
+    {GeS, {Literal(std::numeric_limits<int32_t>::min())}}};
+  // TODO: x >= signed_min is always true, so this could be empty
+  checkOr(eqMax, gesMin, gesMin);
+
+  // Careful of overflow:
+  // x > signed_max || x >= (signed_max + 1 === signed_min) != x > signed_max
+  AndedConstraintSet gtsMax{
+    {GtS, {Literal(std::numeric_limits<int32_t>::max())}}};
+  // TODO: x > signed_max is always false, so this could return a contradiction
+  checkOr(gtsMax, gesMin, empty);
 }
 
 TEST(ConstraintTest, TestOrLoop) {