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

fix a bug in Rule 4.2

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-12-04 11:33:56 -10:00
parent 1ab5e04043
commit 83de6d7e6b
2 changed files with 22 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/nlsat/levelwise.cpp
View file

@ -297,6 +297,7 @@ namespace nlsat {
if (is_const(r)) continue; if (is_const(r)) continue;
TRACE(lws, tout << "resultant: "; ::nlsat::display(tout, m_solver, r); tout << std::endl;); TRACE(lws, tout << "resultant: "; ::nlsat::display(tout, m_solver, r); tout << std::endl;);
if (is_zero(r)) { if (is_zero(r)) {
TRACE(lws, tout << "fail\n";);
m_fail = true; m_fail = true;
return false; return false;
} }
@ -320,8 +321,10 @@ namespace nlsat {
collect_top_level_properties(ps_of_n_level); collect_top_level_properties(ps_of_n_level);
std::vector<std::pair<scoped_anum, poly*>> root_vals; std::vector<std::pair<scoped_anum, poly*>> root_vals;
collect_roots_for_ps(ps_of_n_level, root_vals); collect_roots_for_ps(ps_of_n_level, root_vals);
if (!add_adjacent_resultants(root_vals)) if (!add_adjacent_resultants(root_vals)) {
TRACE(lws, tout << "fail\n";);
m_fail = true; m_fail = true;
}
} }
@ -560,6 +563,7 @@ namespace nlsat {
if (!is_const(disc)) { if (!is_const(disc)) {
for_each_distinct_factor(disc, [&](polynomial::polynomial_ref f) { for_each_distinct_factor(disc, [&](polynomial::polynomial_ref f) {
if (coeffs_are_zeroes_on_sample(f, m_pm, sample(), m_am)) { if (coeffs_are_zeroes_on_sample(f, m_pm, sample(), m_am)) {
TRACE(lws, tout << "fail\n";);
m_fail = true; // ambiguous multiplicity -- not handled yet m_fail = true; // ambiguous multiplicity -- not handled yet
return; return;
} }
@ -579,6 +583,7 @@ namespace nlsat {
if (!is_const(lc)) { if (!is_const(lc)) {
for_each_distinct_factor(lc, [&](polynomial::polynomial_ref f) { for_each_distinct_factor(lc, [&](polynomial::polynomial_ref f) {
if (coeffs_are_zeroes_on_sample(f, m_pm, sample(), m_am)) { if (coeffs_are_zeroes_on_sample(f, m_pm, sample(), m_am)) {
TRACE(lws, tout << "fail\n";);
m_fail = true; m_fail = true;
return; return;
} }
@ -702,11 +707,12 @@ namespace nlsat {
if (sign(coeff, sample(), m_am) == 0) if (sign(coeff, sample(), m_am) == 0)
continue; continue;
for_first_distinct_factor(coeff, [&](const polynomial::polynomial_ref & f) { for_each_distinct_factor(coeff, [&](const polynomial::polynomial_ref & f) {
mk_prop(prop_enum::sgn_inv, f); mk_prop(prop_enum::sgn_inv, f);
}); });
return true; return true;
} }
TRACE(lws, tout << "false\n";);
return false; return false;
} }
@ -860,7 +866,11 @@ or
// nothing is added // nothing is added
} else { } else {
polynomial_ref res = resultant(polynomial_ref(I.l, m_pm), p.m_poly, m_level); polynomial_ref res = resultant(polynomial_ref(I.l, m_pm), p.m_poly, m_level);
if (m_pm.is_zero(res)) { m_fail = true; return;} if (m_pm.is_zero(res)) {
TRACE(lws, tout << "fail\n";);
m_fail = true;
return;
}
// Factor the resultant and add ord_inv for each distinct non-constant factor // Factor the resultant and add ord_inv for each distinct non-constant factor
for_each_distinct_factor(res, [&](polynomial::polynomial_ref f) { mk_prop(prop_enum::ord_inv, f);}); for_each_distinct_factor(res, [&](polynomial::polynomial_ref f) { mk_prop(prop_enum::ord_inv, f);});
} }
@ -981,6 +991,7 @@ or
polynomial_ref r(m_pm); polynomial_ref r(m_pm);
r = resultant(polynomial_ref(a, m_pm), polynomial_ref(b, m_pm), m_level); r = resultant(polynomial_ref(a, m_pm), polynomial_ref(b, m_pm), m_level);
if (m_pm.is_zero(r)) { if (m_pm.is_zero(r)) {
TRACE(lws, tout << "fail\n";);
m_fail = true; m_fail = true;
return; return;
} }

9
src/nlsat/nlsat_solver.cpp
View file

@ -1174,6 +1174,10 @@ namespace nlsat {
used_vars[v] = true; used_vars[v] = true;
} }
display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n"; display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n";
if (m_lemma_count == 60) {
enable_trace("lws");
enable_trace("nlsat_explain");
}
if (m_log_lemma_smtrat) if (m_log_lemma_smtrat)
out << "(set-logic NRA)\n"; out << "(set-logic NRA)\n";
else else
@ -1187,7 +1191,10 @@ namespace nlsat {
for (unsigned i = 0; i < n; ++i) for (unsigned i = 0; i < n; ++i)
display_smt2(out << "(assert ", ~cls[i]) << ")\n"; display_smt2(out << "(assert ", ~cls[i]) << ")\n";
out << "(check-sat)\n(reset)\n"; out << "(check-sat)\n(reset)\n";
if (m_lemma_count == 62) {
std::cout << "early exit\n";
exit(1);
}
} }
clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) { clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {