diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp index a00c50d9e..6eba021f1 100644 --- a/src/muz/rel/dl_base.cpp +++ b/src/muz/rel/dl_base.cpp @@ -518,6 +518,7 @@ namespace datalog { relation_manager & manager = t.get_manager(); table_join_fn * join_fn = manager.mk_join_fn(t, t, m_group_by_cols, m_group_by_cols); table_base * join_table = (*join_fn)(t, t); + dealloc(join_fn); table_base::iterator join_table_it = join_table->begin(); table_base::iterator join_table_end = join_table->end(); @@ -545,6 +546,8 @@ namespace datalog { table_transformer_fn * project_fn = manager.mk_project_fn(*join_table, cols); table_base * gt_table = (*project_fn)(*join_table); + dealloc(project_fn); + join_table->deallocate(); for (unsigned k = 0; k < cols.size(); ++k) { cols[k] = k; @@ -555,6 +558,7 @@ namespace datalog { table_base * result = t.clone(); table_intersection_filter_fn * diff_fn = manager.mk_filter_by_negation_fn(*result, *gt_table, cols, cols); (*diff_fn)(*result, *gt_table); + dealloc(diff_fn); gt_table->deallocate(); return result; } diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index c903519ce..77ba387bb 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -916,6 +916,7 @@ namespace datalog { const relation_signature & r_sig = s.get_signature(); table_min_fn * fn = r_manager.mk_min_fn(source_t, m_group_by_cols, m_min_col); table_base * target_t = (*fn)(source_t); + dealloc(fn); TRACE("dl", tout << "% "; diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 95b35899e..2b78baf05 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -354,7 +354,9 @@ namespace datalog { return product_relation_plugin::get_plugin(*this).mk_empty(s); } - + /** + The newly created object takes ownership of the \c table object. + */ relation_base * relation_manager::mk_table_relation(const relation_signature & s, table_base * table) { SASSERT(s.size()==table->get_signature().size()); return get_table_relation_plugin(table->get_plugin()).mk_from_table(s, table); diff --git a/src/muz/rel/dl_table_relation.cpp b/src/muz/rel/dl_table_relation.cpp index 364c29367..d42d071aa 100644 --- a/src/muz/rel/dl_table_relation.cpp +++ b/src/muz/rel/dl_table_relation.cpp @@ -63,6 +63,9 @@ namespace datalog { return alloc(table_relation, *this, s, t); } + /** + The newly created object takes ownership of the \c t object. + */ relation_base * table_relation_plugin::mk_from_table(const relation_signature & s, table_base * t) { if (&t->get_plugin() == &m_table_plugin) return alloc(table_relation, *this, s, t);