diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 3a62a9b98..cc2dc02c5 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -232,6 +232,7 @@ namespace datalog { context::~context() { reset(); + dealloc(m_params); } void context::reset() { diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index b44f67644..02b00be39 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -46,6 +46,7 @@ Revision History: #include"dl_mk_rule_inliner.h" #include"dl_mk_interp_tail_simplifier.h" #include"dl_mk_bit_blast.h" +#include"dl_mk_separate_negated_tails.h" #include"fixedpoint_params.hpp" @@ -281,6 +282,7 @@ namespace datalog { transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context)); transf.register_plugin(alloc(mk_rule_inliner, m_context)); transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context)); + transf.register_plugin(alloc(mk_separate_negated_tails, m_context)); if (m_context.get_params().bit_blast()) { transf.register_plugin(alloc(mk_bit_blast, m_context, 22000)); diff --git a/src/muz/transforms/dl_mk_separate_negated_tails.cpp b/src/muz/transforms/dl_mk_separate_negated_tails.cpp new file mode 100644 index 000000000..18e7feadf --- /dev/null +++ b/src/muz/transforms/dl_mk_separate_negated_tails.cpp @@ -0,0 +1,119 @@ + +#include "dl_mk_separate_negated_tails.h" +#include "dl_context.h" + +namespace datalog { + + mk_separate_negated_tails::mk_separate_negated_tails(context& ctx, unsigned priority): + plugin(priority), + m(ctx.get_manager()), + rm(ctx.get_rule_manager()), + m_ctx(ctx) + {} + + bool mk_separate_negated_tails::has_private_vars(rule const& r, unsigned j) { + get_private_vars(r, j); + return !m_vars.empty(); + } + + void mk_separate_negated_tails::get_private_vars(rule const& r, unsigned j) { + m_vars.reset(); + m_fv.reset(); + get_free_vars(r.get_head(), m_fv); + for (unsigned i = 0; i < r.get_tail_size(); ++i) { + if (i != j) { + get_free_vars(r.get_tail(i), m_fv); + } + } + + app* p = r.get_tail(j); + for (unsigned i = 0; i < p->get_num_args(); ++i) { + expr* v = p->get_arg(i); + if (is_var(v)) { + unsigned idx = to_var(v)->get_idx(); + if (idx >= m_fv.size() || !m_fv[idx]) { + m_vars.push_back(v); + } + } + } + } + + void mk_separate_negated_tails::abstract_predicate(app* p, app_ref& q, rule_set& rules) { + expr_ref_vector args(m); + sort_ref_vector sorts(m); + func_decl_ref fn(m); + for (unsigned i = 0; i < p->get_num_args(); ++i) { + expr* arg = p->get_arg(i); + if (!m_vars.contains(arg)) { + args.push_back(arg); + sorts.push_back(m.get_sort(arg)); + } + } + fn = m.mk_fresh_func_decl(p->get_decl()->get_name(), symbol("N"), sorts.size(), sorts.c_ptr(), m.mk_bool_sort()); + m_ctx.register_predicate(fn, false); + q = m.mk_app(fn, args.size(), args.c_ptr()); + bool is_neg = true; + rules.add_rule(rm.mk(q, 1, & p, &is_neg)); + } + + void mk_separate_negated_tails::create_rule(rule const&r, rule_set& rules) { + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned ptsz = r.get_positive_tail_size(); + unsigned tsz = r.get_tail_size(); + app_ref_vector tail(m); + app_ref p(m); + svector neg; + for (unsigned i = 0; i < ptsz; ++i) { + tail.push_back(r.get_tail(i)); + neg.push_back(false); + } + for (unsigned i = ptsz; i < utsz; ++i) { + get_private_vars(r, i); + if (!m_vars.empty()) { + abstract_predicate(r.get_tail(i), p, rules); + tail.push_back(p); + neg.push_back(false); + } + else { + neg.push_back(true); + tail.push_back(r.get_tail(i)); + } + } + for (unsigned i = utsz; i < tsz; ++i) { + tail.push_back(r.get_tail(i)); + neg.push_back(false); + } + rules.add_rule(rm.mk(r.get_head(), tail.size(), tail.c_ptr(), neg.c_ptr(), r.name())); + } + + rule_set * mk_separate_negated_tails::operator()(rule_set const& src) { + scoped_ptr result = alloc(rule_set, m_ctx); + bool has_new_rule = false; + unsigned sz = src.get_num_rules(); + for (unsigned i = 0; i < sz; ++i) { + bool change = false; + rule & r = *src.get_rule(i); + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned ptsz = r.get_positive_tail_size(); + for (unsigned j = ptsz; j < utsz; ++j) { + SASSERT(r.is_neg_tail(j)); + if (has_private_vars(r, j)) { + create_rule(r, *result); + has_new_rule = true; + change = true; + break; + } + } + if (!change) { + result->add_rule(&r); + } + } + if (!has_new_rule) { + return 0; + } + else { + result->inherit_predicates(src); + return result.detach(); + } + } +} diff --git a/src/muz/transforms/dl_mk_separate_negated_tails.h b/src/muz/transforms/dl_mk_separate_negated_tails.h new file mode 100644 index 000000000..4b1673307 --- /dev/null +++ b/src/muz/transforms/dl_mk_separate_negated_tails.h @@ -0,0 +1,61 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + mk_separate_negated_tails.h + +Abstract: + + Rule transformer which creates new rules for predicates + in negated tails that use free variables not used + elsewhere. These free variables incur an overhead + on the instructions compiled using dl_compiler. + + Consider the following transformations: + + P(x) :- Exists y, z, u . Q(x,y), !R(y,z), !T(z,u). + => + P(x) :- Exists y, z . Q(x,y), !R(y,z), Exists u . ! T(z,u). + => + P(x) :- Exists y, z . Q(x,y), !R(y,z), TN(z). + TN(z) :- !T(z,u). + + + + +Author: + + Nikolaj Bjorner (nbjorner) 2013-09-09 + +Revision History: + +--*/ + +#ifndef _DL_MK_SEPARAT_NEGATED_TAILS_H_ +#define _DL_MK_SEPARAT_NEGATED_TAILS_H_ + +#include "dl_rule_transformer.h" +#include "dl_context.h" + +namespace datalog { + + class mk_separate_negated_tails : public rule_transformer::plugin { + ast_manager & m; + rule_manager& rm; + context & m_ctx; + ptr_vector m_vars; + ptr_vector m_fv; + + bool has_private_vars(rule const& r, unsigned j); + void get_private_vars(rule const& r, unsigned j); + void abstract_predicate(app* p, app_ref& q, rule_set& rules); + void create_rule(rule const&r, rule_set& rules); + + public: + mk_separate_negated_tails(context& ctx, unsigned priority = 21000); + rule_set * operator()(rule_set const & source); + }; +} + +#endif diff --git a/src/muz/transforms/dl_mk_subsumption_checker.h b/src/muz/transforms/dl_mk_subsumption_checker.h index da42e4202..8d797a9e2 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.h +++ b/src/muz/transforms/dl_mk_subsumption_checker.h @@ -84,7 +84,7 @@ namespace datalog { reset_dealloc_values(m_ground_unconditional_rule_heads); } - rule_set * operator()(rule_set const & source); + virtual rule_set * operator()(rule_set const & source); }; };