mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix #7248

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-06-12 14:26:35 -07:00
parent b831a589e5
commit 35c1cacf44
1 changed files with 15 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/math/grobner/grobner.cpp
View file

@ -468,12 +468,23 @@ void grobner::merge_monomials(ptr_vector<monomial> & monomials) {
void grobner::normalize_coeff(ptr_vector<monomial> & monomials) { void grobner::normalize_coeff(ptr_vector<monomial> & monomials) {
if (monomials.empty()) if (monomials.empty())
return; return;
unsigned sz = monomials.size();
rational c = monomials[0]->m_coeff; rational c = monomials[0]->m_coeff;
if (c.is_one()) if (c.is_one())
return; return;
unsigned sz = monomials.size(); if (c.is_minus_one()) {
for (unsigned i = 0; i < sz; i++) for (unsigned i = 0; i < sz && m_manager.inc(); i++)
monomials[i]->m_coeff.neg();
return;
}
if (c.bitsize() > 1000)
return;
for (unsigned i = 0; i < sz && m_manager.inc(); i++) {
if (monomials[i]->m_coeff.bitsize() > 1000)
continue;
monomials[i]->m_coeff /= c; monomials[i]->m_coeff /= c;
}
} }
/** /**
@ -611,6 +622,8 @@ grobner::equation * grobner::simplify(equation const * source, equation * target
TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source);); TRACE("grobner", tout << "simplifying: "; display_equation(tout, *target); tout << "using: "; display_equation(tout, *source););
if (source->get_num_monomials() == 0) if (source->get_num_monomials() == 0)
return nullptr; return nullptr;
if (!m_manager.inc())
return target;
m_stats.m_simplify++; m_stats.m_simplify++;
bool result = false; bool result = false;
bool simplified; bool simplified;