From 06548a9207307f262dfc12aa260693e2515c45cc Mon Sep 17 00:00:00 2001
From: Alex Reinking <areinking@adobe.com>
Date: Wed, 11 Dec 2024 15:40:29 -0500
Subject: [PATCH] Factor out weaken_condition_under_domain and document logic

---
 src/Func.cpp  | 2 +-
 src/Solve.cpp | 4 ++++
 src/Solve.h   | 7 +++++++
 3 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/Func.cpp b/src/Func.cpp
index 532fed44481b..6c522c6a13e6 100644
--- a/src/Func.cpp
+++ b/src/Func.cpp
@@ -874,7 +874,7 @@ Func Stage::rfactor(const vector<pair<RVar, Var>> &preserved) {
         for (const auto &[var, min, extent] : intermediate_rdom.domain()) {
             intm_rdom.push(var, Interval{min, min + extent - 1});
         }
-        preserved_rdom.set_predicate(simplify(!and_condition_over_domain(simplify(substitute(preserved_map, !preserved_rdom.predicate())), intm_rdom)));
+        preserved_rdom.set_predicate(weaken_condition_under_domain(substitute(preserved_map, preserved_rdom.predicate()), intm_rdom));
     }
 
     // Intermediate func
diff --git a/src/Solve.cpp b/src/Solve.cpp
index 10e6232e379d..e69228781095 100644
--- a/src/Solve.cpp
+++ b/src/Solve.cpp
@@ -1239,6 +1239,10 @@ Expr and_condition_over_domain(const Expr &e, const Scope<Interval> &varying) {
     return simplify(bounds.min);
 }
 
+Expr weaken_condition_under_domain(const Expr &c, const Scope<Interval> &varying) {
+    return simplify(!and_condition_over_domain(simplify(!c), varying));
+}
+
 // Testing code
 
 namespace {
diff --git a/src/Solve.h b/src/Solve.h
index ff5124e508c6..b591aafe1790 100644
--- a/src/Solve.h
+++ b/src/Solve.h
@@ -47,6 +47,13 @@ Interval solve_for_inner_interval(const Expr &c, const std::string &variable);
  * 'and' over the vector lanes, and return a scalar result. */
 Expr and_condition_over_domain(const Expr &c, const Scope<Interval> &varying);
 
+/** Take a conditional that includes variables that vary over some
+ * domain, and convert it to a weaker (less frequently false) condition
+ * that doesn't depend on those variables. Formally, the input expr
+ * implies the output expr. Note that this function might be unable to
+ * provide a better response than simply const_true(). */
+Expr weaken_condition_under_domain(const Expr &c, const Scope<Interval> &varying);
+
 void solve_test();
 
 }  // namespace Internal