ConstraintAnalysis: Remove older redundant constraints

src/ir/constraint.cpp

@@ -137,15 +137,29 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) {
   auto result = proves(c);
   if (result == True) {
     // We already prove c to be true, so it adds nothing.
-    // TODO: we could also see if c proves us true, and replace things we
-    //       already have with c when possible
     return;
   } else if (result == False) {
     // We are now a contradiction.
     isContradiction = true;
     return;
   }
 
+  // If c proves something already present to be true, it can just replace it.
+  for (auto& existing : *this) {
+    auto result = provesPair(c, existing);
+    if (result == True) {
+      existing = c;
+
+      // Sort to ensure we are in the right place.
+      std::sort(begin(), end());
+
+      return;
+    }
+
+    // There cannot be a contradiction here, because we checked for that above.
+    assert(result != False);
+  }
+
   if (size() < MaxConstraints) {
     // Insert into the right place, keeping us sorted.
     insert(std::upper_bound(begin(), end(), c), c);

test/gtest/constraint.cpp

@@ -219,5 +219,26 @@ TEST(ConstraintTest, TestDeduplication) {
   EXPECT_EQ(s.size(), 1);
 }
 
+TEST(ConstraintTest, TestDeredundancy) {
+  Constraint eq0{Eq, {Literal(int32_t(0))}};
+  Constraint ne1{Ne, {Literal(int32_t(1))}};
+
+  // If x == 0, then x != 1 is redundant, and does not need to be added, is it
+  // is implied by x == 0.
+  AndedConstraintSet s;
+  s.set(eq0);
+  s.approximateAnd(ne1);
+  EXPECT_EQ(s.size(), 1);
+  EXPECT_EQ(s[0], eq0);
+
+  // Reverse order, same result, even though we added x == 0 last: we remove
+  // x != 1.
+  AndedConstraintSet t;
+  t.set(ne1);
+  t.approximateAnd(eq0);
+  EXPECT_EQ(t.size(), 1);
+  EXPECT_EQ(t[0], eq0);
+}
+
 // TODO: test an approximateOr of { x = 10 } and { x >= 0 }, once we support
 //       inequalities