ConstraintAnalysis: Add OR fusing of { x == C || x > C } => x >= C

src/ir/constraint.cpp

@@ -205,6 +205,83 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) {
   //       useful to implement that).
 }
 
+namespace {
+
+// Do an OR of a pair of constraints where the terms are known to be equal. If
+// we can't find a good way to express their ORing, return nullopt.
+std::optional<Constraint> approximateOrTermEqualPair(const Abstract::Op aOp,
+                                                     const Abstract::Op bOp,
+                                                     const Term& term) {
+  using namespace Abstract;
+
+  // x == C || x > C  ===  x >= C
+  if (aOp == Eq && bOp == GtS) {
+    return Constraint{GeS, term};
+  }
+
+  // TODO: all the rest
+
+  return {};
+}
+
+// Do an OR of a pair of constraints. If we can't find a good way to express
+// their ORing, return nullopt.
+std::optional<Constraint> approximateOrPair(const Constraint& a,
+                                            const Constraint& b,
+                                            bool recursing = false) {
+  if (a.term == b.term) {
+    if (auto result = approximateOrTermEqualPair(a.op, b.op, a.term)) {
+      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;
+  }
+
+  // TODO: more smarts
+
+  if (!recursing) {
+    // The flipped form may be recognized.
+    return approximateOrPair(b, a, true);
+  }
+
+  return {};
+}
+
+// Do an OR in full detail, looking at every constraint in each of the given
+// sets.
+AndedConstraintSet detailedApproximateOr(const AndedConstraintSet& a,
+                                         const AndedConstraintSet& b) {
+  // We can process this in full detail by looking at all the combinations of
+  // individual constraints, because of the distributive property:
+  //
+  // (A & B) | (C & D) == ((A & B) | C) & ((A & B) | D)
+  //                   == (A | C) & (B | C) & (A | D) & (B | D)
+  //
+  // This is quadratic, but constraint sets are limited to a very small size,
+  // making this reasonable.
+  //
+  // Also, note that we don't need to worry about new contradictions here: ORing
+  // things never leads to a contradiction, and we can assume the inputs are
+  // not contradictions.
+  assert(!a.provesEverything() && !b.provesEverything());
+
+  auto result = AndedConstraintSet::makeProvesNothing();
+  for (auto& ac : a) {
+    for (auto& bc : b) {
+      if (auto combined = approximateOrPair(ac, bc)) {
+        // We found something useful by ORing them, keep it.
+        result.approximateAnd(*combined);
+      }
+    }
+  }
+  return result;
+}
+
+} // anonymous namespace
+
 bool AndedConstraintSet::approximateOr(const AndedConstraintSet& other) {
   // If one proves everything, the only thing that matters is the other.
   if (other.provesEverything()) {
@@ -226,12 +303,11 @@ bool AndedConstraintSet::approximateOr(const AndedConstraintSet& other) {
     return true;
   }
 
-  // TODO smarts: handle <= > and so forth
-
-  // Otherwise, we don't know how to nicely OR these things, and expand to the
-  // trivial set of no constraints.
-  clear();
-  return true;
+  // For more complex cases, do a detailed analysis.
+  auto result = detailedApproximateOr(*this, other);
+  auto changed = (result != *this);
+  *this = result;
+  return changed;
 }
 
 std::optional<LocalConstraint> LocalConstraint::parse(Expression* curr) {

src/ir/constraint.h

@@ -92,6 +92,14 @@ struct AndedConstraintSet : inplace_vector<Constraint, MaxConstraints> {
   // until something changes.
   bool isContradiction = true;
 
+  AndedConstraintSet() = default;
+  AndedConstraintSet(std::initializer_list<Constraint> constraints) {
+    isContradiction = false;
+    for (auto& c : constraints) {
+      approximateAnd(c);
+    }
+  }
+
   // Proving everything (even contradictions) is equivalent to being a
   // contradiction. (This and provesNothing can be seen as the top/bottom of a
   // poset, if one wants to think of things that way.)

test/gtest/constraint.cpp

@@ -240,5 +240,103 @@ TEST(ConstraintTest, TestDeredundancy) {
   EXPECT_EQ(t[0], eq0);
 }
 
-// TODO: test an approximateOr of { x = 10 } and { x >= 0 }, once we support
-//       inequalities
+static void checkOr(const AndedConstraintSet& a,
+                    const AndedConstraintSet& b,
+                    const AndedConstraintSet& result) {
+  auto ored = a;
+  ored.approximateOr(b);
+  EXPECT_EQ(ored, result);
+
+  ored = b;
+  ored.approximateOr(a);
+  EXPECT_EQ(ored, result);
+}
+
+TEST(ConstraintTest, TestOrInequality) {
+  // x == 5 || x >= 0  =>  x >= 0
+  AndedConstraintSet eq5{Constraint{Eq, {Literal(int32_t(5))}}};
+  AndedConstraintSet ge0{Constraint{GeU, {Literal(int32_t(0))}}};
+  checkOr(eq5, ge0, ge0);
+
+  // x == 5 || x > 5  =>  x >= 5
+  AndedConstraintSet gts5{Constraint{GtS, {Literal(int32_t(5))}}};
+  AndedConstraintSet ges5{Constraint{GeS, {Literal(int32_t(5))}}};
+  checkOr(eq5, gts5, ges5);
+
+  // x == 5 || x >= 5  =>  x >= 5
+  checkOr(eq5, ges5, ges5);
+}
+
+TEST(ConstraintTest, TestOrLoop) {
+  // Check common loop patterns:
+  // { x == A } || { x > A && x <= B }   ==>   { x >= A && x <= B }
+
+  // { x == 5 } || { x > 5 && x <= 42 }   ==>   { x >= 5 && x <= 42 }
+  AndedConstraintSet left{Constraint{Eq, {Literal(int32_t(5))}}};
+  AndedConstraintSet right(
+    {{GtS, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}});
+  AndedConstraintSet result(
+    {{GeS, {Literal(int32_t(5))}}, {LeS, {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{Constraint{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{Constraint{Eq, {Literal(int32_t(99))}}};
+  AndedConstraintSet rightOnly5{Constraint{GtS, {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{Constraint{Eq, {Literal(int32_t(4))}}};
+  AndedConstraintSet rightOnly42({{LeS, {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(
+    {{GtS, {Literal(int32_t(6))}}, {LeS, {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{Constraint{Ne, {Literal(int32_t(5))}}};
+  auto empty = AndedConstraintSet::makeProvesNothing();
+  checkOr(leftNe, right, empty);
+
+  // Change the GtS on the right to GtU:
+  // { x == 5 } || { x >U 5 && x <= 42 }   ==>   { x <= 42 }
+  AndedConstraintSet rightGtU(
+    {{GtU, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}});
+  checkOr(left, rightGtU, rightOnly42);
+
+  // Change the LeS on the right to LeU:
+  // { x == 5 } || { x > 5 && x <=U 42 }   ==>   { x >= 5 && x <=U 42 }
+  AndedConstraintSet rightLeU(
+    {{GtS, {Literal(int32_t(5))}}, {LeU, {Literal(int32_t(42))}}});
+  AndedConstraintSet rightGesLeU(
+    {{GeS, {Literal(int32_t(5))}}, {LeU, {Literal(int32_t(42))}}});
+  checkOr(left, rightLeU, rightGesLeU);
+
+  // Add an operation on the right, x != 21:
+  // { x == 5 } || { x >  5 && x <= 42 && x != 21 }   ==>
+  //               { x >= 5 && x <= 42 && x != 21 }
+  AndedConstraintSet rightAdded({{GtS, {Literal(int32_t(5))}},
+                                 {LeS, {Literal(int32_t(42))}},
+                                 {Ne, {Literal(int32_t(21))}}});
+  AndedConstraintSet resultAdded({{GeS, {Literal(int32_t(5))}},
+                                  {LeS, {Literal(int32_t(42))}},
+                                  {Ne, {Literal(int32_t(21))}}});
+  checkOr(left, rightAdded, resultAdded);
+}