From fbb59453c3bf1f8d1041de9f055f93061a1129b0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Apr 2013 09:10:34 -0700 Subject: [PATCH] add loop counter v1 Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_bit_blast.h | 21 +----- src/muz_qe/dl_mk_karr_invariants.cpp | 2 +- src/muz_qe/dl_mk_loop_counter.cpp | 104 +++++++++++++++++++++++++++ src/muz_qe/dl_mk_loop_counter.h | 38 ++++++++++ 4 files changed, 146 insertions(+), 19 deletions(-) create mode 100644 src/muz_qe/dl_mk_loop_counter.cpp create mode 100644 src/muz_qe/dl_mk_loop_counter.h diff --git a/src/muz_qe/dl_mk_bit_blast.h b/src/muz_qe/dl_mk_bit_blast.h index 60c83f6cb..da91c5804 100644 --- a/src/muz_qe/dl_mk_bit_blast.h +++ b/src/muz_qe/dl_mk_bit_blast.h @@ -7,7 +7,7 @@ Module Name: Abstract: - + Functor for bit-blasting a rule set Author: @@ -19,31 +19,16 @@ Revision History: #ifndef _DL_MK_BIT_BLAST_H_ #define _DL_MK_BIT_BLAST_H_ -#include - -#include"map.h" -#include"obj_pair_hashtable.h" -#include"dl_context.h" -#include"dl_rule_set.h" #include"dl_rule_transformer.h" namespace datalog { - /** - \brief Functor for bit-blasting a rule set. - */ - class mk_bit_blast : public rule_transformer::plugin { class impl; - - impl* m_impl; - void blast(expr_ref& b); - void reset(); - + impl* m_impl; public: mk_bit_blast(context & ctx, unsigned priority = 35000); - ~mk_bit_blast(); - + ~mk_bit_blast(); rule_set * operator()(rule_set const & source); }; diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index 6dca35cdf..2596a7337 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -204,7 +204,7 @@ namespace datalog { m_inner_ctx.ensure_opened(); it = source.begin(); for (; it != end; ++it) { - rule_ref r(*it, m_ctx.get_rule_manager()); + rule_ref r(*it, m_inner_ctx.get_rule_manager()); m_inner_ctx.add_rule(r); m_inner_ctx.register_predicate(r->get_decl()); } diff --git a/src/muz_qe/dl_mk_loop_counter.cpp b/src/muz_qe/dl_mk_loop_counter.cpp new file mode 100644 index 000000000..8c9ad7f52 --- /dev/null +++ b/src/muz_qe/dl_mk_loop_counter.cpp @@ -0,0 +1,104 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_loop_counter.cpp + +Abstract: + + Add loop counter argument to relations. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-03-31 + +Revision History: + +--*/ + +#include"dl_mk_loop_counter.h" +#include"dl_context.h" + +namespace datalog { + + mk_loop_counter::mk_loop_counter(context & ctx, unsigned priority): + plugin(priority) { + } + + mk_loop_counter::~mk_loop_counter() { } + + app_ref mk_loop_counter::add_arg(ast_manager& m, app* fn, unsigned idx) { + arith_util a(m); + ptr_vector domain; + expr_ref_vector args(m); + domain.append(fn->get_num_args(), fn->get_decl()->get_domain()); + domain.push_back(a.mk_int()); + args.append(fn->get_num_args(), fn->get_args()); + args.push_back(m.mk_var(idx, a.mk_int())); + func_decl_ref new_fn(m); + new_fn = m.mk_func_decl(fn->get_decl()->get_name(), domain.size(), domain.c_ptr(), m.mk_bool_sort()); + return app_ref(m.mk_app(new_fn, args.size(), args.c_ptr()), m); + } + + rule_set * mk_loop_counter::operator()(rule_set const & source) { + context& ctx = source.get_context(); + ast_manager& m = source.get_manager(); + rule_manager& rm = source.get_rule_manager(); + arith_util a(m); + 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; + rule_counter& vc = rm.get_counter(); + for (unsigned i = 0; i < sz; ++i) { + tail.reset(); + neg.reset(); + rule & r = *source.get_rule(i); + unsigned cnt = vc.get_max_rule_var(r)+1; + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + for (unsigned j = 0; j < utsz; ++j, ++cnt) { + tail.push_back(add_arg(m, r.get_tail(j), cnt)); + neg.push_back(r.is_neg_tail(j)); + ctx.register_predicate(tail.back()->get_decl()); + } + for (unsigned j = utsz; j < tsz; ++j) { + tail.push_back(r.get_tail(j)); + neg.push_back(false); + } + head = add_arg(m, r.get_head(), cnt); + ctx.register_predicate(head->get_decl()); + // set the loop counter to be an increment of the previous + bool found = false; + unsigned last = head->get_num_args()-1; + for (unsigned j = 0; !found && j < utsz; ++j) { + if (head->get_decl() == tail[j]->get_decl()) { + tail.push_back(m.mk_eq(head->get_arg(last), + a.mk_add(tail[j]->get_arg(last), + a.mk_numeral(rational(1), true)))); + neg.push_back(false); + found = true; + } + } + // initialize loop counter to 0 if none was found. + if (!found) { + expr_ref_vector args(m); + args.append(head->get_num_args(), head->get_args()); + args[last] = a.mk_numeral(rational(0), true); + head = m.mk_app(head->get_decl(), args.size(), args.c_ptr()); + } + + new_rule = rm.mk(head, tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true); + result->add_rule(new_rule); + } + + // model converter: remove references to extra argument. + // proof converter: etc. + + return result; + } + +}; diff --git a/src/muz_qe/dl_mk_loop_counter.h b/src/muz_qe/dl_mk_loop_counter.h new file mode 100644 index 000000000..ad2c837a9 --- /dev/null +++ b/src/muz_qe/dl_mk_loop_counter.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_loop_counter.h + +Abstract: + + Add loop counter argument to relations. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-03-31 + +Revision History: + +--*/ +#ifndef _DL_MK_LOOP_COUNTER_H_ +#define _DL_MK_LOOP_COUNTER_H_ + +#include"dl_rule_transformer.h" + +namespace datalog { + + class mk_loop_counter : public rule_transformer::plugin { + app_ref add_arg(ast_manager& m, app* fn, unsigned idx); + public: + mk_loop_counter(context & ctx, unsigned priority = 33000); + ~mk_loop_counter(); + + rule_set * operator()(rule_set const & source); + }; + +}; + +#endif /* _DL_MK_LOOP_COUNTER_H_ */ +