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

fix memory leak in relation_manager, use for loops

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-14 10:16:03 -07:00
parent 187f1a8cbd
commit e94b97376c
1 changed files with 36 additions and 66 deletions
Download patch file Download diff file Expand all files Collapse all files

88
src/muz/rel/dl_relation_manager.cpp
View file

@ -210,11 +210,9 @@ namespace datalog {
if(m_favourite_relation_plugin && m_favourite_relation_plugin->can_handle_signature(s)) { if(m_favourite_relation_plugin && m_favourite_relation_plugin->can_handle_signature(s)) {
return m_favourite_relation_plugin; return m_favourite_relation_plugin;
} }
relation_plugin_vector::iterator rpit = m_relation_plugins.begin(); for (auto * r : m_relation_plugins) {
relation_plugin_vector::iterator rpend = m_relation_plugins.end(); if (r->can_handle_signature(s)) {
for(; rpit!=rpend; ++rpit) { return r;
if((*rpit)->can_handle_signature(s)) {
return *rpit;
} }
} }
return nullptr; return nullptr;
@ -232,11 +230,9 @@ namespace datalog {
if (m_favourite_table_plugin && m_favourite_table_plugin->can_handle_signature(t)) { if (m_favourite_table_plugin && m_favourite_table_plugin->can_handle_signature(t)) {
return m_favourite_table_plugin; return m_favourite_table_plugin;
} }
table_plugin_vector::iterator tpit = m_table_plugins.begin(); for (auto * a : m_table_plugins) {
table_plugin_vector::iterator tpend = m_table_plugins.end(); if (a->can_handle_signature(t)) {
for(; tpit!=tpend; ++tpit) { return a;
if((*tpit)->can_handle_signature(t)) {
return *tpit;
} }
} }
return nullptr; return nullptr;
@ -251,11 +247,9 @@ namespace datalog {
} }
relation_plugin * relation_manager::get_relation_plugin(symbol const& s) { relation_plugin * relation_manager::get_relation_plugin(symbol const& s) {
relation_plugin_vector::iterator rpit = m_relation_plugins.begin(); for (auto* r : m_relation_plugins) {
relation_plugin_vector::iterator rpend = m_relation_plugins.end(); if(r->get_name() == s) {
for(; rpit!=rpend; ++rpit) { return r;
if((*rpit)->get_name()==s) {
return *rpit;
} }
} }
return nullptr; return nullptr;
@ -480,16 +474,14 @@ namespace datalog {
std::string relation_manager::to_nice_string(const relation_signature & s) const { std::string relation_manager::to_nice_string(const relation_signature & s) const {
std::string res("["); std::string res("[");
bool first = true; bool first = true;
relation_signature::const_iterator it = s.begin(); for (auto const& sig : s) {
relation_signature::const_iterator end = s.end();
for(; it!=end; ++it) {
if (first) { if (first) {
first = false; first = false;
} }
else { else {
res += ','; res += ',';
} }
res+=to_nice_string(*it); res += to_nice_string(sig);
} }
res += ']'; res += ']';
@ -497,29 +489,22 @@ namespace datalog {
} }
void relation_manager::display(std::ostream & out) const { void relation_manager::display(std::ostream & out) const {
relation_map::iterator it=m_relations.begin(); for (auto const& kv : m_relations) {
relation_map::iterator end=m_relations.end(); out << "Table " << kv.m_key->get_name() << "\n";
for(;it!=end;++it) { kv.m_value->display(out);
out << "Table " << it->m_key->get_name() << "\n";
it->m_value->display(out);
} }
} }
void relation_manager::display_relation_sizes(std::ostream & out) const { void relation_manager::display_relation_sizes(std::ostream & out) const {
relation_map::iterator it=m_relations.begin(); for (auto const& kv : m_relations) {
relation_map::iterator end=m_relations.end(); out << "Relation " << kv.m_key->get_name() << " has size "
for(;it!=end;++it) { << kv.m_value->get_size_estimate_rows() << "\n";
out << "Relation " << it->m_key->get_name() << " has size "
<< it->m_value->get_size_estimate_rows() << "\n";
} }
} }
void relation_manager::display_output_tables(rule_set const& rules, std::ostream & out) const { void relation_manager::display_output_tables(rule_set const& rules, std::ostream & out) const {
const decl_set & output_preds = rules.get_output_predicates(); const decl_set & output_preds = rules.get_output_predicates();
decl_set::iterator it=output_preds.begin(); for (func_decl * pred : output_preds) {
decl_set::iterator end=output_preds.end();
for(; it!=end; ++it) {
func_decl * pred = *it;
relation_base * rel = try_get_relation(pred); relation_base * rel = try_get_relation(pred);
if (!rel) { if (!rel) {
out << "Tuples in " << pred->get_name() << ": \n"; out << "Tuples in " << pred->get_name() << ": \n";
@ -1016,11 +1001,8 @@ namespace datalog {
SASSERT(plugin.can_handle_signature(res_sign)); SASSERT(plugin.can_handle_signature(res_sign));
table_base * res = plugin.mk_empty(res_sign); table_base * res = plugin.mk_empty(res_sign);
table_base::iterator it = t.begin(); for (table_base::row_interface& a : t) {
table_base::iterator end = t.end(); a.get_fact(m_row);
for(; it!=end; ++it) {
it->get_fact(m_row);
modify_fact(m_row); modify_fact(m_row);
res->add_fact(m_row); res->add_fact(m_row);
} }
@ -1191,11 +1173,8 @@ namespace datalog {
table_fact m_row; table_fact m_row;
public: public:
void operator()(table_base & tgt, const table_base & src, table_base * delta) override { void operator()(table_base & tgt, const table_base & src, table_base * delta) override {
table_base::iterator it = src.begin(); for (table_base::row_interface& a : src) {
table_base::iterator iend = src.end(); a.get_fact(m_row);
for(; it!=iend; ++it) {
it->get_fact(m_row);
if (delta) { if (delta) {
if(!tgt.contains_fact(m_row)) { if(!tgt.contains_fact(m_row)) {
@ -1260,10 +1239,8 @@ namespace datalog {
void operator()(table_base & r) { void operator()(table_base & r) {
m_to_remove.reset(); m_to_remove.reset();
unsigned sz = 0; unsigned sz = 0;
table_base::iterator it = r.begin(); for (table_base::row_interface& a : r) {
table_base::iterator iend = r.end(); a.get_fact(m_row);
for(; it!=iend; ++it) {
it->get_fact(m_row);
if (should_remove(m_row)) { if (should_remove(m_row)) {
m_to_remove.append(m_row.size(), m_row.c_ptr()); m_to_remove.append(m_row.size(), m_row.c_ptr());
++sz; ++sz;
@ -1456,7 +1433,7 @@ namespace datalog {
m_removed_cols(removed_col_cnt, removed_cols) {} m_removed_cols(removed_col_cnt, removed_cols) {}
table_base* operator()(const table_base & tb) override { table_base* operator()(const table_base & tb) override {
table_base *t2 = tb.clone(); scoped_rel<table_base> t2 = tb.clone();
(*m_filter)(*t2); (*m_filter)(*t2);
if (!m_project) { if (!m_project) {
relation_manager & rmgr = t2->get_plugin().get_manager(); relation_manager & rmgr = t2->get_plugin().get_manager();
@ -1572,8 +1549,7 @@ namespace datalog {
TRACE("dl", tout << t1.get_plugin().get_name() << "\n";); TRACE("dl", tout << t1.get_plugin().get_name() << "\n";);
scoped_rel<table_base> aux = t1.clone(); scoped_rel<table_base> aux = t1.clone();
(*m_filter)(*aux); (*m_filter)(*aux);
table_base * res = (*m_project)(*aux); return (*m_project)(*aux);
return res;
} }
}; };
@ -1614,11 +1590,8 @@ namespace datalog {
m_aux_table->reset(); m_aux_table->reset();
} }
for (table_base::row_interface& a : t) {
table_base::iterator it = t.begin(); a.get_fact(m_curr_fact);
table_base::iterator iend = t.end();
for(; it!=iend; ++it) {
it->get_fact(m_curr_fact);
if((*m_mapper)(m_curr_fact.c_ptr()+m_first_functional)) { if((*m_mapper)(m_curr_fact.c_ptr()+m_first_functional)) {
m_aux_table->add_fact(m_curr_fact); m_aux_table->add_fact(m_curr_fact);
} }
@ -1699,10 +1672,7 @@ namespace datalog {
SASSERT(plugin.can_handle_signature(res_sign)); SASSERT(plugin.can_handle_signature(res_sign));
table_base * res = plugin.mk_empty(res_sign); table_base * res = plugin.mk_empty(res_sign);
table_base::iterator it = t.begin(); table_base::iterator it = t.begin(), end = t.end();
table_base::iterator end = t.end();
for (; it != end; ++it) { for (; it != end; ++it) {
mk_project(it); mk_project(it);
if (!res->suggest_fact(m_former_row)) { if (!res->suggest_fact(m_former_row)) {