From 402fdf667d5f5212b9919d103e4924123852db5b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Jul 2024 19:34:24 -0700 Subject: [PATCH] bv updates --- src/ast/sls/bv_sls_eval.cpp | 56 ++++++++++++++++------------------ src/ast/sls/bv_sls_eval.h | 7 ----- src/ast/sls/bv_sls_fixed.cpp | 18 +++++------ src/ast/sls/sls_arith_base.cpp | 2 +- src/ast/sls/sls_bv_plugin.cpp | 20 ++++++------ src/ast/sls/sls_context.cpp | 3 ++ src/ast/sls/sls_context.h | 3 +- 7 files changed, 49 insertions(+), 60 deletions(-) diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 85c0fd5c0..28bb2153b 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -38,7 +38,11 @@ namespace bv { auto& v = wval(e); for (unsigned i = 0; i < v.bw; ++i) m_tmp.set(i, false); - v.set_repair(random_bool(), m_tmp); + v.set_repair(random_bool(), m_tmp); + } + if (bv.is_bv(e)) { + auto& v = wval(e); + v.bits().copy_to(v.nw, v.eval); } } @@ -89,11 +93,13 @@ namespace bv { } bool sls_eval::can_eval1(app* e) const { - expr* x, * y, * z; + expr* x, * y; if (m.is_eq(e, x, y)) - return m.is_bool(x) || bv.is_bv(x); - if (m.is_ite(e, x, y, z)) - return m.is_bool(y) || bv.is_bv(y); + return bv.is_bv(x); + if (m.is_ite(e)) + return bv.is_bv(e); + if (m.is_distinct(e)) + return bv.is_bv(e->get_arg(0)); if (e->get_family_id() == bv.get_fid()) { switch (e->get_decl_kind()) { case OP_BNEG_OVFL: @@ -107,10 +113,8 @@ namespace bv { return true; } } - if (e->get_family_id() == basic_family_id) - return true; if (is_uninterp_const(e)) - return m.is_bool(e) || bv.is_bv(e); + return bv.is_bv(e); return false; } @@ -1843,7 +1847,19 @@ namespace bv { } bool sls_eval::repair_up(expr* e) { - if (!bv.is_bv(e) || !is_app(e)) + if (!is_app(e) || !can_eval1(to_app(e))) + return false; + if (m.is_bool(e)) { + bool b = bval1(to_app(e)); + auto v = ctx.atom2bool_var(e); + if (v == sat::null_bool_var) + ctx.set_value(e, b ? m.mk_true() : m.mk_false()); + else if (ctx.is_true(v) != b) + ctx.flip(v); + return true; + } + + if (!bv.is_bv(e)) return false; auto& v = eval(to_app(e)); for (unsigned i = 0; i < v.nw; ++i) { @@ -1863,18 +1879,11 @@ namespace bv { return *m_values[e->get_id()]; } - void sls_eval::init_eval(app* t) { - if (bv.is_bv(t)) { - auto& v = wval(t); - v.bits().copy_to(v.nw, v.eval); - } - } void sls_eval::commit_eval(app* e) { if (!bv.is_bv(e)) return; - VERIFY(wval(e).commit_eval()); - // todo: if e is shared, then ctx.set_value(). + VERIFY(wval(e).commit_eval()); } void sls_eval::set_random(app* e) { @@ -1895,19 +1904,6 @@ namespace bv { return false; } - bool sls_eval::re_eval_is_correct(app* e) { - if (!can_eval1(e)) - return false; - if (m.is_bool(e)) - return bval0(e) ==bval1(e); - if (bv.is_bv(e)) { - auto const& v = eval(e); - return v.eval == v.bits(); - } - UNREACHABLE(); - return false; - } - expr_ref sls_eval::get_value(app* e) { if (m.is_bool(e)) return expr_ref(m.mk_bool_val(bval0(e)), m); diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index 995bd4aef..794f5f2bd 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -61,7 +61,6 @@ namespace bv { void add_bit_vector(app* e); sls_valuation* alloc_valuation(app* e); - //bool bval1_basic(app* e) const; bool bval1_bv(app* e) const; void fold_oper(bvect& out, app* e, unsigned i, std::function const& f); @@ -137,8 +136,6 @@ namespace bv { public: sls_eval(sls_terms& terms, sls::context& ctx); -// void init_eval(std::function const& eval); - void tighten_range() { m_fix.init(); } void register_term(expr* e); @@ -157,14 +154,10 @@ namespace bv { void commit_eval(app* e); - void init_eval(app* e); - void set_random(app* e); bool eval_is_correct(app* e); - bool re_eval_is_correct(app* e); - expr_ref get_value(app* e); bool bval1(app* e) const; diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index 530fc4b43..cdda79558 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -31,17 +31,15 @@ namespace bv { for (auto e : ctx.subterms()) set_fixed(e); - for (auto const& c : ctx.clauses()) { - if (c.m_clause.size() == 1) { - auto lit = c.m_clause[0]; - auto a = ctx.atom(lit.var()); - if (!a) - continue; - if (is_app(a)) - init_range(to_app(a), lit.sign()); - ev.m_fixed.setx(a->get_id(), true, false); - } + for (auto lit : ctx.unit_literals()) { + auto a = ctx.atom(lit.var()); + if (!a) + continue; + if (is_app(a)) + init_range(to_app(a), lit.sign()); + ev.m_fixed.setx(a->get_id(), true, false); } + for (auto e : ctx.subterms()) propagate_range_up(e); } diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index 219d0bc31..8462f2eea 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -554,7 +554,7 @@ namespace sls { add_args(ineq, y, num_t(-1)); init_ineq(bv, ineq); } - else if (m.is_distinct(e) && a.is_int_real(e->get_arg(0))) { + else if (m.is_distinct(e) && a.is_int_real(to_app(e)->get_arg(0))) { NOT_IMPLEMENTED_YET(); } else if (a.is_is_int(e, x)) diff --git a/src/ast/sls/sls_bv_plugin.cpp b/src/ast/sls/sls_bv_plugin.cpp index 0819caf2d..209576fe9 100644 --- a/src/ast/sls/sls_bv_plugin.cpp +++ b/src/ast/sls/sls_bv_plugin.cpp @@ -29,6 +29,7 @@ namespace sls { void bv_plugin::register_term(expr* e) { m_terms.register_term(e); + m_eval.register_term(e); } expr_ref bv_plugin::get_value(expr* e) { @@ -59,7 +60,7 @@ namespace sls { void bv_plugin::initialize() { if (!m_initialized) { - // compute fixed ranges + m_eval.tighten_range(); m_initialized = true; } } @@ -92,8 +93,9 @@ namespace sls { return; rational val; VERIFY(bv.is_numeral(v, val)); - NOT_IMPLEMENTED_YET(); - // set value of e to val, + auto& w = m_eval.eval(to_app(e)); + w.set_value(w.eval, val); + w.commit_eval(); } void bv_plugin::repair_down(app* e) { @@ -135,17 +137,14 @@ namespace sls { } void bv_plugin::repair_up(app* e) { - if (!bv.is_bv(e)) - ; - else if (m_eval.repair_up(e)) { + if (m_eval.repair_up(e)) { if (!m_eval.eval_is_correct(e)) { verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; } SASSERT(m_eval.eval_is_correct(e)); - for (auto p : ctx.parents(e)) - ctx.new_value_eh(p); + ctx.new_value_eh(e); } - else if (ctx.rand(10) != 0) { + else if (bv.is_bv(e)) { IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e)); m_eval.set_random(e); ctx.new_value_eh(e); @@ -163,5 +162,4 @@ namespace sls { IF_VERBOSE(2, verbose_stream() << "(bvsls :restarts " << m_stats.m_restarts << ")\n"); } - -} +} \ No newline at end of file diff --git a/src/ast/sls/sls_context.cpp b/src/ast/sls/sls_context.cpp index 075bc1dfc..449b811ae 100644 --- a/src/ast/sls/sls_context.cpp +++ b/src/ast/sls/sls_context.cpp @@ -299,6 +299,7 @@ namespace sls { m_relevant.reset(); m_visited.reset(); m_root_literals.reset(); + m_unit_literals.reset(); for (auto const& clause : s.clauses()) { bool has_relevant = false; unsigned n = 0; @@ -317,6 +318,8 @@ namespace sls { if (m_rand() % ++n == 0) selected_lit = lit; } + if (clause.m_clause.size() == 1) + m_unit_literals.push_back(clause.m_clause[0]); if (!has_relevant && selected_lit != sat::null_literal) { m_relevant.insert(m_atoms[selected_lit.var()]->get_id()); m_root_literals.push_back(selected_lit); diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h index 75a12b4f8..ba0054d79 100644 --- a/src/ast/sls/sls_context.h +++ b/src/ast/sls/sls_context.h @@ -94,7 +94,7 @@ namespace sls { expr_ref_vector m_atoms; unsigned_vector m_atom2bool_var; vector> m_parents; - sat::literal_vector m_root_literals; + sat::literal_vector m_root_literals, m_unit_literals; random_gen m_rand; bool m_initialized = false; bool m_new_constraint = false; @@ -140,6 +140,7 @@ namespace sls { unsigned rand() { return m_rand(); } unsigned rand(unsigned n) { return m_rand(n); } sat::literal_vector const& root_literals() const { return m_root_literals; } + sat::literal_vector const& unit_literals() const { return m_unit_literals; } void reinit_relevant();