mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-25 11:26:21 +00:00
Code Activity

Refactor sat_anf_simplifier to use C++17 structured bindings (#8358)

Browse source 
* Initial plan

* Refactor sat_anf_simplifier.cpp to use C++17 structured bindings

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 09:59:26 -08:00 • committed by Nikolaj Bjorner
parent 531bb1c31f
commit b6dab1533b
1 changed files with 17 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/sat/sat_anf_simplifier.cpp
View file

@ -258,8 +258,9 @@ namespace sat {
} }
void anf_simplifier::set_relevant(solver::bin_clause const& b) { void anf_simplifier::set_relevant(solver::bin_clause const& b) {
set_relevant(b.first); auto [l1, l2] = b;
set_relevant(b.second); set_relevant(l1);
set_relevant(l2);
} }
void anf_simplifier::set_relevant(clause const& c) { void anf_simplifier::set_relevant(clause const& c) {
@ -272,7 +273,8 @@ namespace sat {
} }
bool anf_simplifier::is_pre_satisfied(solver::bin_clause const& b) { bool anf_simplifier::is_pre_satisfied(solver::bin_clause const& b) {
return phase_is_true(b.first) || phase_is_true(b.second); auto [l1, l2] = b;
return phase_is_true(l1) || phase_is_true(l2);
} }
bool anf_simplifier::phase_is_true(literal l) { bool anf_simplifier::phase_is_true(literal l) {
@ -286,7 +288,8 @@ namespace sat {
} }
bool anf_simplifier::has_relevant_var(solver::bin_clause const& b) { bool anf_simplifier::has_relevant_var(solver::bin_clause const& b) {
return is_relevant(b.first) || is_relevant(b.second); auto [l1, l2] = b;
return is_relevant(l1) || is_relevant(l2);
} }
/** /**
@ -310,8 +313,9 @@ namespace sat {
} }
static solver::bin_clause normalize(solver::bin_clause const& b) { static solver::bin_clause normalize(solver::bin_clause const& b) {
if (b.first.index() > b.second.index()) { auto [l1, l2] = b;
return solver::bin_clause(b.second, b.first); if (l1.index() > l2.index()) {
return solver::bin_clause(l2, l1);
} }
else { else {
return b; return b;
@ -368,7 +372,10 @@ namespace sat {
for (unsigned i = 0; i < nv; ++i) id2var[var2id[i]] = i; for (unsigned i = 0; i < nv; ++i) id2var[var2id[i]] = i;
for (unsigned i = 0; i < nv; ++i) vl[i] = std::make_pair(i, var2id[i]); for (unsigned i = 0; i < nv; ++i) vl[i] = std::make_pair(i, var2id[i]);
std::sort(vl.begin(), vl.end()); std::sort(vl.begin(), vl.end());
for (unsigned i = 0; i < nv; ++i) l2v[i] = id2var[vl[i].second]; for (unsigned i = 0; i < nv; ++i) {
auto [level, varid] = vl[i];
l2v[i] = id2var[varid];
}
ps.get_manager().reset(l2v); ps.get_manager().reset(l2v);
@ -387,10 +394,11 @@ namespace sat {
#define lit2pdd(_l_) (_l_.sign() ? ~m.mk_var(_l_.var()) : m.mk_var(_l_.var())) #define lit2pdd(_l_) (_l_.sign() ? ~m.mk_var(_l_.var()) : m.mk_var(_l_.var()))
void anf_simplifier::add_bin(solver::bin_clause const& b, pdd_solver& ps) { void anf_simplifier::add_bin(solver::bin_clause const& b, pdd_solver& ps) {
auto [l1, l2] = b;
auto& m = ps.get_manager(); auto& m = ps.get_manager();
dd::pdd p = (lit2pdd(b.first) | lit2pdd(b.second)) ^ true; dd::pdd p = (lit2pdd(l1) | lit2pdd(l2)) ^ true;
ps.add(p); ps.add(p);
TRACE(anf_simplifier, tout << "bin: " << b.first << " " << b.second << " : " << p << "\n";); TRACE(anf_simplifier, tout << "bin: " << l1 << " " << l2 << " : " << p << "\n";);
} }
void anf_simplifier::add_clause(clause const& c, pdd_solver& ps) { void anf_simplifier::add_clause(clause const& c, pdd_solver& ps) {