Solve: treat min/max of booleans as And/Or in SolveForInterval

src/Solve.cpp

@@ -973,6 +973,22 @@ class SolveForInterval : public IRVisitor {
         equiv.accept(this);
     }
 
+    void visit(const Min *op) override {
+        // min of bools is a logical And. These arise from
+        // and_condition_over_domain and the simplifier. Treat it as such so
+        // that Not distributes correctly (otherwise !min(a, b) is mis-solved).
+        internal_assert(op->type.is_bool());
+        Expr equiv = op->a && op->b;
+        equiv.accept(this);
+    }
+
+    void visit(const Max *op) override {
+        // max of bools is a logical Or.
+        internal_assert(op->type.is_bool());
+        Expr equiv = op->a || op->b;
+        equiv.accept(this);
+    }
+
     void visit(const Not *op) override {
         target = !target;
         op->a.accept(this);

test/correctness/solve.cpp

@@ -420,6 +420,20 @@ void test_interval_solutions() {
 
     check_inner_interval(x / 5 < 17, Interval::neg_inf(), 84);
     check_outer_interval(x / 5 < 17, Interval::neg_inf(), 84);
+
+    // min/max of booleans are logical And/Or (and_condition_over_domain and the
+    // simplifier produce these). Solving must treat them as such so that Not
+    // distributes (De Morgan). Regression: !min(...) was solved like !a && !b
+    // instead of !a || !b.
+    // min(x<0, x<2) == (x<0), so !min(...) == (x>=0):
+    check_inner_interval(!min(x < 0, x < 2), 0, Interval::pos_inf());
+    check_outer_interval(!min(x < 0, x < 2), 0, Interval::pos_inf());
+    // max(x<0, x<2) == (x<2), so !max(...) == (x>=2):
+    check_inner_interval(!max(x < 0, x < 2), 2, Interval::pos_inf());
+    check_outer_interval(!max(x < 0, x < 2), 2, Interval::pos_inf());
+    // Non-negated forms: min(x<5,x<9) == (x<5); max(x<5,x<9) == (x<9):
+    check_outer_interval(min(x < 5, x < 9), Interval::neg_inf(), 4);
+    check_outer_interval(max(x < 5, x < 9), Interval::neg_inf(), 8);
 }
 
 void test_and_condition_over_domain() {