From ed2c64208d4284682fbee15a90cafc14bd5931d4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 4 Jun 2026 18:21:26 -0700 Subject: [PATCH] intervals Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_derive.cpp | 291 +++++--------------------------- src/ast/rewriter/seq_derive.h | 1 - 2 files changed, 42 insertions(+), 250 deletions(-) diff --git a/src/ast/rewriter/seq_derive.cpp b/src/ast/rewriter/seq_derive.cpp index 3b8fc5aa7..97aadb850 100644 --- a/src/ast/rewriter/seq_derive.cpp +++ b/src/ast/rewriter/seq_derive.cpp @@ -1021,63 +1021,6 @@ namespace seq { // Evaluate a single atomic condition (char_le or equality) against path constraints. // Returns l_true if path implies cond, l_false if path contradicts cond, l_undef otherwise. - lbool derive::eval_path_cond(path_t const& path, expr* c) { - expr* c_lhs = nullptr, * c_rhs = nullptr; - if (!m_util.is_char_le(c, c_lhs, c_rhs)) - return l_undef; - - unsigned c_lo = 0, c_hi = 0; - for (auto const& [cond, sign] : path) { - expr* p_lhs = nullptr, * p_rhs = nullptr; - if (!m_util.is_char_le(cond, p_lhs, p_rhs)) - continue; - unsigned p_lo = 0, p_hi = 0; - if (sign) { - // cond is negated: ¬cond is true - // ¬(x <= hi) means x > hi, i.e., x >= hi+1 - if (p_lhs == m_ele && m_util.is_const_char(p_rhs, p_hi)) { - // We know x > p_hi (i.e., x >= p_hi+1) - // c is (lo <= x): if lo <= p_hi+1 → c is true (since x >= p_hi+1 >= lo) - if (m_util.is_const_char(c_lhs, c_lo) && c_rhs == m_ele && c_lo <= p_hi + 1) - return l_true; - // c is (x <= hi2): if hi2 <= p_hi → c is false (since x > p_hi >= hi2) - if (c_lhs == m_ele && m_util.is_const_char(c_rhs, c_hi) && c_hi <= p_hi) - return l_false; - } - // ¬(lo <= x) means x < lo, i.e., x <= lo-1 - if (m_util.is_const_char(p_lhs, p_lo) && p_rhs == m_ele && p_lo > 0) { - // We know x < p_lo (i.e., x <= p_lo-1) - // c is (x <= hi): if hi >= p_lo-1 → c is true (since x <= p_lo-1 <= hi) - if (c_lhs == m_ele && m_util.is_const_char(c_rhs, c_hi) && c_hi >= p_lo - 1) - return l_true; - // c is (lo <= x): if lo >= p_lo → c is false (since x < p_lo <= lo) - if (m_util.is_const_char(c_lhs, c_lo) && c_rhs == m_ele && c_lo >= p_lo) - return l_false; - } - } else { - // cond is true (not negated) - // (x <= hi) is true: we know x <= p_hi - if (p_lhs == m_ele && m_util.is_const_char(p_rhs, p_hi)) { - // c is (lo <= x): if lo > p_hi → c is false (x <= p_hi < lo) - if (m_util.is_const_char(c_lhs, c_lo) && c_rhs == m_ele && c_lo > p_hi) - return l_false; - // c is (x <= hi2): if hi2 >= p_hi → c is true (x <= p_hi <= hi2) - if (c_lhs == m_ele && m_util.is_const_char(c_rhs, c_hi) && c_hi >= p_hi) - return l_true; - } - // (lo <= x) is true: we know x >= p_lo - if (m_util.is_const_char(p_lhs, p_lo) && p_rhs == m_ele) { - // c is (x <= hi): if hi < p_lo → c is false (x >= p_lo > hi) - if (c_lhs == m_ele && m_util.is_const_char(c_rhs, c_hi) && c_hi < p_lo) - return l_false; - // c is (lo <= x): if lo <= p_lo → c is true (x >= p_lo >= lo) - if (m_util.is_const_char(c_lhs, c_lo) && c_rhs == m_ele && c_lo <= p_lo) - return l_true; - } - } - } - return l_undef; - } void derive::push_path(path_t& path, expr* c, bool sign) { if (!sign && m.is_and(c)) { @@ -1092,19 +1035,23 @@ namespace seq { } void derive::push_intervals(intervals_t& intervals, expr* c, bool sign) { - expr* lhs = nullptr, * rhs = nullptr; - unsigned val = 0; - if (m_util.is_char_le(c, lhs, rhs)) { - if (!sign) { - if (lhs == m_ele && m_util.is_const_char(rhs, val)) - intersect_intervals(0, val, intervals); - else if (rhs == m_ele && m_util.is_const_char(lhs, val)) - intersect_intervals(val, u().max_char(), intervals); + unsigned lo = 0, hi = 0; + bool negated = false; + if (m_util.is_char_const_range(m_ele, c, lo, hi, negated)) { + // is_char_const_range returns the range [lo, hi] such that + // c ≡ (lo <= x <= hi) when negated=false, or c ≡ ¬(lo <= x <= hi) when negated=true + bool effective_neg = (negated != sign); + // effective_neg=false means condition is asserted true: intersect with [lo, hi] + // effective_neg=true means condition is negated: exclude [lo, hi] + if (!effective_neg) { + if (lo <= hi) + intersect_intervals(lo, hi, intervals); + else + intervals.reset(); // contradictory range } else { - if (lhs == m_ele && m_util.is_const_char(rhs, val)) - exclude_interval(0, val, intervals, u().max_char()); - else if (rhs == m_ele && m_util.is_const_char(lhs, val)) - exclude_interval(val, u().max_char(), intervals, u().max_char()); + if (lo <= hi) + exclude_interval(lo, hi, intervals, u().max_char()); + // else: excluding empty range is a no-op } } else if (!sign && m.is_and(c)) { for (expr* arg : *to_app(c)) @@ -1112,22 +1059,6 @@ namespace seq { } else if (sign && m.is_or(c)) { for (expr* arg : *to_app(c)) push_intervals(intervals, arg, true); - } else if (sign && m.is_and(c)) { - // ¬(and(lo<=x, x<=hi)) → exclude [lo, hi] - unsigned lo = 0, hi = u().max_char(); - bool got_lo = false, got_hi = false; - for (expr* arg : *to_app(c)) { - expr* a_lhs = nullptr, * a_rhs = nullptr; - unsigned a_val = 0; - if (m_util.is_char_le(arg, a_lhs, a_rhs)) { - if (a_lhs == m_ele && m_util.is_const_char(a_rhs, a_val)) - { hi = std::min(hi, a_val); got_hi = true; } - else if (a_rhs == m_ele && m_util.is_const_char(a_lhs, a_val)) - { lo = std::max(lo, a_val); got_lo = true; } - } - } - if (got_lo || got_hi) - exclude_interval(lo, hi, intervals, u().max_char()); } } @@ -1156,64 +1087,31 @@ namespace seq { lbool derive::eval_range_cond(intervals_t const& intervals, expr* c) { if (intervals.empty()) return l_false; - - expr* lhs = nullptr, * rhs = nullptr; - unsigned val = 0; - - // Handle AND of char_le as range [lo, hi] - if (m.is_and(c)) { - unsigned lo = 0, hi = u().max_char(); - bool got_lo = false, got_hi = false; - bool all_char_le = true; - for (expr* arg : *to_app(c)) { - expr* a_lhs = nullptr, * a_rhs = nullptr; - unsigned a_val = 0; - if (m_util.is_char_le(arg, a_lhs, a_rhs)) { - if (a_lhs == m_ele && m_util.is_const_char(a_rhs, a_val)) - { hi = std::min(hi, a_val); got_hi = true; } - else if (a_rhs == m_ele && m_util.is_const_char(a_lhs, a_val)) - { lo = std::max(lo, a_val); got_lo = true; } - else all_char_le = false; - } else all_char_le = false; - } - if (all_char_le && (got_lo || got_hi)) { - if (lo > hi) return l_false; - bool any_overlap = false; - bool all_contained = true; - for (auto const& [r_lo, r_hi] : intervals) { - if (std::max(r_lo, lo) <= std::min(r_hi, hi)) - any_overlap = true; - if (r_lo < lo || r_hi > hi) - all_contained = false; - } - if (!any_overlap) return l_false; - if (all_contained) return l_true; - } + unsigned lo = 0, hi = 0; + bool negated = false; + if (!m_util.is_char_const_range(m_ele, c, lo, hi, negated)) return l_undef; + if (lo > hi) { + // c asserts x in empty range or c asserts x NOT in empty range + return negated ? l_true : l_false; } - - // Handle single char_le - if (!m_util.is_char_le(c, lhs, rhs)) - return l_undef; - - if (lhs == m_ele && m_util.is_const_char(rhs, val)) { - // c is (x <= val): true if all hi <= val, false if all lo > val - bool all_le = true, any_le = false; - for (auto const& [r_lo, r_hi] : intervals) { - if (r_lo <= val) any_le = true; - if (r_hi > val) all_le = false; - } - if (all_le) return l_true; - if (!any_le) return l_false; - } else if (rhs == m_ele && m_util.is_const_char(lhs, val)) { - // c is (val <= x): true if all lo >= val, false if all hi < val - bool all_ge = true, any_ge = false; - for (auto const& [r_lo, r_hi] : intervals) { - if (r_hi >= val) any_ge = true; - if (r_lo < val) all_ge = false; - } - if (all_ge) return l_true; - if (!any_ge) return l_false; + // Check if [lo, hi] overlaps with intervals and/or contains all intervals + bool any_overlap = false; + bool all_contained = true; // all intervals ⊆ [lo, hi] + for (auto const& [r_lo, r_hi] : intervals) { + if (std::max(r_lo, lo) <= std::min(r_hi, hi)) + any_overlap = true; + if (r_lo < lo || r_hi > hi) + all_contained = false; + } + if (!negated) { + // c asserts x ∈ [lo, hi] + if (!any_overlap) return l_false; + if (all_contained) return l_true; + } else { + // c asserts x ∉ [lo, hi] + if (all_contained) return l_false; // all values are in [lo,hi], so ¬(x∈[lo,hi]) is false + if (!any_overlap) return l_true; // no values are in [lo,hi], so ¬(x∈[lo,hi]) is true } return l_undef; } @@ -1255,48 +1153,21 @@ namespace seq { if (!m.is_ite(d, c, t, e)) return expr_ref(d, m); - // Try to evaluate c directly + // Try to evaluate c directly (handles trivially true/false conditions) lbool cond_val = eval_cond(c); if (cond_val == l_true) return simplify_ite_rec(path, intervals, t); if (cond_val == l_false) return simplify_ite_rec(path, intervals, e); - // Use interval-based range reasoning (catches AND range vs disjoint intervals) + // Use interval-based range reasoning lbool range_val = eval_range_cond(intervals, c); if (range_val == l_true) return simplify_ite_rec(path, intervals, t); if (range_val == l_false) return simplify_ite_rec(path, intervals, e); - // When c is an AND (range condition), check each conjunct against the path. - // If any conjunct is contradicted by the path, c is false → take else. - // If all conjuncts are implied by the path, c is true → take then. - if (m.is_and(c)) { - lbool and_result = l_true; - for (expr* arg : *to_app(c)) { - lbool arg_val = eval_path_cond(path, arg); - if (arg_val == l_false) { - and_result = l_false; - break; - } - if (arg_val == l_undef) - and_result = l_undef; - } - if (and_result == l_true) return simplify_ite_rec(path, intervals, t); - if (and_result == l_false) return simplify_ite_rec(path, intervals, e); - } - // When c is a single char_le, also check against the path - else { - lbool c_val = eval_path_cond(path, c); - if (c_val == l_true) return simplify_ite_rec(path, intervals, t); - if (c_val == l_false) return simplify_ite_rec(path, intervals, e); - } - - // Check if c can be determined from the path (legacy checks for equality conditions) + // Check direct structural matches in path (equality conditions) for (auto const& [cond, sign] : path) { - // Direct match: c == cond if (c == cond) return sign ? simplify_ite_rec(path, intervals, e) : simplify_ite_rec(path, intervals, t); - // c is (x = v), cond is (x = w) with sign=false (cond is true, so x=w) - // If v != w, then c is false → take else branch expr* lhs1 = nullptr, * rhs1 = nullptr, * lhs2 = nullptr, * rhs2 = nullptr; if (!sign && m.is_eq(cond, lhs1, rhs1) && m.is_eq(c, lhs2, rhs2)) { if (m.is_value(lhs1)) std::swap(lhs1, rhs1); @@ -1304,84 +1175,6 @@ namespace seq { if (lhs1 == lhs2 && m.are_distinct(rhs1, rhs2)) return simplify_ite_rec(path, intervals, e); } - - // Range constraint: cond is (lo <= x) or (x <= hi) with sign=false - // and c is (x = v). If v is outside the range, c is false. - unsigned v_val = 0, lo_val = 0, hi_val = 0; - if (!sign && m.is_eq(c, lhs2, rhs2)) { - if (m.is_value(lhs2)) std::swap(lhs2, rhs2); - if (m_util.is_const_char(rhs2, v_val)) { - expr* le_lhs = nullptr, * le_rhs = nullptr; - if (m_util.is_char_le(cond, le_lhs, le_rhs) && le_rhs == lhs2 && - m_util.is_const_char(le_lhs, lo_val) && v_val < lo_val) - return simplify_ite_rec(path, intervals, e); - if (m_util.is_char_le(cond, le_lhs, le_rhs) && le_lhs == lhs2 && - m_util.is_const_char(le_rhs, hi_val) && v_val > hi_val) - return simplify_ite_rec(path, intervals, e); - } - } - - // Range implication between char_le conditions: - expr* c_lhs = nullptr, * c_rhs = nullptr; - expr* p_lhs = nullptr, * p_rhs = nullptr; - if (m_util.is_char_le(c, c_lhs, c_rhs) && m_util.is_char_le(cond, p_lhs, p_rhs)) { - unsigned c_lo = 0, c_hi = 0, p_lo = 0, p_hi = 0; - if (sign) { - if (m_util.is_const_char(c_lhs, c_lo) && c_rhs == m_ele && - p_lhs == m_ele && m_util.is_const_char(p_rhs, p_hi) && - c_lo <= p_hi + 1) - return simplify_ite_rec(path, intervals, t); - if (c_lhs == m_ele && m_util.is_const_char(c_rhs, c_hi) && - m_util.is_const_char(p_lhs, p_lo) && p_rhs == m_ele && - p_lo > 0 && p_lo - 1 <= c_hi) - return simplify_ite_rec(path, intervals, t); - } else { - if (m_util.is_const_char(c_lhs, c_lo) && c_rhs == m_ele && - p_lhs == m_ele && m_util.is_const_char(p_rhs, p_hi) && - c_lo > p_hi) - return simplify_ite_rec(path, intervals, e); - if (c_lhs == m_ele && m_util.is_const_char(c_rhs, c_hi) && - m_util.is_const_char(p_lhs, p_lo) && p_rhs == m_ele && - c_hi < p_lo) - return simplify_ite_rec(path, intervals, e); - if (m_util.is_const_char(c_lhs, c_lo) && c_rhs == m_ele && - m_util.is_const_char(p_lhs, p_lo) && p_rhs == m_ele && - c_lo <= p_lo) - return simplify_ite_rec(path, intervals, t); - if (c_lhs == m_ele && m_util.is_const_char(c_rhs, c_hi) && - p_lhs == m_ele && m_util.is_const_char(p_rhs, p_hi) && - c_hi >= p_hi) - return simplify_ite_rec(path, intervals, t); - } - } - } - - // Check if both range bounds are in path and c is (x = v) within range - expr* lhs_c = nullptr, * rhs_c = nullptr; - unsigned v_val = 0; - if (m.is_eq(c, lhs_c, rhs_c)) { - if (m.is_value(lhs_c)) std::swap(lhs_c, rhs_c); - if (m_util.is_const_char(rhs_c, v_val)) { - unsigned lo_bound = 0, hi_bound = UINT_MAX; - bool has_lo = false, has_hi = false; - for (auto const& [cond, sign] : path) { - if (sign) continue; - expr* le_lhs = nullptr, * le_rhs = nullptr; - if (m_util.is_char_le(cond, le_lhs, le_rhs)) { - unsigned bound = 0; - if (le_rhs == lhs_c && m_util.is_const_char(le_lhs, bound)) { - lo_bound = bound; has_lo = true; - } - if (le_lhs == lhs_c && m_util.is_const_char(le_rhs, bound)) { - hi_bound = bound; has_hi = true; - } - } - } - if (has_lo && has_hi && lo_bound <= v_val && v_val <= hi_bound) { - auto [st, se] = simplify_ite_rec(path, intervals, c, t, e); - return mk_ite(c, st, se); - } - } } // Cannot simplify c: recurse into branches with extended paths diff --git a/src/ast/rewriter/seq_derive.h b/src/ast/rewriter/seq_derive.h index 41a3937c3..a524f39ee 100644 --- a/src/ast/rewriter/seq_derive.h +++ b/src/ast/rewriter/seq_derive.h @@ -125,7 +125,6 @@ namespace seq { void push_path(path_t& path, expr* c, bool sign); void push_intervals(intervals_t& intervals, expr* c, bool sign); lbool eval_cond(expr* cond); - lbool eval_path_cond(path_t const& path, expr* c); lbool eval_range_cond(intervals_t const& intervals, expr* c); static void intersect_intervals(unsigned lo, unsigned hi, intervals_t& ranges); static void exclude_interval(unsigned lo, unsigned hi, intervals_t& ranges, unsigned max_char);