From d9cd01f3f7973ca167e4263bba383c566b4db062 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 9 Dec 2015 09:28:17 +0000 Subject: [PATCH] remove a few leftovers from min aggregation cleanup Signed-off-by: Nuno Lopes --- src/muz/rel/dl_base.cpp | 122 ---------------------------- src/muz/rel/dl_base.h | 28 ------- src/muz/rel/dl_compiler.cpp | 3 - src/muz/rel/dl_instruction.cpp | 55 ------------- src/muz/rel/dl_relation_manager.cpp | 6 -- src/muz/rel/dl_relation_manager.h | 3 - src/muz/rel/rel_context.cpp | 8 -- src/test/dl_table.cpp | 70 ---------------- 8 files changed, 295 deletions(-) diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp index 6dc7f2f6e..b7f4d6cef 100644 --- a/src/muz/rel/dl_base.cpp +++ b/src/muz/rel/dl_base.cpp @@ -484,126 +484,4 @@ namespace datalog { } brw.mk_or(disjs.size(), disjs.c_ptr(), fml); } - - class table_plugin::min_fn : public table_min_fn{ - table_signature m_sig; - const unsigned_vector m_group_by_cols; - const unsigned m_col; - public: - min_fn(const table_signature & t_sig, const unsigned_vector& group_by_cols, const unsigned col) - : m_sig(t_sig), - m_group_by_cols(group_by_cols), - m_col(col) {} - - virtual table_base* operator()(table_base const& t) { - //return reference_implementation(t); - return reference_implementation_with_hash(t); - } - - private: - - /** - Reference implementation with negation: - - T1 = join(T, T) by group_cols - T2 = { (t1,t2) in T1 | t1[col] > t2[col] } - T3 = { t1 | (t1,t2) in T2 } - T4 = T \ T3 - - The point of this reference implementation is to show - that the minimum requires negation (set difference). - This is relevant for fixed point computations. - */ - virtual table_base * reference_implementation(const table_base & t) { - relation_manager & manager = t.get_manager(); - scoped_ptr join_fn = manager.mk_join_fn(t, t, m_group_by_cols, m_group_by_cols); - scoped_rel join_table = (*join_fn)(t, t); - - table_base::iterator join_table_it = join_table->begin(); - table_base::iterator join_table_end = join_table->end(); - table_fact row; - - table_element i, j; - - for (; join_table_it != join_table_end; ++join_table_it) { - join_table_it->get_fact(row); - i = row[m_col]; - j = row[t.num_columns() + m_col]; - - if (i > j) { - continue; - } - - join_table->remove_fact(row); - } - - unsigned_vector cols(t.num_columns()); - for (unsigned k = 0; k < cols.size(); ++k) { - cols[k] = cols.size() + k; - SASSERT(cols[k] < join_table->num_columns()); - } - - scoped_ptr project_fn = manager.mk_project_fn(*join_table, cols); - scoped_rel gt_table = (*project_fn)(*join_table); - - for (unsigned k = 0; k < cols.size(); ++k) { - cols[k] = k; - SASSERT(cols[k] < t.num_columns()); - SASSERT(cols[k] < gt_table->num_columns()); - } - - table_base * result = t.clone(); - scoped_ptr diff_fn = manager.mk_filter_by_negation_fn(*result, *gt_table, cols, cols); - (*diff_fn)(*result, *gt_table); - return result; - } - - typedef map < table_fact, table_element, svector_hash_proc, - vector_eq_proc > group_map; - - // Thanks to Nikolaj who kindly helped with the second reference implementation! - virtual table_base * reference_implementation_with_hash(const table_base & t) { - group_map group; - table_base::iterator it = t.begin(); - table_base::iterator end = t.end(); - table_fact row, row2; - table_element current_value, min_value; - for (; it != end; ++it) { - it->get_fact(row); - current_value = row[m_col]; - group_by(row, row2); - group_map::entry* entry = group.find_core(row2); - if (!entry) { - group.insert(row2, current_value); - } - else if (entry->get_data().m_value > current_value) { - entry->get_data().m_value = current_value; - } - } - table_base* result = t.get_plugin().mk_empty(m_sig); - table_base::iterator it2 = t.begin(); - for (; it2 != end; ++it2) { - it2->get_fact(row); - current_value = row[m_col]; - group_by(row, row2); - VERIFY(group.find(row2, min_value)); - if (min_value == current_value) { - result->add_fact(row); - } - } - return result; - } - - void group_by(table_fact const& in, table_fact& out) { - out.reset(); - for (unsigned i = 0; i < m_group_by_cols.size(); ++i) { - out.push_back(in[m_group_by_cols[i]]); - } - } - }; - - table_min_fn * table_plugin::mk_min_fn(const table_base & t, - unsigned_vector & group_by_cols, const unsigned col) { - return alloc(table_plugin::min_fn, t.get_signature(), group_by_cols, col); - } } diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index c26623737..7b6210850 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -192,29 +192,6 @@ namespace datalog { virtual base_object * operator()(const base_object & t1, const base_object & t2) = 0; }; - /** - \brief Aggregate minimum value - - Informally, we want to group rows in a table \c t by \c group_by_cols and - return the minimum value in column \c col among each group. - - Let \c t be a table with N columns. - Let \c group_by_cols be a set of column identifers for table \c t such that |group_by_cols| < N. - Let \c col be a column identifier for table \c t such that \c col is not in \c group_by_cols. - - Let R_col be a set of rows in table \c t such that, for all rows r_i, r_j in R_col - and column identifiers k in \c group_by_cols, r_i[k] = r_j[k]. - - For each R_col, we want to restrict R_col to those rows whose value in column \c col is minimal. - - min_fn(R, group_by_cols, col) = - { row in R | forall row' in R . row'[group_by_cols] = row[group_by_cols] => row'[col] >= row[col] } - */ - class min_fn : public base_fn { - public: - virtual base_object * operator()(const base_object & t) = 0; - }; - class transformer_fn : public base_fn { public: virtual base_object * operator()(const base_object & t) = 0; @@ -879,7 +856,6 @@ namespace datalog { typedef table_infrastructure::base_fn base_table_fn; typedef table_infrastructure::join_fn table_join_fn; - typedef table_infrastructure::min_fn table_min_fn; typedef table_infrastructure::transformer_fn table_transformer_fn; typedef table_infrastructure::union_fn table_union_fn; typedef table_infrastructure::mutator_fn table_mutator_fn; @@ -1044,7 +1020,6 @@ namespace datalog { class table_plugin : public table_infrastructure::plugin_object { friend class relation_manager; - class min_fn; protected: table_plugin(symbol const& n, relation_manager & manager) : plugin_object(n, manager) {} public: @@ -1052,9 +1027,6 @@ namespace datalog { virtual bool can_handle_signature(const table_signature & s) { return s.functional_columns()==0; } protected: - virtual table_min_fn * mk_min_fn(const table_base & t, - unsigned_vector & group_by_cols, const unsigned col); - /** If the returned value is non-zero, the returned object must take ownership of \c mapper. Otherwise \c mapper must remain unmodified. diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 7b26f19c7..67227e7d9 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -467,9 +467,6 @@ namespace datalog { // whether to dealloc the previous result bool dealloc = true; - // setup information for min aggregation - unsigned_vector group_by_cols; - if(pt_len == 2) { reg_idx t1_reg=tail_regs[0]; reg_idx t2_reg=tail_regs[1]; diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index fb7bb9281..2c1850bf4 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -25,7 +25,6 @@ Revision History: #include"rel_context.h" #include"debug.h" #include"warning.h" -#include"dl_table_relation.h" namespace datalog { @@ -886,60 +885,6 @@ namespace datalog { removed_cols, result); } - class instr_min : public instruction { - reg_idx m_source_reg; - reg_idx m_target_reg; - unsigned_vector m_group_by_cols; - unsigned m_min_col; - public: - instr_min(reg_idx source_reg, reg_idx target_reg, const unsigned_vector & group_by_cols, unsigned min_col) - : m_source_reg(source_reg), - m_target_reg(target_reg), - m_group_by_cols(group_by_cols), - m_min_col(min_col) { - } - virtual bool perform(execution_context & ctx) { - log_verbose(ctx); - if (!ctx.reg(m_source_reg)) { - ctx.make_empty(m_target_reg); - return true; - } - - const relation_base & s = *ctx.reg(m_source_reg); - if (!s.from_table()) { - throw default_exception(default_exception::fmt(), "relation is not a table %s", - s.get_plugin().get_name().bare_str()); - } - ++ctx.m_stats.m_min; - const table_relation & tr = static_cast(s); - const table_base & source_t = tr.get_table(); - relation_manager & r_manager = s.get_manager(); - - const relation_signature & r_sig = s.get_signature(); - scoped_ptr fn = r_manager.mk_min_fn(source_t, m_group_by_cols, m_min_col); - table_base * target_t = (*fn)(source_t); - - TRACE("dl", - tout << "% "; - target_t->display(tout); - tout << "\n";); - - relation_base * target_r = r_manager.mk_table_relation(r_sig, target_t); - ctx.set_reg(m_target_reg, target_r); - return true; - } - virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { - out << " MIN AGGR "; - } - virtual void make_annotations(execution_context & ctx) { - } - }; - - instruction * instruction::mk_min(reg_idx source, reg_idx target, const unsigned_vector & group_by_cols, - const unsigned min_col) { - return alloc(instr_min, source, target, group_by_cols, min_col); - } - class instr_select_equal_and_project : public instruction { reg_idx m_src; reg_idx m_result; diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 2b78baf05..ddcdf7ae2 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -1023,12 +1023,6 @@ namespace datalog { return res; } - table_min_fn * relation_manager::mk_min_fn(const table_base & t, - unsigned_vector & group_by_cols, const unsigned col) - { - return t.get_plugin().mk_min_fn(t, group_by_cols, col); - } - class relation_manager::auxiliary_table_transformer_fn { table_fact m_row; public: diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h index cda6373d3..6e1b5737e 100644 --- a/src/muz/rel/dl_relation_manager.h +++ b/src/muz/rel/dl_relation_manager.h @@ -251,9 +251,6 @@ namespace datalog { return mk_join_fn(t1, t2, cols1.size(), cols1.c_ptr(), cols2.c_ptr(), allow_product_relation); } - table_min_fn * mk_min_fn(const table_base & t, - unsigned_vector & group_by_cols, const unsigned col); - /** \brief Return functor that transforms a table into one that lacks columns listed in \c removed_cols array. diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index c6b47f1ed..52dd10202 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -291,27 +291,19 @@ namespace datalog { return res; } -#define _MIN_DONE_ 1 - void rel_context::transform_rules() { rule_transformer transf(m_context); -#ifdef _MIN_DONE_ transf.register_plugin(alloc(mk_coi_filter, m_context)); -#endif transf.register_plugin(alloc(mk_filter_rules, m_context)); transf.register_plugin(alloc(mk_simple_joins, m_context)); if (m_context.unbound_compressor()) { transf.register_plugin(alloc(mk_unbound_compressor, m_context)); } -#ifdef _MIN_DONE_ if (m_context.similarity_compressor()) { transf.register_plugin(alloc(mk_similarity_compressor, m_context)); } -#endif transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context)); -#ifdef _MIN_DONE_ transf.register_plugin(alloc(mk_rule_inliner, m_context)); -#endif transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context)); transf.register_plugin(alloc(mk_separate_negated_tails, m_context)); diff --git a/src/test/dl_table.cpp b/src/test/dl_table.cpp index b14988f11..62eec34bc 100644 --- a/src/test/dl_table.cpp +++ b/src/test/dl_table.cpp @@ -95,78 +95,8 @@ void test_dl_bitvector_table() { test_table(mk_bv_table); } -void test_table_min() { - std::cout << "----- test_table_min -----\n"; - datalog::table_signature sig; - sig.push_back(2); - sig.push_back(4); - sig.push_back(8); - smt_params params; - ast_manager ast_m; - datalog::register_engine re; - datalog::context ctx(ast_m, re, params); - datalog::relation_manager & m = ctx.get_rel_context()->get_rmanager(); - - m.register_plugin(alloc(datalog::bitvector_table_plugin, m)); - - datalog::table_base* tbl = mk_bv_table(m, sig); - datalog::table_base& table = *tbl; - - datalog::table_fact row, row1, row2, row3; - row.push_back(1); - row.push_back(2); - row.push_back(5); - - // Group (1,2,*) - row1 = row; - row[2] = 6; - row2 = row; - row[2] = 5; - row3 = row; - - table.add_fact(row1); - table.add_fact(row2); - table.add_fact(row3); - - // Group (1,3,*) - row[1] = 3; - row1 = row; - row[2] = 7; - row2 = row; - row[2] = 4; - row3 = row; - - table.add_fact(row1); - table.add_fact(row2); - table.add_fact(row3); - - table.display(std::cout); - - unsigned_vector group_by(2); - group_by[0] = 0; - group_by[1] = 1; - - datalog::table_min_fn * min_fn = m.mk_min_fn(table, group_by, 2); - datalog::table_base * min_tbl = (*min_fn)(table); - - min_tbl->display(std::cout); - - row[1] = 2; - row[2] = 5; - SASSERT(min_tbl->contains_fact(row)); - - row[1] = 3; - row[2] = 4; - SASSERT(min_tbl->contains_fact(row)); - - dealloc(min_fn); - min_tbl->deallocate(); - tbl->deallocate(); -} - void tst_dl_table() { test_dl_bitvector_table(); - test_table_min(); } #else void tst_dl_table() {