mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-14 09:09:58 +00:00
Code Activity

Code simplifications in sls_euf_plugin.cpp and realclosure.cpp

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-10 16:17:24 +00:00
parent 54c692622c
commit 42eee12c2f
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)) {
a = g.find(to_app(e)->get_arg(0));
b = g.find(to_app(e)->get_arg(1));
}
if (lit.sign() && m.is_eq(e)) {
if (a && b && a->get_root() == b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not disequal " << lit << " " << mk_pp(e, m) << "\n");
ctx.display(verbose_stream());
UNREACHABLE();
if (lit.sign()) {
if (a && b && a->get_root() == b->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not disequal " << lit << " " << mk_pp(e, m) << "\n");
ctx.display(verbose_stream());
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)) {
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()) {
else if (to_app(e)->get_family_id() != basic_family_id) {
auto* ne = g.find(e);
auto* nf = g.find(m.mk_false());
if (ne && nf && ne->get_root() != nf->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not false " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
if (lit.sign()) {
auto* nf = g.find(m.mk_false());
if (ne && nf && ne->get_root() != nf->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not false " << 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* nt = g.find(m.mk_true());
if (ne && nt && ne->get_root() != nt->get_root()) {
IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n");
//UNREACHABLE();
else {
auto* nt = g.find(m.mk_true());
if (ne && nt && ne->get_root() != nt->get_root()) {
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;
}
unsigned get_sign_condition_size(numeral const &a, unsigned i) {
algebraic * ext = to_algebraic(to_rational_function(a)->ext());
sign_condition* get_ith_sign_condition(algebraic* ext, unsigned i) {
const sign_det * sdt = ext->sdt();
if (!sdt)
return 0;
return nullptr;
sign_condition * sc = sdt->sc(ext->sc_idx());
while (i) {
if (sc) sc = sc->prev();
while (i && sc) {
sc = sc->prev();
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)
return 0;
return ext->sdt()->qs()[sc->qidx()].size();
@ -3468,14 +3473,7 @@ namespace realclosure {
if (!is_algebraic(a))
return 0;
algebraic * ext = to_algebraic(to_rational_function(a)->ext());
const sign_det * sdt = ext->sdt();
if (!sdt)
return 0;
sign_condition * sc = sdt->sc(ext->sc_idx());
while (i) {
if (sc) sc = sc->prev();
i--;
}
sign_condition * sc = get_ith_sign_condition(ext, i);
if (!sc)
return 0;
const polynomial & q = ext->sdt()->qs()[sc->qidx()];
@ -3487,14 +3485,7 @@ namespace realclosure {
if (!is_algebraic(a))
return numeral();
algebraic * ext = to_algebraic(to_rational_function(a)->ext());
const sign_det * sdt = ext->sdt();
if (!sdt)
return numeral();
sign_condition * sc = sdt->sc(ext->sc_idx());
while (i) {
if (sc) sc = sc->prev();
i--;
}
sign_condition * sc = get_ith_sign_condition(ext, i);
if (!sc)
return numeral();
const polynomial & q = ext->sdt()->qs()[sc->qidx()];