mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-28 21:08:43 +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 GitHub
parent de445858b3
commit cd774b6fdb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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) {
set_relevant(b.first);
set_relevant(b.second);
auto [l1, l2] = b;
set_relevant(l1);
set_relevant(l2);
}
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) {
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) {
@ -286,7 +288,8 @@ namespace sat {
}
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) {
if (b.first.index() > b.second.index()) {
return solver::bin_clause(b.second, b.first);
auto [l1, l2] = b;
if (l1.index() > l2.index()) {
return solver::bin_clause(l2, l1);
}
else {
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) vl[i] = std::make_pair(i, var2id[i]);
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);
@ -387,10 +394,11 @@ namespace sat {
#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) {
auto [l1, l2] = b;
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);
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) {