diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp index cb0fc9e17..4e5e95e13 100644 --- a/src/sat/smt/bv_internalize.cpp +++ b/src/sat/smt/bv_internalize.cpp @@ -290,6 +290,10 @@ namespace bv { TRACE("bv", tout << "add-bit: v" << v << "[" << idx << "] " << l << " " << literal2expr(l) << "@" << s().scope_lvl() << "\n";); SASSERT(m_num_scopes == 0); s().set_external(l.var()); + euf::enode* n = bool_var2enode(l.var()); + if (!n->is_attached_to(get_id())) + mk_var(n); + set_bit_eh(v, l, idx); } @@ -307,7 +311,7 @@ namespace bv { SASSERT(m_bits[v][idx] == l); if (s().value(l) != l_undef && s().lvl(l) == 0) register_true_false_bit(v, idx); - else if (m_bits[v].size() > 1) { + else { atom* b = mk_atom(l.var()); if (b->m_occs) find_new_diseq_axioms(*b, v, idx); @@ -613,7 +617,7 @@ namespace bv { SASSERT(hi - lo + 1 == get_bv_size(v)); SASSERT(lo <= hi && hi < get_bv_size(arg_v)); m_bits[v].reset(); - for (unsigned i = lo; i <= hi; ++i) + for (unsigned i = lo; i <= hi; ++i) add_bit(v, m_bits[arg_v][i]); find_wpos(v); } diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index a0ec0e75b..4aeb2ff43 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -74,7 +74,6 @@ namespace bv { is_bv(v2) && m_bits[v2].size() == sz && get_fixed_value(v2, val2) && val1 == val2; - if (!is_current) m_fixed_var_table.insert(key, v1); else if (n1->get_root() != var2enode(v2)->get_root()) { @@ -380,11 +379,12 @@ namespace bv { } void solver::asserted(literal l) { + atom* a = get_bv2a(l.var()); TRACE("bv", tout << "asserted: " << l << "\n";); if (a) { force_push(); - m_prop_queue.push_back(propagation_item(a)); + m_prop_queue.push_back(propagation_item(a)); for (auto p : a->m_bit2occ) { del_eq_occurs(p.first, p.second); } @@ -530,6 +530,7 @@ namespace bv { } bool solver::set_root(literal l, literal r) { + return false; atom* a = get_bv2a(l.var()); if (!a) return true; @@ -624,6 +625,16 @@ namespace bv { return out; } + std::ostream& solver::display(std::ostream& out, atom const& a) const { + out << a.m_bv << "\n"; + for (auto vp : a) + out << vp.first << "[" << vp.second << "]\n"; + for (auto e : a.eqs()) + out << e.m_bv1 << " " << e.m_bv2 << "\n"; + return out; + } + + void solver::collect_statistics(statistics& st) const { st.update("bv conflicts", m_stats.m_num_conflicts); st.update("bv diseqs", m_stats.m_num_diseq_static); @@ -680,6 +691,7 @@ namespace bv { void solver::init_use_list(sat::ext_use_list& ul) {} bool solver::is_blocked(literal l, sat::ext_constraint_idx) { return false; } bool solver::check_model(sat::model const& m) const { return true; } + void solver::finalize_model(model& mdl) {} unsigned solver::max_var(unsigned w) const { return w; } void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) { diff --git a/src/sat/smt/bv_solver.h b/src/sat/smt/bv_solver.h index 67f5d56cb..90f455d3e 100644 --- a/src/sat/smt/bv_solver.h +++ b/src/sat/smt/bv_solver.h @@ -175,6 +175,7 @@ namespace bv { atom* m_atom{ nullptr }; explicit propagation_item(atom* a) : m_atom(a) {} explicit propagation_item(var_pos const& vp) : m_vp(vp) {} + bool operator==(propagation_item const& other) const { if (m_atom) return m_atom == other.m_atom; return false; } }; @@ -300,6 +301,8 @@ namespace bv { bool check_zero_one_bits(theory_var v); void check_missing_propagation() const; void validate_atoms() const; + + std::ostream& display(std::ostream& out, atom const& a) const; public: solver(euf::solver& ctx, theory_id id); @@ -332,6 +335,7 @@ namespace bv { void init_use_list(sat::ext_use_list& ul) override; bool is_blocked(literal l, sat::ext_constraint_idx) override; bool check_model(sat::model const& m) const override; + void finalize_model(model& mdl) override; unsigned max_var(unsigned w) const override; void new_eq_eh(euf::th_eq const& eq) override; diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index f845eb6e9..0f39a0ce8 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -203,9 +203,11 @@ namespace euf { if (!m.is_bool(e)) continue; unsigned id = n->get_root_id(); + if (!m_values.get(id)) + continue; bool tt = m.is_true(m_values.get(id)); if (mdl.is_true(e) != tt) { - IF_VERBOSE(0, verbose_stream() << "Failed to evaluate " << id << " " << mk_bounded_pp(e, m) << "\n"); + IF_VERBOSE(0, verbose_stream() << "Failed to evaluate " << id << " " << mk_bounded_pp(e, m) << " " << mdl(e) << " " << mk_bounded_pp(m_values.get(id), m) << "\n"); } } diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 78d428edb..b9dba36f7 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -81,16 +81,16 @@ namespace euf { ast_manager& m; sat::sat_internalizer& si; - smt_params m_config; - euf::egraph m_egraph; - euf_trail_stack m_trail; - stats m_stats; - th_rewriter m_rewriter; - func_decl_ref_vector m_unhandled_functions; - sat::lookahead* m_lookahead{ nullptr }; + smt_params m_config; + euf::egraph m_egraph; + euf_trail_stack m_trail; + stats m_stats; + th_rewriter m_rewriter; + func_decl_ref_vector m_unhandled_functions; + sat::lookahead* m_lookahead{ nullptr }; ast_manager* m_to_m; sat::sat_internalizer* m_to_si; - scoped_ptr m_ackerman; + scoped_ptr m_ackerman; scoped_ptr m_dual_solver; user::solver* m_user_propagator{ nullptr }; th_solver* m_qsolver { nullptr };