From ae3d16bc50aebf8c1643549f444f486ee6f5f285 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Dec 2014 16:18:09 -0800 Subject: [PATCH 1/7] fix overflow and integrality bugs reported by Phan Signed-off-by: Nikolaj Bjorner --- src/muz/base/rule_properties.cpp | 4 +-- src/muz/base/rule_properties.h | 1 + src/muz/rel/dl_mk_explanations.cpp | 4 +++ src/muz/rel/karr_relation.h | 2 +- src/muz/rel/rel_context.cpp | 2 +- src/smt/theory_arith_aux.h | 42 ++++++++++++++++-------------- 6 files changed, 32 insertions(+), 23 deletions(-) diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp index 7f019c74e..f5cac29e5 100644 --- a/src/muz/base/rule_properties.cpp +++ b/src/muz/base/rule_properties.cpp @@ -26,7 +26,7 @@ Notes: using namespace datalog; rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p): - m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_generate_proof(false) {} + m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_generate_proof(false) {} rule_properties::~rule_properties() {} @@ -168,7 +168,7 @@ void rule_properties::operator()(app* n) { if (m_is_predicate(n)) { insert(m_interp_pred, m_rule); } - else if (is_uninterp(n)) { + else if (is_uninterp(n) && !m_dl.is_rule_sort(n->get_decl()->get_range())) { m_uninterp_funs.insert(n->get_decl(), m_rule); } else if (m_dt.is_accessor(n)) { diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h index bfff8cbe4..a16f63507 100644 --- a/src/muz/base/rule_properties.h +++ b/src/muz/base/rule_properties.h @@ -32,6 +32,7 @@ namespace datalog { context& m_ctx; i_expr_pred& m_is_predicate; datatype_util m_dt; + dl_decl_util m_dl; bool m_generate_proof; rule* m_rule; obj_map m_quantifiers; diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index 60a10190a..e650b6e6b 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -434,6 +434,7 @@ namespace datalog { relation_union_fn * explanation_relation_plugin::mk_union_fn(const relation_base & tgt, const relation_base & src, const relation_base * delta) { + std::cout << "check kind: " << check_kind(tgt) << "\n"; if (!check_kind(tgt) || (delta && !check_kind(*delta))) { return 0; } @@ -854,7 +855,10 @@ namespace datalog { scoped_ptr product_fun = rmgr.mk_join_fn(orig_rel, *m_e_fact_relation, 0, 0, 0); SASSERT(product_fun); scoped_rel aux_extended_rel = (*product_fun)(orig_rel, *m_e_fact_relation); + TRACE("dl", tout << aux_extended_rel << " " << aux_extended_rel->get_plugin().get_name() << "\n"; + tout << e_rel.get_plugin().get_name() << "\n";); scoped_ptr union_fun = rmgr.mk_union_fn(e_rel, *aux_extended_rel); + TRACE("dl", tout << union_fun << "\n";); SASSERT(union_fun); (*union_fun)(e_rel, *aux_extended_rel); } diff --git a/src/muz/rel/karr_relation.h b/src/muz/rel/karr_relation.h index 00a92748a..72448f026 100644 --- a/src/muz/rel/karr_relation.h +++ b/src/muz/rel/karr_relation.h @@ -45,7 +45,7 @@ namespace datalog { {} virtual bool can_handle_signature(const relation_signature & sig) { - return true; + return get_manager().get_context().karr(); } static symbol get_name() { return symbol("karr_relation"); } diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index c5c4d6d95..0d07b7c81 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -115,7 +115,7 @@ namespace datalog { rm.register_plugin(alloc(bound_relation_plugin, rm)); rm.register_plugin(alloc(interval_relation_plugin, rm)); - rm.register_plugin(alloc(karr_relation_plugin, rm)); + if (m_context.karr()) rm.register_plugin(alloc(karr_relation_plugin, rm)); rm.register_plugin(alloc(product_set_plugin, rm)); rm.register_plugin(alloc(udoc_plugin, rm)); rm.register_plugin(alloc(check_relation_plugin, rm)); diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 15d1edee9..30c92feea 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1377,11 +1377,11 @@ namespace smt { SASSERT(satisfy_bounds()); result = skipped_row?BEST_EFFORT:OPTIMIZED; break; - } + } if (x_i == null_theory_var) { // can increase/decrease x_j as much as we want. - if (inc && upper(x_j)) { + if (inc && upper(x_j) && !skipped_row) { update_value(x_j, upper_bound(x_j) - get_value(x_j)); TRACE("opt", tout << "moved v" << x_j << " to upper bound\n";); SASSERT(valid_row_assignment()); @@ -1389,7 +1389,7 @@ namespace smt { SASSERT(satisfy_integrality()); continue; } - if (!inc && lower(x_j)) { + if (!inc && lower(x_j) && !skipped_row) { update_value(x_j, lower_bound(x_j) - get_value(x_j)); TRACE("opt", tout << "moved v" << x_j << " to lower bound\n";); SASSERT(valid_row_assignment()); @@ -1463,6 +1463,7 @@ namespace smt { template bool theory_arith::move_to_bound(theory_var x_i, bool move_to_lower) { inf_numeral delta, delta_abs; + numeral lc(1); if (move_to_lower) { delta = lower_bound(x_i) - get_value(x_i); @@ -1475,7 +1476,7 @@ namespace smt { TRACE("opt", tout << "Original delta: " << delta << "\n";); - delta_abs = abs(delta); + delta_abs = abs(delta); // // Decrease absolute value of delta according to bounds on rows where x_i is used. // @@ -1483,28 +1484,31 @@ namespace smt { typename svector::iterator it = c.begin_entries(); typename svector::iterator end = c.end_entries(); for (; it != end && delta_abs.is_pos(); ++it) { - if (!it->is_dead()) { - row & r = m_rows[it->m_row_id]; - theory_var s = r.get_base_var(); - if (s != null_theory_var && !is_quasi_base(s)) { - numeral const & coeff = r[it->m_row_idx].m_coeff; - SASSERT(!coeff.is_zero()); - bool inc_s = coeff.is_pos() ? move_to_lower : !move_to_lower; // NSB: review this.. - bound * b = get_bound(s, inc_s); - if (b) { - inf_numeral delta2 = abs((get_value(s) - b->get_value())/coeff); - if (delta2 < delta_abs) { - delta_abs = delta2; - } + if (it->is_dead()) continue; + row & r = m_rows[it->m_row_id]; + theory_var s = r.get_base_var(); + if (s != null_theory_var && !is_quasi_base(s)) { + numeral const & coeff = r[it->m_row_idx].m_coeff; + SASSERT(!coeff.is_zero()); + bool inc_s = coeff.is_pos() ? move_to_lower : !move_to_lower; // NSB: review this.. + bound * b = get_bound(s, inc_s); + if (b) { + inf_numeral delta2 = abs((get_value(s) - b->get_value())/coeff); + if (delta2 < delta_abs) { + delta_abs = delta2; } } + if (is_int(x_i)) { + lc = lcm(lc, denominator(abs(coeff))); + } } } bool truncated = false; if (is_int(x_i)) { - truncated = !delta_abs.is_int(); - delta_abs = floor(delta_abs); + inf_numeral tmp = delta_abs/lc; + truncated = !tmp.is_int(); + delta_abs = lc*floor(tmp); } if (move_to_lower) { From 1d18934ddb2296b9029cb81222d8a9b96ca471de Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Dec 2014 16:19:38 -0800 Subject: [PATCH 2/7] fix overflow and integrality bugs reported by Phan Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_mk_explanations.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp index e650b6e6b..55c87f66e 100644 --- a/src/muz/rel/dl_mk_explanations.cpp +++ b/src/muz/rel/dl_mk_explanations.cpp @@ -434,7 +434,6 @@ namespace datalog { relation_union_fn * explanation_relation_plugin::mk_union_fn(const relation_base & tgt, const relation_base & src, const relation_base * delta) { - std::cout << "check kind: " << check_kind(tgt) << "\n"; if (!check_kind(tgt) || (delta && !check_kind(*delta))) { return 0; } From 21ea48bfd85dcb7d2e5c7bd03c87fb6e50ef8797 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 15 Dec 2014 16:27:35 -0800 Subject: [PATCH 3/7] epsilon should have real type, reported by GeorgeKarpenkov, codeplex issue 145 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 03f0f016f..a7f4d29b5 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -995,7 +995,7 @@ namespace opt { args.push_back(m_arith.mk_numeral(r, r.is_int())); } if (!eps.is_zero()) { - expr* ep = m.mk_const(symbol("epsilon"), m_arith.mk_int()); + expr* ep = m.mk_const(symbol("epsilon"), m_arith.mk_real()); if (eps.is_one()) { args.push_back(ep); } From a7c7b70e19a7d7b6b6b09d872161730f36bc6a3c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 22 Dec 2014 12:49:31 +0000 Subject: [PATCH 4/7] muZ Datalog: be more aggressive when forming join_project --- src/muz/rel/dl_compiler.cpp | 32 ++++++++++++++++++++++++++------ 1 file changed, 26 insertions(+), 6 deletions(-) diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index c512598a0..648c91e4a 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -408,13 +408,14 @@ namespace datalog { void compiler::get_local_indexes_for_projection(app * t, var_counter & globals, unsigned ofs, unsigned_vector & res) { + // TODO: this can be optimized to avoid renames in some cases unsigned n = t->get_num_args(); for(unsigned i = 0; iget_arg(i); - if(!is_var(e) || globals.get(to_var(e)->get_idx())!=0) { - continue; + if (is_var(e) && globals.get(to_var(e)->get_idx()) > 0) { + globals.update(to_var(e)->get_idx(), -1); + res.push_back(i + ofs); } - res.push_back(i+ofs); } } @@ -422,11 +423,30 @@ namespace datalog { SASSERT(r->get_positive_tail_size()==2); ast_manager & m = m_context.get_manager(); rule_counter counter; - counter.count_rule_vars(m, r); + // leave one column copy per var in the head (avoids later duplication) + counter.count_vars(m, r->get_head(), -1); + + // take interp & neg preds into account (at least 1 column copy if referenced) + unsigned n = r->get_tail_size(); + if (n > 2) { + rule_counter counter_tail; + for (unsigned i = 2; i < n; ++i) { + counter_tail.count_vars(m, r->get_tail(i)); + } + + rule_counter::iterator I = counter_tail.begin(), E = counter_tail.end(); + for (; I != E; ++I) { + int& n = counter.get(I->m_key); + if (n == 0) + n = -1; + } + } + app * t1 = r->get_tail(0); app * t2 = r->get_tail(1); - counter.count_vars(m, t1, -1); - counter.count_vars(m, t2, -1); + counter.count_vars(m, t1); + counter.count_vars(m, t2); + get_local_indexes_for_projection(t1, counter, 0, res); get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res); } From 4ee83c1774a86d973224241986f740b4947c2031 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 22 Dec 2014 12:53:35 +0000 Subject: [PATCH 5/7] Datalog/DoC: add fast path for join_project for the case 'h(X) :- f(X), g(X).' Signed-off-by: Nuno Lopes --- src/muz/rel/udoc_relation.cpp | 34 ++++++++++++++++++++++++++++++++++ src/muz/rel/udoc_relation.h | 1 + 2 files changed, 35 insertions(+) diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index b3abf7998..9d562b17a 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -1028,7 +1028,9 @@ namespace datalog { } class udoc_plugin::join_project_fn : public convenient_relation_join_project_fn { +#if 0 udoc_plugin::join_fn m_joiner; +#endif union_find_default_ctx union_ctx; bit_vector m_to_delete; subset_ints m_equalities; @@ -1043,7 +1045,9 @@ namespace datalog { t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2, removed_col_cnt, rm_cols), +#if 0 m_joiner(t1.get_plugin(), t1, t2, col_cnt, cols1, cols2), +#endif m_equalities(union_ctx) { udoc_plugin& p = t1.get_plugin(); @@ -1152,12 +1156,42 @@ namespace datalog { }; + + class udoc_plugin::join_project_and_fn : public convenient_relation_join_project_fn { + public: + join_project_and_fn(udoc_relation const& t1, udoc_relation const& t2, + unsigned col_cnt, const unsigned *cols1, const unsigned *cols2, + unsigned removed_col_cnt, unsigned const *rm_cols) + : convenient_relation_join_project_fn(t1.get_signature(), t2.get_signature(), + col_cnt, cols1, cols2, removed_col_cnt, rm_cols) {} + + virtual relation_base* operator()(relation_base const& t1, relation_base const& t2) { + udoc_relation *result = get(t1.clone()); + result->get_udoc().intersect(result->get_dm(), get(t2).get_udoc()); + return result; + } + }; + relation_join_fn * udoc_plugin::mk_join_project_fn( relation_base const& t1, relation_base const& t2, unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, unsigned removed_col_cnt, const unsigned * removed_cols) { if (!check_kind(t1) || !check_kind(t2)) return 0; + // special case where we have h(X) :- f(X), g(X). + if (joined_col_cnt == removed_col_cnt && + t1.get_signature().size() == joined_col_cnt && + t2.get_signature().size() == joined_col_cnt) { + for (unsigned i = 0; i < removed_col_cnt; ++i) { + if (removed_cols[i] != i) + goto general_fn; + } + return alloc(join_project_and_fn, get(t1), get(t2), + joined_col_cnt, cols1, cols2, + removed_col_cnt, removed_cols); + } + + general_fn: return alloc(join_project_fn, get(t1), get(t2), joined_col_cnt, cols1, cols2, removed_col_cnt, removed_cols); diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h index 7934521a8..7cad3b348 100644 --- a/src/muz/rel/udoc_relation.h +++ b/src/muz/rel/udoc_relation.h @@ -82,6 +82,7 @@ namespace datalog { friend class udoc_relation; class join_fn; class join_project_fn; + class join_project_and_fn; class project_fn; class union_fn; class rename_fn; From dddb31fc37c87de35e97aa90fcc54d7ac55afe31 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 22 Dec 2014 13:03:06 +0000 Subject: [PATCH 6/7] minor optimization to previous patch Signed-off-by: Nuno Lopes --- src/muz/rel/udoc_relation.cpp | 12 +++--------- 1 file changed, 3 insertions(+), 9 deletions(-) diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 9d562b17a..37cc91778 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -1157,13 +1157,9 @@ namespace datalog { }; - class udoc_plugin::join_project_and_fn : public convenient_relation_join_project_fn { + class udoc_plugin::join_project_and_fn : public relation_join_fn { public: - join_project_and_fn(udoc_relation const& t1, udoc_relation const& t2, - unsigned col_cnt, const unsigned *cols1, const unsigned *cols2, - unsigned removed_col_cnt, unsigned const *rm_cols) - : convenient_relation_join_project_fn(t1.get_signature(), t2.get_signature(), - col_cnt, cols1, cols2, removed_col_cnt, rm_cols) {} + join_project_and_fn() {} virtual relation_base* operator()(relation_base const& t1, relation_base const& t2) { udoc_relation *result = get(t1.clone()); @@ -1186,9 +1182,7 @@ namespace datalog { if (removed_cols[i] != i) goto general_fn; } - return alloc(join_project_and_fn, get(t1), get(t2), - joined_col_cnt, cols1, cols2, - removed_col_cnt, removed_cols); + return alloc(join_project_and_fn); } general_fn: From ee71c434b6a936d62f6fab43cdc31b31407baaf7 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 22 Dec 2014 14:17:07 +0000 Subject: [PATCH 7/7] muZ/datalog: remove a few spurious make_empty() calls from the instruction handlers Signed-off-by: Nuno Lopes --- src/muz/rel/dl_instruction.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index b2837c710..7fbe2f5ad 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -266,7 +266,6 @@ namespace datalog { : m_clone(clone), m_src(src), m_tgt(tgt) {} virtual bool perform(execution_context & ctx) { if (ctx.reg(m_src)) log_verbose(ctx); - ctx.make_empty(m_tgt); if (m_clone) { ctx.set_reg(m_tgt, ctx.reg(m_src) ? ctx.reg(m_src)->clone() : 0); } @@ -370,9 +369,9 @@ namespace datalog { m_cols2(col_cnt, cols2), m_res(result) {} virtual bool perform(execution_context & ctx) { log_verbose(ctx); - ctx.make_empty(m_res); ++ctx.m_stats.m_join; if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) { + ctx.make_empty(m_res); return true; } relation_join_fn * fn; @@ -755,8 +754,8 @@ namespace datalog { reg_idx tgt) : m_projection(projection), m_src(src), m_cols(col_cnt, cols), m_tgt(tgt) {} virtual bool perform(execution_context & ctx) { - ctx.make_empty(m_tgt); if (!ctx.reg(m_src)) { + ctx.make_empty(m_tgt); return true; } @@ -823,8 +822,8 @@ namespace datalog { } virtual bool perform(execution_context & ctx) { log_verbose(ctx); - ctx.make_empty(m_res); if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) { + ctx.make_empty(m_res); return true; } ++ctx.m_stats.m_join_project; @@ -1000,7 +999,6 @@ namespace datalog { virtual bool perform(execution_context & ctx) { log_verbose(ctx); ++ctx.m_stats.m_unary_singleton; - ctx.make_empty(m_tgt); relation_base * rel = ctx.get_rel_context().get_rmanager().mk_empty_relation(m_sig, m_pred); rel->add_fact(m_fact); ctx.set_reg(m_tgt, rel); @@ -1034,7 +1032,6 @@ namespace datalog { virtual bool perform(execution_context & ctx) { log_verbose(ctx); ++ctx.m_stats.m_total; - ctx.make_empty(m_tgt); ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred)); return true; }