From 13262a0fc52f9d3919046fb3444ebea22a9be2a3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Jun 2013 13:13:47 -0500 Subject: [PATCH] missing files Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_magic_symbolic.cpp | 133 ++++++++++++++++++++++++++++ src/muz_qe/dl_mk_magic_symbolic.h | 40 +++++++++ 2 files changed, 173 insertions(+) create mode 100644 src/muz_qe/dl_mk_magic_symbolic.cpp create mode 100644 src/muz_qe/dl_mk_magic_symbolic.h diff --git a/src/muz_qe/dl_mk_magic_symbolic.cpp b/src/muz_qe/dl_mk_magic_symbolic.cpp new file mode 100644 index 000000000..2820ecaef --- /dev/null +++ b/src/muz_qe/dl_mk_magic_symbolic.cpp @@ -0,0 +1,133 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_magic_symbolic.cpp + +Abstract: + + Create Horn clauses for magic symbolic flow. + + Q(x) :- A(y), B(z), phi1(x,y,z). + Q(x) :- C(y), phi2(x,y). + A(x) :- C(y), phi3(x,y). + A(x) :- A(y), phi3(x,y). + B(x) :- C(y), A(z), phi4(x,y,z). + C(x) :- phi5(x). + + Transformed clauses: + + Q_ans(x) :- Q_query(x), A_ans(y), B_ans(z), phi1(x,y,z). + Q_ans(x) :- Q_query(x), C_ans(y), phi2(x,y). + Q_query(x) :- true. + + A_ans(x) :- A_query(x), C_ans(y), phi2(x,y) + A_ans(x) :- A_query(x), A_ans(y), phi3(x,y). + A_query(y) :- Q_query(x), phi1(x,y,z). + A_query(y) :- A_query(x), phi3(x,y). + A_query(z) :- B_query(x), C_ans(y), phi4(x,y,z). + + B_ans(x) :- B_query(x), C_ans(y), A_ans(z), phi4(x,y,z). + B_query(z) :- Q_query(x), A_ans(y), phi1(x,y,z). + + C_ans(x) :- C_query(x), phi5(x). + C_query(y) :- Q_query(x), phi2(x,y). + C_query(y) :- Q_query(x), phi3(x,y). + C_query(y) :- B_query(x), phi4(x,y,z). + +General scheme: + A(x) :- P1(x_1), ..., Pn(x_n), phi(x,x1,..,x_n). + + P(x) :- Prefix(x,y,z), A(z) ... + + A_ans(x) :- A_query(x), P_i_ans(x_i), phi(x,..). + A_query(z) :- P_query(x), Prefix_ans(x,y,z). + +Author: + + Nikolaj Bjorner (nbjorner) 2013-06-19 + +Revision History: + +--*/ + +#include"dl_mk_magic_symbolic.h" +#include"dl_context.h" + +namespace datalog { + + + mk_magic_symbolic::mk_magic_symbolic(context & ctx, unsigned priority): + plugin(priority), + m(ctx.get_manager()), + m_ctx(ctx) { + } + + mk_magic_symbolic::~mk_magic_symbolic() { } + + rule_set * mk_magic_symbolic::operator()(rule_set const & source) { + if (!m_ctx.get_params().magic()) { + return 0; + } + context& ctx = source.get_context(); + rule_manager& rm = source.get_rule_manager(); + rule_set * result = alloc(rule_set, ctx); + unsigned sz = source.get_num_rules(); + rule_ref new_rule(rm); + app_ref_vector tail(m); + app_ref head(m); + svector neg; + for (unsigned i = 0; i < sz; ++i) { + rule & r = *source.get_rule(i); + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + tail.reset(); + neg.reset(); + for (unsigned j = utsz; j < tsz; ++j) { + tail.push_back(r.get_tail(j)); + neg.push_back(false); + } + tail.push_back(mk_query(r.get_head())); + neg.push_back(false); + for (unsigned j = 0; j < utsz; ++j) { + tail.push_back(mk_ans(r.get_tail(j))); + neg.push_back(false); + } + new_rule = rm.mk(mk_ans(r.get_head()), tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true); + if (source.is_output_predicate(r.get_decl())) { + result->set_output_predicate(new_rule->get_decl()); + } + + result->add_rule(new_rule); + for (unsigned j = 0; j < utsz; ++j) { + new_rule = rm.mk(mk_query(r.get_tail(j)), tail.size()-utsz+j, tail.c_ptr(), neg.c_ptr(), r.name(), true); + result->add_rule(new_rule); + } + + } + TRACE("dl", result->display(tout);); + return result; + } + + app_ref mk_magic_symbolic::mk_query(app* q) { + string_buffer<64> name; + func_decl* f = q->get_decl(); + name << f->get_name() << "!query"; + func_decl_ref g(m); + g = m.mk_func_decl(symbol(name.c_str()), f->get_arity(), f->get_domain(), f->get_range()); + m_ctx.register_predicate(g, false); + return app_ref(m.mk_app(g, q->get_num_args(), q->get_args()), m); + } + + app_ref mk_magic_symbolic::mk_ans(app* q) { + string_buffer<64> name; + func_decl* f = q->get_decl(); + func_decl_ref g(m); + name << f->get_name() << "!ans"; + g = m.mk_func_decl(symbol(name.c_str()), f->get_arity(), f->get_domain(), f->get_range()); + m_ctx.register_predicate(g, false); + return app_ref(m.mk_app(g, q->get_num_args(), q->get_args()), m); + } + +}; diff --git a/src/muz_qe/dl_mk_magic_symbolic.h b/src/muz_qe/dl_mk_magic_symbolic.h new file mode 100644 index 000000000..ce9ca1145 --- /dev/null +++ b/src/muz_qe/dl_mk_magic_symbolic.h @@ -0,0 +1,40 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_magic_symbolic.h + +Abstract: + + Create Horn clauses for magic symbolic transformation. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-06-19 + +Revision History: + +--*/ +#ifndef _DL_MK_MAGIC_SYMBOLIC_H_ +#define _DL_MK_MAGIC_SYMBOLIC_H_ + +#include"dl_rule_transformer.h" + +namespace datalog { + + class mk_magic_symbolic : public rule_transformer::plugin { + ast_manager& m; + context& m_ctx; + app_ref mk_ans(app* q); + app_ref mk_query(app* q); + public: + mk_magic_symbolic(context & ctx, unsigned priority = 33037); + ~mk_magic_symbolic(); + rule_set * operator()(rule_set const & source); + }; + +}; + +#endif /* _DL_MK_MAGIC_SYMBOLIC_H_ */ +