mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-28 12:58:43 +00:00
Code Activity

Refactor bv_solver to use structured bindings for var_pos patterns (#8384)

Browse source 
* Initial plan

* Refactor bv_solver.cpp to use C++17 structured bindings for var_pos patterns

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback: simplify bit_trail constructor and remove unnecessary pair reconstruction

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-27 11:48:21 -08:00 • committed by GitHub
parent ea1ebdeae0
commit ccc20449dc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 23 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -29,10 +29,14 @@ namespace bv {
solver::var_pos vp;
sat::literal lit;
public:
bit_trail(solver& s, var_pos vp) : s(s), vp(vp), lit(s.m_bits[vp.first][vp.second]) {}
bit_trail(solver& s, var_pos vp) : s(s), vp(vp) {
auto [v, idx] = vp;
lit = s.m_bits[v][idx];
}
void undo() override {
s.m_bits[vp.first][vp.second] = lit;
auto [v, idx] = vp;
s.m_bits[v][idx] = lit;
}
};
@ -149,9 +153,7 @@ namespace bv {
void solver::find_new_diseq_axioms(atom& a, theory_var v, unsigned idx) {
literal l = m_bits[v][idx];
l.neg();
for (auto vp : a) {
theory_var v2 = vp.first;
unsigned idx2 = vp.second;
for (auto [v2, idx2] : a) {
if (idx == idx2 && m_bits[v2].size() == m_bits[v].size() && m_bits[v2][idx2] == l )
mk_new_diseq_axiom(v, v2, idx);
}
@ -190,8 +192,8 @@ namespace bv {
}
}
else if (m.is_bool(e) && (a = m_bool_var2atom.get(expr2literal(e).var(), nullptr))) {
for (var_pos vp : *a)
out << " " << var2enode(vp.first)->get_expr_id() << "[" << vp.second << "]";
for (auto [v, idx] : *a)
out << " " << var2enode(v)->get_expr_id() << "[" << idx << "]";
}
else
out << " " << mk_bounded_pp(e, m, 1);
@ -527,8 +529,8 @@ namespace bv {
if (a) {
force_push();
m_prop_queue.push_back(propagation_item(a));
for (auto p : a->m_bit2occ)
del_eq_occurs(p.first, p.second);
for (auto [v, idx] : a->m_bit2occ)
del_eq_occurs(v, idx);
}
}
@ -581,8 +583,7 @@ namespace bv {
}
bool solver::propagate_bits(var_pos entry) {
theory_var v1 = entry.first;
unsigned idx = entry.second;
auto [v1, idx] = entry;
SASSERT(idx < m_bits[v1].size());
if (m_wpos[v1] == idx)
find_wpos(v1);
@ -632,8 +633,8 @@ namespace bv {
for (auto kv : m_delay_internalize)
delay.push_back(std::make_pair(kv.m_key, kv.m_value));
flet<bool> _cheap1(m_cheap_axioms, true);
for (auto kv : delay)
if (!check_delay_internalized(kv.first))
for (auto [e, mode] : delay)
if (!check_delay_internalized(e))
ok = false;
if (!ok)
return sat::check_result::CR_CONTINUE;
@ -641,8 +642,8 @@ namespace bv {
// if (repair_model()) return sat::check_result::DONE;
flet<bool> _cheap2(m_cheap_axioms, false);
for (auto kv : delay)
if (!check_delay_internalized(kv.first))
for (auto [e, mode] : delay)
if (!check_delay_internalized(e))
ok = false;
if (!ok)
@ -678,16 +679,16 @@ namespace bv {
atom* a = get_bv2a(l.var());
if (!a)
return true;
for (auto vp : *a) {
sat::literal l2 = m_bits[vp.first][vp.second];
for (auto [v, idx] : *a) {
sat::literal l2 = m_bits[v][idx];
if (l2.var() == r.var())
continue;
SASSERT(l2.var() == l.var());
VERIFY(l2.var() == l.var());
sat::literal r2 = (l.sign() == l2.sign()) ? r : ~r;
ctx.push(vector2_value_trail<bits_vector, sat::literal>(m_bits, vp.first, vp.second));
m_bits[vp.first][vp.second] = r2;
set_bit_eh(vp.first, r2, vp.second);
ctx.push(vector2_value_trail<bits_vector, sat::literal>(m_bits, v, idx));
m_bits[v][idx] = r2;
set_bit_eh(v, r2, idx);
}
ctx.push(bit_occs_trail(*this, *a));
a->m_occs = nullptr;
@ -773,8 +774,8 @@ namespace bv {
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 [v, idx] : a)
out << v << "[" << idx << "]\n";
for (auto e : a.eqs())
out << e.m_bv1 << " " << e.m_bv2 << "\n";
return out;