mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-02 15:17:54 +00:00
Code Activity

Merge pull request #8918 from Z3Prover/copilot/code-simplification-march-2026

Browse source 
Simplify conditional logic in sls_euf_plugin.cpp and extract sign condition helper in realclosure.cpp
This commit is contained in:
Nikolaj Bjorner 2026-03-10 10:03:22 -07:00 • committed by GitHub
commit bb11a56a67
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 37 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

49
src/ast/sls/sls_euf_plugin.cpp
View file

@ -287,34 +287,35 @@ namespace sls {
if (m.is_eq(e)) { if (m.is_eq(e)) {
a = g.find(to_app(e)->get_arg(0)); a = g.find(to_app(e)->get_arg(0));
b = g.find(to_app(e)->get_arg(1)); b = g.find(to_app(e)->get_arg(1));
} if (lit.sign()) {
if (lit.sign() && m.is_eq(e)) { if (a && b && a->get_root() == b->get_root()) {
if (a && b && a->get_root() == b->get_root()) { IF_VERBOSE(0, verbose_stream() << "not disequal " << lit << " " << mk_pp(e, m) << "\n");
IF_VERBOSE(0, verbose_stream() << "not disequal " << lit << " " << mk_pp(e, m) << "\n"); ctx.display(verbose_stream());
ctx.display(verbose_stream()); UNREACHABLE();
UNREACHABLE(); }
}
else {
if (a && b && a->get_root() != b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not equal " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
} }
} }
else if (!lit.sign() && m.is_eq(e)) { else if (to_app(e)->get_family_id() != basic_family_id) {
if (a && b && a->get_root() != b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not equal " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
}
else if (to_app(e)->get_family_id() != basic_family_id && lit.sign()) {
auto* ne = g.find(e); auto* ne = g.find(e);
auto* nf = g.find(m.mk_false()); if (lit.sign()) {
if (ne && nf && ne->get_root() != nf->get_root()) { auto* nf = g.find(m.mk_false());
IF_VERBOSE(0, verbose_stream() << "not false " << lit << " " << mk_pp(e, m) << "\n"); if (ne && nf && ne->get_root() != nf->get_root()) {
//UNREACHABLE(); IF_VERBOSE(0, verbose_stream() << "not false " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
}
} }
} else {
else if (to_app(e)->get_family_id() != basic_family_id && !lit.sign()) { auto* nt = g.find(m.mk_true());
auto* ne = g.find(e); if (ne && nt && ne->get_root() != nt->get_root()) {
auto* nt = g.find(m.mk_true()); IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n");
if (ne && nt && ne->get_root() != nt->get_root()) { //UNREACHABLE();
IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n"); }
//UNREACHABLE();
} }
} }

33
src/math/realclosure/realclosure.cpp
View file

@ -3448,16 +3448,21 @@ namespace realclosure {
return true; return true;
} }
unsigned get_sign_condition_size(numeral const &a, unsigned i) { sign_condition* get_ith_sign_condition(algebraic* ext, unsigned i) {
algebraic * ext = to_algebraic(to_rational_function(a)->ext());
const sign_det * sdt = ext->sdt(); const sign_det * sdt = ext->sdt();
if (!sdt) if (!sdt)
return 0; return nullptr;
sign_condition * sc = sdt->sc(ext->sc_idx()); sign_condition * sc = sdt->sc(ext->sc_idx());
while (i) { while (i && sc) {
if (sc) sc = sc->prev(); sc = sc->prev();
i--; i--;
} }
return sc;
}
unsigned get_sign_condition_size(numeral const &a, unsigned i) {
algebraic * ext = to_algebraic(to_rational_function(a)->ext());
sign_condition * sc = get_ith_sign_condition(ext, i);
if (!sc) if (!sc)
return 0; return 0;
return ext->sdt()->qs()[sc->qidx()].size(); return ext->sdt()->qs()[sc->qidx()].size();
@ -3468,14 +3473,7 @@ namespace realclosure {
if (!is_algebraic(a)) if (!is_algebraic(a))
return 0; return 0;
algebraic * ext = to_algebraic(to_rational_function(a)->ext()); algebraic * ext = to_algebraic(to_rational_function(a)->ext());
const sign_det * sdt = ext->sdt(); sign_condition * sc = get_ith_sign_condition(ext, i);
if (!sdt)
return 0;
sign_condition * sc = sdt->sc(ext->sc_idx());
while (i) {
if (sc) sc = sc->prev();
i--;
}
if (!sc) if (!sc)
return 0; return 0;
const polynomial & q = ext->sdt()->qs()[sc->qidx()]; const polynomial & q = ext->sdt()->qs()[sc->qidx()];
@ -3487,14 +3485,7 @@ namespace realclosure {
if (!is_algebraic(a)) if (!is_algebraic(a))
return numeral(); return numeral();
algebraic * ext = to_algebraic(to_rational_function(a)->ext()); algebraic * ext = to_algebraic(to_rational_function(a)->ext());
const sign_det * sdt = ext->sdt(); sign_condition * sc = get_ith_sign_condition(ext, i);
if (!sdt)
return numeral();
sign_condition * sc = sdt->sc(ext->sc_idx());
while (i) {
if (sc) sc = sc->prev();
i--;
}
if (!sc) if (!sc)
return numeral(); return numeral();
const polynomial & q = ext->sdt()->qs()[sc->qidx()]; const polynomial & q = ext->sdt()->qs()[sc->qidx()];