mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-03 07:37:54 +00:00
Code Activity

nla_grobner: remove dead code and fix indentation (#9423)

Browse source 
* Initial plan

* [code-simplifier] nla_grobner: remove dead code and fix indentation

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/1dc7dd96-d7d7-4fca-94b4-bde677fee842

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-04-29 11:12:45 -07:00 • committed by GitHub
parent 6d38d5ed41
commit 09396b72dd
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/math/lp/nla_grobner.cpp
View file

@ -108,10 +108,6 @@ namespace nla {
} }
} }
// DEBUG_CODE(for (auto e : m_solver.equations()) check_missing_propagation(*e););
// for (auto e : m_solver.equations()) check_missing_propagation(*e);
if (c().params().arith_nl_grobner_adaptive()) if (c().params().arith_nl_grobner_adaptive())
update_growth_boost(productive); update_growth_boost(productive);
@ -120,7 +116,7 @@ namespace nla {
++m_delay_base; ++m_delay_base;
if (m_quota > 0) if (m_quota > 0)
--m_quota; --m_quota;
IF_VERBOSE(5, verbose_stream() << "grobner miss, quota " << m_quota << "\n"); IF_VERBOSE(5, verbose_stream() << "grobner miss, quota " << m_quota << "\n");
IF_VERBOSE(5, diagnose_pdd_miss(verbose_stream())); IF_VERBOSE(5, diagnose_pdd_miss(verbose_stream()));
@ -235,8 +231,6 @@ namespace nla {
if (vars.empty() || !q.is_linear()) if (vars.empty() || !q.is_linear())
return false; return false;
// IF_VERBOSE(0, verbose_stream() << "factored " << q << " : " << vars << "\n");
auto [t, offset] = linear_to_term(q); auto [t, offset] = linear_to_term(q);
vector<ineq> ineqs; vector<ineq> ineqs;
@ -251,7 +245,6 @@ namespace nla {
add_dependencies(lemma, eq); add_dependencies(lemma, eq);
for (auto const& i : ineqs) for (auto const& i : ineqs)
lemma |= i; lemma |= i;
//lemma.display(verbose_stream());
return true; return true;
} }
@ -584,19 +577,6 @@ namespace nla {
} }
TRACE(grobner, m_solver.display(tout)); TRACE(grobner, m_solver.display(tout));
#if 0
IF_VERBOSE(2, m_pdd_grobner.display(verbose_stream()));
dd::pdd_eval eval(m_pdd_manager);
eval.var2val() = [&](unsigned j){ return val(j); };
for (auto* e : m_pdd_grobner.equations()) {
dd::pdd p = e->poly();
rational v = eval(p);
if (p.is_linear() && !eval(p).is_zero()) {
IF_VERBOSE(0, verbose_stream() << "violated linear constraint " << p << "\n");
}
}
#endif
struct dd::solver::config cfg; struct dd::solver::config cfg;
cfg.m_max_steps = m_solver.equations().size(); cfg.m_max_steps = m_solver.equations().size();
cfg.m_max_simplified = c().params().arith_nl_grobner_max_simplified(); cfg.m_max_simplified = c().params().arith_nl_grobner_max_simplified();
@ -628,8 +608,6 @@ namespace nla {
std::ostream& grobner::diagnose_pdd_miss(std::ostream& out) { std::ostream& grobner::diagnose_pdd_miss(std::ostream& out) {
// m_pdd_grobner.display(out);
dd::pdd_eval eval; dd::pdd_eval eval;
eval.var2val() = [&](unsigned j){ return val(j); }; eval.var2val() = [&](unsigned j){ return val(j); };
for (auto* e : m_solver.equations()) { for (auto* e : m_solver.equations()) {