diff --git a/src/Solve.cpp b/src/Solve.cpp index 8b976fbcaabe..190e6e620c55 100644 --- a/src/Solve.cpp +++ b/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); diff --git a/test/correctness/solve.cpp b/test/correctness/solve.cpp index 606bfdcb1a64..33ed7d2f3ce6 100644 --- a/test/correctness/solve.cpp +++ b/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() {