mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

add trail to avoid stale references in expr2var

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-24 04:15:52 -08:00
parent 3f1b7866ca
commit 15d853dc04
2 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/simplifiers/bound_simplifier.cpp
View file

@ -208,6 +208,8 @@ void bound_simplifier::tighten_bound(dependent_expr const& de) {
assert_upper(x, n - k, true);
}
// x != k, k <= x -> k < x
if (m.is_not(f, f) && m.is_eq(f, x, y)) {
if (a.is_numeral(x))
@ -222,6 +224,7 @@ void bound_simplifier::tighten_bound(dependent_expr const& de) {
assert_upper(x, n, true);
}
}
}
void bound_simplifier::assert_upper(expr* x, rational const& n, bool strict) {
@ -449,6 +452,7 @@ void bound_simplifier::reset() {
bp.reset();
m_var2expr.reset();
m_expr2var.reset();
m_trail.reset();
}
#if 0

3
src/ast/simplifiers/bound_simplifier.h
View file

@ -40,6 +40,7 @@ class bound_simplifier : public dependent_expr_simplifier {
dep_intervals m_interval;
ptr_vector<expr> m_var2expr;
unsigned_vector m_expr2var;
expr_ref_vector m_trail;
mpq_buffer m_num_buffer;
var_buffer m_var_buffer;
unsigned m_num_reduced = 0;
@ -71,6 +72,7 @@ class bound_simplifier : public dependent_expr_simplifier {
if (e != core_e)
m_expr2var.setx(core_e->get_id(), v, UINT_MAX);
m_var2expr.push_back(core_e);
m_trail.push_back(e);
}
return v;
}
@ -100,6 +102,7 @@ public:
m_rewriter(m),
bp(nm, m_alloc, p),
m_interval(m.limit()),
m_trail(m),
m_num_buffer(nm) {
updt_params(p);
}