mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

make reset updates recursive

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-24 14:16:34 -07:00
parent 47b793a5e0
commit d6b89ba2d5
1 changed files with 11 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/ast/sls/sls_arith_base.cpp
View file

@ -1500,13 +1500,7 @@ namespace sls {
add_update(w, delta);
}
for (auto const& [coeff, w] : coeffs)
if (is_mul(w)) {
auto const& [w1, c, monomial] = get_mul(w);
for (auto [w1, p] : monomial)
add_reset_update(w1);
}
else
add_reset_update(w);
add_reset_update(w);
if (apply_update())
return eval_is_correct(v);
@ -1769,6 +1763,16 @@ namespace sls {
m_last_delta = 0;
if (is_fixed(x))
return;
if (is_mul(x)) {
auto const& [w1, c, monomial] = get_mul(x);
for (auto [w1, p] : monomial)
add_reset_update(w1);
}
if (is_add(x)) {
auto const& ad = get_add(x);
for (auto [c, w] : ad.m_args)
add_reset_update(w);
}
auto const& vi = m_vars[x];
auto const& lo = vi.m_lo;
auto const& hi = vi.m_hi;