mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

loop counting

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-01 09:15:23 -07:00
parent fbb59453c3
commit 2e0c5f5042
2 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/muz_qe/dl_mk_loop_counter.cpp
View file

@ -23,13 +23,14 @@ Revision History:
namespace datalog { namespace datalog {
mk_loop_counter::mk_loop_counter(context & ctx, unsigned priority): mk_loop_counter::mk_loop_counter(context & ctx, unsigned priority):
plugin(priority) { plugin(priority),
m(ctx.get_manager()),
a(m) {
} }
mk_loop_counter::~mk_loop_counter() { } mk_loop_counter::~mk_loop_counter() { }
app_ref mk_loop_counter::add_arg(ast_manager& m, app* fn, unsigned idx) { app_ref mk_loop_counter::add_arg(app* fn, unsigned idx) {
arith_util a(m);
ptr_vector<sort> domain; ptr_vector<sort> domain;
expr_ref_vector args(m); expr_ref_vector args(m);
domain.append(fn->get_num_args(), fn->get_decl()->get_domain()); domain.append(fn->get_num_args(), fn->get_decl()->get_domain());
@ -43,9 +44,7 @@ namespace datalog {
rule_set * mk_loop_counter::operator()(rule_set const & source) { rule_set * mk_loop_counter::operator()(rule_set const & source) {
context& ctx = source.get_context(); context& ctx = source.get_context();
ast_manager& m = source.get_manager();
rule_manager& rm = source.get_rule_manager(); rule_manager& rm = source.get_rule_manager();
arith_util a(m);
rule_set * result = alloc(rule_set, ctx); rule_set * result = alloc(rule_set, ctx);
unsigned sz = source.get_num_rules(); unsigned sz = source.get_num_rules();
rule_ref new_rule(rm); rule_ref new_rule(rm);
@ -61,7 +60,7 @@ namespace datalog {
unsigned utsz = r.get_uninterpreted_tail_size(); unsigned utsz = r.get_uninterpreted_tail_size();
unsigned tsz = r.get_tail_size(); unsigned tsz = r.get_tail_size();
for (unsigned j = 0; j < utsz; ++j, ++cnt) { for (unsigned j = 0; j < utsz; ++j, ++cnt) {
tail.push_back(add_arg(m, r.get_tail(j), cnt)); tail.push_back(add_arg(r.get_tail(j), cnt));
neg.push_back(r.is_neg_tail(j)); neg.push_back(r.is_neg_tail(j));
ctx.register_predicate(tail.back()->get_decl()); ctx.register_predicate(tail.back()->get_decl());
} }
@ -69,7 +68,7 @@ namespace datalog {
tail.push_back(r.get_tail(j)); tail.push_back(r.get_tail(j));
neg.push_back(false); neg.push_back(false);
} }
head = add_arg(m, r.get_head(), cnt); head = add_arg(r.get_head(), cnt);
ctx.register_predicate(head->get_decl()); ctx.register_predicate(head->get_decl());
// set the loop counter to be an increment of the previous // set the loop counter to be an increment of the previous
bool found = false; bool found = false;

5
src/muz_qe/dl_mk_loop_counter.h
View file

@ -20,11 +20,14 @@ Revision History:
#define _DL_MK_LOOP_COUNTER_H_ #define _DL_MK_LOOP_COUNTER_H_
#include"dl_rule_transformer.h" #include"dl_rule_transformer.h"
#include"arith_decl_plugin.h"
namespace datalog { namespace datalog {
class mk_loop_counter : public rule_transformer::plugin { class mk_loop_counter : public rule_transformer::plugin {
app_ref add_arg(ast_manager& m, app* fn, unsigned idx); ast_manager& m;
arith_util a;
app_ref add_arg(app* fn, unsigned idx);
public: public:
mk_loop_counter(context & ctx, unsigned priority = 33000); mk_loop_counter(context & ctx, unsigned priority = 33000);
~mk_loop_counter(); ~mk_loop_counter();