mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

more agressive freeing memory from nla_grobner

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-17 11:42:36 -10:00
parent 62dc731b5b
commit 13ff96b40b
2 changed files with 12 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -220,18 +220,24 @@ bool grobner_core::compute_basis_step() {
return true; return true;
} }
m_stats.m_compute_steps++; m_stats.m_compute_steps++;
simplify_using_to_superpose(*eq); unsigned mem_size = m_nex_creator.size();
simplify_eq_by_using_to_superpose(*eq);
if (equation_is_too_complex(eq)) if (equation_is_too_complex(eq)) {
m_nex_creator.pop(mem_size);
return false; return false;
}
mem_size = m_nex_creator.size();
if (!simplify_to_superpose_with_eq(eq)) { if (!simplify_to_superpose_with_eq(eq)) {
m_nex_creator.pop(mem_size);
return false; return false;
} }
TRACE("grobner", tout << "eq = "; display_equation(tout, *eq);); TRACE("grobner", tout << "eq = "; display_equation(tout, *eq););
mem_size = m_nex_creator.size();
superpose(eq); superpose(eq);
if (equation_is_too_complex(eq)) { if (equation_is_too_complex(eq)) {
TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";); TRACE("grobner", display_equation(tout, *eq) << " is too complex: deleting it\n;";);
del_equation(eq); del_equation(eq);
m_nex_creator.pop(mem_size);
return false; return false;
} }
insert_to_superpose(eq); insert_to_superpose(eq);
@ -259,7 +265,7 @@ grobner_core::equation* grobner_core::pick_next() {
return r; return r;
} }
void grobner_core::simplify_using_to_superpose(equation& eq) { void grobner_core::simplify_eq_by_using_to_superpose(equation& eq) {
bool simplified; bool simplified;
TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";); TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of m_to_superpose of size " << m_to_superpose.size() << "\n";);
do { do {

2
src/math/lp/nla_grobner.h
View file

@ -121,7 +121,7 @@ private:
bool compute_basis_step(); bool compute_basis_step();
bool simplify_source_target(equation const& source, equation& target); bool simplify_source_target(equation const& source, equation& target);
void simplify_using_to_superpose(equation &); void simplify_eq_by_using_to_superpose(equation &);
bool simplify_target_monomials(equation const& source, equation& target); bool simplify_target_monomials(equation const& source, equation& target);
void process_simplified_target(equation* target, ptr_buffer<equation>& to_remove); void process_simplified_target(equation* target, ptr_buffer<equation>& to_remove);
bool simplify_to_superpose_with_eq(equation*); bool simplify_to_superpose_with_eq(equation*);