From 37e3f98618a5b9b5538d01a4388103a1cbe4642e Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 12:30:25 -0700
Subject: [PATCH 01/89] comparisons

---
 src/ir/constraint.cpp | 41 +++++++++++++++++++++++++++++------------
 1 file changed, 29 insertions(+), 12 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index e6119600442..3e438337f72 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -24,36 +24,53 @@ namespace wasm::constraint {
 
 namespace {
 
+Result TrueFalse(bool x) {
+  return x ? True : False;
+}
+
+Result TrueFalse(Literal x) {
+  return TrueFalse(x.getUnsigned());
+}
+
 // Evaluate whether a => b, where a and b are operations on constants.
 Result provesConstantPair(Abstract::Op aOp,
                           const Literal& aConstant,
                           Abstract::Op bOp,
                           const Literal& bConstant) {
-  // x == X =?=> x == Y. True iff X == Y.
-  if (aOp == Abstract::Eq && bOp == Abstract::Eq) {
-    return aConstant == bConstant ? True : False;
-  }
-
-  // x == X =?=> x != Y. True iff X != Y.
-  if (aOp == Abstract::Eq && bOp == Abstract::Ne) {
-    return aConstant == bConstant ? False : True;
+  // a == A =?=> a op B. Simply apply A to the operation against B.
+  if (aOp == Abstract::Eq) {
+    switch (bOp) {
+      case Abstract::Eq:
+        return TrueFalse(aConstant == bConstant);
+      case Abstract::Ne:
+        return TrueFalse(aConstant != bConstant);
+      case Abstract::LtS:
+        return TrueFalse(aConstant.ltS(bConstant));
+      case Abstract::LeS:
+        return TrueFalse(aConstant.leS(bConstant));
+      case Abstract::GtS:
+        return TrueFalse(aConstant.gtS(bConstant));
+      case Abstract::GeS:
+        return TrueFalse(aConstant.geS(bConstant));
+      default: {}
+    }
   }
 
-  // x != X =?=> x == Y. False if X = Y, else unknown.
+  // a != A =?=> a == B. False if A = B, else unknown.
   if (aOp == Abstract::Ne && bOp == Abstract::Eq) {
     if (aConstant == bConstant) {
       return False;
     }
   }
 
-  // x != X =?=> x != Y. True if X = Y, else unknown.
+  // a != A =?=> a != B. True if A = B, else unknown.
   if (aOp == Abstract::Ne && bOp == Abstract::Ne) {
     if (aConstant == bConstant) {
       return True;
     }
-  }
+  }  
 
-  // TODO: handle >, >=, <, and <=
+  // TODO: handle all the rest of >, >=, <, and <=
   return Unknown;
 }
 

From aa3dc24ca0f5fc530a02f22a08e0f6f562d15914 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 12:30:31 -0700
Subject: [PATCH 02/89] fmt

---
 src/ir/constraint.cpp | 13 +++++--------
 1 file changed, 5 insertions(+), 8 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 3e438337f72..cde009bfdca 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -24,13 +24,9 @@ namespace wasm::constraint {
 
 namespace {
 
-Result TrueFalse(bool x) {
-  return x ? True : False;
-}
+Result TrueFalse(bool x) { return x ? True : False; }
 
-Result TrueFalse(Literal x) {
-  return TrueFalse(x.getUnsigned());
-}
+Result TrueFalse(Literal x) { return TrueFalse(x.getUnsigned()); }
 
 // Evaluate whether a => b, where a and b are operations on constants.
 Result provesConstantPair(Abstract::Op aOp,
@@ -52,7 +48,8 @@ Result provesConstantPair(Abstract::Op aOp,
         return TrueFalse(aConstant.gtS(bConstant));
       case Abstract::GeS:
         return TrueFalse(aConstant.geS(bConstant));
-      default: {}
+      default: {
+      }
     }
   }
 
@@ -68,7 +65,7 @@ Result provesConstantPair(Abstract::Op aOp,
     if (aConstant == bConstant) {
       return True;
     }
-  }  
+  }
 
   // TODO: handle all the rest of >, >=, <, and <=
   return Unknown;

From 6c7e2b02f9295fd240ef42f8be49b14984c21c15 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 12:34:06 -0700
Subject: [PATCH 03/89] work

---
 test/lit/passes/constraint-analysis.wast | 76 ++++++++++++++++++++++++
 1 file changed, 76 insertions(+)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 14e804a53f7..fe8967a55be 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -3924,5 +3924,81 @@
       )
     )
   )
+
+  ;; CHECK:      (func $constant-inequalities-lt_s (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-lt_s (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.lt_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 41)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.lt_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 42)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.lt_u
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:    (i32.const 43)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-lt_s
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.lt_s
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.lt_s
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.lt_s
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.lt_s
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
 )
 

From 88547337dcdfcf9752287957aabd8388ea3316dc Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 12:35:57 -0700
Subject: [PATCH 04/89] work

---
 src/ir/constraint.cpp                    |   8 +
 test/lit/passes/constraint-analysis.wast | 485 ++++++++++++++++++++++-
 2 files changed, 480 insertions(+), 13 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index cde009bfdca..7366a7645b5 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -48,6 +48,14 @@ Result provesConstantPair(Abstract::Op aOp,
         return TrueFalse(aConstant.gtS(bConstant));
       case Abstract::GeS:
         return TrueFalse(aConstant.geS(bConstant));
+      case Abstract::LtU:
+        return TrueFalse(aConstant.ltU(bConstant));
+      case Abstract::LeU:
+        return TrueFalse(aConstant.leU(bConstant));
+      case Abstract::GtU:
+        return TrueFalse(aConstant.gtU(bConstant));
+      case Abstract::GeU:
+        return TrueFalse(aConstant.geU(bConstant));
       default: {
       }
     }
diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index fe8967a55be..ed98a224652 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -3949,22 +3949,13 @@
   ;; OPTIN-NEXT:   (i32.const 42)
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT:  (drop
-  ;; OPTIN-NEXT:   (i32.lt_u
-  ;; OPTIN-NEXT:    (local.get $x)
-  ;; OPTIN-NEXT:    (i32.const 41)
-  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (i32.const 0)
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT:  (drop
-  ;; OPTIN-NEXT:   (i32.lt_u
-  ;; OPTIN-NEXT:    (local.get $x)
-  ;; OPTIN-NEXT:    (i32.const 42)
-  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (i32.const 0)
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT:  (drop
-  ;; OPTIN-NEXT:   (i32.lt_u
-  ;; OPTIN-NEXT:    (local.get $x)
-  ;; OPTIN-NEXT:    (i32.const 43)
-  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (i32.const 1)
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT:  (drop
   ;; OPTIN-NEXT:   (i32.const 0)
@@ -4000,5 +3991,473 @@
       )
     )
   )
-)
 
+  ;; CHECK:      (func $constant-inequalities-le_s (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-le_s (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-le_s
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.le_s
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.le_s
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.le_s
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.le_s
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-gt_s (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-gt_s (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-gt_s
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.gt_s
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.gt_s
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.gt_s
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.gt_s
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-ge_s (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-ge_s (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-ge_s
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.ge_s
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.ge_s
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.ge_s
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.ge_s
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-lt_u (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-lt_u (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-lt_u
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.lt_u
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.lt_u
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.lt_u
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.lt_u
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-le_u (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-le_u (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-le_u
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.le_u
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.le_u
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.le_u
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.le_u
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-gt_u (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-gt_u (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-gt_u
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.gt_u
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.gt_u
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.gt_u
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.gt_u
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+
+  ;; CHECK:      (func $constant-inequalities-ge_u (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 42)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (drop
+  ;; CHECK-NEXT:   (i32.const 0)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $constant-inequalities-ge_u (type $1)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (local.set $x
+  ;; OPTIN-NEXT:   (i32.const 42)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 1)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT:  (drop
+  ;; OPTIN-NEXT:   (i32.const 0)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $constant-inequalities-ge_u
+    (local $x i32)
+    (local.set $x
+      (i32.const 42)
+    )
+    (drop
+      (i32.ge_u
+        (local.get $x)
+        (i32.const 41)
+      )
+    )
+    (drop
+      (i32.ge_u
+        (local.get $x)
+        (i32.const 42)
+      )
+    )
+    (drop
+      (i32.ge_u
+        (local.get $x)
+        (i32.const 43)
+      )
+    )
+    (drop
+      (i32.ge_u
+        (local.get $x)
+        (i32.const -1)
+      )
+    )
+  )
+)

From f9ae5f1ccde34e3c151ab83078d67d113f8f3881 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 12:38:22 -0700
Subject: [PATCH 05/89] work

---
 test/lit/passes/constraint-analysis.wast | 1 +
 1 file changed, 1 insertion(+)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index ed98a224652..f8c9af32993 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -3962,6 +3962,7 @@
   ;; OPTIN-NEXT:  )
   ;; OPTIN-NEXT: )
   (func $constant-inequalities-lt_s
+    ;; A constant in $x is checked against inequalities using constants.
     (local $x i32)
     (local.set $x
       (i32.const 42)

From f708a61ce1b2e7e549249497b038f5e8fa76fa85 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 13:49:44 -0700
Subject: [PATCH 06/89] work

---
 src/ir/constraint.cpp                    | 12 ++++++-
 test/lit/passes/constraint-analysis.wast | 46 ++++++++++++++++++++++++
 2 files changed, 57 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 7366a7645b5..72c0d125803 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -32,7 +32,8 @@ Result TrueFalse(Literal x) { return TrueFalse(x.getUnsigned()); }
 Result provesConstantPair(Abstract::Op aOp,
                           const Literal& aConstant,
                           Abstract::Op bOp,
-                          const Literal& bConstant) {
+                          const Literal& bConstant,
+                          bool recursing=false) {
   // a == A =?=> a op B. Simply apply A to the operation against B.
   if (aOp == Abstract::Eq) {
     switch (bOp) {
@@ -75,6 +76,15 @@ Result provesConstantPair(Abstract::Op aOp,
     }
   }
 
+  if (!recursing) {
+    // The flipped operation may tell us something:  y ==> !x  implies
+    // x ==> y  is false (because if not, then x would prove y, and y would
+    // prove !x, a contradiction).
+    if (provesConstantPair(bOp, bConstant, aOp, aConstant, true) == False) {
+      return False;
+    }
+  }
+
   // TODO: handle all the rest of >, >=, <, and <=
   return Unknown;
 }
diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index f8c9af32993..35d3b003c8d 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -4461,4 +4461,50 @@
       )
     )
   )
+
+  ;; CHECK:      (func $flipped-contradiction (type $9) (result i32)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (loop $loop
+  ;; CHECK-NEXT:   (br_if $loop
+  ;; CHECK-NEXT:    (i32.const 1)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (br_if $loop
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (unreachable)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $flipped-contradiction (type $9) (result i32)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (loop $loop
+  ;; OPTIN-NEXT:   (br_if $loop
+  ;; OPTIN-NEXT:    (i32.const 1)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (br_if $loop
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (unreachable)
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $flipped-contradiction (result i32)
+    (local $x i32)
+    (loop $loop (result i32)
+      ;; If we do not branch, we add the constraint x >= 1.
+      (br_if $loop
+        (i32.lt_u
+          (local.get $x)
+          (i32.const 1)
+        )
+      )
+      ;; If we do not branch, we add the constraint x == 0. This contradicts the
+      ;; one before, making the code after us unreachable.
+      (br_if $loop
+        (local.get $x)
+      )
+      ;; An eqz that will become unreachable.
+      (i32.eqz
+        (i32.const 0)
+      )
+    )
+  )
 )

From d00bed6d8460d6a77809b369533f6303519a4712 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 13:50:39 -0700
Subject: [PATCH 07/89] work

---
 src/ir/constraint.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 72c0d125803..78cad40f2bb 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -33,7 +33,7 @@ Result provesConstantPair(Abstract::Op aOp,
                           const Literal& aConstant,
                           Abstract::Op bOp,
                           const Literal& bConstant,
-                          bool recursing=false) {
+                          bool recursing = false) {
   // a == A =?=> a op B. Simply apply A to the operation against B.
   if (aOp == Abstract::Eq) {
     switch (bOp) {

From e58adf7e4db3731fe544fd2462862a043d7726e8 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Tue, 21 Jul 2026 13:52:28 -0700
Subject: [PATCH 08/89] work

---
 test/lit/passes/constraint-analysis.wast | 64 +++++++++++++++++++++---
 1 file changed, 56 insertions(+), 8 deletions(-)

diff --git a/test/lit/passes/constraint-analysis.wast b/test/lit/passes/constraint-analysis.wast
index 35d3b003c8d..0f9a7f02d90 100644
--- a/test/lit/passes/constraint-analysis.wast
+++ b/test/lit/passes/constraint-analysis.wast
@@ -2854,7 +2854,7 @@
     )
   )
 
-  ;; CHECK:      (func $local-changes-if (type $6) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; CHECK:      (func $local-changes-if (type $7) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
   ;; CHECK-NEXT:  (if
   ;; CHECK-NEXT:   (i32.eq
   ;; CHECK-NEXT:    (local.get $x)
@@ -2911,7 +2911,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $local-changes-if (type $6) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
+  ;; OPTIN:      (func $local-changes-if (type $7) (param $x i32) (param $y i32) (param $z i32) (param $w i32)
   ;; OPTIN-NEXT:  (if
   ;; OPTIN-NEXT:   (i32.eq
   ;; OPTIN-NEXT:    (local.get $x)
@@ -3547,7 +3547,7 @@
     )
   )
 
-  ;; CHECK:      (func $simple-array-sum (type $7) (param $param (ref $array)) (result i32)
+  ;; CHECK:      (func $simple-array-sum (type $8) (param $param (ref $array)) (result i32)
   ;; CHECK-NEXT:  (local $index i32)
   ;; CHECK-NEXT:  (local $sum i32)
   ;; CHECK-NEXT:  (local $len i32)
@@ -3592,7 +3592,7 @@
   ;; CHECK-NEXT:   (br $loop)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $simple-array-sum (type $7) (param $param (ref $array)) (result i32)
+  ;; OPTIN:      (func $simple-array-sum (type $8) (param $param (ref $array)) (result i32)
   ;; OPTIN-NEXT:  (local $index i32)
   ;; OPTIN-NEXT:  (local $sum i32)
   ;; OPTIN-NEXT:  (local $len i32)
@@ -3767,7 +3767,7 @@
     )
   )
 
-  ;; CHECK:      (func $iloop (type $8) (param $0 f32)
+  ;; CHECK:      (func $iloop (type $9) (param $0 f32)
   ;; CHECK-NEXT:  (local $1 f32)
   ;; CHECK-NEXT:  (local.set $0
   ;; CHECK-NEXT:   (local.get $1)
@@ -3792,7 +3792,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $iloop (type $8) (param $0 f32)
+  ;; OPTIN:      (func $iloop (type $9) (param $0 f32)
   ;; OPTIN-NEXT:  (local $1 f32)
   ;; OPTIN-NEXT:  (local.set $0
   ;; OPTIN-NEXT:   (local.get $1)
@@ -4462,7 +4462,7 @@
     )
   )
 
-  ;; CHECK:      (func $flipped-contradiction (type $9) (result i32)
+  ;; CHECK:      (func $flipped-contradiction (type $6) (result i32)
   ;; CHECK-NEXT:  (local $x i32)
   ;; CHECK-NEXT:  (loop $loop
   ;; CHECK-NEXT:   (br_if $loop
@@ -4474,7 +4474,7 @@
   ;; CHECK-NEXT:   (unreachable)
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  ;; OPTIN:      (func $flipped-contradiction (type $9) (result i32)
+  ;; OPTIN:      (func $flipped-contradiction (type $6) (result i32)
   ;; OPTIN-NEXT:  (local $x i32)
   ;; OPTIN-NEXT:  (loop $loop
   ;; OPTIN-NEXT:   (br_if $loop
@@ -4507,4 +4507,52 @@
       )
     )
   )
+
+  ;; CHECK:      (func $flipped-contradiction-no (type $6) (result i32)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (loop $loop (result i32)
+  ;; CHECK-NEXT:   (br_if $loop
+  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (br_if $loop
+  ;; CHECK-NEXT:    (local.get $x)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (i32.eqz
+  ;; CHECK-NEXT:    (i32.const 0)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  ;; OPTIN:      (func $flipped-contradiction-no (type $6) (result i32)
+  ;; OPTIN-NEXT:  (local $x i32)
+  ;; OPTIN-NEXT:  (loop $loop (result i32)
+  ;; OPTIN-NEXT:   (br_if $loop
+  ;; OPTIN-NEXT:    (i32.const 0)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (br_if $loop
+  ;; OPTIN-NEXT:    (local.get $x)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:   (i32.eqz
+  ;; OPTIN-NEXT:    (i32.const 0)
+  ;; OPTIN-NEXT:   )
+  ;; OPTIN-NEXT:  )
+  ;; OPTIN-NEXT: )
+  (func $flipped-contradiction-no (result i32)
+    ;; As above, but with lt replaced by gt. Now the constraints are x <= 1 and
+    ;; x == 0, which do not contradict, and nothing becomes unreachable.
+    (local $x i32)
+    (loop $loop (result i32)
+      (br_if $loop
+        (i32.gt_u
+          (local.get $x)
+          (i32.const 1)
+        )
+      )
+      (br_if $loop
+        (local.get $x)
+      )
+      (i32.eqz
+        (i32.const 0)
+      )
+    )
+  )
 )

From d9f1f87a6c4960f105f480e8234820b4643304ef Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 22 Jul 2026 09:12:32 -0700
Subject: [PATCH 09/89] test

---
 .../lit/passes/constraint-analysis-loops.wast | 50 +++++++++++++++++++
 1 file changed, 50 insertions(+)
 create mode 100644 test/lit/passes/constraint-analysis-loops.wast

diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
new file mode 100644
index 00000000000..7b6f84bc1aa
--- /dev/null
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -0,0 +1,50 @@
+;; NOTE: Assertions have been generated by update_lit_checks.py and should not be edited.
+
+;; RUN: wasm-opt %s --constraint-analysis -all -S -o - | filecheck %s
+
+(module
+  (import "a" "b" (func $import (result i32)))
+
+  (func $bound
+    (local $x i32)
+    (loop $loop
+      ;; We arrive at the loop top with {x == 0} or {x > 0 && x <= 100}. Those
+      ;; OR into {x >= 0 && x <= 100} - that is, the x == 0 and x > 0 combine
+      ;; into x >= 0.
+      (drop
+        (i32.ge_s
+          (local.get $x)
+          (i32.const 0)
+        )
+      )
+      (drop
+        (i32.le_s
+          (local.get $x)
+          (i32.const 100)
+        )
+      )
+      ;; Set $x to an unknown value before applying the constraints below on the
+      ;; way back to the loop top.
+      (local.set $x
+        (call $import)
+      )
+      (if
+        (i32.gt_s
+          (local.get $x)
+          (i32.const 0)
+        )
+        (then
+          (if
+            (i32.le_s
+              (local.get $x)
+              (i32.const 100)
+            )
+            (then
+              (br $loop)
+            )
+          )
+        )
+      )
+    )
+  )
+)

From 1617154812ffae1a234cebfc242320bcbf5469ac Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 22 Jul 2026 09:12:50 -0700
Subject: [PATCH 10/89] work

---
 .../lit/passes/constraint-analysis-loops.wast | 38 +++++++++++++++++++
 1 file changed, 38 insertions(+)

diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
index 7b6f84bc1aa..18dec2613b0 100644
--- a/test/lit/passes/constraint-analysis-loops.wast
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -3,8 +3,46 @@
 ;; RUN: wasm-opt %s --constraint-analysis -all -S -o - | filecheck %s
 
 (module
+  ;; CHECK:      (import "a" "b" (func $import (type $0) (result i32)))
   (import "a" "b" (func $import (result i32)))
 
+  ;; CHECK:      (func $bound (type $1)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (loop $loop
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.ge_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.le_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 100)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (local.set $x
+  ;; CHECK-NEXT:    (call $import)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (if
+  ;; CHECK-NEXT:    (i32.gt_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (then
+  ;; CHECK-NEXT:     (if
+  ;; CHECK-NEXT:      (i32.le_s
+  ;; CHECK-NEXT:       (local.get $x)
+  ;; CHECK-NEXT:       (i32.const 100)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (then
+  ;; CHECK-NEXT:       (br $loop)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
   (func $bound
     (local $x i32)
     (loop $loop

From 0da07408f643edb131f6bd2f5c92a5a36ff8f994 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 22 Jul 2026 09:14:47 -0700
Subject: [PATCH 11/89] work

---
 .../lit/passes/constraint-analysis-loops.wast | 80 ++++++++++++++++++-
 1 file changed, 78 insertions(+), 2 deletions(-)

diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
index 18dec2613b0..4277bdbc2ea 100644
--- a/test/lit/passes/constraint-analysis-loops.wast
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -3,10 +3,10 @@
 ;; RUN: wasm-opt %s --constraint-analysis -all -S -o - | filecheck %s
 
 (module
-  ;; CHECK:      (import "a" "b" (func $import (type $0) (result i32)))
+  ;; CHECK:      (import "a" "b" (func $import (type $1) (result i32)))
   (import "a" "b" (func $import (result i32)))
 
-  ;; CHECK:      (func $bound (type $1)
+  ;; CHECK:      (func $bound (type $0)
   ;; CHECK-NEXT:  (local $x i32)
   ;; CHECK-NEXT:  (loop $loop
   ;; CHECK-NEXT:   (drop
@@ -85,4 +85,80 @@
       )
     )
   )
+
+  ;; CHECK:      (func $bound-flipped (type $0)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (loop $loop
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.ge_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.le_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 100)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (local.set $x
+  ;; CHECK-NEXT:    (call $import)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (if
+  ;; CHECK-NEXT:    (i32.le_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 100)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (then
+  ;; CHECK-NEXT:     (if
+  ;; CHECK-NEXT:      (i32.gt_s
+  ;; CHECK-NEXT:       (local.get $x)
+  ;; CHECK-NEXT:       (i32.const 0)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (then
+  ;; CHECK-NEXT:       (br $loop)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  (func $bound-flipped
+    (local $x i32)
+    ;; As above, but with the ifs flipped. We optimize the same way.
+    (loop $loop
+      (drop
+        (i32.ge_s
+          (local.get $x)
+          (i32.const 0)
+        )
+      )
+      (drop
+        (i32.le_s
+          (local.get $x)
+          (i32.const 100)
+        )
+      )
+      (local.set $x
+        (call $import)
+      )
+      (if
+        (i32.le_s
+          (local.get $x)
+          (i32.const 100)
+        )
+        (then
+          (if
+            (i32.gt_s
+              (local.get $x)
+              (i32.const 0)
+            )
+            (then
+              (br $loop)
+            )
+          )
+        )
+      )
+    )
+  )
 )

From e793be34154c2093a69d28b6dba4be692fa64caf Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 22 Jul 2026 09:23:10 -0700
Subject: [PATCH 12/89] work

---
 src/ir/constraint.cpp | 28 +++++++++++++++++++++++++---
 1 file changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 78cad40f2bb..e2599f4520a 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -205,6 +205,21 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) {
   //       useful to implement that).
 }
 
+namespace {
+
+// Do an approximate OR on two inputs that are incompatible, that is, that each
+// proves the other false. Such disjoint cases are sometimes simple to handle.
+//
+// If we recognize a pattern, we update |self| and return whether anything
+// changed (otherwise, we return nullopt).
+std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
+                                          const AndedConstraintSet& other) {
+  // Otherwise, we have no idea.
+  return {};
+}
+
+} // anonymous namespace
+
 bool AndedConstraintSet::approximateOr(const AndedConstraintSet& other) {
   // If one proves everything, the only thing that matters is the other.
   if (other.provesEverything()) {
@@ -218,15 +233,22 @@ bool AndedConstraintSet::approximateOr(const AndedConstraintSet& other) {
   // If this is already implied by current constraints, then it is redundant.
   // E.g. if we are { x = 10 } and other is { x >= 0 } then all we need is
   // { x >= 0 } as the result of the OR.
-  if (other.proves(*this) == True) {
+  auto otherProves = other.proves(*this);
+  if (otherProves == True) {
     return false;
   }
-  if (proves(other) == True) {
+  auto thisProves = proves(other);
+  if (thisProves == True) {
     *this = other;
     return true;
   }
 
-  // TODO smarts: handle <= > and so forth
+  if (otherProves == False && thisProves == False) {
+    if (auto result = approximateOrDisjoint(*this, other)) {
+      return *result;
+    }
+  }
+  // TODO more 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.

From e508ca69660a469dddaf1f4681438f183ee528ae Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 22 Jul 2026 09:28:06 -0700
Subject: [PATCH 13/89] work

---
 src/ir/constraint.cpp                          | 7 +++++++
 test/lit/passes/constraint-analysis-loops.wast | 8 +++++---
 2 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index e2599f4520a..ec6b20793a6 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -214,6 +214,13 @@ namespace {
 // changed (otherwise, we return nullopt).
 std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
                                           const AndedConstraintSet& other) {
+  // Simple range fusing, add a constant to turn > into >=:
+  //
+  //   { x == C } || { x > C && x <= D }  ===  { x >= C && x <= D }
+  //
+  // (note that we don't need to care about D: if the inequalities did not
+  // describe a contradiction before, they do not do so after, either)
+
   // Otherwise, we have no idea.
   return {};
 }
diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
index 4277bdbc2ea..0072ba7b1e0 100644
--- a/test/lit/passes/constraint-analysis-loops.wast
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -46,7 +46,7 @@
   (func $bound
     (local $x i32)
     (loop $loop
-      ;; We arrive at the loop top with {x == 0} or {x > 0 && x <= 100}. Those
+      ;; We arrive at the loop top with {x == 0} || {x > 0 && x <= 100}. Those
       ;; OR into {x >= 0 && x <= 100} - that is, the x == 0 and x > 0 combine
       ;; into x >= 0.
       (drop
@@ -123,7 +123,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  (func $bound-flipped
+  (;;func $bound-flipped
     (local $x i32)
     ;; As above, but with the ifs flipped. We optimize the same way.
     (loop $loop
@@ -160,5 +160,7 @@
         )
       )
     )
-  )
+  ;;)
+  ;; TODO: unsigned
+  ;; TODO: non-zero
 )

From 48ee24c1848df9a7225971fa106155eae3edf531 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Wed, 22 Jul 2026 09:58:11 -0700
Subject: [PATCH 14/89] work

---
 src/ir/constraint.cpp | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index ec6b20793a6..7c890265324 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -207,19 +207,19 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) {
 
 namespace {
 
-// Do an approximate OR on two inputs that are incompatible, that is, that each
-// proves the other false. Such disjoint cases are sometimes simple to handle.
+// Do an approximate OR on two inputs that are disjoint, that is, each proves
+// the other false.
 //
 // If we recognize a pattern, we update |self| and return whether anything
 // changed (otherwise, we return nullopt).
 std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
                                           const AndedConstraintSet& other) {
-  // Simple range fusing, add a constant to turn > into >=:
+  // Simple range fusing, add an equality to turn > into >=:
   //
-  //   { x == C } || { x > C && x <= D }  ===  { x >= C && x <= D }
+  //   x == A || x > X   ===   x >= A
   //
-  // (note that we don't need to care about D: if the inequalities did not
-  // describe a contradiction before, they do not do so after, either)
+  Var A;
+  if (match(set(self, Abstract::Eq, A), set(other, Abstract::GtS, A),
 
   // Otherwise, we have no idea.
   return {};

From b31d7f9028ec6b62b3382fe0699a4b8d2a438887 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 09:36:26 -0700
Subject: [PATCH 15/89] work

---
 src/ir/constraint.cpp | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 7c890265324..4849ffd9492 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -214,12 +214,17 @@ namespace {
 // changed (otherwise, we return nullopt).
 std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
                                           const AndedConstraintSet& other) {
-  // Simple range fusing, add an equality to turn > into >=:
+  // Simple range fusing, add an equality to turn > into >= :
   //
-  //   x == A || x > X   ===   x >= A
+  //   { x == A } || { x > A && x <= B } , A <= B   ===   { x >= A && X <= B }
   //
-  Var A;
-  if (match(set(self, Abstract::Eq, A), set(other, Abstract::GtS, A),
+  // XXX but we do need the other part of other, x < B and A < B
+  Var A, B;
+  if (match().set(self, Abstract::Eq, A)
+             .set(other, Abstract::GtS, A, Abstract::LeS, B)
+             .require(A, LeS, B)) {
+    flipped? look for both and flipped, and return pointer to the first .set()?
+  }
 
   // Otherwise, we have no idea.
   return {};
@@ -259,6 +264,9 @@ bool AndedConstraintSet::approximateOr(const AndedConstraintSet& other) {
 
   // Otherwise, we don't know how to nicely OR these things, and expand to the
   // trivial set of no constraints.
+  // TODO: We could keep constraints that appear on both sides and only drop the
+  //       others. In fact, we could do that first, and leave smarts only to the
+  //       others.
   clear();
   return true;
 }

From f0dd6c8f32845e452585477fedb39f29c21e1f04 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 09:53:03 -0700
Subject: [PATCH 16/89] work

---
 src/ir/constraint.cpp | 37 ++++++++++++++++++++++++++++++++++---
 1 file changed, 34 insertions(+), 3 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 4849ffd9492..1c5bf0870c9 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -207,6 +207,36 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) {
 
 namespace {
 
+// A variable in a match. If we see the same Var - identified by address - in
+// two places, it must be equal in them. We can also perform checks on different
+// Vars afterwards, e.g., whether one is greater than the other.
+struct Var {};
+
+// A match constraint: an abstraction over a normal Constraint, which can also
+// contain Vars.
+struct MC {
+  Abstract::Op op;
+  Var& term;
+};
+
+// A matcher object. This pattern-matches over AndedConstraintSets, in a way
+// that follows the rules of logic.
+struct Match {
+  // Add a set of constraints that contains one item. For convenience, this uses
+  // the builder pattern, i.e. it returns this Match object.
+  Match& set(MC& mc);
+
+  // Add above, but now the set contains two items, both provided here.
+  Match& set(MC& mc1, MC& mc2);
+
+  // Add a requirement on this pattern, a demand on the Vars.
+  Match& require(Var& a, Abstract::Op, Var& b);
+
+  // Check if the pattern matches given inputs. The order of the inputs does not
+  // matter.
+  bool checkUnordered(const AndedConstraintSets& a, const AndedConstraintSets& constraints b);
+};
+
 // Do an approximate OR on two inputs that are disjoint, that is, each proves
 // the other false.
 //
@@ -220,9 +250,10 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //
   // XXX but we do need the other part of other, x < B and A < B
   Var A, B;
-  if (match().set(self, Abstract::Eq, A)
-             .set(other, Abstract::GtS, A, Abstract::LeS, B)
-             .require(A, LeS, B)) {
+  if (Match().set(MC(Abstract::Eq, A))
+             .set(MC(Abstract::GtS, A), MC(Abstract::LeS, B))
+             .require(A, LeS, B)
+             .check(self, other)) {
     flipped? look for both and flipped, and return pointer to the first .set()?
   }
 

From cf8f32e2a7cfef6695250e31d76a43605055ad2c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:08:37 -0700
Subject: [PATCH 17/89] work

---
 src/ir/constraint.cpp | 51 ++++++++++++++++++++++++++++---------------
 1 file changed, 34 insertions(+), 17 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 1c5bf0870c9..bfe43caa714 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -212,31 +212,47 @@ namespace {
 // Vars afterwards, e.g., whether one is greater than the other.
 struct Var {};
 
-// A match constraint: an abstraction over a normal Constraint, which can also
+// A matcher constraint: an abstraction over a normal Constraint, which can also
 // contain Vars.
-struct MC {
+struct MatcherConstraint {
   Abstract::Op op;
   Var& term;
 };
 
+// A matcher AndedConstraintSet, which abstracts over the normal one to support
+// MatcherConstraints.
+using MatcherSet = public inplace_vector<MatcherConstraint, MaxConstraints>;
+
 // A matcher object. This pattern-matches over AndedConstraintSets, in a way
 // that follows the rules of logic.
-struct Match {
-  // Add a set of constraints that contains one item. For convenience, this uses
-  // the builder pattern, i.e. it returns this Match object.
-  Match& set(MC& mc);
-
-  // Add above, but now the set contains two items, both provided here.
-  Match& set(MC& mc1, MC& mc2);
+struct Matcher {
+  // Set up a pattern containing two sets of constraints.
+  Matcher(const MatcherSet& ms1, const MatcherSet& ms2) 
 
   // Add a requirement on this pattern, a demand on the Vars.
-  Match& require(Var& a, Abstract::Op, Var& b);
+  //
+  // For convenience, return this Matcher object (i.e. the builder pattern).
+  Matcher& require(Var& a, Abstract::Op, Var& b);
 
   // Check if the pattern matches given inputs. The order of the inputs does not
   // matter.
-  bool checkUnordered(const AndedConstraintSets& a, const AndedConstraintSets& constraints b);
+  bool checkUnordered(const AndedConstraintSets& a, const AndedConstraintSets& constraints b) {
+    return checkUnorderedInternal(a, b);
+  }
+
+private:
+  bool checkUnorderedInternal(const AndedConstraintSets& a, const AndedConstraintSets& constraints b, bool flipped = false);
 };
 
+Matcher::Matcher(const MatcherSet& ms1, const MatcherSet& ms2) {
+}
+
+Matcher& Matcher::require(Var& a, Abstract::Op, Var& b) {
+}
+
+bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedConstraintSets& constraints b, bool flipped {
+}
+
 // Do an approximate OR on two inputs that are disjoint, that is, each proves
 // the other false.
 //
@@ -244,17 +260,18 @@ struct Match {
 // changed (otherwise, we return nullopt).
 std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
                                           const AndedConstraintSet& other) {
+  using M = Matcher;
+  using MC = MatcherConstraint;
+
   // Simple range fusing, add an equality to turn > into >= :
   //
   //   { x == A } || { x > A && x <= B } , A <= B   ===   { x >= A && X <= B }
   //
-  // XXX but we do need the other part of other, x < B and A < B
   Var A, B;
-  if (Match().set(MC(Abstract::Eq, A))
-             .set(MC(Abstract::GtS, A), MC(Abstract::LeS, B))
-             .require(A, LeS, B)
-             .check(self, other)) {
-    flipped? look for both and flipped, and return pointer to the first .set()?
+  if (M().set(MC(Abstract::Eq, A))
+               .set(MC(Abstract::GtS, A), MC(Abstract::LeS, B))
+               .require(A, LeS, B)
+               .check(self, other)) {
   }
 
   // Otherwise, we have no idea.

From f6b58b4c3a06d503562e101bd03f4f3f3d7c27f0 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:11:25 -0700
Subject: [PATCH 18/89] work

---
 src/ir/constraint.cpp | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index bfe43caa714..cfcd6c01290 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -227,12 +227,12 @@ using MatcherSet = public inplace_vector<MatcherConstraint, MaxConstraints>;
 // that follows the rules of logic.
 struct Matcher {
   // Set up a pattern containing two sets of constraints.
-  Matcher(const MatcherSet& ms1, const MatcherSet& ms2) 
+  Matcher(const MatcherSet& ms1, const MatcherSet& ms2);
 
   // Add a requirement on this pattern, a demand on the Vars.
   //
   // For convenience, return this Matcher object (i.e. the builder pattern).
-  Matcher& require(Var& a, Abstract::Op, Var& b);
+  Matcher& require(Var& a, Abstract::Op op, Var& b);
 
   // Check if the pattern matches given inputs. The order of the inputs does not
   // matter.
@@ -242,12 +242,24 @@ struct Matcher {
 
 private:
   bool checkUnorderedInternal(const AndedConstraintSets& a, const AndedConstraintSets& constraints b, bool flipped = false);
+
+  const MatcherSet& ms1;
+  const MatcherSet& ms2;
+
+  struct Requirement {
+    Var& a;
+    Abstract::Op op;
+    Var& b;
+  };
+
+  SmallVector<Requirement, 2> requirements;
 };
 
-Matcher::Matcher(const MatcherSet& ms1, const MatcherSet& ms2) {
+Matcher::Matcher(const MatcherSet& ms1, const MatcherSet& ms2) : ms1(ms1), ms2(ms2) {
 }
 
-Matcher& Matcher::require(Var& a, Abstract::Op, Var& b) {
+Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
+  requirements.push_back({a, op, b});
 }
 
 bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedConstraintSets& constraints b, bool flipped {

From 60e9620b4a204a89c6d28b6263ee02d9178d5c27 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:13:28 -0700
Subject: [PATCH 19/89] work

---
 src/ir/constraint.cpp | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index cfcd6c01290..d77d4a99bd5 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -262,7 +262,15 @@ Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
   requirements.push_back({a, op, b});
 }
 
-bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedConstraintSets& constraints b, bool flipped {
+bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedConstraintSets& constraints b, bool flipped) {
+
+
+  // Perhaps the flipped inputs match, if we didn't already try that.
+  if (!flipped) {
+    return checkUnorderedInternal(b, a, true);
+  }
+
+  return false;
 }
 
 // Do an approximate OR on two inputs that are disjoint, that is, each proves

From a4fc9e9166726bb768912fe710841e6f1ba20349 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:21:13 -0700
Subject: [PATCH 20/89] work

---
 src/ir/constraint.cpp | 43 ++++++++++++++++++++++++++++++++++++-------
 1 file changed, 36 insertions(+), 7 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index d77d4a99bd5..83f43a3ba4e 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -210,6 +210,7 @@ namespace {
 // A variable in a match. If we see the same Var - identified by address - in
 // two places, it must be equal in them. We can also perform checks on different
 // Vars afterwards, e.g., whether one is greater than the other.
+// TODO: optimize all this, if it matters
 struct Var {};
 
 // A matcher constraint: an abstraction over a normal Constraint, which can also
@@ -263,14 +264,42 @@ Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
 }
 
 bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedConstraintSets& constraints b, bool flipped) {
+  auto returnFalse = [&]() {
+    // Before returning false, see if the flipped inputs match, if we didn't
+    // already try that.
+    if (!flipped) {
+      return checkUnorderedInternal(b, a, true);
+    }
+    return false;
+  };
 
+  if (a.size() != ms1.size() || b.size() != ms2.size()) {
+    return returnFalse();
+  }
 
-  // Perhaps the flipped inputs match, if we didn't already try that.
-  if (!flipped) {
-    return checkUnorderedInternal(b, a, true);
+  // The sizes match, at least. Parse in more detail, building up a mapping of
+  // Vars to concrete Terms.
+  std::unordered_map<Var*, Term> varTermMap;
+
+  auto parse = [&](const AndedConstraintSet& input, const MatcherSet& pattern) {
+    for (Index i = 0; i < input.size(); i++) {
+      if (input[i].op != pattern[i].op) {
+        return false;
+      }
+
+      
+    }
+    return true;
+  };
+
+  if (!parse(a, ms1) || !parse(b, ms2)) {
+    return returnFalse();
   }
 
-  return false;
+  // Check requirements on the vars.
+  ..
+
+  return returnFalse();
 }
 
 // Do an approximate OR on two inputs that are disjoint, that is, each proves
@@ -289,9 +318,9 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //
   Var A, B;
   if (M().set(MC(Abstract::Eq, A))
-               .set(MC(Abstract::GtS, A), MC(Abstract::LeS, B))
-               .require(A, LeS, B)
-               .check(self, other)) {
+         .set(MC(Abstract::GtS, A), MC(Abstract::LeS, B))
+         .require(A, LeS, B)
+         .check(self, other)) {
   }
 
   // Otherwise, we have no idea.

From 7d337dc7456e7e5df8dba057e327c7efee982a00 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:25:02 -0700
Subject: [PATCH 21/89] work

---
 src/ir/constraint.cpp | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 83f43a3ba4e..9340031306b 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -287,7 +287,17 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedCo
         return false;
       }
 
-      
+      if (auto iter = varTermMap.find(&pattern.term);
+          iter != varTermMap.end()) {
+        // The Var in the pattern is already mapped and known. The input here
+        // must match the prior appearance.
+        if (input[i].term != iter->second) {
+          return false;
+        }
+      } else {
+        // This is a new Var.
+        varTermMap[&pattern.term] = input[i].term;
+      }
     }
     return true;
   };

From fb0786970b38cc45d10fd545339af6e222e7227f Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:29:25 -0700
Subject: [PATCH 22/89] work

---
 src/ir/constraint.cpp | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 9340031306b..606548152df 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -278,25 +278,24 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedCo
   }
 
   // The sizes match, at least. Parse in more detail, building up a mapping of
-  // Vars to concrete Terms.
+  // Vars to concrete Terms
   std::unordered_map<Var*, Term> varTermMap;
 
   auto parse = [&](const AndedConstraintSet& input, const MatcherSet& pattern) {
     for (Index i = 0; i < input.size(); i++) {
+      // The operation must match.
       if (input[i].op != pattern[i].op) {
         return false;
       }
 
-      if (auto iter = varTermMap.find(&pattern.term);
-          iter != varTermMap.end()) {
+      // The term must match, or define a new unknown value.
+      auto [iter, inserted] = varTermMap.insert({&pattern.term, input[i].term});
+      if (inserted) {
         // The Var in the pattern is already mapped and known. The input here
         // must match the prior appearance.
         if (input[i].term != iter->second) {
           return false;
         }
-      } else {
-        // This is a new Var.
-        varTermMap[&pattern.term] = input[i].term;
       }
     }
     return true;

From 023cb402fa989e4676984c5fb634601b18b99d1e Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:32:34 -0700
Subject: [PATCH 23/89] work

---
 src/ir/constraint.cpp | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 606548152df..18ba9fd3525 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -248,9 +248,9 @@ struct Matcher {
   const MatcherSet& ms2;
 
   struct Requirement {
-    Var& a;
+    Var* a;
     Abstract::Op op;
-    Var& b;
+    Var* b;
   };
 
   SmallVector<Requirement, 2> requirements;
@@ -260,7 +260,7 @@ Matcher::Matcher(const MatcherSet& ms1, const MatcherSet& ms2) : ms1(ms1), ms2(m
 }
 
 Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
-  requirements.push_back({a, op, b});
+  requirements.push_back({&a, op, &b});
 }
 
 bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedConstraintSets& constraints b, bool flipped) {
@@ -306,7 +306,12 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedCo
   }
 
   // Check requirements on the vars.
-  ..
+  for (auto& [a, op, b] : requirements) {
+    auto aTerm = varTermMap[a];
+    auto bTerm = varTermMap[b];
+
+    if (provesPair(const Constraint& a, const Constraint& b) {
+  }
 
   return returnFalse();
 }

From 6268c82480c8ee042bb5dc6172602560b18d1054 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:34:31 -0700
Subject: [PATCH 24/89] work

---
 src/ir/constraint.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 18ba9fd3525..cd037437bcc 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -310,7 +310,10 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedCo
     auto aTerm = varTermMap[a];
     auto bTerm = varTermMap[b];
 
-    if (provesPair(const Constraint& a, const Constraint& b) {
+    // Check if { x == a } proves { x op b } is true.
+    if (provesPair(Constraint{Abstract::Eq, aTerm}, Constraint{op, bTerm}) != True) {
+      return returnFalse();
+    }
   }
 
   return returnFalse();

From f15411c2e84dfef6aad30c0cef3ea99c0d24e7d1 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:34:40 -0700
Subject: [PATCH 25/89] work

---
 src/ir/constraint.cpp | 27 +++++++++++++++++----------
 1 file changed, 17 insertions(+), 10 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index cd037437bcc..90d487442e8 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -237,12 +237,15 @@ struct Matcher {
 
   // Check if the pattern matches given inputs. The order of the inputs does not
   // matter.
-  bool checkUnordered(const AndedConstraintSets& a, const AndedConstraintSets& constraints b) {
+  bool checkUnordered(const AndedConstraintSets& a,
+                      const AndedConstraintSets& constraints b) {
     return checkUnorderedInternal(a, b);
   }
 
 private:
-  bool checkUnorderedInternal(const AndedConstraintSets& a, const AndedConstraintSets& constraints b, bool flipped = false);
+  bool checkUnorderedInternal(const AndedConstraintSets& a,
+                              const AndedConstraintSets& constraints b,
+                              bool flipped = false);
 
   const MatcherSet& ms1;
   const MatcherSet& ms2;
@@ -256,14 +259,16 @@ struct Matcher {
   SmallVector<Requirement, 2> requirements;
 };
 
-Matcher::Matcher(const MatcherSet& ms1, const MatcherSet& ms2) : ms1(ms1), ms2(ms2) {
-}
+Matcher::Matcher(const MatcherSet& ms1, const MatcherSet& ms2)
+  : ms1(ms1), ms2(ms2) {}
 
 Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
   requirements.push_back({&a, op, &b});
 }
 
-bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedConstraintSets& constraints b, bool flipped) {
+bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a,
+                                     const AndedConstraintSets& constraints b,
+                                     bool flipped) {
   auto returnFalse = [&]() {
     // Before returning false, see if the flipped inputs match, if we didn't
     // already try that.
@@ -311,7 +316,8 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a, const AndedCo
     auto bTerm = varTermMap[b];
 
     // Check if { x == a } proves { x op b } is true.
-    if (provesPair(Constraint{Abstract::Eq, aTerm}, Constraint{op, bTerm}) != True) {
+    if (provesPair(Constraint{Abstract::Eq, aTerm}, Constraint{op, bTerm}) !=
+        True) {
       return returnFalse();
     }
   }
@@ -334,10 +340,11 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //   { x == A } || { x > A && x <= B } , A <= B   ===   { x >= A && X <= B }
   //
   Var A, B;
-  if (M().set(MC(Abstract::Eq, A))
-         .set(MC(Abstract::GtS, A), MC(Abstract::LeS, B))
-         .require(A, LeS, B)
-         .check(self, other)) {
+  if (M()
+        .set(MC(Abstract::Eq, A))
+        .set(MC(Abstract::GtS, A), MC(Abstract::LeS, B))
+        .require(A, LeS, B)
+        .check(self, other)) {
   }
 
   // Otherwise, we have no idea.

From fd6101074b240e524397ced637dc819e5921804c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:36:50 -0700
Subject: [PATCH 26/89] work

---
 src/ir/constraint.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 90d487442e8..5f2f6e4a349 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -334,6 +334,7 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
                                           const AndedConstraintSet& other) {
   using M = Matcher;
   using MC = MatcherConstraint;
+  using namespace Abstract;
 
   // Simple range fusing, add an equality to turn > into >= :
   //
@@ -341,8 +342,8 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //
   Var A, B;
   if (M()
-        .set(MC(Abstract::Eq, A))
-        .set(MC(Abstract::GtS, A), MC(Abstract::LeS, B))
+        .set(MC(Eq, A))
+        .set(MC(GtS, A), MC(LeS, B))
         .require(A, LeS, B)
         .check(self, other)) {
   }

From 9a7e163cf7f032b8c5cd17a03a5a13630608b080 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:38:58 -0700
Subject: [PATCH 27/89] work

---
 src/ir/constraint.cpp | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 5f2f6e4a349..0721d01d79f 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -222,7 +222,7 @@ struct MatcherConstraint {
 
 // A matcher AndedConstraintSet, which abstracts over the normal one to support
 // MatcherConstraints.
-using MatcherSet = public inplace_vector<MatcherConstraint, MaxConstraints>;
+using MatcherSet = inplace_vector<MatcherConstraint, MaxConstraints>;
 
 // A matcher object. This pattern-matches over AndedConstraintSets, in a way
 // that follows the rules of logic.
@@ -237,14 +237,14 @@ struct Matcher {
 
   // Check if the pattern matches given inputs. The order of the inputs does not
   // matter.
-  bool checkUnordered(const AndedConstraintSets& a,
-                      const AndedConstraintSets& constraints b) {
+  bool checkUnordered(const AndedConstraintSet& a,
+                      const AndedConstraintSet& b) {
     return checkUnorderedInternal(a, b);
   }
 
 private:
-  bool checkUnorderedInternal(const AndedConstraintSets& a,
-                              const AndedConstraintSets& constraints b,
+  bool checkUnorderedInternal(const AndedConstraintSet& a,
+                              const AndedConstraintSet& b,
                               bool flipped = false);
 
   const MatcherSet& ms1;
@@ -264,10 +264,11 @@ Matcher::Matcher(const MatcherSet& ms1, const MatcherSet& ms2)
 
 Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
   requirements.push_back({&a, op, &b});
+  return *this;
 }
 
-bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a,
-                                     const AndedConstraintSets& constraints b,
+bool Matcher::checkUnorderedInternal(const AndedConstraintSet& a,
+                                     const AndedConstraintSet& b,
                                      bool flipped) {
   auto returnFalse = [&]() {
     // Before returning false, see if the flipped inputs match, if we didn't
@@ -294,7 +295,7 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSets& a,
       }
 
       // The term must match, or define a new unknown value.
-      auto [iter, inserted] = varTermMap.insert({&pattern.term, input[i].term});
+      auto [iter, inserted] = varTermMap.insert({&pattern[i].term, input[i].term});
       if (inserted) {
         // The Var in the pattern is already mapped and known. The input here
         // must match the prior appearance.

From 9458a8a8ff58d4a9793063b35aea9d94e420a712 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:39:07 -0700
Subject: [PATCH 28/89] work

---
 src/ir/constraint.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 0721d01d79f..bdc7cfae912 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -295,7 +295,8 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSet& a,
       }
 
       // The term must match, or define a new unknown value.
-      auto [iter, inserted] = varTermMap.insert({&pattern[i].term, input[i].term});
+      auto [iter, inserted] =
+        varTermMap.insert({&pattern[i].term, input[i].term});
       if (inserted) {
         // The Var in the pattern is already mapped and known. The input here
         // must match the prior appearance.

From 0628af6960283b989ed43461aae59f6ee83736e0 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:39:50 -0700
Subject: [PATCH 29/89] work

---
 src/ir/constraint.cpp | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index bdc7cfae912..dae3b510ac3 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -343,9 +343,7 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //   { x == A } || { x > A && x <= B } , A <= B   ===   { x >= A && X <= B }
   //
   Var A, B;
-  if (M()
-        .set(MC(Eq, A))
-        .set(MC(GtS, A), MC(LeS, B))
+  if (M(MS(MC(Eq, A)), MS(MC(GtS, A), MC(LeS, B)))
         .require(A, LeS, B)
         .check(self, other)) {
   }

From 7e267baf14ba13144c570ee6eddc666f84acfe01 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:41:07 -0700
Subject: [PATCH 30/89] work

---
 src/ir/constraint.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index dae3b510ac3..c5e8e636ca9 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -334,8 +334,8 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSet& a,
 // changed (otherwise, we return nullopt).
 std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
                                           const AndedConstraintSet& other) {
-  using M = Matcher;
   using MC = MatcherConstraint;
+  using MS = MatcherSet;
   using namespace Abstract;
 
   // Simple range fusing, add an equality to turn > into >= :
@@ -343,7 +343,7 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //   { x == A } || { x > A && x <= B } , A <= B   ===   { x >= A && X <= B }
   //
   Var A, B;
-  if (M(MS(MC(Eq, A)), MS(MC(GtS, A), MC(LeS, B)))
+  if (Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)}) 
         .require(A, LeS, B)
         .check(self, other)) {
   }

From 71736fd439189cfd74b31c9df452d03047f63ca1 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:41:16 -0700
Subject: [PATCH 31/89] work

---
 src/ir/constraint.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index c5e8e636ca9..10ad4996aba 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -343,7 +343,7 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //   { x == A } || { x > A && x <= B } , A <= B   ===   { x >= A && X <= B }
   //
   Var A, B;
-  if (Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)}) 
+  if (Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
         .require(A, LeS, B)
         .check(self, other)) {
   }

From 859faa7e0af689cbfdc6fb985d17338992a97f5f Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:41:41 -0700
Subject: [PATCH 32/89] work

---
 src/ir/constraint.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 10ad4996aba..9abf2e9daa0 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -335,7 +335,6 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSet& a,
 std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
                                           const AndedConstraintSet& other) {
   using MC = MatcherConstraint;
-  using MS = MatcherSet;
   using namespace Abstract;
 
   // Simple range fusing, add an equality to turn > into >= :

From e72fa61b12e0b37530e32f0d15d2f86617918029 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:42:19 -0700
Subject: [PATCH 33/89] work

---
 src/ir/constraint.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 9abf2e9daa0..dc43a01dc7e 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -344,7 +344,8 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   Var A, B;
   if (Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
         .require(A, LeS, B)
-        .check(self, other)) {
+        .checkUnordered(self, other)) {
+    // ..
   }
 
   // Otherwise, we have no idea.

From ebcfa8066e517f76990fec6e752cc2089a58b126 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:43:01 -0700
Subject: [PATCH 34/89] work

---
 src/ir/constraint.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index dc43a01dc7e..0dcebefdcf5 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -217,7 +217,9 @@ struct Var {};
 // contain Vars.
 struct MatcherConstraint {
   Abstract::Op op;
-  Var& term;
+  Var* term;
+
+  MatcherConstraint(Abstract::Op op, Var& term) : op(op), term(&term) {}
 };
 
 // A matcher AndedConstraintSet, which abstracts over the normal one to support

From 8c76ee7c6a7f5ab82682b1d3fef313bd4882aa62 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:43:44 -0700
Subject: [PATCH 35/89] work

---
 src/ir/constraint.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 0dcebefdcf5..58c2cb486f3 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -298,7 +298,7 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSet& a,
 
       // The term must match, or define a new unknown value.
       auto [iter, inserted] =
-        varTermMap.insert({&pattern[i].term, input[i].term});
+        varTermMap.insert({pattern[i].term, input[i].term});
       if (inserted) {
         // The Var in the pattern is already mapped and known. The input here
         // must match the prior appearance.

From 65f7508c983b8147004ad371626f23e3e8daf988 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 11:46:13 -0700
Subject: [PATCH 36/89] work

---
 src/ir/constraint.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 58c2cb486f3..91c151a2434 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -217,8 +217,9 @@ struct Var {};
 // contain Vars.
 struct MatcherConstraint {
   Abstract::Op op;
-  Var* term;
+  Var* term = nullptr;
 
+  MatcherConstraint() = default;
   MatcherConstraint(Abstract::Op op, Var& term) : op(op), term(&term) {}
 };
 

From f28a35aa65a5be55086c3b17a52baffd94bb9008 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 12:49:25 -0700
Subject: [PATCH 37/89] work

---
 src/ir/constraint.cpp                         | 38 ++++++++++-------
 .../lit/passes/constraint-analysis-loops.wast | 41 +------------------
 2 files changed, 25 insertions(+), 54 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 91c151a2434..5e4fe9e20f0 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -239,14 +239,16 @@ struct Matcher {
   Matcher& require(Var& a, Abstract::Op op, Var& b);
 
   // Check if the pattern matches given inputs. The order of the inputs does not
-  // matter.
-  bool checkUnordered(const AndedConstraintSet& a,
+  // matter. Returns the address of the input that matches the first of the
+  // patterns (that is, if a matches ms1 in the constructor, we return &a, and
+  // otherwise &b), or nullptr of the match failed.
+  const AndedConstraintSet* checkUnordered(const AndedConstraintSet& a,
                       const AndedConstraintSet& b) {
     return checkUnorderedInternal(a, b);
   }
 
 private:
-  bool checkUnorderedInternal(const AndedConstraintSet& a,
+  const AndedConstraintSet* checkUnorderedInternal(const AndedConstraintSet& a,
                               const AndedConstraintSet& b,
                               bool flipped = false);
 
@@ -270,20 +272,20 @@ Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
   return *this;
 }
 
-bool Matcher::checkUnorderedInternal(const AndedConstraintSet& a,
+const AndedConstraintSet* Matcher::checkUnorderedInternal(const AndedConstraintSet& a,
                                      const AndedConstraintSet& b,
                                      bool flipped) {
-  auto returnFalse = [&]() {
-    // Before returning false, see if the flipped inputs match, if we didn't
-    // already try that.
+  auto fail = [&]() -> const AndedConstraintSet* {
+    // We failed, but try the flipped inputs if we haven't already.
     if (!flipped) {
-      return checkUnorderedInternal(b, a, true);
+      // If we match, flip the output to return the right thing.
+      return checkUnorderedInternal(b, a, true) ? &b : nullptr;
     }
-    return false;
+    return nullptr;
   };
 
   if (a.size() != ms1.size() || b.size() != ms2.size()) {
-    return returnFalse();
+    return fail();
   }
 
   // The sizes match, at least. Parse in more detail, building up a mapping of
@@ -312,7 +314,7 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSet& a,
   };
 
   if (!parse(a, ms1) || !parse(b, ms2)) {
-    return returnFalse();
+    return fail();
   }
 
   // Check requirements on the vars.
@@ -323,11 +325,11 @@ bool Matcher::checkUnorderedInternal(const AndedConstraintSet& a,
     // Check if { x == a } proves { x op b } is true.
     if (provesPair(Constraint{Abstract::Eq, aTerm}, Constraint{op, bTerm}) !=
         True) {
-      return returnFalse();
+      return fail();
     }
   }
 
-  return returnFalse();
+  return &a;
 }
 
 // Do an approximate OR on two inputs that are disjoint, that is, each proves
@@ -345,10 +347,16 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //   { x == A } || { x > A && x <= B } , A <= B   ===   { x >= A && X <= B }
   //
   Var A, B;
-  if (Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
+  if (auto* x = Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
         .require(A, LeS, B)
         .checkUnordered(self, other)) {
-    // ..
+    // x refers to the set with the equality constraint. We can reuse the other
+    // one, with a small change.
+    if (x == &self) {
+      self = other;
+    }
+    self[0].op = GeS;
+    return true;
   }
 
   // Otherwise, we have no idea.
diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
index 0072ba7b1e0..7276cc5d76e 100644
--- a/test/lit/passes/constraint-analysis-loops.wast
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -3,10 +3,10 @@
 ;; RUN: wasm-opt %s --constraint-analysis -all -S -o - | filecheck %s
 
 (module
-  ;; CHECK:      (import "a" "b" (func $import (type $1) (result i32)))
+  ;; CHECK:      (import "a" "b" (func $import (type $0) (result i32)))
   (import "a" "b" (func $import (result i32)))
 
-  ;; CHECK:      (func $bound (type $0)
+  ;; CHECK:      (func $bound (type $1)
   ;; CHECK-NEXT:  (local $x i32)
   ;; CHECK-NEXT:  (loop $loop
   ;; CHECK-NEXT:   (drop
@@ -86,43 +86,6 @@
     )
   )
 
-  ;; CHECK:      (func $bound-flipped (type $0)
-  ;; CHECK-NEXT:  (local $x i32)
-  ;; CHECK-NEXT:  (loop $loop
-  ;; CHECK-NEXT:   (drop
-  ;; CHECK-NEXT:    (i32.ge_s
-  ;; CHECK-NEXT:     (local.get $x)
-  ;; CHECK-NEXT:     (i32.const 0)
-  ;; CHECK-NEXT:    )
-  ;; CHECK-NEXT:   )
-  ;; CHECK-NEXT:   (drop
-  ;; CHECK-NEXT:    (i32.le_s
-  ;; CHECK-NEXT:     (local.get $x)
-  ;; CHECK-NEXT:     (i32.const 100)
-  ;; CHECK-NEXT:    )
-  ;; CHECK-NEXT:   )
-  ;; CHECK-NEXT:   (local.set $x
-  ;; CHECK-NEXT:    (call $import)
-  ;; CHECK-NEXT:   )
-  ;; CHECK-NEXT:   (if
-  ;; CHECK-NEXT:    (i32.le_s
-  ;; CHECK-NEXT:     (local.get $x)
-  ;; CHECK-NEXT:     (i32.const 100)
-  ;; CHECK-NEXT:    )
-  ;; CHECK-NEXT:    (then
-  ;; CHECK-NEXT:     (if
-  ;; CHECK-NEXT:      (i32.gt_s
-  ;; CHECK-NEXT:       (local.get $x)
-  ;; CHECK-NEXT:       (i32.const 0)
-  ;; CHECK-NEXT:      )
-  ;; CHECK-NEXT:      (then
-  ;; CHECK-NEXT:       (br $loop)
-  ;; CHECK-NEXT:      )
-  ;; CHECK-NEXT:     )
-  ;; CHECK-NEXT:    )
-  ;; CHECK-NEXT:   )
-  ;; CHECK-NEXT:  )
-  ;; CHECK-NEXT: )
   (;;func $bound-flipped
     (local $x i32)
     ;; As above, but with the ifs flipped. We optimize the same way.

From 2b6e73b35013f2311138653f9c92e22545e19dc3 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 12:49:32 -0700
Subject: [PATCH 38/89] work

---
 src/ir/constraint.cpp | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 5e4fe9e20f0..f72907af60e 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -243,14 +243,14 @@ struct Matcher {
   // patterns (that is, if a matches ms1 in the constructor, we return &a, and
   // otherwise &b), or nullptr of the match failed.
   const AndedConstraintSet* checkUnordered(const AndedConstraintSet& a,
-                      const AndedConstraintSet& b) {
+                                           const AndedConstraintSet& b) {
     return checkUnorderedInternal(a, b);
   }
 
 private:
   const AndedConstraintSet* checkUnorderedInternal(const AndedConstraintSet& a,
-                              const AndedConstraintSet& b,
-                              bool flipped = false);
+                                                   const AndedConstraintSet& b,
+                                                   bool flipped = false);
 
   const MatcherSet& ms1;
   const MatcherSet& ms2;
@@ -272,9 +272,8 @@ Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
   return *this;
 }
 
-const AndedConstraintSet* Matcher::checkUnorderedInternal(const AndedConstraintSet& a,
-                                     const AndedConstraintSet& b,
-                                     bool flipped) {
+const AndedConstraintSet* Matcher::checkUnorderedInternal(
+  const AndedConstraintSet& a, const AndedConstraintSet& b, bool flipped) {
   auto fail = [&]() -> const AndedConstraintSet* {
     // We failed, but try the flipped inputs if we haven't already.
     if (!flipped) {
@@ -348,8 +347,8 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //
   Var A, B;
   if (auto* x = Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
-        .require(A, LeS, B)
-        .checkUnordered(self, other)) {
+                  .require(A, LeS, B)
+                  .checkUnordered(self, other)) {
     // x refers to the set with the equality constraint. We can reuse the other
     // one, with a small change.
     if (x == &self) {

From 753490d9e329be81ab79e8298b06e9f7f8de504f Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 13:01:20 -0700
Subject: [PATCH 39/89] work

---
 src/ir/constraint.cpp | 29 ++++++++++++++++++++++++-----
 1 file changed, 24 insertions(+), 5 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index f72907af60e..9b0857d3acf 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -221,6 +221,16 @@ struct MatcherConstraint {
 
   MatcherConstraint() = default;
   MatcherConstraint(Abstract::Op op, Var& term) : op(op), term(&term) {}
+
+  bool operator==(const MatcherConstraint&) const = default;
+  bool operator<(const MatcherConstraint& other) const {
+    // Ordered in a parallel way to Constraints, so that when we compare, things
+    // line up.
+    if (op != other.op) {
+      return op < other.op;
+    }
+    return term < other.term;
+  }
 };
 
 // A matcher AndedConstraintSet, which abstracts over the normal one to support
@@ -231,7 +241,7 @@ using MatcherSet = inplace_vector<MatcherConstraint, MaxConstraints>;
 // that follows the rules of logic.
 struct Matcher {
   // Set up a pattern containing two sets of constraints.
-  Matcher(const MatcherSet& ms1, const MatcherSet& ms2);
+  Matcher(const MatcherSet& ms1_, const MatcherSet& ms2_);
 
   // Add a requirement on this pattern, a demand on the Vars.
   //
@@ -252,8 +262,8 @@ struct Matcher {
                                                    const AndedConstraintSet& b,
                                                    bool flipped = false);
 
-  const MatcherSet& ms1;
-  const MatcherSet& ms2;
+  MatcherSet ms1;
+  MatcherSet ms2;
 
   struct Requirement {
     Var* a;
@@ -264,8 +274,13 @@ struct Matcher {
   SmallVector<Requirement, 2> requirements;
 };
 
-Matcher::Matcher(const MatcherSet& ms1, const MatcherSet& ms2)
-  : ms1(ms1), ms2(ms2) {}
+Matcher::Matcher(const MatcherSet& ms1_, const MatcherSet& ms2_)
+  : ms1(ms1_), ms2(ms2_) {
+  // Sort the sets like Constraints are sorted, so that when we compare, things
+  // line up.
+  std::sort(ms1.begin(), ms1.end());
+  std::sort(ms2.begin(), ms2.end());
+}
 
 Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
   requirements.push_back({&a, op, &b});
@@ -274,6 +289,7 @@ Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
 
 const AndedConstraintSet* Matcher::checkUnorderedInternal(
   const AndedConstraintSet& a, const AndedConstraintSet& b, bool flipped) {
+
   auto fail = [&]() -> const AndedConstraintSet* {
     // We failed, but try the flipped inputs if we haven't already.
     if (!flipped) {
@@ -341,6 +357,8 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   using MC = MatcherConstraint;
   using namespace Abstract;
 
+std::cout << self << " OR " << other << '\n';
+
   // Simple range fusing, add an equality to turn > into >= :
   //
   //   { x == A } || { x > A && x <= B } , A <= B   ===   { x >= A && X <= B }
@@ -355,6 +373,7 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
       self = other;
     }
     self[0].op = GeS;
+std::cout << "MATACHHH\n";
     return true;
   }
 

From fa1144aab54a5518caafab94a34dd7b819f663e1 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 13:02:00 -0700
Subject: [PATCH 40/89] work

---
 src/ir/constraint.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 9b0857d3acf..c088a1a2069 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -357,7 +357,7 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   using MC = MatcherConstraint;
   using namespace Abstract;
 
-std::cout << self << " OR " << other << '\n';
+  std::cout << self << " OR " << other << '\n';
 
   // Simple range fusing, add an equality to turn > into >= :
   //
@@ -373,7 +373,7 @@ std::cout << self << " OR " << other << '\n';
       self = other;
     }
     self[0].op = GeS;
-std::cout << "MATACHHH\n";
+    std::cout << "MATACHHH\n";
     return true;
   }
 

From dc858e875057f2b7c963294cfc50a9c9b15cd1b4 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 13:15:28 -0700
Subject: [PATCH 41/89] work

---
 src/ir/constraint.cpp | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index c088a1a2069..d0167d4d70a 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -248,17 +248,21 @@ struct Matcher {
   // For convenience, return this Matcher object (i.e. the builder pattern).
   Matcher& require(Var& a, Abstract::Op op, Var& b);
 
+  // When a match succeeds, we return a map of Vars to Terms, allowing the user
+  // to find out what each Var matched against.
+  using VarTermMap = std::unordered_map<Var*, Term>;
+
   // Check if the pattern matches given inputs. The order of the inputs does not
   // matter. Returns the address of the input that matches the first of the
   // patterns (that is, if a matches ms1 in the constructor, we return &a, and
   // otherwise &b), or nullptr of the match failed.
-  const AndedConstraintSet* checkUnordered(const AndedConstraintSet& a,
+  std::optional<VarTermMap> checkUnordered(const AndedConstraintSet& a,
                                            const AndedConstraintSet& b) {
     return checkUnorderedInternal(a, b);
   }
 
 private:
-  const AndedConstraintSet* checkUnorderedInternal(const AndedConstraintSet& a,
+  std::optional<VarTermMap> checkUnorderedInternal(const AndedConstraintSet& a,
                                                    const AndedConstraintSet& b,
                                                    bool flipped = false);
 
@@ -287,16 +291,15 @@ Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
   return *this;
 }
 
-const AndedConstraintSet* Matcher::checkUnorderedInternal(
+std::optional<Matcher::VarTermMap> Matcher::checkUnorderedInternal(
   const AndedConstraintSet& a, const AndedConstraintSet& b, bool flipped) {
 
-  auto fail = [&]() -> const AndedConstraintSet* {
+  auto fail = [&]() -> std::optional<Matcher::VarTermMap> {
     // We failed, but try the flipped inputs if we haven't already.
     if (!flipped) {
-      // If we match, flip the output to return the right thing.
-      return checkUnorderedInternal(b, a, true) ? &b : nullptr;
+      return checkUnorderedInternal(b, a, true);
     }
-    return nullptr;
+    return {};
   };
 
   if (a.size() != ms1.size() || b.size() != ms2.size()) {
@@ -305,7 +308,7 @@ const AndedConstraintSet* Matcher::checkUnorderedInternal(
 
   // The sizes match, at least. Parse in more detail, building up a mapping of
   // Vars to concrete Terms
-  std::unordered_map<Var*, Term> varTermMap;
+  VarTermMap varTermMap;
 
   auto parse = [&](const AndedConstraintSet& input, const MatcherSet& pattern) {
     for (Index i = 0; i < input.size(); i++) {
@@ -344,7 +347,7 @@ const AndedConstraintSet* Matcher::checkUnorderedInternal(
     }
   }
 
-  return &a;
+  return varTermMap;
 }
 
 // Do an approximate OR on two inputs that are disjoint, that is, each proves
@@ -364,16 +367,13 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //   { x == A } || { x > A && x <= B } , A <= B   ===   { x >= A && X <= B }
   //
   Var A, B;
-  if (auto* x = Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
+  if (auto result = Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
                   .require(A, LeS, B)
                   .checkUnordered(self, other)) {
-    // x refers to the set with the equality constraint. We can reuse the other
-    // one, with a small change.
-    if (x == &self) {
-      self = other;
-    }
-    self[0].op = GeS;
-    std::cout << "MATACHHH\n";
+    Term aValue = (*result)[&A];
+    Term bValue = (*result)[&B];
+    self = AndedConstraintSet({GeS, aValue}, {LeS, bValue}); // TODO !&
+    std::cout << "MATACHHH " << self << "\n";
     return true;
   }
 

From ed9d41f31f8dad40e4bcd243492d427f97e18771 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 13:21:49 -0700
Subject: [PATCH 42/89] work

---
 src/ir/constraint.cpp | 2 +-
 src/ir/constraint.h   | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index d0167d4d70a..7675f01b4b6 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -372,7 +372,7 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
                   .checkUnordered(self, other)) {
     Term aValue = (*result)[&A];
     Term bValue = (*result)[&B];
-    self = AndedConstraintSet({GeS, aValue}, {LeS, bValue}); // TODO !&
+    self = AndedConstraintSet({{GeS, aValue}, {LeS, bValue}}); // TODO !&
     std::cout << "MATACHHH " << self << "\n";
     return true;
   }
diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index 4412c53a21b..71870187a48 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -92,6 +92,13 @@ struct AndedConstraintSet : inplace_vector<Constraint, MaxConstraints> {
   // until something changes.
   bool isContradiction = true;
 
+  AndedConstraintSet() = default;
+  AndedConstraintSet(std::initializer_list<Constraint> constraints)
+    : inplace_vector<Constraint, MaxConstraints>(constraints),
+      isContradiction(false) {
+    std::sort(begin(), end());
+  }
+
   // 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.)

From 00b33c57ee4bd8c52058d862f0ecd7f7c819055c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 13:21:57 -0700
Subject: [PATCH 43/89] work

---
 src/ir/constraint.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 7675f01b4b6..9434a3dd96d 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -368,8 +368,8 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //
   Var A, B;
   if (auto result = Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
-                  .require(A, LeS, B)
-                  .checkUnordered(self, other)) {
+                      .require(A, LeS, B)
+                      .checkUnordered(self, other)) {
     Term aValue = (*result)[&A];
     Term bValue = (*result)[&B];
     self = AndedConstraintSet({{GeS, aValue}, {LeS, bValue}}); // TODO !&

From e470ae1f9761969b2f8cc6e5db49d86d2c228bb4 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 13:38:18 -0700
Subject: [PATCH 44/89] work

---
 src/ir/constraint.cpp | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 9434a3dd96d..b80ea41c059 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -250,7 +250,12 @@ struct Matcher {
 
   // When a match succeeds, we return a map of Vars to Terms, allowing the user
   // to find out what each Var matched against.
-  using VarTermMap = std::unordered_map<Var*, Term>;
+  struct VarTermMap : public std::unordered_map<Var*, Term> {
+    // As a convenience, allow using the object instead of the pointer.
+    Term& operator[](Var& var) {
+      return std::unordered_map<Var*, Term>::operator[](&var);
+    }
+  };
 
   // Check if the pattern matches given inputs. The order of the inputs does not
   // matter. Returns the address of the input that matches the first of the
@@ -337,8 +342,8 @@ std::optional<Matcher::VarTermMap> Matcher::checkUnorderedInternal(
 
   // Check requirements on the vars.
   for (auto& [a, op, b] : requirements) {
-    auto aTerm = varTermMap[a];
-    auto bTerm = varTermMap[b];
+    auto aTerm = varTermMap[*a];
+    auto bTerm = varTermMap[*b];
 
     // Check if { x == a } proves { x op b } is true.
     if (provesPair(Constraint{Abstract::Eq, aTerm}, Constraint{op, bTerm}) !=
@@ -370,9 +375,9 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   if (auto result = Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
                       .require(A, LeS, B)
                       .checkUnordered(self, other)) {
-    Term aValue = (*result)[&A];
-    Term bValue = (*result)[&B];
-    self = AndedConstraintSet({{GeS, aValue}, {LeS, bValue}}); // TODO !&
+    Term aValue = (*result)[A];
+    Term bValue = (*result)[B];
+    self = AndedConstraintSet({{GeS, aValue}, {LeS, bValue}});
     std::cout << "MATACHHH " << self << "\n";
     return true;
   }

From 65f85dd70f4296d0246f499ce3178f39b1ca84b2 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 13:40:37 -0700
Subject: [PATCH 45/89] work

---
 .../lit/passes/constraint-analysis-loops.wast | 49 ++++++++++++++-----
 1 file changed, 37 insertions(+), 12 deletions(-)

diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
index 7276cc5d76e..506c2bb90e6 100644
--- a/test/lit/passes/constraint-analysis-loops.wast
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -3,23 +3,17 @@
 ;; RUN: wasm-opt %s --constraint-analysis -all -S -o - | filecheck %s
 
 (module
-  ;; CHECK:      (import "a" "b" (func $import (type $0) (result i32)))
+  ;; CHECK:      (import "a" "b" (func $import (type $1) (result i32)))
   (import "a" "b" (func $import (result i32)))
 
-  ;; CHECK:      (func $bound (type $1)
+  ;; CHECK:      (func $bound (type $0)
   ;; CHECK-NEXT:  (local $x i32)
   ;; CHECK-NEXT:  (loop $loop
   ;; CHECK-NEXT:   (drop
-  ;; CHECK-NEXT:    (i32.ge_s
-  ;; CHECK-NEXT:     (local.get $x)
-  ;; CHECK-NEXT:     (i32.const 0)
-  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (i32.const 1)
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:   (drop
-  ;; CHECK-NEXT:    (i32.le_s
-  ;; CHECK-NEXT:     (local.get $x)
-  ;; CHECK-NEXT:     (i32.const 100)
-  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (i32.const 1)
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:   (local.set $x
   ;; CHECK-NEXT:    (call $import)
@@ -86,7 +80,38 @@
     )
   )
 
-  (;;func $bound-flipped
+  ;; CHECK:      (func $bound-flipped (type $0)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (loop $loop
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.const 1)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.const 1)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (local.set $x
+  ;; CHECK-NEXT:    (call $import)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (if
+  ;; CHECK-NEXT:    (i32.le_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 100)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (then
+  ;; CHECK-NEXT:     (if
+  ;; CHECK-NEXT:      (i32.gt_s
+  ;; CHECK-NEXT:       (local.get $x)
+  ;; CHECK-NEXT:       (i32.const 0)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (then
+  ;; CHECK-NEXT:       (br $loop)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  (func $bound-flipped
     (local $x i32)
     ;; As above, but with the ifs flipped. We optimize the same way.
     (loop $loop
@@ -123,7 +148,7 @@
         )
       )
     )
-  ;;)
+  )
   ;; TODO: unsigned
   ;; TODO: non-zero
 )

From 2ac15140adea94d24d8118e997abc00cb07bb48c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 13:48:44 -0700
Subject: [PATCH 46/89] work

---
 src/ir/constraint.cpp                         |  3 -
 .../lit/passes/constraint-analysis-loops.wast | 85 ++++++++++++++++++-
 2 files changed, 83 insertions(+), 5 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index b80ea41c059..a73df02d7f1 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -365,8 +365,6 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   using MC = MatcherConstraint;
   using namespace Abstract;
 
-  std::cout << self << " OR " << other << '\n';
-
   // Simple range fusing, add an equality to turn > into >= :
   //
   //   { x == A } || { x > A && x <= B } , A <= B   ===   { x >= A && X <= B }
@@ -378,7 +376,6 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
     Term aValue = (*result)[A];
     Term bValue = (*result)[B];
     self = AndedConstraintSet({{GeS, aValue}, {LeS, bValue}});
-    std::cout << "MATACHHH " << self << "\n";
     return true;
   }
 
diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
index 506c2bb90e6..0e85cb8f9c4 100644
--- a/test/lit/passes/constraint-analysis-loops.wast
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -80,7 +80,7 @@
     )
   )
 
-  ;; CHECK:      (func $bound-flipped (type $0)
+  ;; CHECK:      (func $bound-flipped-ifs (type $0)
   ;; CHECK-NEXT:  (local $x i32)
   ;; CHECK-NEXT:  (loop $loop
   ;; CHECK-NEXT:   (drop
@@ -111,7 +111,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  (func $bound-flipped
+  (func $bound-flipped-ifs
     (local $x i32)
     ;; As above, but with the ifs flipped. We optimize the same way.
     (loop $loop
@@ -149,6 +149,87 @@
       )
     )
   )
+
+  ;; CHECK:      (func $bound-nonconstant (type $2) (param $p i32)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (loop $loop
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.ge_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (local.get $p)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.le_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 100)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (local.set $x
+  ;; CHECK-NEXT:    (call $import)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (if
+  ;; CHECK-NEXT:    (i32.gt_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (local.get $p)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (then
+  ;; CHECK-NEXT:     (if
+  ;; CHECK-NEXT:      (i32.le_s
+  ;; CHECK-NEXT:       (local.get $x)
+  ;; CHECK-NEXT:       (i32.const 100)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (then
+  ;; CHECK-NEXT:       (br $loop)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  (func $bound-nonconstant (param $p i32)
+    (local $x i32)
+    ;; As above, but rather than zero we have an unknown param $p. We can't
+    ;; optimize since we don't know how $p relates to 100: if $p is negative,
+    ;; we have something like {x == 200} || {x > 200 && x <= 100}. The RHS is
+    ;; a contradiction (at runtime), and we don't want to get into the
+    ;; complexity of reasoning about such things, so we do not optimize here.
+    (loop $loop
+      (drop
+        (i32.ge_s
+          (local.get $x)
+          (local.get $p)
+        )
+      )
+      (drop
+        (i32.le_s
+          (local.get $x)
+          (i32.const 100)
+        )
+      )
+      (local.set $x
+        (call $import)
+      )
+      (if
+        (i32.gt_s
+          (local.get $x)
+          (local.get $p)
+        )
+        (then
+          (if
+            (i32.le_s
+              (local.get $x)
+              (i32.const 100)
+            )
+            (then
+              (br $loop)
+            )
+          )
+        )
+      )
+    )
+  )
+
   ;; TODO: unsigned
   ;; TODO: non-zero
 )

From e713c6b5346475259098ed634ee2ba942de01d58 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 13:53:04 -0700
Subject: [PATCH 47/89] work

---
 .../lit/passes/constraint-analysis-loops.wast | 85 ++++++++++++++++++-
 1 file changed, 83 insertions(+), 2 deletions(-)

diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
index 0e85cb8f9c4..e2a6c301b20 100644
--- a/test/lit/passes/constraint-analysis-loops.wast
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -150,7 +150,7 @@
     )
   )
 
-  ;; CHECK:      (func $bound-nonconstant (type $2) (param $p i32)
+  ;; CHECK:      (func $bound-nonconstant-no (type $2) (param $p i32)
   ;; CHECK-NEXT:  (local $x i32)
   ;; CHECK-NEXT:  (loop $loop
   ;; CHECK-NEXT:   (drop
@@ -187,7 +187,7 @@
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:  )
   ;; CHECK-NEXT: )
-  (func $bound-nonconstant (param $p i32)
+  (func $bound-nonconstant-no (param $p i32)
     (local $x i32)
     ;; As above, but rather than zero we have an unknown param $p. We can't
     ;; optimize since we don't know how $p relates to 100: if $p is negative,
@@ -230,6 +230,87 @@
     )
   )
 
+  ;; CHECK:      (func $bound-no_eq-no (type $0)
+  ;; CHECK-NEXT:  (local $x i32)
+  ;; CHECK-NEXT:  (local.set $x
+  ;; CHECK-NEXT:   (i32.const 1)
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT:  (loop $loop
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.ge_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (drop
+  ;; CHECK-NEXT:    (i32.const 1)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (local.set $x
+  ;; CHECK-NEXT:    (call $import)
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:   (if
+  ;; CHECK-NEXT:    (i32.gt_s
+  ;; CHECK-NEXT:     (local.get $x)
+  ;; CHECK-NEXT:     (i32.const 0)
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:    (then
+  ;; CHECK-NEXT:     (if
+  ;; CHECK-NEXT:      (i32.le_s
+  ;; CHECK-NEXT:       (local.get $x)
+  ;; CHECK-NEXT:       (i32.const 100)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:      (then
+  ;; CHECK-NEXT:       (br $loop)
+  ;; CHECK-NEXT:      )
+  ;; CHECK-NEXT:     )
+  ;; CHECK-NEXT:    )
+  ;; CHECK-NEXT:   )
+  ;; CHECK-NEXT:  )
+  ;; CHECK-NEXT: )
+  (func $bound-no_eq-no
+    (local $x i32)
+    ;; As the original testcase, but replacing x == 0 with x == 1.
+    (local.set $x
+      (i32.const -1)
+    )
+    (loop $loop
+      ;; We could infer this TODO
+      (drop
+        (i32.ge_s
+          (local.get $x)
+          (i32.const 0)
+        )
+      )
+      ;; This is true (1 <= 100, and also if we come from the branch below).
+      (drop
+        (i32.le_s
+          (local.get $x)
+          (i32.const 100)
+        )
+      )
+      (local.set $x
+        (call $import)
+      )
+      (if
+        (i32.gt_s
+          (local.get $x)
+          (i32.const 0)
+        )
+        (then
+          (if
+            (i32.le_s
+              (local.get $x)
+              (i32.const 100)
+            )
+            (then
+              (br $loop)
+            )
+          )
+        )
+      )
+    )
+  )
+
   ;; TODO: unsigned
   ;; TODO: non-zero
 )

From f478cd05bbfeabc3c87466d89c13711d1eca5b96 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:04:05 -0700
Subject: [PATCH 48/89] work

---
 src/ir/constraint.cpp                         |  1 +
 src/ir/constraint.h                           |  9 +-
 test/gtest/constraint.cpp                     | 16 +++-
 .../lit/passes/constraint-analysis-loops.wast | 84 -------------------
 4 files changed, 20 insertions(+), 90 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index a73df02d7f1..e4350a96ee8 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -377,6 +377,7 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
     Term bValue = (*result)[B];
     self = AndedConstraintSet({{GeS, aValue}, {LeS, bValue}});
     return true;
+    // TODO: unsigned etc.
   }
 
   // Otherwise, we have no idea.
diff --git a/src/ir/constraint.h b/src/ir/constraint.h
index 71870187a48..9fea231fbc7 100644
--- a/src/ir/constraint.h
+++ b/src/ir/constraint.h
@@ -93,10 +93,11 @@ struct AndedConstraintSet : inplace_vector<Constraint, MaxConstraints> {
   bool isContradiction = true;
 
   AndedConstraintSet() = default;
-  AndedConstraintSet(std::initializer_list<Constraint> constraints)
-    : inplace_vector<Constraint, MaxConstraints>(constraints),
-      isContradiction(false) {
-    std::sort(begin(), end());
+  AndedConstraintSet(std::initializer_list<Constraint> constraints) {
+    isContradiction = false;
+    for (auto& c : constraints) {
+      approximateAnd(c);
+    }
   }
 
   // Proving everything (even contradictions) is equivalent to being a
diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index ea3fc10167c..b98b8e955f4 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -240,5 +240,17 @@ TEST(ConstraintTest, TestDeredundancy) {
   EXPECT_EQ(t[0], eq0);
 }
 
-// TODO: test an approximateOr of { x = 10 } and { x >= 0 }, once we support
-//       inequalities
+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))}}};
+
+  auto ored = eq5;
+  ored.approximateOr(ge0);
+  EXPECT_EQ(ored, ge0);
+
+  ored = ge0;
+  ored.approximateOr(eq5);
+  EXPECT_EQ(ored, ge0);
+}
+
diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
index e2a6c301b20..75ed4711729 100644
--- a/test/lit/passes/constraint-analysis-loops.wast
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -229,88 +229,4 @@
       )
     )
   )
-
-  ;; CHECK:      (func $bound-no_eq-no (type $0)
-  ;; CHECK-NEXT:  (local $x i32)
-  ;; CHECK-NEXT:  (local.set $x
-  ;; CHECK-NEXT:   (i32.const 1)
-  ;; CHECK-NEXT:  )
-  ;; CHECK-NEXT:  (loop $loop
-  ;; CHECK-NEXT:   (drop
-  ;; CHECK-NEXT:    (i32.ge_s
-  ;; CHECK-NEXT:     (local.get $x)
-  ;; CHECK-NEXT:     (i32.const 0)
-  ;; CHECK-NEXT:    )
-  ;; CHECK-NEXT:   )
-  ;; CHECK-NEXT:   (drop
-  ;; CHECK-NEXT:    (i32.const 1)
-  ;; CHECK-NEXT:   )
-  ;; CHECK-NEXT:   (local.set $x
-  ;; CHECK-NEXT:    (call $import)
-  ;; CHECK-NEXT:   )
-  ;; CHECK-NEXT:   (if
-  ;; CHECK-NEXT:    (i32.gt_s
-  ;; CHECK-NEXT:     (local.get $x)
-  ;; CHECK-NEXT:     (i32.const 0)
-  ;; CHECK-NEXT:    )
-  ;; CHECK-NEXT:    (then
-  ;; CHECK-NEXT:     (if
-  ;; CHECK-NEXT:      (i32.le_s
-  ;; CHECK-NEXT:       (local.get $x)
-  ;; CHECK-NEXT:       (i32.const 100)
-  ;; CHECK-NEXT:      )
-  ;; CHECK-NEXT:      (then
-  ;; CHECK-NEXT:       (br $loop)
-  ;; CHECK-NEXT:      )
-  ;; CHECK-NEXT:     )
-  ;; CHECK-NEXT:    )
-  ;; CHECK-NEXT:   )
-  ;; CHECK-NEXT:  )
-  ;; CHECK-NEXT: )
-  (func $bound-no_eq-no
-    (local $x i32)
-    ;; As the original testcase, but replacing x == 0 with x == 1.
-    (local.set $x
-      (i32.const -1)
-    )
-    (loop $loop
-      ;; We could infer this TODO
-      (drop
-        (i32.ge_s
-          (local.get $x)
-          (i32.const 0)
-        )
-      )
-      ;; This is true (1 <= 100, and also if we come from the branch below).
-      (drop
-        (i32.le_s
-          (local.get $x)
-          (i32.const 100)
-        )
-      )
-      (local.set $x
-        (call $import)
-      )
-      (if
-        (i32.gt_s
-          (local.get $x)
-          (i32.const 0)
-        )
-        (then
-          (if
-            (i32.le_s
-              (local.get $x)
-              (i32.const 100)
-            )
-            (then
-              (br $loop)
-            )
-          )
-        )
-      )
-    )
-  )
-
-  ;; TODO: unsigned
-  ;; TODO: non-zero
 )

From 70085e5e0f784c921521d7b72beda66890353de4 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:11:03 -0700
Subject: [PATCH 49/89] work

---
 src/ir/constraint.cpp     |  2 +-
 test/gtest/constraint.cpp | 29 +++++++++++++++++++++++------
 2 files changed, 24 insertions(+), 7 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index e4350a96ee8..0ccb138efbf 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -367,7 +367,7 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
 
   // Simple range fusing, add an equality to turn > into >= :
   //
-  //   { x == A } || { x > A && x <= B } , A <= B   ===   { x >= A && X <= B }
+  //   { x == A } || { x > A && x <= B } , A <= B   ==>   { x >= A && X <= B }
   //
   Var A, B;
   if (auto result = Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index b98b8e955f4..406e99b1cd4 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -240,17 +240,34 @@ TEST(ConstraintTest, TestDeredundancy) {
   EXPECT_EQ(t[0], eq0);
 }
 
+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);
+}
+
+TEST(ConstraintTest, TestOrOrDisjoint) {
+  // { x == A } || { x > A && x <= B } , A <= B   ==>   { x >= A && X <= B }
+
+  AndedConstraintSet left{Constraint{Eq, {Literal(int32_t(5))}}};
+
+  AndedConstraintSet right({Constraint{GtS, {Literal(int32_t(5))}},
+                           Constraint{LeS, {Literal(int32_t(42)}});
 
-  auto ored = eq5;
-  ored.approximateOr(ge0);
-  EXPECT_EQ(ored, ge0);
+  AndedConstraintSet result({Constraint{GeS, {Literal(int32_t(5))}},
+                            Constraint{LeS, {Literal(int32_t(42)}});
 
-  ored = ge0;
-  ored.approximateOr(eq5);
-  EXPECT_EQ(ored, ge0);
+  checkOr(left, right, result);
 }
 

From d153b16b3c3e938e4215946fec1769082a704cf0 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:13:42 -0700
Subject: [PATCH 50/89] work

---
 test/gtest/constraint.cpp | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 406e99b1cd4..3447a066807 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -240,7 +240,9 @@ TEST(ConstraintTest, TestDeredundancy) {
   EXPECT_EQ(t[0], eq0);
 }
 
-static void checkOr(const AndedConstraintSet& a, const AndedConstraintSet& b, const AndedConstraintSet& result) {
+static void checkOr(const AndedConstraintSet& a,
+                    const AndedConstraintSet& b,
+                    const AndedConstraintSet& result) {
   auto ored = a;
   ored.approximateOr(b);
   EXPECT_EQ(ored, result);
@@ -262,12 +264,11 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
 
   AndedConstraintSet left{Constraint{Eq, {Literal(int32_t(5))}}};
 
-  AndedConstraintSet right({Constraint{GtS, {Literal(int32_t(5))}},
-                           Constraint{LeS, {Literal(int32_t(42)}});
+  auto right = AndedConstraintSet({{GtS, {Literal(int32_t(5))}},
+                           {LeS, {Literal(int32_t(42)}});
 
-  AndedConstraintSet result({Constraint{GeS, {Literal(int32_t(5))}},
-                            Constraint{LeS, {Literal(int32_t(42)}});
+  AndedConstraintSet result({{GeS, {Literal(int32_t(5))}},
+                            {LeS, {Literal(int32_t(42)}});
 
   checkOr(left, right, result);
 }
-

From e16c4c6a8c23c34513f4a4bdc112c92fc5f299ea Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:17:04 -0700
Subject: [PATCH 51/89] work

---
 test/gtest/constraint.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 3447a066807..0701a3bfb77 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -264,11 +264,11 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
 
   AndedConstraintSet left{Constraint{Eq, {Literal(int32_t(5))}}};
 
-  auto right = AndedConstraintSet({{GtS, {Literal(int32_t(5))}},
-                           {LeS, {Literal(int32_t(42)}});
+  AndedConstraintSet right({{GtS, {Literal(int32_t(5))}},
+                                   {LeS, {Literal(int32_t(42))}}});
 
   AndedConstraintSet result({{GeS, {Literal(int32_t(5))}},
-                            {LeS, {Literal(int32_t(42)}});
+                             {LeS, {Literal(int32_t(42))}}});
 
   checkOr(left, right, result);
 }

From 5ad4c40e1a7ea8a9a3753e7d5b6fb45a9f1b91c9 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:17:10 -0700
Subject: [PATCH 52/89] work

---
 test/gtest/constraint.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 0701a3bfb77..85b84ba5092 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -264,11 +264,11 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
 
   AndedConstraintSet left{Constraint{Eq, {Literal(int32_t(5))}}};
 
-  AndedConstraintSet right({{GtS, {Literal(int32_t(5))}},
-                                   {LeS, {Literal(int32_t(42))}}});
+  AndedConstraintSet right(
+    {{GtS, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}});
 
-  AndedConstraintSet result({{GeS, {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);
 }

From abcfee84644fda6413b0322767a7c3889637c20d Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:22:06 -0700
Subject: [PATCH 53/89] work

---
 test/gtest/constraint.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 85b84ba5092..07bb8895ab5 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -271,4 +271,12 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
     {{GeS, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}});
 
   checkOr(left, right, result);
+
+  // Change 5 on the left to 7. 7 is in the range on the right, so we end up
+  // with the right.
+  AndedConstraintSet left7{Constraint{Eq, {Literal(int32_t(7))}}};
+  checkOr(left7, right, right);
+
+  AndedConstraintSet empty{};
+  empty.setProvesNothing();
 }

From a3d9a548fa7090752790ed39f8565d42ed84f677 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:22:44 -0700
Subject: [PATCH 54/89] work

---
 test/gtest/constraint.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 07bb8895ab5..32e973a25e3 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -277,6 +277,8 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
   AndedConstraintSet left7{Constraint{Eq, {Literal(int32_t(7))}}};
   checkOr(left7, right, right);
 
+  // Change 5 on the left to 4. Now we fail to find anything.
+  AndedConstraintSet left4{Constraint{Eq, {Literal(int32_t(4))}}};
   AndedConstraintSet empty{};
-  empty.setProvesNothing();
+  checkOr(left7, right, empty);
 }

From 4b161807009eab0390f2993851346aa6769bf64c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:24:47 -0700
Subject: [PATCH 55/89] work

---
 test/gtest/constraint.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 32e973a25e3..f25d0febdfc 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -280,5 +280,6 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
   // Change 5 on the left to 4. Now we fail to find anything.
   AndedConstraintSet left4{Constraint{Eq, {Literal(int32_t(4))}}};
   AndedConstraintSet empty{};
-  checkOr(left7, right, empty);
+  empty.setProvesNothing();
+  checkOr(left4, right, empty); XXX
 }

From 14e509861a1b60b63b483ceac920637d7a5a5782 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:41:02 -0700
Subject: [PATCH 56/89] work

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

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 0ccb138efbf..79508d6228d 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -325,7 +325,7 @@ std::optional<Matcher::VarTermMap> Matcher::checkUnorderedInternal(
       // The term must match, or define a new unknown value.
       auto [iter, inserted] =
         varTermMap.insert({pattern[i].term, input[i].term});
-      if (inserted) {
+      if (!inserted) {
         // The Var in the pattern is already mapped and known. The input here
         // must match the prior appearance.
         if (input[i].term != iter->second) {
diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index f25d0febdfc..8293bd2f685 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -281,5 +281,5 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
   AndedConstraintSet left4{Constraint{Eq, {Literal(int32_t(4))}}};
   AndedConstraintSet empty{};
   empty.setProvesNothing();
-  checkOr(left4, right, empty); XXX
+  checkOr(left4, right, empty); //XXX
 }

From 3c5951642c71834c8e0a7019b8793ffb7b880e79 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:41:26 -0700
Subject: [PATCH 57/89] work

---
 test/gtest/constraint.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 8293bd2f685..8afd972989f 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -280,6 +280,5 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
   // Change 5 on the left to 4. Now we fail to find anything.
   AndedConstraintSet left4{Constraint{Eq, {Literal(int32_t(4))}}};
   AndedConstraintSet empty{};
-  empty.setProvesNothing();
-  checkOr(left4, right, empty); //XXX
+  checkOr(left4, right, empty);
 }

From ea598cbc8d7cbd7baf22f498f171e549dc4000d0 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:43:19 -0700
Subject: [PATCH 58/89] work

---
 test/gtest/constraint.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 8afd972989f..4176c3080ff 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -281,4 +281,9 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
   AndedConstraintSet left4{Constraint{Eq, {Literal(int32_t(4))}}};
   AndedConstraintSet empty{};
   checkOr(left4, right, empty);
+
+  // Change 5 on the right to 6. Again we fail to find anything
+  AndedConstraintSet right6(
+    {{GtS, {Literal(int32_t(6))}}, {LeS, {Literal(int32_t(42))}}});
+  checkOr(left, right6, empty);
 }

From f31ae728b12c7e43b4186094f59492e4aeeb6cf7 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:44:48 -0700
Subject: [PATCH 59/89] work

---
 test/gtest/constraint.cpp | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 4176c3080ff..35f63f21a2e 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -272,6 +272,8 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
 
   checkOr(left, right, result);
 
+  // Changes to constants:
+
   // Change 5 on the left to 7. 7 is in the range on the right, so we end up
   // with the right.
   AndedConstraintSet left7{Constraint{Eq, {Literal(int32_t(7))}}};
@@ -282,8 +284,15 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
   AndedConstraintSet empty{};
   checkOr(left4, right, empty);
 
-  // Change 5 on the right to 6. Again we fail to find anything
+  // Change 5 on the right to 6. Again we fail to find anything.
   AndedConstraintSet right6(
     {{GtS, {Literal(int32_t(6))}}, {LeS, {Literal(int32_t(42))}}});
   checkOr(left, right6, empty);
+
+  // Changes to operations:
+
+  // Change the Eq on the left to Ne. We fail.
+  AndedConstraintSet leftNe{Constraint{Ne, {Literal(int32_t(5))}}};
+  checkOr(leftNe, right, empty);
+
 }

From 6a3d5bc19160c2c0cfed3b6b319ae814b2e4dfd6 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:45:48 -0700
Subject: [PATCH 60/89] work

---
 test/gtest/constraint.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 35f63f21a2e..bfca3d71f00 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -295,4 +295,10 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
   AndedConstraintSet leftNe{Constraint{Ne, {Literal(int32_t(5))}}};
   checkOr(leftNe, right, empty);
 
+  // Change the GtS on the right to GtU. We fail.
+  AndedConstraintSet rightGtU(
+    {{GtU, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}});
+  checkOr(left, rightGtU, empty);
+
+
 }

From 437174c3e60dce6c9ed5b9f7a3ee9cfbb6044e9f Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:46:25 -0700
Subject: [PATCH 61/89] work

---
 test/gtest/constraint.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index bfca3d71f00..131a02a4714 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -300,5 +300,8 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
     {{GtU, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}});
   checkOr(left, rightGtU, empty);
 
-
+  // Change the LeS on the right to LeU. We fail.
+  AndedConstraintSet rightLeU(
+    {{GtS, {Literal(int32_t(5))}}, {LeU, {Literal(int32_t(42))}}});
+  checkOr(left, rightLeU, empty);
 }

From ba4f0b52f3f834a108b3056c248609eb7bb3b684 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:55:41 -0700
Subject: [PATCH 62/89] work

---
 src/ir/constraint.cpp     | 5 +++--
 test/gtest/constraint.cpp | 7 ++++++-
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 79508d6228d..181673f54c0 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -367,11 +367,12 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
 
   // Simple range fusing, add an equality to turn > into >= :
   //
-  //   { x == A } || { x > A && x <= B } , A <= B   ==>   { x >= A && X <= B }
+  //   { x == A } || { x > A && x <= B } , A < B   ==>   { x >= A && X <= B }
   //
+  // (A < B is required to avoid a contradiction on the right)
   Var A, B;
   if (auto result = Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
-                      .require(A, LeS, B)
+                      .require(A, LtS, B)
                       .checkUnordered(self, other)) {
     Term aValue = (*result)[A];
     Term bValue = (*result)[B];
diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 131a02a4714..e90d69fd5fc 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -260,7 +260,7 @@ TEST(ConstraintTest, TestOrInequality) {
 }
 
 TEST(ConstraintTest, TestOrOrDisjoint) {
-  // { x == A } || { x > A && x <= B } , A <= B   ==>   { x >= A && X <= B }
+  // { x == A } || { x > A && x <= B } , A < B   ==>   { x >= A && X <= B }
 
   AndedConstraintSet left{Constraint{Eq, {Literal(int32_t(5))}}};
 
@@ -304,4 +304,9 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
   AndedConstraintSet rightLeU(
     {{GtS, {Literal(int32_t(5))}}, {LeU, {Literal(int32_t(42))}}});
   checkOr(left, rightLeU, empty);
+
+  // Add an operation on the right, x != 21. We fail. TODO
+  AndedConstraintSet rightAdded(
+    {{GtS, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}, {Ne, {Literal(int32_t(21))}}});
+  checkOr(left, rightAdded, empty);
 }

From 8a4f04a6928045daf4967dacefbaad7e9ef3bcc7 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:55:48 -0700
Subject: [PATCH 63/89] work

---
 test/gtest/constraint.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index e90d69fd5fc..ef4a5b5347e 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -306,7 +306,8 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
   checkOr(left, rightLeU, empty);
 
   // Add an operation on the right, x != 21. We fail. TODO
-  AndedConstraintSet rightAdded(
-    {{GtS, {Literal(int32_t(5))}}, {LeS, {Literal(int32_t(42))}}, {Ne, {Literal(int32_t(21))}}});
+  AndedConstraintSet rightAdded({{GtS, {Literal(int32_t(5))}},
+                                 {LeS, {Literal(int32_t(42))}},
+                                 {Ne, {Literal(int32_t(21))}}});
   checkOr(left, rightAdded, empty);
 }

From 1b9efc0c1ee94535f5c09126ce2caf11301c29dd Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 14:56:59 -0700
Subject: [PATCH 64/89] work

---
 src/ir/constraint.cpp | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 181673f54c0..295e47cf8e1 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -374,9 +374,8 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   if (auto result = Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
                       .require(A, LtS, B)
                       .checkUnordered(self, other)) {
-    Term aValue = (*result)[A];
-    Term bValue = (*result)[B];
-    self = AndedConstraintSet({{GeS, aValue}, {LeS, bValue}});
+    auto& values = *result;
+    self = AndedConstraintSet({{GeS, values[A]}, {LeS, values[B]}});
     return true;
     // TODO: unsigned etc.
   }

From 078905013fc87fe4cd9c990e2a1b9a4e0148262c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 15:19:49 -0700
Subject: [PATCH 65/89] work

---
 src/ir/constraint.cpp | 27 +++++++++++++++++----------
 1 file changed, 17 insertions(+), 10 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 295e47cf8e1..c3aa361030c 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -208,15 +208,19 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) {
 namespace {
 
 // A variable in a match. If we see the same Var - identified by address - in
-// two places, it must be equal in them. We can also perform checks on different
-// Vars afterwards, e.g., whether one is greater than the other.
-// TODO: optimize all this, if it matters
+// two places, it must be equal in them. For example,
+//
+//  Var A;
+//  ..match expression with foo(A, A)..
+//
+// The matcher will check that foo is sent the same thing twice.
 struct Var {};
 
 // A matcher constraint: an abstraction over a normal Constraint, which can also
 // contain Vars.
 struct MatcherConstraint {
   Abstract::Op op;
+  // Var addresses are how we identify them, so we store a pointer.
   Var* term = nullptr;
 
   MatcherConstraint() = default;
@@ -237,19 +241,22 @@ struct MatcherConstraint {
 // MatcherConstraints.
 using MatcherSet = inplace_vector<MatcherConstraint, MaxConstraints>;
 
-// A matcher object. This pattern-matches over AndedConstraintSets, in a way
-// that follows the rules of logic.
+// A matcher object. This pattern-matches over abstractions of
+// AndedConstraintSets.
 struct Matcher {
   // Set up a pattern containing two sets of constraints.
   Matcher(const MatcherSet& ms1_, const MatcherSet& ms2_);
 
-  // Add a requirement on this pattern, a demand on the Vars.
+  // Add a requirement on this pattern, a demand on the Vars. For example, we
+  // can require that Var A - whatever we matched it as - is less than Var B -
+  // whatever we matched that as.
   //
   // For convenience, return this Matcher object (i.e. the builder pattern).
   Matcher& require(Var& a, Abstract::Op op, Var& b);
 
   // When a match succeeds, we return a map of Vars to Terms, allowing the user
-  // to find out what each Var matched against.
+  // to find out what each Var matched against. For example, the pattern foo(A)
+  // when matched successfully against foo(5) will provide a mapping of A to 5.
   struct VarTermMap : public std::unordered_map<Var*, Term> {
     // As a convenience, allow using the object instead of the pointer.
     Term& operator[](Var& var) {
@@ -258,9 +265,7 @@ struct Matcher {
   };
 
   // Check if the pattern matches given inputs. The order of the inputs does not
-  // matter. Returns the address of the input that matches the first of the
-  // patterns (that is, if a matches ms1 in the constructor, we return &a, and
-  // otherwise &b), or nullptr of the match failed.
+  // matter. Returns the mapping described above, if we succeed.
   std::optional<VarTermMap> checkUnordered(const AndedConstraintSet& a,
                                            const AndedConstraintSet& b) {
     return checkUnorderedInternal(a, b);
@@ -299,6 +304,8 @@ Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
 std::optional<Matcher::VarTermMap> Matcher::checkUnorderedInternal(
   const AndedConstraintSet& a, const AndedConstraintSet& b, bool flipped) {
 
+  // TODO: optimize all this for speed
+
   auto fail = [&]() -> std::optional<Matcher::VarTermMap> {
     // We failed, but try the flipped inputs if we haven't already.
     if (!flipped) {

From 5f0ad621d03471602f52266985f98e0e9439e502 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 15:20:59 -0700
Subject: [PATCH 66/89] work

---
 src/ir/constraint.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index c3aa361030c..8b4196a4eef 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -319,7 +319,7 @@ std::optional<Matcher::VarTermMap> Matcher::checkUnorderedInternal(
   }
 
   // The sizes match, at least. Parse in more detail, building up a mapping of
-  // Vars to concrete Terms
+  // Vars to concrete Terms.
   VarTermMap varTermMap;
 
   auto parse = [&](const AndedConstraintSet& input, const MatcherSet& pattern) {
@@ -353,7 +353,7 @@ std::optional<Matcher::VarTermMap> Matcher::checkUnorderedInternal(
     auto bTerm = varTermMap[*b];
 
     // Check if { x == a } proves { x op b } is true.
-    if (provesPair(Constraint{Abstract::Eq, aTerm}, Constraint{op, bTerm}) !=
+    if (provesPair({Abstract::Eq, aTerm}, {op, bTerm}) !=
         True) {
       return fail();
     }

From 242dd6e045a531a6685290aa0b18e53286b442f2 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 15:22:25 -0700
Subject: [PATCH 67/89] work

---
 src/ir/constraint.cpp | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 8b4196a4eef..c6678fcf579 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -369,7 +369,6 @@ std::optional<Matcher::VarTermMap> Matcher::checkUnorderedInternal(
 // changed (otherwise, we return nullopt).
 std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
                                           const AndedConstraintSet& other) {
-  using MC = MatcherConstraint;
   using namespace Abstract;
 
   // Simple range fusing, add an equality to turn > into >= :
@@ -378,11 +377,11 @@ std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
   //
   // (A < B is required to avoid a contradiction on the right)
   Var A, B;
-  if (auto result = Matcher({MC(Eq, A)}, {MC(GtS, A), MC(LeS, B)})
+  if (auto result = Matcher({{Eq, A}}, {{GtS, A}, {LeS, B}})
                       .require(A, LtS, B)
                       .checkUnordered(self, other)) {
     auto& values = *result;
-    self = AndedConstraintSet({{GeS, values[A]}, {LeS, values[B]}});
+    self = {{GeS, values[A]}, {LeS, values[B]}};
     return true;
     // TODO: unsigned etc.
   }

From cda9027617716dc3fca433aac805ee4ef5ba054a Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 15:26:51 -0700
Subject: [PATCH 68/89] work

---
 test/gtest/constraint.cpp | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index ef4a5b5347e..7394805c169 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -260,7 +260,7 @@ TEST(ConstraintTest, TestOrInequality) {
 }
 
 TEST(ConstraintTest, TestOrOrDisjoint) {
-  // { x == A } || { x > A && x <= B } , A < B   ==>   { x >= A && X <= B }
+  // { x == A } || { x > A && x <= B } , A < B   ==>   { x >= A && x <= B }
 
   AndedConstraintSet left{Constraint{Eq, {Literal(int32_t(5))}}};
 
@@ -279,12 +279,16 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
   AndedConstraintSet left7{Constraint{Eq, {Literal(int32_t(7))}}};
   checkOr(left7, right, right);
 
-  // Change 5 on the left to 4. Now we fail to find anything.
-  AndedConstraintSet left4{Constraint{Eq, {Literal(int32_t(4))}}};
+  // Change 5 on the left to 99. Now we fail to find anything.
+  AndedConstraintSet left99{Constraint{Eq, {Literal(int32_t(99))}}};
   AndedConstraintSet empty{};
+  checkOr(left99, right, empty);
+
+  // Change 5 on the left to 4. We fail.
+  AndedConstraintSet left4{Constraint{Eq, {Literal(int32_t(4))}}};
   checkOr(left4, right, empty);
 
-  // Change 5 on the right to 6. Again we fail to find anything.
+  // Change 5 on the right to 6. We fail.
   AndedConstraintSet right6(
     {{GtS, {Literal(int32_t(6))}}, {LeS, {Literal(int32_t(42))}}});
   checkOr(left, right6, empty);
@@ -305,7 +309,7 @@ TEST(ConstraintTest, TestOrOrDisjoint) {
     {{GtS, {Literal(int32_t(5))}}, {LeU, {Literal(int32_t(42))}}});
   checkOr(left, rightLeU, empty);
 
-  // Add an operation on the right, x != 21. We fail. TODO
+  // Add an operation on the right, x != 21. We fail. TODO: optimize here
   AndedConstraintSet rightAdded({{GtS, {Literal(int32_t(5))}},
                                  {LeS, {Literal(int32_t(42))}},
                                  {Ne, {Literal(int32_t(21))}}});

From b1419797f2b24b8ae0c0e38d9329ebc509c1ce20 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 15:27:18 -0700
Subject: [PATCH 69/89] work

---
 src/ir/constraint.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index c6678fcf579..9e42fe042dc 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -353,8 +353,7 @@ std::optional<Matcher::VarTermMap> Matcher::checkUnorderedInternal(
     auto bTerm = varTermMap[*b];
 
     // Check if { x == a } proves { x op b } is true.
-    if (provesPair({Abstract::Eq, aTerm}, {op, bTerm}) !=
-        True) {
+    if (provesPair({Abstract::Eq, aTerm}, {op, bTerm}) != True) {
       return fail();
     }
   }

From 32fa2b3ff7fbfb61025d36b863d3840391c9178c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 16:46:35 -0700
Subject: [PATCH 70/89] UNDO

---
 src/ir/constraint.cpp | 202 +-----------------------------------------
 1 file changed, 3 insertions(+), 199 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 9e42fe042dc..78cad40f2bb 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -205,192 +205,6 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) {
   //       useful to implement that).
 }
 
-namespace {
-
-// A variable in a match. If we see the same Var - identified by address - in
-// two places, it must be equal in them. For example,
-//
-//  Var A;
-//  ..match expression with foo(A, A)..
-//
-// The matcher will check that foo is sent the same thing twice.
-struct Var {};
-
-// A matcher constraint: an abstraction over a normal Constraint, which can also
-// contain Vars.
-struct MatcherConstraint {
-  Abstract::Op op;
-  // Var addresses are how we identify them, so we store a pointer.
-  Var* term = nullptr;
-
-  MatcherConstraint() = default;
-  MatcherConstraint(Abstract::Op op, Var& term) : op(op), term(&term) {}
-
-  bool operator==(const MatcherConstraint&) const = default;
-  bool operator<(const MatcherConstraint& other) const {
-    // Ordered in a parallel way to Constraints, so that when we compare, things
-    // line up.
-    if (op != other.op) {
-      return op < other.op;
-    }
-    return term < other.term;
-  }
-};
-
-// A matcher AndedConstraintSet, which abstracts over the normal one to support
-// MatcherConstraints.
-using MatcherSet = inplace_vector<MatcherConstraint, MaxConstraints>;
-
-// A matcher object. This pattern-matches over abstractions of
-// AndedConstraintSets.
-struct Matcher {
-  // Set up a pattern containing two sets of constraints.
-  Matcher(const MatcherSet& ms1_, const MatcherSet& ms2_);
-
-  // Add a requirement on this pattern, a demand on the Vars. For example, we
-  // can require that Var A - whatever we matched it as - is less than Var B -
-  // whatever we matched that as.
-  //
-  // For convenience, return this Matcher object (i.e. the builder pattern).
-  Matcher& require(Var& a, Abstract::Op op, Var& b);
-
-  // When a match succeeds, we return a map of Vars to Terms, allowing the user
-  // to find out what each Var matched against. For example, the pattern foo(A)
-  // when matched successfully against foo(5) will provide a mapping of A to 5.
-  struct VarTermMap : public std::unordered_map<Var*, Term> {
-    // As a convenience, allow using the object instead of the pointer.
-    Term& operator[](Var& var) {
-      return std::unordered_map<Var*, Term>::operator[](&var);
-    }
-  };
-
-  // Check if the pattern matches given inputs. The order of the inputs does not
-  // matter. Returns the mapping described above, if we succeed.
-  std::optional<VarTermMap> checkUnordered(const AndedConstraintSet& a,
-                                           const AndedConstraintSet& b) {
-    return checkUnorderedInternal(a, b);
-  }
-
-private:
-  std::optional<VarTermMap> checkUnorderedInternal(const AndedConstraintSet& a,
-                                                   const AndedConstraintSet& b,
-                                                   bool flipped = false);
-
-  MatcherSet ms1;
-  MatcherSet ms2;
-
-  struct Requirement {
-    Var* a;
-    Abstract::Op op;
-    Var* b;
-  };
-
-  SmallVector<Requirement, 2> requirements;
-};
-
-Matcher::Matcher(const MatcherSet& ms1_, const MatcherSet& ms2_)
-  : ms1(ms1_), ms2(ms2_) {
-  // Sort the sets like Constraints are sorted, so that when we compare, things
-  // line up.
-  std::sort(ms1.begin(), ms1.end());
-  std::sort(ms2.begin(), ms2.end());
-}
-
-Matcher& Matcher::require(Var& a, Abstract::Op op, Var& b) {
-  requirements.push_back({&a, op, &b});
-  return *this;
-}
-
-std::optional<Matcher::VarTermMap> Matcher::checkUnorderedInternal(
-  const AndedConstraintSet& a, const AndedConstraintSet& b, bool flipped) {
-
-  // TODO: optimize all this for speed
-
-  auto fail = [&]() -> std::optional<Matcher::VarTermMap> {
-    // We failed, but try the flipped inputs if we haven't already.
-    if (!flipped) {
-      return checkUnorderedInternal(b, a, true);
-    }
-    return {};
-  };
-
-  if (a.size() != ms1.size() || b.size() != ms2.size()) {
-    return fail();
-  }
-
-  // The sizes match, at least. Parse in more detail, building up a mapping of
-  // Vars to concrete Terms.
-  VarTermMap varTermMap;
-
-  auto parse = [&](const AndedConstraintSet& input, const MatcherSet& pattern) {
-    for (Index i = 0; i < input.size(); i++) {
-      // The operation must match.
-      if (input[i].op != pattern[i].op) {
-        return false;
-      }
-
-      // The term must match, or define a new unknown value.
-      auto [iter, inserted] =
-        varTermMap.insert({pattern[i].term, input[i].term});
-      if (!inserted) {
-        // The Var in the pattern is already mapped and known. The input here
-        // must match the prior appearance.
-        if (input[i].term != iter->second) {
-          return false;
-        }
-      }
-    }
-    return true;
-  };
-
-  if (!parse(a, ms1) || !parse(b, ms2)) {
-    return fail();
-  }
-
-  // Check requirements on the vars.
-  for (auto& [a, op, b] : requirements) {
-    auto aTerm = varTermMap[*a];
-    auto bTerm = varTermMap[*b];
-
-    // Check if { x == a } proves { x op b } is true.
-    if (provesPair({Abstract::Eq, aTerm}, {op, bTerm}) != True) {
-      return fail();
-    }
-  }
-
-  return varTermMap;
-}
-
-// Do an approximate OR on two inputs that are disjoint, that is, each proves
-// the other false.
-//
-// If we recognize a pattern, we update |self| and return whether anything
-// changed (otherwise, we return nullopt).
-std::optional<bool> approximateOrDisjoint(AndedConstraintSet& self,
-                                          const AndedConstraintSet& other) {
-  using namespace Abstract;
-
-  // Simple range fusing, add an equality to turn > into >= :
-  //
-  //   { x == A } || { x > A && x <= B } , A < B   ==>   { x >= A && X <= B }
-  //
-  // (A < B is required to avoid a contradiction on the right)
-  Var A, B;
-  if (auto result = Matcher({{Eq, A}}, {{GtS, A}, {LeS, B}})
-                      .require(A, LtS, B)
-                      .checkUnordered(self, other)) {
-    auto& values = *result;
-    self = {{GeS, values[A]}, {LeS, values[B]}};
-    return true;
-    // TODO: unsigned etc.
-  }
-
-  // Otherwise, we have no idea.
-  return {};
-}
-
-} // anonymous namespace
-
 bool AndedConstraintSet::approximateOr(const AndedConstraintSet& other) {
   // If one proves everything, the only thing that matters is the other.
   if (other.provesEverything()) {
@@ -404,28 +218,18 @@ bool AndedConstraintSet::approximateOr(const AndedConstraintSet& other) {
   // If this is already implied by current constraints, then it is redundant.
   // E.g. if we are { x = 10 } and other is { x >= 0 } then all we need is
   // { x >= 0 } as the result of the OR.
-  auto otherProves = other.proves(*this);
-  if (otherProves == True) {
+  if (other.proves(*this) == True) {
     return false;
   }
-  auto thisProves = proves(other);
-  if (thisProves == True) {
+  if (proves(other) == True) {
     *this = other;
     return true;
   }
 
-  if (otherProves == False && thisProves == False) {
-    if (auto result = approximateOrDisjoint(*this, other)) {
-      return *result;
-    }
-  }
-  // TODO more smarts: handle <= > and so forth
+  // 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.
-  // TODO: We could keep constraints that appear on both sides and only drop the
-  //       others. In fact, we could do that first, and leave smarts only to the
-  //       others.
   clear();
   return true;
 }

From 51cf381c4ffdac06c29c9f4ffc46976c4d5718d5 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 16:51:51 -0700
Subject: [PATCH 71/89] go

---
 src/ir/constraint.cpp | 29 +++++++++++++++++++++++------
 1 file changed, 23 insertions(+), 6 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 78cad40f2bb..58f355d1ab3 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -205,6 +205,24 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) {
   //       useful to implement that).
 }
 
+namespace {
+
+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)
+  //
+  // 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());
+
+}
+
+} // 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 +244,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) {

From 60d3fdf9040da5b00dc1530cf69300a7ffb1cd98 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 17:00:57 -0700
Subject: [PATCH 72/89] go

---
 src/ir/constraint.cpp | 42 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 42 insertions(+)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 58f355d1ab3..701c73e7cdd 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -207,6 +207,38 @@ void AndedConstraintSet::approximateAnd(const Constraint& c) {
 
 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> approximateOrTermedPair(const Constraint& a, const Constraint &b) {
+  using namespace Abstract;
+
+  // x == C || x > C  ===  x >= C
+  if (a.op == Eq && b.op == GtS) {
+    return Constraint{GeS, a.term};
+  }
+
+  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 = approximateOrTermedPair(a, b)) {
+      return result;
+    }
+  }
+
+  // TODO: more smarts
+
+  if (!recursing) {
+    // The flipped form may be recognized.
+    return approximateOrPair(b, a);
+  }
+}
+
+// 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:
@@ -219,6 +251,16 @@ AndedConstraintSet detailedApproximateOr(const AndedConstraintSet& a, const Ande
   // not contradictions.
   assert(!a.provesEverything() && !b.provesEverything());
 
+  AndedConstraintSet result;
+  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

From 8362896e2bd69110a94e751574a9295fb119cac2 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Thu, 23 Jul 2026 17:01:05 -0700
Subject: [PATCH 73/89] form

---
 src/ir/constraint.cpp | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 701c73e7cdd..a931a534c65 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -209,7 +209,8 @@ 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> approximateOrTermedPair(const Constraint& a, const Constraint &b) {
+std::optional<Constraint> approximateOrTermedPair(const Constraint& a,
+                                                  const Constraint& b) {
   using namespace Abstract;
 
   // x == C || x > C  ===  x >= C
@@ -222,7 +223,9 @@ std::optional<Constraint> approximateOrTermedPair(const Constraint& a, const Con
 
 // 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) {
+std::optional<Constraint> approximateOrPair(const Constraint& a,
+                                            const Constraint& b,
+                                            bool recursing = false) {
   if (a.term == b.term) {
     if (auto result = approximateOrTermedPair(a, b)) {
       return result;
@@ -239,7 +242,8 @@ std::optional<Constraint> approximateOrPair(const Constraint& a, const Constrain
 
 // Do an OR in full detail, looking at every constraint in each of the given
 // sets.
-AndedConstraintSet detailedApproximateOr(const AndedConstraintSet& a, const AndedConstraintSet& b) {
+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:
   //

From d350b97155a14a477b0b867d2a9dee1a83b08098 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 08:44:20 -0700
Subject: [PATCH 74/89] work

---
 src/ir/constraint.cpp     |  8 +++++++-
 test/gtest/constraint.cpp | 14 ++++++++++++--
 2 files changed, 19 insertions(+), 3 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index a931a534c65..99b15a8f7d0 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -236,8 +236,10 @@ std::optional<Constraint> approximateOrPair(const Constraint& a,
 
   if (!recursing) {
     // The flipped form may be recognized.
-    return approximateOrPair(b, a);
+    return approximateOrPair(b, a, true);
   }
+
+  return {};
 }
 
 // Do an OR in full detail, looking at every constraint in each of the given
@@ -250,12 +252,16 @@ AndedConstraintSet detailedApproximateOr(const AndedConstraintSet& a,
   // (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());
 
   AndedConstraintSet result;
+  result.setProvesNothing();
   for (auto& ac : a) {
     for (auto& bc : b) {
       if (auto combined = approximateOrPair(ac, bc)) {
diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 7394805c169..7823acb6c80 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -243,6 +243,7 @@ TEST(ConstraintTest, TestDeredundancy) {
 static void checkOr(const AndedConstraintSet& a,
                     const AndedConstraintSet& b,
                     const AndedConstraintSet& result) {
+std::cout << "checkOr " << a << " || " << b << '\n';
   auto ored = a;
   ored.approximateOr(b);
   EXPECT_EQ(ored, result);
@@ -257,10 +258,19 @@ TEST(ConstraintTest, TestOrInequality) {
   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, TestOrOrDisjoint) {
-  // { x == A } || { x > A && x <= B } , A < B   ==>   { x >= A && x <= B }
+TEST(ConstraintTest, TestOrLoop) {
+  // Check common loop patterns:
+  // { x == A } || { x > A && x <= B }   ==>   { x >= A && x <= B }
 
   AndedConstraintSet left{Constraint{Eq, {Literal(int32_t(5))}}};
 

From b56f4669e6eb945b2bbe6b7d201374ff0163e277 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:02:32 -0700
Subject: [PATCH 75/89] work

---
 src/ir/constraint.cpp | 50 ++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 47 insertions(+), 3 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 99b15a8f7d0..4db685b063d 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -209,8 +209,8 @@ 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> approximateOrTermedPair(const Constraint& a,
-                                                  const Constraint& b) {
+std::optional<Constraint> approximateOrTermEqualPair(const Constraint& a,
+                                                     const Constraint& b) {
   using namespace Abstract;
 
   // x == C || x > C  ===  x >= C
@@ -221,17 +221,61 @@ std::optional<Constraint> approximateOrTermedPair(const Constraint& a,
   return {};
 }
 
+std::optional<Constraint> approximateOrConstantPair(Abstract::Op aOp,
+                          const Literal& aConstant,
+                          Abstract::Op bOp,
+                          const Literal& bConstant) {
+  // a == A =?=> a op B. Simply apply A to the operation against B.
+  if (aOp == Abstract::Eq) {
+XXX
+    switch (bOp) {
+      case Abstract::Eq:
+        return TrueFalse(aConstant == bConstant);
+      case Abstract::Ne:
+        return TrueFalse(aConstant != bConstant);
+      case Abstract::LtS:
+        return TrueFalse(aConstant.ltS(bConstant));
+      case Abstract::LeS:
+        return TrueFalse(aConstant.leS(bConstant));
+      case Abstract::GtS:
+        return TrueFalse(aConstant.gtS(bConstant));
+      case Abstract::GeS:
+        return TrueFalse(aConstant.geS(bConstant));
+      case Abstract::LtU:
+        return TrueFalse(aConstant.ltU(bConstant));
+      case Abstract::LeU:
+        return TrueFalse(aConstant.leU(bConstant));
+      case Abstract::GtU:
+        return TrueFalse(aConstant.gtU(bConstant));
+      case Abstract::GeU:
+        return TrueFalse(aConstant.geU(bConstant));
+      default: {
+      }
+    }
+  }
+
+}
+
 // 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 = approximateOrTermedPair(a, b)) {
+    if (auto result = approximateOrTermEqualPair(a, b)) {
       return result;
     }
   }
 
+  if (auto* ac = std::get_if<Literal>(&a.term)) {
+    if (auto* bc = std::get_if<Literal>(&b.term)) {
+      // If a proves b, e.g. x = 5 proves x >= 0 is true, then the OR is b.
+      if (provesConstantPair(a.op, *ac, b.op, *bc) == True) {
+        return b;
+      }
+    }
+  }
+
   // TODO: more smarts
 
   if (!recursing) {

From c536d88c43a187ad631d668dbb382a09ddf146f8 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:06:16 -0700
Subject: [PATCH 76/89] work

---
 src/ir/constraint.cpp     | 35 -----------------------------------
 test/gtest/constraint.cpp |  9 ++++++---
 2 files changed, 6 insertions(+), 38 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 4db685b063d..47daea0f8a8 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -221,41 +221,6 @@ std::optional<Constraint> approximateOrTermEqualPair(const Constraint& a,
   return {};
 }
 
-std::optional<Constraint> approximateOrConstantPair(Abstract::Op aOp,
-                          const Literal& aConstant,
-                          Abstract::Op bOp,
-                          const Literal& bConstant) {
-  // a == A =?=> a op B. Simply apply A to the operation against B.
-  if (aOp == Abstract::Eq) {
-XXX
-    switch (bOp) {
-      case Abstract::Eq:
-        return TrueFalse(aConstant == bConstant);
-      case Abstract::Ne:
-        return TrueFalse(aConstant != bConstant);
-      case Abstract::LtS:
-        return TrueFalse(aConstant.ltS(bConstant));
-      case Abstract::LeS:
-        return TrueFalse(aConstant.leS(bConstant));
-      case Abstract::GtS:
-        return TrueFalse(aConstant.gtS(bConstant));
-      case Abstract::GeS:
-        return TrueFalse(aConstant.geS(bConstant));
-      case Abstract::LtU:
-        return TrueFalse(aConstant.ltU(bConstant));
-      case Abstract::LeU:
-        return TrueFalse(aConstant.leU(bConstant));
-      case Abstract::GtU:
-        return TrueFalse(aConstant.gtU(bConstant));
-      case Abstract::GeU:
-        return TrueFalse(aConstant.geU(bConstant));
-      default: {
-      }
-    }
-  }
-
-}
-
 // 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,
diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 7823acb6c80..9f981f3c176 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -289,13 +289,16 @@ TEST(ConstraintTest, TestOrLoop) {
   AndedConstraintSet left7{Constraint{Eq, {Literal(int32_t(7))}}};
   checkOr(left7, right, right);
 
-  // Change 5 on the left to 99. Now we fail to find anything.
+  // Change 5 on the left to 99:
+  // { x == 99 } || { x > 5 && x <= 42 }   ==>   { x > 5 }
   AndedConstraintSet left99{Constraint{Eq, {Literal(int32_t(99))}}};
-  AndedConstraintSet empty{};
-  checkOr(left99, right, empty);
+  AndedConstraintSet rightOnly5{Constraint{GtS, {Literal(int32_t(5))}}};
+  checkOr(left99, right, rightOnly5);
 
   // Change 5 on the left to 4. We fail.
   AndedConstraintSet left4{Constraint{Eq, {Literal(int32_t(4))}}};
+  AndedConstraintSet empty;
+  empty.setProvesNothing();
   checkOr(left4, right, empty);
 
   // Change 5 on the right to 6. We fail.

From 0f48d73af1f5349377f096a08a7f5697f976d34f Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:08:16 -0700
Subject: [PATCH 77/89] work

---
 test/gtest/constraint.cpp | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 9f981f3c176..817cf6dbb46 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -295,15 +295,17 @@ TEST(ConstraintTest, TestOrLoop) {
   AndedConstraintSet rightOnly5{Constraint{GtS, {Literal(int32_t(5))}}};
   checkOr(left99, right, rightOnly5);
 
-  // Change 5 on the left to 4. We fail.
+  // Change 5 on the left to 4:
+  // { x == 4 } || { x > 5 && x <= 42 }   ==>   { x <= 42 }
   AndedConstraintSet left4{Constraint{Eq, {Literal(int32_t(4))}}};
-  AndedConstraintSet empty;
-  empty.setProvesNothing();
-  checkOr(left4, right, empty);
+  AndedConstraintSet rightOnly42({{LeS, {Literal(int32_t(42))}}});
+  checkOr(left4, right, rightOnly42);
 
   // Change 5 on the right to 6. We fail.
   AndedConstraintSet right6(
     {{GtS, {Literal(int32_t(6))}}, {LeS, {Literal(int32_t(42))}}});
+  AndedConstraintSet empty;
+  empty.setProvesNothing();
   checkOr(left, right6, empty);
 
   // Changes to operations:

From d8747d79db3df33e6743c9a2eb071c876bf3620c Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:10:57 -0700
Subject: [PATCH 78/89] work

---
 test/gtest/constraint.cpp | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 817cf6dbb46..6c5c13f53fb 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -272,20 +272,18 @@ 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 }
   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. 7 is in the range on the right, so we end up
-  // with the right.
+  // Change 5 on the left to 7:
+  // { x == 7 } || { x > 5 && x <= 42 }   ==>   { x > 5 }
   AndedConstraintSet left7{Constraint{Eq, {Literal(int32_t(7))}}};
   checkOr(left7, right, right);
 
@@ -301,17 +299,18 @@ TEST(ConstraintTest, TestOrLoop) {
   AndedConstraintSet rightOnly42({{LeS, {Literal(int32_t(42))}}});
   checkOr(left4, right, rightOnly42);
 
-  // Change 5 on the right to 6. We fail.
+  // 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))}}});
-  AndedConstraintSet empty;
-  empty.setProvesNothing();
-  checkOr(left, right6, empty);
+  checkOr(left, right6, rightOnly42);
 
   // Changes to operations:
 
   // Change the Eq on the left to Ne. We fail.
   AndedConstraintSet leftNe{Constraint{Ne, {Literal(int32_t(5))}}};
+  AndedConstraintSet empty;
+  empty.setProvesNothing();
   checkOr(leftNe, right, empty);
 
   // Change the GtS on the right to GtU. We fail.

From 09ebda294faa1a3307b98a4a4aa85212c6df2c57 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:17:25 -0700
Subject: [PATCH 79/89] work

---
 test/gtest/constraint.cpp | 26 +++++++++++++++++---------
 1 file changed, 17 insertions(+), 9 deletions(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 6c5c13f53fb..0faf818fe50 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -307,25 +307,33 @@ TEST(ConstraintTest, TestOrLoop) {
 
   // Changes to operations:
 
-  // Change the Eq on the left to Ne. We fail.
+  // Change the Eq on the left to Ne. We fail to find anything for the OR.
   AndedConstraintSet leftNe{Constraint{Ne, {Literal(int32_t(5))}}};
-  AndedConstraintSet empty;
-  empty.setProvesNothing();
+  auto empty = AndedConstraintSet::makeProvesNothing();
   checkOr(leftNe, right, empty);
 
-  // Change the GtS on the right to GtU. We fail.
+  // 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, empty);
+  checkOr(left, rightGtU, rightOnly42);
 
-  // Change the LeS on the right to LeU. We fail.
+  // 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))}}});
-  checkOr(left, rightLeU, empty);
+  AndedConstraintSet rightGesLeU(
+    {{GeS, {Literal(int32_t(5))}}, {LeU, {Literal(int32_t(42))}}});
+  checkOr(left, rightLeU, rightGesLeU);
 
-  // Add an operation on the right, x != 21. We fail. TODO: optimize here
+  // 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))}}});
-  checkOr(left, rightAdded, empty);
+  AndedConstraintSet resultAdded({{GeS, {Literal(int32_t(5))}},
+                                  {LeS, {Literal(int32_t(42))}},
+                                  {Ne, {Literal(int32_t(21))}}});
+  checkOr(left, rightAdded, resultAdded);
 }

From 5d4a89fdd9161853bd6b9680020b52775850eb38 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:18:04 -0700
Subject: [PATCH 80/89] work

---
 test/gtest/constraint.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index 0faf818fe50..d364bf2a68e 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -243,7 +243,6 @@ TEST(ConstraintTest, TestDeredundancy) {
 static void checkOr(const AndedConstraintSet& a,
                     const AndedConstraintSet& b,
                     const AndedConstraintSet& result) {
-std::cout << "checkOr " << a << " || " << b << '\n';
   auto ored = a;
   ored.approximateOr(b);
   EXPECT_EQ(ored, result);

From 7cd6884d6de0168340e229ba51ec5b63b919c998 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:18:11 -0700
Subject: [PATCH 81/89] work

---
 test/gtest/constraint.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index d364bf2a68e..e511b073551 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -326,7 +326,7 @@ TEST(ConstraintTest, TestOrLoop) {
   checkOr(left, rightLeU, rightGesLeU);
 
   // Add an operation on the right, x != 21:
-  // { x == 5 } || { x >  5 && x <= 42 && 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))}},

From 9b7cac85346c6bd8f314be1413508d1d7133be10 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:20:58 -0700
Subject: [PATCH 82/89] work

---
 test/lit/passes/constraint-analysis-loops.wast | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/test/lit/passes/constraint-analysis-loops.wast b/test/lit/passes/constraint-analysis-loops.wast
index 75ed4711729..5d90de1096f 100644
--- a/test/lit/passes/constraint-analysis-loops.wast
+++ b/test/lit/passes/constraint-analysis-loops.wast
@@ -162,7 +162,7 @@
   ;; CHECK-NEXT:   (drop
   ;; CHECK-NEXT:    (i32.le_s
   ;; CHECK-NEXT:     (local.get $x)
-  ;; CHECK-NEXT:     (i32.const 100)
+  ;; CHECK-NEXT:     (local.get $p)
   ;; CHECK-NEXT:    )
   ;; CHECK-NEXT:   )
   ;; CHECK-NEXT:   (local.set $x
@@ -189,12 +189,9 @@
   ;; CHECK-NEXT: )
   (func $bound-nonconstant-no (param $p i32)
     (local $x i32)
-    ;; As above, but rather than zero we have an unknown param $p. We can't
-    ;; optimize since we don't know how $p relates to 100: if $p is negative,
-    ;; we have something like {x == 200} || {x > 200 && x <= 100}. The RHS is
-    ;; a contradiction (at runtime), and we don't want to get into the
-    ;; complexity of reasoning about such things, so we do not optimize here.
+    ;; As above, but rather than zero we have an unknown param $p.
     (loop $loop
+      ;; We can infer nothing here, as p is unknown, and x might be 0 or <= 100.
       (drop
         (i32.ge_s
           (local.get $x)
@@ -204,7 +201,7 @@
       (drop
         (i32.le_s
           (local.get $x)
-          (i32.const 100)
+          (local.get $p)
         )
       )
       (local.set $x

From 8678398a87120e7988daf5d4da702d88181faf34 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:23:02 -0700
Subject: [PATCH 83/89] work

---
 src/ir/constraint.cpp | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 47daea0f8a8..23680bae888 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -209,15 +209,16 @@ 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 Constraint& a,
-                                                     const Constraint& b) {
+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 (a.op == Eq && b.op == GtS) {
-    return Constraint{GeS, a.term};
+  if (aOp == Eq && bOp == GtS) {
+    return Constraint{GeS, term};
   }
 
+  // TODO: all the rest
+
   return {};
 }
 
@@ -227,7 +228,7 @@ std::optional<Constraint> approximateOrPair(const Constraint& a,
                                             const Constraint& b,
                                             bool recursing = false) {
   if (a.term == b.term) {
-    if (auto result = approximateOrTermEqualPair(a, b)) {
+    if (auto result = approximateOrTermEqualPair(a.op, b.op, a.term)) {
       return result;
     }
   }

From b11e9844c28b72251a4bc389acaa6c5a838f82a3 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:24:33 -0700
Subject: [PATCH 84/89] work

---
 src/ir/constraint.cpp | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 23680bae888..3aa86feeac5 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -233,13 +233,9 @@ std::optional<Constraint> approximateOrPair(const Constraint& a,
     }
   }
 
-  if (auto* ac = std::get_if<Literal>(&a.term)) {
-    if (auto* bc = std::get_if<Literal>(&b.term)) {
-      // If a proves b, e.g. x = 5 proves x >= 0 is true, then the OR is b.
-      if (provesConstantPair(a.op, *ac, b.op, *bc) == True) {
-        return b;
-      }
-    }
+  // 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

From 0069b7ab9fb0bac973ee2ae448eaef746db74465 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:24:51 -0700
Subject: [PATCH 85/89] work

---
 src/ir/constraint.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 3aa86feeac5..46db76488b8 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -209,7 +209,9 @@ 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) {
+std::optional<Constraint> approximateOrTermEqualPair(const Abstract::Op aOp,
+                                                     const Abstract::Op bOp,
+                                                     const Term& term) {
   using namespace Abstract;
 
   // x == C || x > C  ===  x >= C

From 2ce896fb58bdd00d24c2eccf6259d80cdc2e9af4 Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 09:25:34 -0700
Subject: [PATCH 86/89] work

---
 src/ir/constraint.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/ir/constraint.cpp b/src/ir/constraint.cpp
index 46db76488b8..6b60512abfc 100644
--- a/src/ir/constraint.cpp
+++ b/src/ir/constraint.cpp
@@ -268,8 +268,7 @@ AndedConstraintSet detailedApproximateOr(const AndedConstraintSet& a,
   // not contradictions.
   assert(!a.provesEverything() && !b.provesEverything());
 
-  AndedConstraintSet result;
-  result.setProvesNothing();
+  auto result = AndedConstraintSet::makeProvesNothing();
   for (auto& ac : a) {
     for (auto& bc : b) {
       if (auto combined = approximateOrPair(ac, bc)) {

From d6599aa09d709a549ee5ea019f1330d10b66370a Mon Sep 17 00:00:00 2001
From: Alon Zakai <alonzakai@gmail.com>
Date: Fri, 24 Jul 2026 10:11:57 -0700
Subject: [PATCH 87/89] Update test/gtest/constraint.cpp

Co-authored-by: Thomas Lively <tlively123@gmail.com>
---
 test/gtest/constraint.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index e511b073551..d8fedcd190b 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -271,7 +271,7 @@ 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 == 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))}}});

From 128e9f4e48ad8666fbcda48a2383e13988a28755 Mon Sep 17 00:00:00 2001
From: Alon Zakai <alonzakai@gmail.com>
Date: Fri, 24 Jul 2026 10:12:19 -0700
Subject: [PATCH 88/89] Update test/gtest/constraint.cpp

Co-authored-by: Thomas Lively <tlively123@gmail.com>
---
 test/gtest/constraint.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index d8fedcd190b..c5113d48f85 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -282,7 +282,7 @@ TEST(ConstraintTest, TestOrLoop) {
   // Changes to constants:
 
   // Change 5 on the left to 7:
-  // { x == 7 } || { x > 5 && x <= 42 }   ==>   { x > 5 }
+  // { x == 7 } || { x > 5 && x <= 42 }   ==>   { x > 5 && x <= 42}
   AndedConstraintSet left7{Constraint{Eq, {Literal(int32_t(7))}}};
   checkOr(left7, right, right);
 

From e11289e0cd4a86940f24d294c57350ebb9af2e9f Mon Sep 17 00:00:00 2001
From: Alon Zakai <azakai@google.com>
Date: Fri, 24 Jul 2026 10:16:30 -0700
Subject: [PATCH 89/89] work

---
 test/gtest/constraint.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/test/gtest/constraint.cpp b/test/gtest/constraint.cpp
index c5113d48f85..ce25048f59b 100644
--- a/test/gtest/constraint.cpp
+++ b/test/gtest/constraint.cpp
@@ -288,12 +288,14 @@ TEST(ConstraintTest, TestOrLoop) {
 
   // 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);
@@ -307,6 +309,8 @@ TEST(ConstraintTest, TestOrLoop) {
   // 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);