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

remove memory leaks in nex_creator

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-04 17:23:16 -07:00
parent 3e009a237f
commit efe7d132ee
2 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/nex_creator.cpp
View file

@ -233,10 +233,7 @@ bool nex_creator::less_than_on_mul_nex(const nex_mul* a, const nex* b) const {
case expr_type::MUL: case expr_type::MUL:
return less_than_on_mul(a, to_mul(b)); return less_than_on_mul(a, to_mul(b));
case expr_type::SUM: case expr_type::SUM:
{ return lt(a, (*to_sum(b))[0]);
const nex* fc = *(to_sum(b)->begin());
return lt(a, fc);
}
default: default:
UNREACHABLE(); UNREACHABLE();
return false; return false;
@ -446,7 +443,7 @@ bool nex_creator::process_mul_in_simplify_sum(nex_mul* em, std::map<nex*, ration
if (em->size() == 2 && (*em)[1].pow() == 1) { if (em->size() == 2 && (*em)[1].pow() == 1) {
found = register_in_join_map(map, (*em)[1].e(), r); found = register_in_join_map(map, (*em)[1].e(), r);
} else { } else {
nex_mul * m = new nex_mul(); nex_mul * m = mk_mul();
for (it++; it != end; it++) { for (it++; it != end; it++) {
m->add_child_in_power(it->e(), it->pow()); m->add_child_in_power(it->e(), it->pow());
} }

7
src/math/lp/nex_creator.h
View file

@ -96,7 +96,7 @@ public:
void simplify_children_of_mul(vector<nex_pow> & children); void simplify_children_of_mul(vector<nex_pow> & children);
nex * clone(const nex* a) { nex * clone(const nex* a) {
switch (a->type()) { switch (a->type()) {
case expr_type::VAR: { case expr_type::VAR: {
auto v = to_var(a); auto v = to_var(a);
@ -148,7 +148,10 @@ public:
delete e; delete e;
m_allocated.clear(); m_allocated.clear();
} }
~nex_creator() {
clear();
}
unsigned size() const { return m_allocated.size(); } unsigned size() const { return m_allocated.size(); }
nex_sum* mk_sum() { nex_sum* mk_sum() {