Factor out weaken_condition_under_domain and document logic

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

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 {

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