mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 15:16:29 +00:00
Code Activity

intervals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-04 18:21:26 -07:00
parent dc8179212e
commit ed2c64208d
2 changed files with 42 additions and 250 deletions
Download patch file Download diff file Expand all files Collapse all files

291
src/ast/rewriter/seq_derive.cpp
View file

@ -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

1
src/ast/rewriter/seq_derive.h
View file

@ -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);