From 140fb7942dd051f4e8db608ef2d9b260353e7416 Mon Sep 17 00:00:00 2001 From: Alex Horn Date: Wed, 10 Jun 2015 18:09:56 +0100 Subject: [PATCH 01/11] Add datalog infrastructure for min aggregation function This patch adds an instruction to the datalog interpreter and constructs a new AST node for min aggregation functions. The compiler is currently still work in progress and depends on changes made to the handling of simple joins and the preprocessor. Signed-off-by: Alex Horn --- src/ast/dl_decl_plugin.cpp | 68 +++++++++++++++- src/ast/dl_decl_plugin.h | 59 ++++++++++++++ src/muz/base/dl_rule.h | 7 ++ src/muz/base/dl_rule_set.h | 1 + src/muz/rel/dl_base.cpp | 122 ++++++++++++++++++++++++++++ src/muz/rel/dl_base.h | 28 +++++++ src/muz/rel/dl_instruction.cpp | 54 ++++++++++++ src/muz/rel/dl_instruction.h | 3 + src/muz/rel/dl_relation_manager.cpp | 5 ++ src/muz/rel/dl_relation_manager.h | 3 + src/test/dl_table.cpp | 71 +++++++++++++++- 11 files changed, 418 insertions(+), 3 deletions(-) diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index badf8a59d..305ac1779 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -44,7 +44,8 @@ namespace datalog { m_num_sym("N"), m_lt_sym("<"), m_le_sym("<="), - m_rule_sym("R") + m_rule_sym("R"), + m_min_sym("min") { } @@ -490,6 +491,66 @@ namespace datalog { return m_manager->mk_func_decl(m_clone_sym, 1, &s, s, info); } + /** + In SMT2 syntax, we can write \c ((_ min R N) v_0 v_1 ... v_k)) where 0 <= N <= k, + R is a relation of sort V_0 x V_1 x ... x V_k and each v_i is a zero-arity function + (also known as a "constant" in SMT2 parlance) whose range is of sort V_i. + + Example: + + (define-sort number_t () (_ BitVec 2)) + (declare-rel numbers (number_t number_t)) + (declare-rel is_min (number_t number_t)) + + (declare-var x number_t) + (declare-var y number_t) + + (rule (numbers #b00 #b11)) + (rule (numbers #b00 #b01)) + + (rule (=> (and (numbers x y) ((_ min numbers 1) x y)) (is_min x y))) + + This says that we want to find the mininum y grouped by x. + */ + func_decl * dl_decl_plugin::mk_min(decl_kind k, unsigned num_parameters, parameter const * parameters) { + if (num_parameters < 2) { + m_manager->raise_exception("invalid min aggregate definition due to missing parameters"); + return 0; + } + + parameter const & relation_parameter = parameters[0]; + if (!relation_parameter.is_ast() || !is_func_decl(relation_parameter.get_ast())) { + m_manager->raise_exception("invalid min aggregate definition, first parameter is not a function declaration"); + return 0; + } + + func_decl* f = to_func_decl(relation_parameter.get_ast()); + if (!m_manager->is_bool(f->get_range())) { + m_manager->raise_exception("invalid min aggregate definition, first paramater must be a predicate"); + return 0; + } + + parameter const & min_col_parameter = parameters[1]; + if (!min_col_parameter.is_int()) { + m_manager->raise_exception("invalid min aggregate definition, second parameter must be an integer"); + return 0; + } + + if (min_col_parameter.get_int() < 0) { + m_manager->raise_exception("invalid min aggregate definition, second parameter must be non-negative"); + return 0; + } + + if ((unsigned)min_col_parameter.get_int() >= f->get_arity()) { + m_manager->raise_exception("invalid min aggregate definition, second parameter exceeds the arity of the relation"); + return 0; + } + + func_decl_info info(m_family_id, k, num_parameters, parameters); + SASSERT(f->get_info() == 0); + return m_manager->mk_func_decl(m_min_sym, f->get_arity(), f->get_domain(), f->get_range(), info); + } + func_decl * dl_decl_plugin::mk_func_decl( decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { @@ -617,6 +678,9 @@ namespace datalog { break; } + case OP_DL_MIN: + return mk_min(k, num_parameters, parameters); + default: m_manager->raise_exception("operator not recognized"); return 0; @@ -627,7 +691,7 @@ namespace datalog { } void dl_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { - + op_names.push_back(builtin_name(m_min_sym.bare_str(), OP_DL_MIN)); } void dl_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h index 65b00235c..e3bc4dd63 100644 --- a/src/ast/dl_decl_plugin.h +++ b/src/ast/dl_decl_plugin.h @@ -50,6 +50,7 @@ namespace datalog { OP_DL_LT, OP_DL_REP, OP_DL_ABS, + OP_DL_MIN, LAST_RA_OP }; @@ -71,6 +72,7 @@ namespace datalog { symbol m_lt_sym; symbol m_le_sym; symbol m_rule_sym; + symbol m_min_sym; bool check_bounds(char const* msg, unsigned low, unsigned up, unsigned val) const; bool check_domain(unsigned low, unsigned up, unsigned val) const; @@ -94,12 +96,69 @@ namespace datalog { func_decl * mk_compare(decl_kind k, symbol const& sym, sort*const* domain); func_decl * mk_clone(sort* r); func_decl * mk_rule(unsigned arity); + func_decl * mk_min(decl_kind k, unsigned num_parameters, parameter const * parameters); sort * mk_finite_sort(unsigned num_params, parameter const* params); sort * mk_relation_sort(unsigned num_params, parameter const* params); sort * mk_rule_sort(); public: + /** + Is \c decl a min aggregation function? + */ + static bool is_aggregate(const func_decl* const decl) + { + return decl->get_decl_kind() == OP_DL_MIN; + } + + /** + \pre: is_aggregate(aggregate) + + \returns function declaration of predicate which is subject to min aggregation function + */ + static func_decl * min_func_decl(const func_decl* const aggregate) + { + SASSERT(is_aggregate(aggregate)); + parameter const & relation_parameter = aggregate->get_parameter(0); + return to_func_decl(relation_parameter.get_ast()); + } + + /** + \pre: is_aggregate(aggregate) + + \returns column identifier (starting at zero) which is minimized by aggregation function + */ + static unsigned min_col(const func_decl* const aggregate) + { + SASSERT(is_aggregate(aggregate)); + return (unsigned)aggregate->get_parameter(1).get_int(); + } + + /** + \pre: is_aggregate(aggregate) + + \returns column identifiers for the "group by" in the given min aggregation function + */ + static unsigned_vector group_by_cols(const func_decl* const aggregate) + { + SASSERT(is_aggregate(aggregate)); + unsigned _min_col = min_col(aggregate); + if (aggregate->get_arity() == 0U) + return unsigned_vector(); + + unsigned col_num = 0; + unsigned_vector cols(aggregate->get_arity() - 1U); + for (unsigned i = 0; i < cols.size(); ++i, ++col_num) + { + if (col_num == _min_col) + ++col_num; + + cols[i] = col_num; + } + + return cols; + } + dl_decl_plugin(); virtual ~dl_decl_plugin() {} diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index bdca80d0b..468b9f88c 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -346,6 +346,13 @@ namespace datalog { bool is_neg_tail(unsigned i) const { SASSERT(i < m_tail_size); return GET_TAG(m_tail[i]) == 1; } + /** + A predicate P(Xj) can be annotated by adding an interpreted predicate of the form ((_ min P N) ...) + where N is the column number that should be used for the min aggregation function. + Such an interpreted predicate is an example for which this function returns true. + */ + bool is_min_tail(unsigned i) const { return dl_decl_plugin::is_aggregate(get_tail(i)->get_decl()); } + /** Check whether predicate p is in the interpreted tail. diff --git a/src/muz/base/dl_rule_set.h b/src/muz/base/dl_rule_set.h index e13d92105..5201d9257 100644 --- a/src/muz/base/dl_rule_set.h +++ b/src/muz/base/dl_rule_set.h @@ -179,6 +179,7 @@ namespace datalog { void compute_deps(); void compute_tc_deps(); bool stratified_negation(); + public: rule_set(context & ctx); rule_set(const rule_set & rs); diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp index 95efccce8..a00c50d9e 100644 --- a/src/muz/rel/dl_base.cpp +++ b/src/muz/rel/dl_base.cpp @@ -485,4 +485,126 @@ 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(); + 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); + + 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()); + } + + table_transformer_fn * project_fn = manager.mk_project_fn(*join_table, cols); + table_base * 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(); + table_intersection_filter_fn * diff_fn = manager.mk_filter_by_negation_fn(*result, *gt_table, cols, cols); + (*diff_fn)(*result, *gt_table); + gt_table->deallocate(); + 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 268cc602e..6ab1b2a96 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -192,6 +192,29 @@ 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; @@ -856,6 +879,7 @@ 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; @@ -1020,6 +1044,7 @@ 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: @@ -1027,6 +1052,9 @@ 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_instruction.cpp b/src/muz/rel/dl_instruction.cpp index 7eb8d4375..c903519ce 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -25,6 +25,7 @@ Revision History: #include"rel_context.h" #include"debug.h" #include"warning.h" +#include"dl_table_relation.h" namespace datalog { @@ -883,6 +884,59 @@ 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("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(); + 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); + + 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; diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h index 3910f6d0b..a02346b99 100644 --- a/src/muz/rel/dl_instruction.h +++ b/src/muz/rel/dl_instruction.h @@ -93,6 +93,7 @@ namespace datalog { unsigned m_filter_interp_project; unsigned m_filter_id; unsigned m_filter_eq; + unsigned m_min; stats() { reset(); } void reset() { memset(this, 0, sizeof(*this)); } }; @@ -284,6 +285,8 @@ namespace datalog { static instruction * mk_join_project(reg_idx rel1, reg_idx rel2, unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, const unsigned * removed_cols, reg_idx result); + static instruction * mk_min(reg_idx source, reg_idx target, const unsigned_vector & group_by_cols, + const unsigned min_col); static instruction * mk_rename(reg_idx src, unsigned cycle_len, const unsigned * permutation_cycle, reg_idx tgt); static instruction * mk_filter_by_negation(reg_idx tgt, reg_idx neg_rel, unsigned col_cnt, diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 6a9bb7f2a..95b35899e 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -1021,6 +1021,11 @@ 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; diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h index 53d7f21e2..f91b7496a 100644 --- a/src/muz/rel/dl_relation_manager.h +++ b/src/muz/rel/dl_relation_manager.h @@ -251,6 +251,9 @@ 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/test/dl_table.cpp b/src/test/dl_table.cpp index d24200f9b..06eb62fa1 100644 --- a/src/test/dl_table.cpp +++ b/src/test/dl_table.cpp @@ -1,4 +1,4 @@ -#ifdef _WINDOWS +#if defined(_WINDOWS) || defined(_CYGWIN) #include "dl_context.h" #include "dl_table.h" #include "dl_register_engine.h" @@ -91,9 +91,78 @@ 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() { From e6ffa5d2a5155666c02eca038148f992b12903bd Mon Sep 17 00:00:00 2001 From: Alex Horn Date: Wed, 10 Jun 2015 19:59:57 +0100 Subject: [PATCH 02/11] Enable datalog plugin for AST extensions Signed-off-by: Alex Horn --- src/cmd_context/cmd_context.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 50afc1735..c8d5e8cab 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -621,6 +621,7 @@ void cmd_context::init_manager_core(bool new_manager) { register_plugin(symbol("seq"), alloc(seq_decl_plugin), logic_has_seq()); register_plugin(symbol("pb"), alloc(pb_decl_plugin), !has_logic()); register_plugin(symbol("fpa"), alloc(fpa_decl_plugin), logic_has_fpa()); + register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic()); } else { // the manager was created by an external module From 9b7c5658c8f9b7e42607d3e56cb339821b1f12eb Mon Sep 17 00:00:00 2001 From: Alex Horn Date: Wed, 10 Jun 2015 20:06:09 +0100 Subject: [PATCH 03/11] Ignore min aggregation functions in compiler for now Signed-off-by: Alex Horn --- src/muz/rel/dl_compiler.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 59ba260a4..76b7f7c36 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -597,7 +597,8 @@ namespace datalog { unsigned ft_len = r->get_tail_size(); // full tail ptr_vector tail; for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { - tail.push_back(r->get_tail(tail_index)); + if (!r->is_min_tail(tail_index)) + tail.push_back(r->get_tail(tail_index)); } expr_ref_vector binding(m); From 132f984d5142bdc676da614796bd59da2a06caa1 Mon Sep 17 00:00:00 2001 From: Alex Horn Date: Wed, 10 Jun 2015 20:19:14 +0100 Subject: [PATCH 04/11] Add syntactical min checker The purpose of this patch is to find out more about the "shape" of the constraints in our benchmarks. In particular, we would like to determine whether aggregation and negation, together, appear in recursive rules. Signed-off-by: Alex Horn --- src/muz/base/dl_rule_set.cpp | 45 +++++++++++++++++++++++++++++++++++- src/muz/base/dl_rule_set.h | 2 +- 2 files changed, 45 insertions(+), 2 deletions(-) diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp index ad3b512a3..555b592ef 100644 --- a/src/muz/base/dl_rule_set.cpp +++ b/src/muz/base/dl_rule_set.cpp @@ -400,7 +400,7 @@ namespace datalog { SASSERT(!is_closed()); //the rule_set is not already closed m_deps.populate(*this); m_stratifier = alloc(rule_stratifier, m_deps); - if (!stratified_negation()) { + if (!stratified_negation() || !check_min()) { m_stratifier = 0; m_deps.reset(); return false; @@ -441,6 +441,49 @@ namespace datalog { return true; } + bool rule_set::check_min() { + // For now, we check the following: + // + // if a min aggregation function occurs in an SCC, is this SCC + // free of any other non-monotonic functions, e.g. negation? + const unsigned NEG_BIT = 1U << 0; + const unsigned MIN_BIT = 1U << 1; + + ptr_vector::const_iterator it = m_rules.c_ptr(); + ptr_vector::const_iterator end = m_rules.c_ptr() + m_rules.size(); + unsigned_vector component_status(m_stratifier->get_strats().size()); + + for (; it != end; it++) { + rule * r = *it; + app * head = r->get_head(); + func_decl * head_decl = head->get_decl(); + unsigned head_strat = get_predicate_strat(head_decl); + unsigned n = r->get_tail_size(); + for (unsigned i = 0; i < n; i++) { + func_decl * tail_decl = r->get_tail(i)->get_decl(); + unsigned strat = get_predicate_strat(tail_decl); + + if (r->is_neg_tail(i)) { + SASSERT(strat < component_status.size()); + component_status[strat] |= NEG_BIT; + } + + if (r->is_min_tail(i)) { + SASSERT(strat < component_status.size()); + component_status[strat] |= MIN_BIT; + } + } + } + + const unsigned CONFLICT = NEG_BIT | MIN_BIT; + for (unsigned k = 0; k < component_status.size(); ++k) { + if (component_status[k] == CONFLICT) + return false; + } + + return true; + } + void rule_set::replace_rules(const rule_set & src) { if (this != &src) { reset(); diff --git a/src/muz/base/dl_rule_set.h b/src/muz/base/dl_rule_set.h index 5201d9257..a7d09b099 100644 --- a/src/muz/base/dl_rule_set.h +++ b/src/muz/base/dl_rule_set.h @@ -179,7 +179,7 @@ namespace datalog { void compute_deps(); void compute_tc_deps(); bool stratified_negation(); - + bool check_min(); public: rule_set(context & ctx); rule_set(const rule_set & rs); From 565c0f785f6672e15d1675cf5973446d0d9b6c34 Mon Sep 17 00:00:00 2001 From: Alex Horn Date: Thu, 11 Jun 2015 08:59:57 +0100 Subject: [PATCH 05/11] Fix memory leaks Signed-off-by: Alex Horn --- src/muz/rel/dl_base.cpp | 4 ++++ src/muz/rel/dl_instruction.cpp | 1 + src/muz/rel/dl_relation_manager.cpp | 4 +++- src/muz/rel/dl_table_relation.cpp | 3 +++ 4 files changed, 11 insertions(+), 1 deletion(-) 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); From c8a123b7dd21284fb71f516fd39abae8f3fdaf26 Mon Sep 17 00:00:00 2001 From: Alex Horn Date: Thu, 11 Jun 2015 16:16:47 +0100 Subject: [PATCH 06/11] Disable a few rule transformations For this prototype, we need to disable three rule transformations, namely coi_filter, similarity_compressor, rule_inliner. But disabling the inliner causes problems with the tracer in the datalog interpreter. Since a new proprocessor is underway, we skip the problematic trace outputs for now. Signed-off-by: Alex Horn --- src/muz/rel/dl_instruction.cpp | 4 ++-- src/muz/rel/rel_context.cpp | 6 ++++++ 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index 77ba387bb..f93f88a76 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -553,7 +553,7 @@ namespace datalog { if (r.fast_empty()) { ctx.make_empty(m_reg); } - TRACE("dl_verbose", r.display(tout <<"post-filter-interpreted:\n");); + //TRACE("dl_verbose", r.display(tout <<"post-filter-interpreted:\n");); return true; } @@ -610,7 +610,7 @@ namespace datalog { if (ctx.reg(m_res)->fast_empty()) { ctx.make_empty(m_res); } - TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n");); + //TRACE("dl_verbose", reg.display(tout << "post-filter-interpreted-and-project:\n");); return true; } diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index c3ffdceae..44f59486e 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -292,17 +292,23 @@ namespace datalog { 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)); From 8c097044e87e4db52bd808cf8a8e20b3d5b1a0c3 Mon Sep 17 00:00:00 2001 From: Alex Horn Date: Thu, 11 Jun 2015 16:23:26 +0100 Subject: [PATCH 07/11] Add basic compiler support for min aggregation function Signed-off-by: Alex Horn --- src/muz/rel/dl_compiler.cpp | 48 +++++++++++++++++++++++++++++++++++++ src/muz/rel/dl_compiler.h | 18 ++++++++++++++ 2 files changed, 66 insertions(+) diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 76b7f7c36..c35985e98 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -73,6 +73,12 @@ namespace datalog { vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result)); } + void compiler::make_min(reg_idx source, reg_idx & target, const unsigned_vector & group_by_cols, + const unsigned min_col, instruction_block & acc) { + target = get_register(m_reg_signatures[source], true, source); + acc.push_back(instruction::mk_min(source, target, group_by_cols, min_col)); + } + void compiler::make_filter_interpreted_and_project(reg_idx src, app_ref & cond, const unsigned_vector & removed_cols, reg_idx & result, bool reuse, instruction_block & acc) { SASSERT(!removed_cols.empty()); @@ -440,6 +446,30 @@ namespace datalog { get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res); } + void compiler::find_min_aggregates(const rule * r, ptr_vector& min_aggregates) { + unsigned ut_len = r->get_uninterpreted_tail_size(); + unsigned ft_len = r->get_tail_size(); // full tail + func_decl * aggregate; + for (unsigned tail_index = ut_len; tail_index < ft_len; ++tail_index) { + aggregate = r->get_tail(tail_index)->get_decl(); + if (dl_decl_plugin::is_aggregate(aggregate)) { + min_aggregates.push_back(aggregate); + } + } + } + + bool compiler::prepare_min_aggregate(const func_decl * decl, const ptr_vector& min_aggregates, + unsigned_vector & group_by_cols, unsigned & min_col) { + for (unsigned i = 0; i < min_aggregates.size(); ++i) { + if (dl_decl_plugin::min_func_decl(min_aggregates[i]) == decl) { + group_by_cols = dl_decl_plugin::group_by_cols(min_aggregates[i]); + min_col = dl_decl_plugin::min_col(min_aggregates[i]); + return true; + } + } + return false; + } + void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs, reg_idx delta_reg, bool use_widening, instruction_block & acc) { @@ -465,6 +495,12 @@ namespace datalog { // whether to dealloc the previous result bool dealloc = true; + // setup information for min aggregation + ptr_vector min_aggregates; + find_min_aggregates(r, min_aggregates); + unsigned_vector group_by_cols; + unsigned min_col; + if(pt_len == 2) { reg_idx t1_reg=tail_regs[0]; reg_idx t2_reg=tail_regs[1]; @@ -473,6 +509,14 @@ namespace datalog { SASSERT(m_reg_signatures[t1_reg].size()==a1->get_num_args()); SASSERT(m_reg_signatures[t2_reg].size()==a2->get_num_args()); + if (prepare_min_aggregate(a1->get_decl(), min_aggregates, group_by_cols, min_col)) { + make_min(t1_reg, single_res, group_by_cols, min_col, acc); + } + + if (prepare_min_aggregate(a2->get_decl(), min_aggregates, group_by_cols, min_col)) { + make_min(t2_reg, single_res, group_by_cols, min_col, acc); + } + variable_intersection a1a2(m_context.get_manager()); a1a2.populate(a1,a2); @@ -514,6 +558,10 @@ namespace datalog { single_res = tail_regs[0]; dealloc = false; + if (prepare_min_aggregate(a->get_decl(), min_aggregates, group_by_cols, min_col)) { + make_min(single_res, single_res, group_by_cols, min_col, acc); + } + SASSERT(m_reg_signatures[single_res].size() == a->get_num_args()); unsigned n=a->get_num_args(); diff --git a/src/muz/rel/dl_compiler.h b/src/muz/rel/dl_compiler.h index 4902b9387..a9e37a8a3 100644 --- a/src/muz/rel/dl_compiler.h +++ b/src/muz/rel/dl_compiler.h @@ -120,6 +120,22 @@ namespace datalog { instruction_observer m_instruction_observer; expr_free_vars m_free_vars; + /** + \brief Finds all the min aggregation functions in the premise of a given rule. + */ + static void find_min_aggregates(const rule * r, ptr_vector& min_aggregates); + + /** + \brief Decides whether a predicate is subject to a min aggregation function. + + If \c decl is subject to a min aggregation function, the output parameters are written + with the neccessary information. + + \returns true if the output paramaters have been written + */ + static bool prepare_min_aggregate(const func_decl * decl, const ptr_vector& min_aggregates, + unsigned_vector & group_by_cols, unsigned & min_col); + /** If true, the union operation on the underlying structure only provides the information whether the updated relation has changed or not. In this case we do not get anything @@ -146,6 +162,8 @@ namespace datalog { void make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result, bool reuse_t1, instruction_block & acc); + void make_min(reg_idx source, reg_idx & target, const unsigned_vector & group_by_cols, + const unsigned min_col, instruction_block & acc); void make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, const unsigned_vector & removed_cols, reg_idx & result, bool reuse_t1, instruction_block & acc); void make_filter_interpreted_and_project(reg_idx src, app_ref & cond, From 868b430b8bf0150ff7d7597f649e6bfa3899d3d1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2015 10:19:29 -0700 Subject: [PATCH 08/11] use scoped pointers instead of explicit deallocation (robust under exceptions) Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_base.cpp | 15 +++++---------- src/muz/rel/dl_instruction.cpp | 3 +-- 2 files changed, 6 insertions(+), 12 deletions(-) diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp index 6eba021f1..6dc7f2f6e 100644 --- a/src/muz/rel/dl_base.cpp +++ b/src/muz/rel/dl_base.cpp @@ -516,9 +516,8 @@ namespace datalog { */ virtual table_base * reference_implementation(const table_base & t) { 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); + 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(); @@ -544,10 +543,8 @@ namespace datalog { SASSERT(cols[k] < join_table->num_columns()); } - 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(); + 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; @@ -556,10 +553,8 @@ namespace datalog { } table_base * result = t.clone(); - table_intersection_filter_fn * diff_fn = manager.mk_filter_by_negation_fn(*result, *gt_table, cols, cols); + scoped_ptr 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 f93f88a76..f8145b922 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -914,9 +914,8 @@ namespace datalog { relation_manager & r_manager = s.get_manager(); 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); + scoped_ptr 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 << "% "; From ca31c979fe2fb13ac5bf25dbd072b729d35de5cb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Jun 2015 12:00:21 -0700 Subject: [PATCH 09/11] re-enable transformations Signed-off-by: Nikolaj Bjorner --- src/muz/rel/rel_context.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 44f59486e..d2a2f0181 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -290,6 +290,8 @@ namespace datalog { return res; } +#define _MIN_DONE_ 1 + void rel_context::transform_rules() { rule_transformer transf(m_context); #ifdef _MIN_DONE_ From f84d6bf5bb2c031478dfa72c10bcbb957995dc7f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 12 Jun 2015 12:58:07 +0100 Subject: [PATCH 10/11] Bugfix for QF_FP tactic --- src/tactic/fpa/qffp_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index fbce1668e..485e837ee 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -53,7 +53,7 @@ struct has_fp_to_real_predicate { class has_fp_to_real_probe : public probe { public: virtual result operator()(goal const & g) { - return !test(g); + return test(g); } virtual ~has_fp_to_real_probe() {} From 6980fb3035c08905d1de7cada591843cd4dd5448 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 12 Jun 2015 12:58:19 +0100 Subject: [PATCH 11/11] Bugfix for distinct of floats. --- src/ast/fpa/fpa2bv_converter.cpp | 14 ++++++++++++++ src/ast/fpa/fpa2bv_converter.h | 1 + src/ast/fpa/fpa2bv_rewriter.h | 11 +++++++++-- 3 files changed, 24 insertions(+), 2 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 4c199ebc6..baba7b701 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -93,6 +93,20 @@ void fpa2bv_converter::mk_ite(expr * c, expr * t, expr * f, expr_ref & result) { mk_fp(sgn, e, s, result); } +void fpa2bv_converter::mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + // Note: in SMT there is only one NaN, so multiple of them are considered + // equal, thus (distinct NaN NaN) is false, even if the two NaNs have + // different bitwise representations (see also mk_eq). + result = m.mk_true(); + for (unsigned i = 0; i < num; i++) { + for (unsigned j = i+1; j < num; j++) { + expr_ref eq(m); + mk_eq(args[i], args[j], eq); + m_simp.mk_and(result, m.mk_not(eq), result); + } + } +} + void fpa2bv_converter::mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 0); SASSERT(f->get_num_parameters() == 1); diff --git a/src/ast/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h index 4b3c1a6ca..b0881a364 100644 --- a/src/ast/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -80,6 +80,7 @@ public: void mk_eq(expr * a, expr * b, expr_ref & result); void mk_ite(expr * c, expr * t, expr * f, expr_ref & result); + void mk_distinct(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_rounding_mode(func_decl * f, expr_ref & result); void mk_numeral(func_decl * f, unsigned num, expr * const * args, expr_ref & result); diff --git a/src/ast/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h index ed885a4cc..fa88c227c 100644 --- a/src/ast/fpa/fpa2bv_rewriter.h +++ b/src/ast/fpa/fpa2bv_rewriter.h @@ -103,8 +103,7 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { } return BR_FAILED; } - - if (m().is_ite(f)) { + else if (m().is_ite(f)) { SASSERT(num == 3); if (m_conv.is_float(args[1])) { m_conv.mk_ite(args[0], args[1], args[2], result); @@ -112,6 +111,14 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { } return BR_FAILED; } + else if (m().is_distinct(f)) { + sort * ds = f->get_domain()[0]; + if (m_conv.is_float(ds) || m_conv.is_rm(ds)) { + m_conv.mk_distinct(f, num, args, result); + return BR_DONE; + } + return BR_FAILED; + } if (m_conv.is_float_family(f)) { switch (f->get_decl_kind()) {