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 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 GitHub
parent e4ba45925e
commit 851e69d7d2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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) {
m_consequent = c;
m_eq = p;
if (m_eq.first && m_eq.first->get_id() > m_eq.second->get_id())
std::swap(m_eq.first, m_eq.second);
auto& [n1, n2] = m_eq;
if (n1 && n1->get_id() > n2->get_id())
std::swap(n1, n2);
m_proof_hint = pma;
m_num_literals = n_lits;
m_num_eqs = n_eqs;
@ -246,8 +247,9 @@ namespace euf {
m_eqs = reinterpret_cast<enode_pair*>(base_ptr);
for (i = 0; i < n_eqs; ++i) {
m_eqs[i] = eqs[i];
if (m_eqs[i].first->get_id() > m_eqs[i].second->get_id())
std::swap(m_eqs[i].first, m_eqs[i].second);
auto& [n1, n2] = m_eqs[i];
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 {
for (auto lit : euf::th_explain::lits(*this))
out << lit << " ";
for (auto eq : euf::th_explain::eqs(*this))
out << eq.first->get_expr_id() << " == " << eq.second->get_expr_id() << " ";
for (auto [n1, n2] : euf::th_explain::eqs(*this))
out << n1->get_expr_id() << " == " << n2->get_expr_id() << " ";
if (m_consequent != sat::null_literal)
out << "--> " << m_consequent;
if (m_eq.first != nullptr)
out << "--> " << m_eq.first->get_expr_id() << " == " << m_eq.second->get_expr_id();
auto [n1, n2] = m_eq;
if (n1 != nullptr)
out << "--> " << n1->get_expr_id() << " == " << n2->get_expr_id();
if (m_proof_hint != nullptr)
out << " p ";
return out;