mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

port Grobner: address memory issues

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-28 11:50:51 -07:00
parent 36db31e154
commit 8744d987a3
2 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -184,15 +184,11 @@ bool nla_grobner::is_better_choice(equation * eq1, equation * eq2) {
} }
void nla_grobner::del_equation(equation * eq) { void nla_grobner::del_equation(equation * eq) {
NOT_IMPLEMENTED_YET();
/*
m_to_superpose.erase(eq); m_to_superpose.erase(eq);
m_to_simplify.erase(eq); m_to_simplify.erase(eq);
SASSERT(m_equations_to_delete[eq->m_bidx] == eq); SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
m_equations_to_delete[eq->m_bidx] = 0; m_equations_to_delete[eq->m_bidx] = 0;
del_monomials(eq->m_exp);
dealloc(eq); dealloc(eq);
*/
} }
nla_grobner::equation* nla_grobner::pick_next() { nla_grobner::equation* nla_grobner::pick_next() {
@ -526,7 +522,7 @@ void nla_grobner::superpose(equation * eq1, equation * eq2) {
if (!find_b_c(ab, ac, b, c)) { if (!find_b_c(ab, ac, b, c)) {
return; return;
} }
equation* eq = new equation(); // to do - need no remove !!!!!!!!!!!!!!!!!!! equation* eq = alloc(equation);
init_equation(eq, expr_superpose( eq1->exp(), eq2->exp(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep())); init_equation(eq, expr_superpose( eq1->exp(), eq2->exp(), ab, ac, b, c), m_dep_manager.mk_join(eq1->dep(), eq2->dep()));
insert_to_simplify(eq); insert_to_simplify(eq);
} }
@ -764,7 +760,7 @@ void nla_grobner::assert_eq_0(nex* e, ci_dependency * dep) {
TRACE("grobner", tout << "e = " << *e << "\n";); TRACE("grobner", tout << "e = " << *e << "\n";);
if (e == nullptr) if (e == nullptr)
return; return;
equation * eq = new equation(); equation * eq = alloc(equation);
init_equation(eq, e, dep); init_equation(eq, e, dep);
insert_to_simplify(eq); insert_to_simplify(eq);
} }
@ -779,6 +775,10 @@ void nla_grobner::init_equation(equation* eq, nex*e, ci_dependency * dep) {
SASSERT(m_equations_to_delete[eq->m_bidx] == eq); SASSERT(m_equations_to_delete[eq->m_bidx] == eq);
} }
nla_grobner::~nla_grobner() {
del_equations(0);
}
std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency* dep) const { std::ostream& nla_grobner::display_dependency(std::ostream& out, ci_dependency* dep) const {
svector<lp::constraint_index> expl; svector<lp::constraint_index> expl;
m_dep_manager.linearize(dep, expl); m_dep_manager.linearize(dep, expl);

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

@ -97,6 +97,7 @@ class nla_grobner : common {
public: public:
nla_grobner(core *core); nla_grobner(core *core);
void grobner_lemmas(); void grobner_lemmas();
~nla_grobner();
private: private:
bool scan_for_linear(ptr_vector<equation>& eqs); bool scan_for_linear(ptr_vector<equation>& eqs);
void find_nl_cluster(); void find_nl_cluster();