mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

Fix crash exposed in QF_UFNIA

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-24 15:31:10 -08:00
parent 9e8dd68ee6
commit f6e7dcff47
4 changed files with 37 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -543,7 +543,7 @@ namespace sls {
bool arith_base<num_t>::find_lin_moves(sat::literal lit) {
m_updates.reset();
auto* ineq = get_ineq(lit.var());
num_t a, b;
num_t a(0), b(0);
if (!ineq)
return false;
if (!ineq->m_is_linear) {
@ -947,6 +947,9 @@ namespace sls {
m_vars[v].m_def_idx = idx;
m_vars[v].m_op = k;
m_vars[v].set_value(val);
m_vars[vx].m_ops.push_back(v);
if (vy != vx)
m_vars[vy].m_ops.push_back(v);
return v;
}
@ -1854,7 +1857,7 @@ namespace sls {
for (auto const& [x, nl] : ineq->m_nonlinear) {
if (is_fixed(x))
continue;
if (is_add(x) || is_mul(x))
if (is_add(x) || is_mul(x) || is_op(x))
;
else if (is_linear(x, nl, b))
find_linear_moves(*ineq, x, b);
@ -1905,7 +1908,7 @@ namespace sls {
bool arith_base<num_t>::find_reset_moves(sat::literal lit) {
m_updates.reset();
auto* ineq = get_ineq(lit.var());
num_t a, b;
num_t a(0), b(0);
if (!ineq)
return false;
for (auto const& [x, nl] : ineq->m_nonlinear)
@ -2853,25 +2856,6 @@ namespace sls {
m_fixed_atoms.insert(bv);
}
template<typename num_t>
void arith_base<num_t>::add_lookahead(sat::bool_var bv) {
auto* ineq = get_ineq(bv);
if (!ineq)
return;
num_t na, nb;
for (auto const& [x, nl] : ineq->m_nonlinear) {
if (is_fixed(x))
continue;
if (is_add(x) || is_mul(x))
;
else if (is_linear(x, nl, nb))
find_linear_moves(*ineq, x, nb);
else if (is_quadratic(x, nl, na, nb))
find_quadratic_moves(*ineq, x, na, nb, ineq->m_args_value);
else
;
}
}
// for every variable e, for every atom containing e
// add lookahead for e.
@ -3211,8 +3195,8 @@ namespace sls {
for (auto const& idx : vi.m_muls) {
auto& [x, monomial] = m_muls[idx];
num_t new_prod(1);
for (auto [w, p] : monomial)
new_prod *= power_of(v == w ? new_value : value(w), p);
for (auto [w, p] : monomial)
new_prod *= power_of(value(w), p);
update_args_value(x, new_prod);
}
@ -3220,10 +3204,12 @@ namespace sls {
auto& ad = m_adds[idx];
num_t new_sum(ad.m_coeff);
for (auto [c, w] : ad.m_args)
new_sum += c * (v == w ? new_value : value(w));
new_sum += c * value(w);
update_args_value(ad.m_var, new_sum);
}
for (auto const& x : vi.m_ops)
update_args_value(x, value1(x));
for (auto const& [coeff, bv] : vi.m_linear_occurs) {
auto& ineq = *get_ineq(bv);

5
src/ast/sls/sls_arith_base.h
View file

@ -122,8 +122,7 @@ namespace sls {
vector<std::pair<num_t, sat::bool_var>> m_linear_occurs;
sat::bool_var_vector m_bool_vars_of;
unsigned_vector m_clauses_of;
unsigned_vector m_muls;
unsigned_vector m_adds;
unsigned_vector m_muls, m_adds, m_ops;
optional<bound> m_lo, m_hi;
vector<num_t> m_finite_domain;
@ -277,6 +276,7 @@ namespace sls {
bool is_mul(var_t v) const { return m_vars[v].m_op == arith_op_kind::OP_MUL; }
bool is_add(var_t v) const { return m_vars[v].m_op == arith_op_kind::OP_ADD; }
bool is_op(var_t v) const { return m_vars[v].m_op != arith_op_kind::LAST_ARITH_OP && m_vars[v].m_op != arith_op_kind::OP_MUL && m_vars[v].m_op != arith_op_kind::OP_ADD; }
mul_def const& get_mul(var_t v) const { SASSERT(is_mul(v)); return m_muls[m_vars[v].m_def_idx]; }
add_def const& get_add(var_t v) const { SASSERT(is_add(v)); return m_adds[m_vars[v].m_def_idx]; }
@ -385,7 +385,6 @@ namespace sls {
double lookahead(expr* e, bool update_score);
void add_lookahead(bool_info& i, expr* e);
void add_lookahead(bool_info& i, sat::bool_var bv);
void add_lookahead(sat::bool_var bv);
ptr_vector<expr> const& get_fixable_exprs(expr* e);
bool apply_move(expr* f, ptr_vector<expr> const& vars, arith_move_type t);
expr* get_candidate_unsat();

26
src/ast/sls/sls_arith_clausal.cpp
View file

@ -127,10 +127,30 @@ namespace sls {
tout << "\n";);
for (auto v : ctx.unsat_vars())
a.add_lookahead(v);
add_lookahead(v);
}
template<typename num_t>
void arith_clausal<num_t>::add_lookahead(sat::bool_var bv) {
auto* ineq = a.get_ineq(bv);
if (!ineq)
return;
num_t na, nb;
for (auto const& [x, nl] : ineq->m_nonlinear) {
if (a.is_fixed(x))
continue;
if (a.is_add(x) || a.is_mul(x) || a.is_op(x))
;
else if (a.is_linear(x, nl, nb))
a.find_linear_moves(*ineq, x, nb);
else if (a.is_quadratic(x, nl, na, nb))
a.find_quadratic_moves(*ineq, x, na, nb, ineq->m_args_value);
else
;
}
}
/**
* \brief walk over literals that are false in some clause.
* Try to determine if flipping them to true improves the overall score.
@ -162,7 +182,7 @@ namespace sls {
--sz;
a.m_bool_var_atoms.swap_elems(idx, sz);
if (occurs_negative(bv))
a.add_lookahead(bv);
add_lookahead(bv);
else
++i;
}
@ -171,7 +191,7 @@ namespace sls {
for (unsigned i = 0; i < sz; ++i) {
bv = a.m_bool_var_atoms[i];
if (occurs_negative(bv))
a.add_lookahead(bv);
add_lookahead(bv);
}
}
}

1
src/ast/sls/sls_arith_clausal.h
View file

@ -64,6 +64,7 @@ namespace sls {
void critical_move(var_t v, num_t const& delta, move_t mt);
void lookahead(var_t v, num_t const& delta);
double get_score(var_t v, num_t const& delta);
void add_lookahead(sat::bool_var bv);
unsigned m_no_improve_bool = 0;