mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 12:21:21 +00:00
Code Activity

Merge branch 'unstable' of https://github.com/mschlaipfer/z3 into unstable

Browse source
This commit is contained in:
Nuno Lopes 2015-05-18 16:38:19 +01:00
commit d8dc86f558
10 changed files with 28 additions and 29 deletions
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; 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(); unsigned n = pred->get_num_args();
for (unsigned i = 0; i < n; i++) { for (unsigned i = 0; i < n; i++) {
m_fv(pred->get_arg(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); unsigned get_max_var(bool & has_var);
public: public:
var_counter() {} 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_max_var(expr* e);
unsigned get_next_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; svector<bool> tail_neg;
app_ref head(r->get_head(), m); app_ref head(r->get_head(), m);
vctr.count_vars(m, head); vctr.count_vars(head);
for (unsigned i = 0; i < ut_len; i++) { for (unsigned i = 0; i < ut_len; i++) {
app * t = r->get_tail(i); app * t = r->get_tail(i);
vctr.count_vars(m, t); vctr.count_vars(t);
tail.push_back(t); tail.push_back(t);
tail_neg.push_back(r->is_neg_tail(i)); 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(); reset();
count_vars(m, r->get_head(), 1); count_vars(r->get_head(), 1);
unsigned n = r->get_tail_size(); unsigned n = r->get_tail_size();
for (unsigned i = 0; i < n; i++) { 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 { class rule_counter : public var_counter {
public: public:
rule_counter(){} 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); 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) { void compiler::get_local_indexes_for_projection(rule * r, unsigned_vector & res) {
SASSERT(r->get_positive_tail_size()==2); SASSERT(r->get_positive_tail_size()==2);
ast_manager & m = m_context.get_manager();
rule_counter counter; rule_counter counter;
// leave one column copy per var in the head (avoids later duplication) // 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) // take interp & neg preds into account (at least 1 column copy if referenced)
unsigned n = r->get_tail_size(); unsigned n = r->get_tail_size();
if (n > 2) { if (n > 2) {
rule_counter counter_tail; rule_counter counter_tail;
for (unsigned i = 2; i < n; ++i) { 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(); rule_counter::iterator I = counter_tail.begin(), E = counter_tail.end();
@ -434,8 +433,8 @@ namespace datalog {
app * t1 = r->get_tail(0); app * t1 = r->get_tail(0);
app * t2 = r->get_tail(1); app * t2 = r->get_tail(1);
counter.count_vars(m, t1); counter.count_vars(t1);
counter.count_vars(m, t2); counter.count_vars(t2);
get_local_indexes_for_projection(t1, counter, 0, res); get_local_indexes_for_projection(t1, counter, 0, res);
get_local_indexes_for_projection(t2, counter, t1->get_num_args(), 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 * mk_explanations::get_e_rule(rule * r) {
rule_counter ctr; rule_counter ctr;
ctr.count_rule_vars(m_manager, r); ctr.count_rule_vars(r);
unsigned max_var; unsigned max_var;
unsigned next_var = ctr.get_max_positive(max_var) ? (max_var+1) : 0; unsigned next_var = ctr.get_max_positive(max_var) ? (max_var+1) : 0;
unsigned head_var = next_var++; 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; rule_counter ctr;
ctr.count_rule_vars(m_manager, r); ctr.count_rule_vars(r);
unsigned max_var_idx, new_var_idx_base; unsigned max_var_idx, new_var_idx_base;
if (ctr.get_max_positive(max_var_idx)) { if (ctr.get_max_positive(max_var_idx)) {
new_var_idx_base = max_var_idx+1; 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) { void register_rule(rule * r) {
rule_counter counter; rule_counter counter;
counter.count_rule_vars(m, r, 1); counter.count_rule_vars(r, 1);
ptr_vector<app> & rule_content = ptr_vector<app> & rule_content =
m_rules_content.insert_if_not_there2(r, ptr_vector<app>())->get_data().m_value; 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++) { for(unsigned i=0; i+1 < pos_tail_size; i++) {
app * t1 = r->get_tail(i); app * t1 = r->get_tail(i);
var_idx_set t1_vars = rm.collect_vars(t1); 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++) { for(unsigned j=i+1; j<pos_tail_size; j++) {
app * t2 = r->get_tail(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); var_idx_set scope_vars = rm.collect_vars(t2);
scope_vars |= t1_vars; scope_vars |= t1_vars;
var_idx_set non_local_vars; var_idx_set non_local_vars;
counter.collect_positive(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); set_intersection(non_local_vars, scope_vars);
register_pair(t1, t2, r, non_local_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(); app * head = r->get_head();
var_counter counter; var_counter counter;
counter.count_vars(m, head, 1); counter.count_vars(head, 1);
unsigned tail_size=r->get_tail_size(); unsigned tail_size=r->get_tail_size();
unsigned pos_tail_size=r->get_positive_tail_size(); unsigned pos_tail_size=r->get_positive_tail_size();
for(unsigned i=pos_tail_size; i<tail_size; i++) { 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++) { 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 //add edges that contain added tails
@ -477,7 +477,7 @@ namespace datalog {
app * a_tail = added_tails.back(); //added tail app * a_tail = added_tails.back(); //added tail
var_idx_set a_tail_vars = rm.collect_vars(a_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++) { for(unsigned i=0; i<len; i++) {
app * o_tail = rule_content[i]; //other tail app * o_tail = rule_content[i]; //other tail
@ -486,17 +486,17 @@ namespace datalog {
continue; 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); var_idx_set scope_vars = rm.collect_vars(o_tail);
scope_vars |= a_tail_vars; scope_vars |= a_tail_vars;
var_idx_set non_local_vars; var_idx_set non_local_vars;
counter.collect_positive(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); set_intersection(non_local_vars, scope_vars);
register_pair(o_tail, a_tail, r, non_local_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(); 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(); unsigned n = head_pred->get_arity();
rm.get_counter().reset(); 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++) { for (unsigned i=0; i<n; i++) {
expr * arg = head->get_arg(i); expr * arg = head->get_arg(i);
@ -125,7 +125,7 @@ namespace datalog {
unsigned head_arity = head_pred->get_arity(); unsigned head_arity = head_pred->get_arity();
rm.get_counter().reset(); rm.get_counter().reset();
rm.get_counter().count_vars(m, head); rm.get_counter().count_vars(head);
unsigned arg_index; unsigned arg_index;
for (arg_index = 0; arg_index < head_arity; arg_index++) { for (arg_index = 0; arg_index < head_arity; arg_index++) {