From 5a5570ef4e9c268fe23ef4d2853f8ade8ffd5bad Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Jan 2025 11:12:08 -0800 Subject: [PATCH] remove type check in insert_update Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_bv_lookahead.cpp | 22 +++++++--------------- src/smt/theory_lra.cpp | 16 +--------------- 2 files changed, 8 insertions(+), 30 deletions(-) diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp index bb48e4a07..9c7522c53 100644 --- a/src/ast/sls/sls_bv_lookahead.cpp +++ b/src/ast/sls/sls_bv_lookahead.cpp @@ -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)) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 15eca3d88..821b5be2a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -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; ) {