mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-06 12:02:25 +00:00
Code Activity

remove unused code

Browse source
This commit is contained in:
Lev Nachmanson 2025-11-21 13:55:54 -10:00
parent 0886513de1
commit 26a472fb3c
1 changed files with 0 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

21
src/nlsat/nlsat_explain.cpp
View file

@ -921,27 +921,6 @@ namespace nlsat {
}
int ensure_sign(polynomial_ref & p) {
#if 0
polynomial_ref f(m_pm);
factor(p, m_factors);
m_is_even.reset();
unsigned num_factors = m_factors.size();
int s = 1;
for (unsigned i = 0; i < num_factors; i++) {
f = m_factors.get(i);
s *= sign(f);
m_is_even.push_back(false);
}
if (num_factors > 0) {
atom::kind k = atom::EQ;
if (s == 0) k = atom::EQ;
if (s < 0) k = atom::LT;
if (s > 0) k = atom::GT;
bool_var b = m_solver.mk_ineq_atom(k, num_factors, m_factors.c_ptr(), m_is_even.c_ptr());
add_literal(literal(b, true));
}
return s;
#else
int s = sign(p);
if (!is_const(p)) {
TRACE(nlsat_explain, tout << p << "\n";);