mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

remove type check in insert_update

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-01-06 11:12:08 -08:00
parent 67827bfe56
commit 5a5570ef4e
2 changed files with 8 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/ast/sls/sls_bv_lookahead.cpp
View file

@ -370,11 +370,8 @@ namespace sls {
auto v1 = m_ev.get_bool_value(y);
return (is_true == (v0 == v1)) ? 1 : 0;
}
if (m.is_ite(a, x, y, z)) {
auto v0 = m_ev.get_bool_value(x);
return v0 ? new_score(y, is_true) : new_score(z, is_true);
}
if (m.is_ite(a, x, y, z))
return m_ev.get_bool_value(x) ? new_score(y, is_true) : new_score(z, is_true);
if (is_true && m.is_eq(a, x, y) && bv.is_bv(x)) {
auto const& vx = wval(x);
auto const& vy = wval(y);
@ -387,10 +384,9 @@ namespace sls {
//verbose_stream() << "hamming distance " << mk_bounded_pp(a, m) << " " << d << "\n";
return d;
}
else if (!is_true && m.is_eq(a, x, y) && bv.is_bv(x)) {
return 0;
}
else if (bv.is_ule(a, x, y)) {
if (!is_true && m.is_eq(a, x, y) && bv.is_bv(x))
return 0;
if (bv.is_ule(a, x, y)) {
auto const& vx = wval(x);
auto const& vy = wval(y);
@ -417,7 +413,7 @@ namespace sls {
double dbl = n.get_double();
return (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
}
else if (bv.is_sle(a, x, y)) {
if (bv.is_sle(a, x, y)) {
auto const& vx = wval(x);
auto const& vy = wval(y);
// x += 2^bw-1
@ -445,7 +441,7 @@ namespace sls {
double dbl = n.get_double();
return (dbl > 1.0) ? 0.0 : (dbl < 0.0) ? 1.0 : 1.0 - dbl;
}
else if (is_true && m.is_distinct(a) && bv.is_bv(to_app(a)->get_arg(0))) {
if (is_true && m.is_distinct(a) && bv.is_bv(to_app(a)->get_arg(0))) {
double np = 0, nd = 0;
for (unsigned i = 0; i < to_app(a)->get_num_args(); ++i) {
auto const& vi = wval(to_app(a)->get_arg(i));
@ -651,8 +647,6 @@ namespace sls {
for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
auto e = m_update_stack[depth][i];
TRACE("bv_verbose", tout << "update " << mk_bounded_pp(e, m) << "\n";);
VERIFY(m.is_bool(e) || bv.is_bv(e));
if (t == e)
;
@ -744,8 +738,6 @@ namespace sls {
}
void bv_lookahead::insert_update_stack(expr* e) {
if (!bv.is_bv(e) && !m.is_bool(e))
return;
unsigned depth = get_depth(e);
m_update_stack.reserve(depth + 1);
if (!m_in_update_stack.is_marked(e) && is_app(e)) {

16
src/smt/theory_lra.cpp
View file

@ -719,21 +719,7 @@ class theory_lra::imp {
report_equality_of_fixed_vars(vi, vi_equal);
m_new_def = true;
}
void internalize_eq(theory_var v1, theory_var v2) {
app_ref term(m.mk_fresh_const("eq", a.mk_real()), m);
scoped_internalize_state st(*this);
st.vars().push_back(v1);
st.vars().push_back(v2);
st.coeffs().push_back(rational::one());
st.coeffs().push_back(rational::minus_one());
theory_var z = internalize_linearized_def(term, st);
lpvar vi = register_theory_var_in_lar_solver(z);
add_def_constraint_and_equality(vi, lp::LE, rational::zero());
add_def_constraint_and_equality(vi, lp::GE, rational::zero());
TRACE("arith",
tout << "v" << v1 << " = " << "v" << v2 << ": " << pp(v1) << " = " << pp(v2) << "\n");
}
void del_bounds(unsigned old_size) {
for (unsigned i = m_bounds_trail.size(); i-- > old_size; ) {