mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

Refactor count_vars and count_rule_vars

Browse source 
ast_manager m was not used
This commit is contained in:
Matthias Schlaipfer 2015-05-13 19:15:59 +01:00
parent 09afb31d4c
commit c82319b358
10 changed files with 28 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/ast_counter.cpp
View file

@ -86,7 +86,7 @@ int counter::get_max_counter_value() const {
return res;
}
void var_counter::count_vars(ast_manager & m, const app * pred, int coef) {
void var_counter::count_vars(const app * pred, int coef) {
unsigned n = pred->get_num_args();
for (unsigned i = 0; i < n; i++) {
m_fv(pred->get_arg(i));

2
src/ast/rewriter/ast_counter.h
View file

@ -76,7 +76,7 @@ protected:
unsigned get_max_var(bool & has_var);
public:
var_counter() {}
void count_vars(ast_manager & m, const app * t, int coef = 1);
void count_vars(const app * t, int coef = 1);
unsigned get_max_var(expr* e);
unsigned get_next_var(expr* e);
};

4
src/muz/base/dl_rule.cpp
View file

@ -682,11 +682,11 @@ namespace datalog {
svector<bool> tail_neg;
app_ref head(r->get_head(), m);
vctr.count_vars(m, head);
vctr.count_vars(head);
for (unsigned i = 0; i < ut_len; i++) {
app * t = r->get_tail(i);
vctr.count_vars(m, t);
vctr.count_vars(t);
tail.push_back(t);
tail_neg.push_back(r->is_neg_tail(i));
}

6
src/muz/base/dl_util.cpp
View file

@ -256,12 +256,12 @@ namespace datalog {
}
void rule_counter::count_rule_vars(ast_manager & m, const rule * r, int coef) {
void rule_counter::count_rule_vars(const rule * r, int coef) {
reset();
count_vars(m, r->get_head(), 1);
count_vars(r->get_head(), 1);
unsigned n = r->get_tail_size();
for (unsigned i = 0; i < n; i++) {
count_vars(m, r->get_tail(i), coef);
count_vars(r->get_tail(i), coef);
}
}

2
src/muz/base/dl_util.h
View file

@ -347,7 +347,7 @@ namespace datalog {
class rule_counter : public var_counter {
public:
rule_counter(){}
void count_rule_vars(ast_manager & m, const rule * r, int coef = 1);
void count_rule_vars(const rule * r, int coef = 1);
unsigned get_max_rule_var(const rule& r);
};

9
src/muz/rel/dl_compiler.cpp
View file

@ -411,17 +411,16 @@ namespace datalog {
void compiler::get_local_indexes_for_projection(rule * r, unsigned_vector & res) {
SASSERT(r->get_positive_tail_size()==2);
ast_manager & m = m_context.get_manager();
rule_counter counter;
// leave one column copy per var in the head (avoids later duplication)
counter.count_vars(m, r->get_head(), -1);
counter.count_vars(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));
counter_tail.count_vars(r->get_tail(i));
}
rule_counter::iterator I = counter_tail.begin(), E = counter_tail.end();
@ -434,8 +433,8 @@ namespace datalog {
app * t1 = r->get_tail(0);
app * t2 = r->get_tail(1);
counter.count_vars(m, t1);
counter.count_vars(m, t2);
counter.count_vars(t1);
counter.count_vars(t2);
get_local_indexes_for_projection(t1, counter, 0, res);
get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res);

2
src/muz/rel/dl_mk_explanations.cpp
View file

@ -705,7 +705,7 @@ namespace datalog {
rule * mk_explanations::get_e_rule(rule * r) {
rule_counter ctr;
ctr.count_rule_vars(m_manager, r);
ctr.count_rule_vars(r);
unsigned max_var;
unsigned next_var = ctr.get_max_positive(max_var) ? (max_var+1) : 0;
unsigned head_var = next_var++;

2
src/muz/rel/dl_mk_similarity_compressor.cpp
View file

@ -381,7 +381,7 @@ namespace datalog {
}
rule_counter ctr;
ctr.count_rule_vars(m_manager, r);
ctr.count_rule_vars(r);
unsigned max_var_idx, new_var_idx_base;
if (ctr.get_max_positive(max_var_idx)) {
new_var_idx_base = max_var_idx+1;

24
src/muz/rel/dl_mk_simple_joins.cpp
View file

@ -316,7 +316,7 @@ namespace datalog {
void register_rule(rule * r) {
rule_counter counter;
counter.count_rule_vars(m, r, 1);
counter.count_rule_vars(r, 1);
ptr_vector<app> & rule_content =
m_rules_content.insert_if_not_there2(r, ptr_vector<app>())->get_data().m_value;
@ -329,19 +329,19 @@ namespace datalog {
for(unsigned i=0; i+1 < pos_tail_size; i++) {
app * t1 = r->get_tail(i);
var_idx_set t1_vars = rm.collect_vars(t1);
counter.count_vars(m, t1, -1); //temporarily remove t1 variables from counter
counter.count_vars(t1, -1); //temporarily remove t1 variables from counter
for(unsigned j=i+1; j<pos_tail_size; j++) {
app * t2 = r->get_tail(j);
counter.count_vars(m, t2, -1); //temporarily remove t2 variables from counter
counter.count_vars(t2, -1); //temporarily remove t2 variables from counter
var_idx_set scope_vars = rm.collect_vars(t2);
scope_vars |= t1_vars;
var_idx_set non_local_vars;
counter.collect_positive(non_local_vars);
counter.count_vars(m, t2, 1); //restore t2 variables in counter
counter.count_vars(t2, 1); //restore t2 variables in counter
set_intersection(non_local_vars, scope_vars);
register_pair(t1, t2, r, non_local_vars);
}
counter.count_vars(m, t1, 1); //restore t1 variables in counter
counter.count_vars(t1, 1); //restore t1 variables in counter
}
}
@ -460,16 +460,16 @@ namespace datalog {
app * head = r->get_head();
var_counter counter;
counter.count_vars(m, head, 1);
counter.count_vars(head, 1);
unsigned tail_size=r->get_tail_size();
unsigned pos_tail_size=r->get_positive_tail_size();
for(unsigned i=pos_tail_size; i<tail_size; i++) {
counter.count_vars(m, r->get_tail(i), 1);
counter.count_vars(r->get_tail(i), 1);
}
for(unsigned i=0; i<len; i++) {
counter.count_vars(m, rule_content[i], 1);
counter.count_vars(rule_content[i], 1);
}
//add edges that contain added tails
@ -477,7 +477,7 @@ namespace datalog {
app * a_tail = added_tails.back(); //added tail
var_idx_set a_tail_vars = rm.collect_vars(a_tail);
counter.count_vars(m, a_tail, -1); //temporarily remove a_tail variables from counter
counter.count_vars(a_tail, -1); //temporarily remove a_tail variables from counter
for(unsigned i=0; i<len; i++) {
app * o_tail = rule_content[i]; //other tail
@ -486,17 +486,17 @@ namespace datalog {
continue;
}
counter.count_vars(m, o_tail, -1); //temporarily remove o_tail variables from counter
counter.count_vars(o_tail, -1); //temporarily remove o_tail variables from counter
var_idx_set scope_vars = rm.collect_vars(o_tail);
scope_vars |= a_tail_vars;
var_idx_set non_local_vars;
counter.collect_positive(non_local_vars);
counter.count_vars(m, o_tail, 1); //restore o_tail variables in counter
counter.count_vars(o_tail, 1); //restore o_tail variables in counter
set_intersection(non_local_vars, scope_vars);
register_pair(o_tail, a_tail, r, non_local_vars);
}
counter.count_vars(m, a_tail, 1); //restore t1 variables in counter
counter.count_vars(a_tail, 1); //restore t1 variables in counter
added_tails.pop_back();
}
}

4
src/muz/transforms/dl_mk_unbound_compressor.cpp
View file

@ -93,7 +93,7 @@ namespace datalog {
unsigned n = head_pred->get_arity();
rm.get_counter().reset();
rm.get_counter().count_vars(m, head, 1);
rm.get_counter().count_vars(head, 1);
for (unsigned i=0; i<n; i++) {
expr * arg = head->get_arg(i);
@ -125,7 +125,7 @@ namespace datalog {
unsigned head_arity = head_pred->get_arity();
rm.get_counter().reset();
rm.get_counter().count_vars(m, head);
rm.get_counter().count_vars(head);
unsigned arg_index;
for (arg_index = 0; arg_index < head_arity; arg_index++) {