mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-03 07:37:54 +00:00
Code Activity

Refactor sat_th to use structured bindings for enode_pair patterns (#8386)

Browse source 
* Initial plan

* Apply structured bindings to enode_pair patterns in sat_th.cpp

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 12:02:28 -08:00 • committed by Nikolaj Bjorner
parent c7a4b6e4c4
commit 49cb81d538
1 changed files with 11 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/sat/smt/sat_th.cpp
View file

@ -232,8 +232,9 @@ namespace euf {
th_explain::th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& p, th_proof_hint const* pma) { th_explain::th_explain(unsigned n_lits, sat::literal const* lits, unsigned n_eqs, enode_pair const* eqs, sat::literal c, enode_pair const& p, th_proof_hint const* pma) {
m_consequent = c; m_consequent = c;
m_eq = p; m_eq = p;
if (m_eq.first && m_eq.first->get_id() > m_eq.second->get_id()) auto& [n1, n2] = m_eq;
std::swap(m_eq.first, m_eq.second); if (n1 && n1->get_id() > n2->get_id())
std::swap(n1, n2);
m_proof_hint = pma; m_proof_hint = pma;
m_num_literals = n_lits; m_num_literals = n_lits;
m_num_eqs = n_eqs; m_num_eqs = n_eqs;
@ -246,8 +247,9 @@ namespace euf {
m_eqs = reinterpret_cast<enode_pair*>(base_ptr); m_eqs = reinterpret_cast<enode_pair*>(base_ptr);
for (i = 0; i < n_eqs; ++i) { for (i = 0; i < n_eqs; ++i) {
m_eqs[i] = eqs[i]; m_eqs[i] = eqs[i];
if (m_eqs[i].first->get_id() > m_eqs[i].second->get_id()) auto& [n1, n2] = m_eqs[i];
std::swap(m_eqs[i].first, m_eqs[i].second); if (n1->get_id() > n2->get_id())
std::swap(n1, n2);
} }
} }
@ -303,12 +305,13 @@ namespace euf {
std::ostream& th_explain::display(std::ostream& out) const { std::ostream& th_explain::display(std::ostream& out) const {
for (auto lit : euf::th_explain::lits(*this)) for (auto lit : euf::th_explain::lits(*this))
out << lit << " "; out << lit << " ";
for (auto eq : euf::th_explain::eqs(*this)) for (auto [n1, n2] : euf::th_explain::eqs(*this))
out << eq.first->get_expr_id() << " == " << eq.second->get_expr_id() << " "; out << n1->get_expr_id() << " == " << n2->get_expr_id() << " ";
if (m_consequent != sat::null_literal) if (m_consequent != sat::null_literal)
out << "--> " << m_consequent; out << "--> " << m_consequent;
if (m_eq.first != nullptr) auto [n1, n2] = m_eq;
out << "--> " << m_eq.first->get_expr_id() << " == " << m_eq.second->get_expr_id(); if (n1 != nullptr)
out << "--> " << n1->get_expr_id() << " == " << n2->get_expr_id();
if (m_proof_hint != nullptr) if (m_proof_hint != nullptr)
out << " p "; out << " p ";
return out; return out;