mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 20:05:51 +00:00
Code Activity

revert the behavior of add_zero_assumption (#7631)

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-04-28 16:07:46 -07:00 • committed by GitHub
parent 6af61fa0f4
commit f89e133d52
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 1 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/nlsat/nlsat_explain.cpp
View file

@ -282,8 +282,6 @@ namespace nlsat {
// then only the factors that are zero in the current interpretation needed to be considered. // then only the factors that are zero in the current interpretation needed to be considered.
// I don't want to create a nested conjunction in the clause. // I don't want to create a nested conjunction in the clause.
// Then, I assert p_i1 * ... * p_im != 0 // Then, I assert p_i1 * ... * p_im != 0
bool is_linear = true;
unsigned x = max_var(p);
{ {
restore_factors _restore(m_factors, m_factors_save); restore_factors _restore(m_factors, m_factors_save);
factor(p, m_factors); factor(p, m_factors);
@ -296,33 +294,10 @@ namespace nlsat {
if (is_zero(sign(f))) { if (is_zero(sign(f))) {
m_zero_fs.push_back(m_factors.get(i)); m_zero_fs.push_back(m_factors.get(i));
m_is_even.push_back(false); m_is_even.push_back(false);
is_linear &= m_pm.degree(f, x) <= 1;
} }
} }
} }
if (!is_linear) {
scoped_anum_vector& roots = m_roots_tmp;
roots.reset();
m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
unsigned num_roots = roots.size();
if (num_roots > 0) {
anum const& x_val = m_assignment.value(x);
for (unsigned i = 0; i < num_roots; i++) {
int s = m_am.compare(x_val, roots[i]);
if (s != 0)
continue;
TRACE("nlsat_explain", tout << "adding (zero assumption) root " << "\n");
add_root_literal(atom::ROOT_EQ, x, i + 1, p);
return;
}
display(verbose_stream() << "polynomial ", p);
m_solver.display(verbose_stream());
UNREACHABLE();
}
}
SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it. SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it.
literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data()); literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data());
l.neg(); l.neg();
TRACE("nlsat_explain", tout << "adding (zero assumption) literal:\n"; display(tout, l); tout << "\n";); TRACE("nlsat_explain", tout << "adding (zero assumption) literal:\n"; display(tout, l); tout << "\n";);

2
src/nlsat/nlsat_solver.cpp
View file

@ -3400,7 +3400,7 @@ namespace nlsat {
case atom::ROOT_GT: out << "(> "; proc(out, a.x()); out << " " << yn << ")"; break; case atom::ROOT_GT: out << "(> "; proc(out, a.x()); out << " " << yn << ")"; break;
case atom::ROOT_LE: out << "(<= "; proc(out, a.x()); out << " " << yn << ")"; break; case atom::ROOT_LE: out << "(<= "; proc(out, a.x()); out << " " << yn << ")"; break;
case atom::ROOT_GE: out << "(>= "; proc(out, a.x()); out << " " << yn << ")"; break; case atom::ROOT_GE: out << "(>= "; proc(out, a.x()); out << " " << yn << ")"; break;
case atom::ROOT_EQ: out << "(= "; proc(out, a.x()); out << " " << yn << ")"; NOT_IMPLEMENTED_YET(); break; case atom::ROOT_EQ: out << "(= "; proc(out, a.x()); out << " " << yn << ")"; break;
default: UNREACHABLE(); break; default: UNREACHABLE(); break;
} }
out << "))"; out << "))";