mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 00:48:45 +00:00
Code Activity

#5532

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-08 06:19:49 +02:00
parent 8c406c161e
commit c4d0ded7b7
2 changed files with 28 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/sat/smt/bv_solver.cpp
View file

@ -673,25 +673,33 @@ namespace bv {
for (theory_var i = 0; i < static_cast<theory_var>(get_num_vars()); ++i) for (theory_var i = 0; i < static_cast<theory_var>(get_num_vars()); ++i)
if (find(i) != i) if (find(i) != i)
result->m_find.set_root(i, find(i)); result->m_find.set_root(i, find(i));
result->m_prop_queue.append(m_prop_queue);
for (unsigned i = 0; i < m_bool_var2atom.size(); ++i) {
atom* a = m_bool_var2atom[i];
if (!a)
continue;
atom* new_a = new (result->get_region()) atom(i); auto clone_atom = [&](atom const& a) {
result->m_bool_var2atom.setx(i, new_a, nullptr); atom* new_a = new (result->get_region()) atom(a.m_bv);
for (auto vp : *a) result->m_bool_var2atom.setx(a.m_bv, new_a, nullptr);
new_a->m_occs = new (result->get_region()) var_pos_occ(vp.first, vp.second, new_a->m_occs); for (auto [v, p] : a)
for (eq_occurs const& occ : a->eqs()) { new_a->m_occs = new (result->get_region()) var_pos_occ(v, p, new_a->m_occs);
for (eq_occurs const& occ : a.eqs()) {
expr* e = occ.m_node->get_expr(); expr* e = occ.m_node->get_expr();
expr_ref e2(tr(e), tr.to()); expr_ref e2(tr(e), tr.to());
euf::enode* n = ctx.get_enode(e2); euf::enode* n = ctx.get_enode(e2);
SASSERT(tr.to().contains(e2));
new_a->m_eqs = new (result->get_region()) eq_occurs(occ.m_bv1, occ.m_bv2, occ.m_idx, occ.m_v1, occ.m_v2, occ.m_literal, n, new_a->m_eqs); new_a->m_eqs = new (result->get_region()) eq_occurs(occ.m_bv1, occ.m_bv2, occ.m_idx, occ.m_v1, occ.m_v2, occ.m_literal, n, new_a->m_eqs);
} }
new_a->m_def = a->m_def; new_a->m_def = a.m_def;
new_a->m_var = a->m_var; new_a->m_var = a.m_var;
// validate_atoms(); };
for (atom* a : m_bool_var2atom)
if (a)
clone_atom(*a);
// validate_atoms();
for (auto p : m_prop_queue) {
propagation_item q = p;
if (p.is_atom())
q = propagation_item(result->get_bv2a(p.m_atom->m_bv));
result->m_prop_queue.push_back(q);
} }
return result; return result;
} }

13
src/sat/smt/bv_solver.h
View file

@ -161,11 +161,11 @@ namespace bv {
struct atom { struct atom {
bool_var m_bv; bool_var m_bv;
eq_occurs* m_eqs; eq_occurs* m_eqs = nullptr;
var_pos_occ * m_occs; var_pos_occ * m_occs = nullptr;
svector<std::pair<atom*, eq_occurs*>> m_bit2occ; svector<std::pair<atom*, eq_occurs*>> m_bit2occ;
literal m_var { sat::null_literal }; literal m_var = sat::null_literal;
literal m_def { sat::null_literal }; literal m_def = sat::null_literal;
atom(bool_var b) :m_bv(b), m_eqs(nullptr), m_occs(nullptr) {} atom(bool_var b) :m_bv(b), m_eqs(nullptr), m_occs(nullptr) {}
~atom() { m_bit2occ.clear(); } ~atom() { m_bit2occ.clear(); }
var_pos_it begin() const { return var_pos_it(m_occs); } var_pos_it begin() const { return var_pos_it(m_occs); }
@ -174,11 +174,12 @@ namespace bv {
}; };
struct propagation_item { struct propagation_item {
var_pos m_vp { var_pos(0, 0) }; var_pos m_vp = var_pos(0, 0) ;
atom* m_atom{ nullptr }; atom* m_atom = nullptr;
explicit propagation_item(atom* a) : m_atom(a) {} explicit propagation_item(atom* a) : m_atom(a) {}
explicit propagation_item(var_pos const& vp) : m_vp(vp) {} 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; } bool operator==(propagation_item const& other) const { if (m_atom) return m_atom == other.m_atom; return false; }
bool is_atom() const { return m_atom != nullptr; }
}; };