mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-26 01:14:36 +00:00
Code Activity

fix an assert statement

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-10-17 18:08:01 -07:00
parent 881d74278d
commit b09199c6e6
3 changed files with 25 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/nlsat/levelwise.cpp
View file

@ -475,7 +475,7 @@ namespace nlsat {
// add a property to m_Q if an equivalent one is not already present.
// Equivalence: same m_prop_tag and same level; require the same poly as well.
void add_to_Q_if_new(const property & pr, unsigned level) {
SASSERT(pr.m_prop_tag != ord_inv || (pr.m_poly && !m_pm.is_zero(pr.m_poly)));
for (auto const & q : to_vector(m_Q[level])) {
if (q.m_prop_tag != pr.m_prop_tag) continue;
if (q.m_poly != pr.m_poly) continue;
@ -800,12 +800,9 @@ or
// nothing is added
} else {
polynomial_ref res = resultant(polynomial_ref(I.l, m_pm), p.m_poly, m_level);
if (res) {
if (m_pm.is_zero(res)) { m_fail = true; return;}
// 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);});
}
} else {
/*
@ -920,8 +917,13 @@ or
poly *a = m_rel.m_rfunc[pair.first].ire.p;
poly *b = m_rel.m_rfunc[pair.second].ire.p;
SASSERT(max_var(a) == max_var(b) && max_var(b) == m_level) ;
polynomial_ref r(m_pm);
r = resultant(polynomial_ref(a, m_pm), polynomial_ref(b, m_pm), m_level);
if (m_pm.is_zero(r)) {
m_fail = true;
return;
}
TRACE(lws, tout << "resultant of (" << pair.first << "," << pair.second << "):";
::nlsat::display(tout, m_solver, a) << "\n";
::nlsat::display(tout,m_solver, b)<< "\nresultant:"; ::nlsat::display(tout, m_solver, r) << "\n");

2
src/nlsat/nlsat_explain.cpp
View file

@ -1156,7 +1156,7 @@ namespace nlsat {
m_todo.reset();
break;
}
TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, m_solver, x);
TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, m_solver, x);
tout << "\npolynomials\n";
display(tout, m_solver, ps); tout << "\n";);
add_lcs(ps, x);

22
src/nlsat/nlsat_solver.cpp
View file

@ -1,3 +1,4 @@
// int tttt = 0;
/*++
Copyright (c) 2012 Microsoft Corporation
@ -1116,8 +1117,9 @@ namespace nlsat {
}
void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid) {
++m_lemma_count;
out << "(set-logic NRA)\n";
// ++tttt;
// if (tttt != 5225555) return;
out << "(set-logic NIA)\n";
if (is_valid) {
display_smt2_bool_decls(out);
display_smt2_arith_decls(out);
@ -1126,10 +1128,14 @@ namespace nlsat {
display_smt2(out);
for (unsigned i = 0; i < n; ++i)
display_smt2(out << "(assert ", ~cls[i]) << ")\n";
display(out << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n";
display(out << "(echo \"#" << m_lemma_count++ /*tttt*/ << " ", n, cls) << "\")\n";
out << "(check-sat)\n(reset)\n";
TRACE(nlsat, display(tout << "(echo \"#" << m_lemma_count << " ", n, cls) << "\")\n");
// if (tttt == 5223333) {
// std::cout << "exit\n";
// exit(1);
// }
}
clause * mk_clause_core(unsigned num_lits, literal const * lits, bool learned, _assumption_set a) {
@ -2200,6 +2206,13 @@ namespace nlsat {
}
void resolve_lazy_justification(bool_var b, lazy_justification const & jst) {
// if (tttt == 52133333) {
// enable_trace("nlsat");
// enable_trace("nlsat_solver");
// enable_trace("nlsat_explain");
// enable_trace("lws");
// enable_trace("nlsat_resolve");
// }
TRACE(nlsat_resolve, tout << "resolving lazy_justification for b" << b << "\n";);
unsigned sz = jst.num_lits();
@ -2211,9 +2224,6 @@ namespace nlsat {
print_out_as_math(verbose_stream(), jst) << std::endl;
// verbose_stream() << "\nend of assignment lemma\n";
}
m_lazy_clause.reset();
m_explain.compute_conflict_explanation(jst.num_lits(), jst.lits(), m_lazy_clause);