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

Integrating synchronize pass

Browse source
This commit is contained in:
Arie Gurfinkel 2018-07-24 11:45:40 -04:00
parent 8400122596
commit 0516e6f21f
2 changed files with 105 additions and 99 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

174
src/muz/transforms/dl_mk_synchronize.cpp
View file

@ -22,6 +22,8 @@ Revision History:
namespace datalog { namespace datalog {
typedef mk_synchronize::item_set_vector item_set_vector;
mk_synchronize::mk_synchronize(context& ctx, unsigned priority): mk_synchronize::mk_synchronize(context& ctx, unsigned priority):
rule_transformer::plugin(priority, false), rule_transformer::plugin(priority, false),
m_ctx(ctx), m_ctx(ctx),
@ -29,15 +31,16 @@ namespace datalog {
rm(ctx.get_rule_manager()) rm(ctx.get_rule_manager())
{} {}
bool mk_synchronize::is_recursive_app(rule & r, app * app) const { bool mk_synchronize::is_recursive(rule &r, func_decl &decl) const {
func_decl* head_decl = r.get_head()->get_decl(); func_decl *hdecl = r.get_head()->get_decl();
func_decl* app_decl = app->get_decl(); // AG: shouldn't decl appear in the body?
if (head_decl == app_decl) { if (hdecl == &decl) return true;
return true; auto & strata = m_stratifier->get_strats();
} unsigned num_of_stratum = m_stratifier->get_predicate_strat(hdecl);
rule_stratifier::comp_vector const & strata = m_stratifier->get_strats(); return strata[num_of_stratum]->contains(&decl);
unsigned num_of_stratum = m_stratifier->get_predicate_strat(head_decl); }
return strata[num_of_stratum]->contains(app_decl); bool mk_synchronize::is_recursive(rule &r, expr &e) const {
return is_app(&e) && is_recursive(r, *to_app(&e)->get_decl());
} }
bool mk_synchronize::has_recursive_premise(app * app) const { bool mk_synchronize::has_recursive_premise(app * app) const {
@ -50,33 +53,29 @@ namespace datalog {
return strata[num_of_stratum]->size() > 1; return strata[num_of_stratum]->size() > 1;
} }
ptr_vector<rule_stratifier::item_set> mk_synchronize::add_merged_decls(ptr_vector<app> & apps) { item_set_vector mk_synchronize::add_merged_decls(ptr_vector<app> & apps) {
unsigned n = apps.size(); unsigned sz = apps.size();
ptr_vector<rule_stratifier::item_set> merged_decls; item_set_vector merged_decls;
merged_decls.resize(n); merged_decls.resize(sz);
ptr_vector<func_decl> app_decls; auto & strata = m_stratifier->get_strats();
app_decls.resize(n); for (unsigned j = 0; j < sz; ++j) {
for (unsigned j = 0; j < n; ++j) { unsigned nos;
app_decls[j] = apps[j]->get_decl(); nos = m_stratifier->get_predicate_strat(apps[j]->get_decl());
} merged_decls[j] = strata[nos];
rule_stratifier::comp_vector const & strata = m_stratifier->get_strats();
for (unsigned j = 0; j < n; ++j) {
unsigned num_of_stratum = m_stratifier->get_predicate_strat(app_decls[j]);
merged_decls[j] = strata[num_of_stratum];
} }
return merged_decls; return merged_decls;
} }
void mk_synchronize::add_new_rel_symbols(unsigned idx, ptr_vector<rule_stratifier::item_set> const & decls, void mk_synchronize::add_new_rel_symbols(unsigned idx,
ptr_vector<func_decl> & decls_buf, bool & was_added) { item_set_vector const & decls,
ptr_vector<func_decl> & decls_buf,
bool & was_added) {
if (idx >= decls.size()) { if (idx >= decls.size()) {
string_buffer<> buffer; string_buffer<> buffer;
ptr_vector<sort> domain; ptr_vector<sort> domain;
ptr_vector<func_decl>::const_iterator it = decls_buf.begin(), end = decls_buf.end(); for (auto &d : decls_buf) {
for (; it != end; ++it) { buffer << d->get_name() << "!!";
buffer << (*it)->get_name(); domain.append(d->get_arity(), d->get_domain());
buffer << "!!";
domain.append((*it)->get_arity(), (*it)->get_domain());
} }
symbol new_name = symbol(buffer.c_str()); symbol new_name = symbol(buffer.c_str());
@ -84,6 +83,7 @@ namespace datalog {
if (!cache.contains(new_name)) { if (!cache.contains(new_name)) {
was_added = true; was_added = true;
func_decl* orig = decls_buf[0]; func_decl* orig = decls_buf[0];
// AG : is this ref counted
func_decl* product_pred = m_ctx.mk_fresh_head_predicate(new_name, func_decl* product_pred = m_ctx.mk_fresh_head_predicate(new_name,
symbol::null, domain.size(), domain.c_ptr(), orig); symbol::null, domain.size(), domain.c_ptr(), orig);
cache.insert(new_name, product_pred); cache.insert(new_name, product_pred);
@ -91,15 +91,16 @@ namespace datalog {
return; return;
} }
rule_stratifier::item_set const & pred_decls = *decls[idx]; // AG: why recursive?
for (rule_stratifier::item_set::iterator it = pred_decls.begin(); it != pred_decls.end(); ++it) { for (auto &p : *decls[idx]) {
decls_buf[idx] = *it; decls_buf[idx] = p;
add_new_rel_symbols(idx + 1, decls, decls_buf, was_added); add_new_rel_symbols(idx + 1, decls, decls_buf, was_added);
} }
} }
void mk_synchronize::replace_applications(rule & r, rule_set & rules, ptr_vector<app> & apps) { void mk_synchronize::replace_applications(rule & r, rule_set & rules,
app* replacing = product_application(apps); ptr_vector<app> & apps) {
app_ref replacing = product_application(apps);
ptr_vector<app> new_tail; ptr_vector<app> new_tail;
svector<bool> new_tail_neg; svector<bool> new_tail_neg;
@ -135,7 +136,10 @@ namespace datalog {
rules.replace_rule(&r, new_rule.get()); rules.replace_rule(&r, new_rule.get());
} }
rule_ref mk_synchronize::rename_bound_vars_in_rule(rule * r, unsigned & var_idx) { rule_ref mk_synchronize::rename_bound_vars_in_rule(rule * r,
unsigned & var_idx) {
// AG: shift all variables in a rule so that lowest var index is var_idx?
// AG: update var_idx in the process?
ptr_vector<sort> sorts; ptr_vector<sort> sorts;
r->get_vars(m, sorts); r->get_vars(m, sorts);
expr_ref_vector revsub(m); expr_ref_vector revsub(m);
@ -152,17 +156,18 @@ namespace datalog {
return new_rule; return new_rule;
} }
vector<rule_ref_vector> mk_synchronize::rename_bound_vars(ptr_vector<rule_stratifier::item_set> const & heads, vector<rule_ref_vector> mk_synchronize::rename_bound_vars(item_set_vector const & heads,
rule_set & rules) { rule_set & rules) {
// AG: is every item_set in heads corresponds to rules that are merged?
// AG: why are bound variables renamed in the first place?
// AG: the data structure seems too complex
vector<rule_ref_vector> result; vector<rule_ref_vector> result;
unsigned var_idx = 0; unsigned var_idx = 0;
for (unsigned i = 0; i < heads.size(); ++i) { for (auto item : heads) {
rule_ref_vector dst_vector(rm); rule_ref_vector dst_vector(rm);
for (rule_stratifier::item_set::iterator it = heads[i]->begin(); it != heads[i]->end(); ++it) { for (auto *head : *item) {
func_decl * head = *it; for (auto *r : rules.get_predicate_rules(head)) {
rule_vector const & src_rules = rules.get_predicate_rules(head); rule_ref new_rule = rename_bound_vars_in_rule(r, var_idx);
for (unsigned j = 0; j < src_rules.size(); ++j) {
rule_ref new_rule = rename_bound_vars_in_rule(src_rules[j], var_idx);
dst_vector.push_back(new_rule.get()); dst_vector.push_back(new_rule.get());
} }
} }
@ -171,9 +176,11 @@ namespace datalog {
return result; return result;
} }
void mk_synchronize::add_rec_tail(vector< ptr_vector<app> > & recursive_calls, ptr_vector<app> & new_tail, void mk_synchronize::add_rec_tail(vector< ptr_vector<app> > & recursive_calls,
svector<bool> & new_tail_neg, unsigned & tail_idx) { app_ref_vector & new_tail,
int max_size = recursive_calls[0].size(); svector<bool> & new_tail_neg,
unsigned & tail_idx) {
int max_size = 0;
unsigned n = recursive_calls.size(); unsigned n = recursive_calls.size();
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
if (recursive_calls[i].size() > max_size) { if (recursive_calls[i].size() > max_size) {
@ -194,11 +201,12 @@ namespace datalog {
} }
} }
void mk_synchronize::add_non_rec_tail(rule & r, ptr_vector<app> & new_tail, svector<bool> & new_tail_neg, void mk_synchronize::add_non_rec_tail(rule & r, app_ref_vector & new_tail,
unsigned & tail_idx) { svector<bool> & new_tail_neg,
unsigned & tail_idx) {
for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) { for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) {
app* tail = r.get_tail(i); app* tail = r.get_tail(i);
if (!is_recursive_app(r, tail)) { if (!is_recursive(r, *tail)) {
++tail_idx; ++tail_idx;
new_tail[tail_idx] = tail; new_tail[tail_idx] = tail;
new_tail_neg[tail_idx] = false; new_tail_neg[tail_idx] = false;
@ -216,15 +224,14 @@ namespace datalog {
} }
} }
app* mk_synchronize::product_application(ptr_vector<app> const &apps) { app_ref mk_synchronize::product_application(ptr_vector<app> const &apps) {
ptr_vector<app>::const_iterator it = apps.begin(), end = apps.end();
unsigned args_num = 0; unsigned args_num = 0;
string_buffer<> buffer; string_buffer<> buffer;
for (; it != end; ++it) { // AG: factor out into mk_name
buffer << (*it)->get_decl()->get_name(); for (auto *app : apps) {
buffer << "!!"; buffer << app->get_decl()->get_name() << "!!";
args_num += (*it)->get_num_args(); args_num += app->get_num_args();
} }
symbol name = symbol(buffer.c_str()); symbol name = symbol(buffer.c_str());
@ -233,15 +240,13 @@ namespace datalog {
ptr_vector<expr> args; ptr_vector<expr> args;
args.resize(args_num); args.resize(args_num);
it = apps.begin(); unsigned idx = 0;
for (unsigned args_idx = 0; it != end; ++it) { for (auto *a : apps) {
app* a = *it; for (unsigned i = 0, sz = a->get_num_args(); i < sz; ++i, ++idx)
for (unsigned i = 0; i < a->get_num_args(); ++i, ++args_idx) { args[idx] = a->get_arg(i);
args[args_idx] = a->get_arg(i);
}
} }
return m.mk_app(pred, args_num, args.c_ptr()); return app_ref(m.mk_app(pred, args_num, args.c_ptr()), m);
} }
rule_ref mk_synchronize::product_rule(rule_ref_vector const & rules) { rule_ref mk_synchronize::product_rule(rule_ref_vector const & rules) {
@ -261,7 +266,7 @@ namespace datalog {
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
heads[i] = rules[i]->get_head(); heads[i] = rules[i]->get_head();
} }
app* product_head = product_application(heads); app_ref product_head = product_application(heads);
unsigned product_tail_length = 0; unsigned product_tail_length = 0;
bool has_recursion = false; bool has_recursion = false;
vector< ptr_vector<app> > recursive_calls; vector< ptr_vector<app> > recursive_calls;
@ -271,7 +276,7 @@ namespace datalog {
product_tail_length += rule.get_tail_size(); product_tail_length += rule.get_tail_size();
for (unsigned j = 0; j < rule.get_positive_tail_size(); ++j) { for (unsigned j = 0; j < rule.get_positive_tail_size(); ++j) {
app* tail = rule.get_tail(j); app* tail = rule.get_tail(j);
if (is_recursive_app(rule, tail)) { if (is_recursive(rule, *tail)) {
has_recursion = true; has_recursion = true;
recursive_calls[i].push_back(tail); recursive_calls[i].push_back(tail);
} }
@ -281,7 +286,7 @@ namespace datalog {
} }
} }
ptr_vector<app> new_tail; app_ref_vector new_tail(m);
svector<bool> new_tail_neg; svector<bool> new_tail_neg;
new_tail.resize(product_tail_length); new_tail.resize(product_tail_length);
new_tail_neg.resize(product_tail_length); new_tail_neg.resize(product_tail_length);
@ -302,41 +307,36 @@ namespace datalog {
return new_rule; return new_rule;
} }
void mk_synchronize::merge_rules(unsigned idx, rule_ref_vector & buf, vector<rule_ref_vector> const & merged_rules, void mk_synchronize::merge_rules(unsigned idx, rule_ref_vector & buf,
rule_set & all_rules) { vector<rule_ref_vector> const & merged_rules,
rule_set & all_rules) {
if (idx >= merged_rules.size()) { if (idx >= merged_rules.size()) {
rule_ref product = product_rule(buf); rule_ref product = product_rule(buf);
all_rules.add_rule(product.get()); all_rules.add_rule(product.get());
return; return;
} }
rule_ref_vector const & pred_rules = merged_rules[idx]; for (auto *r : merged_rules[idx]) {
for (rule_ref_vector::iterator it = pred_rules.begin(); it != pred_rules.end(); ++it) { buf[idx] = r;
buf[idx] = *it;
merge_rules(idx + 1, buf, merged_rules, all_rules); merge_rules(idx + 1, buf, merged_rules, all_rules);
} }
} }
void mk_synchronize::merge_applications(rule & r, rule_set & rules) { void mk_synchronize::merge_applications(rule & r, rule_set & rules) {
ptr_vector<app> non_recursive_applications; ptr_vector<app> non_recursive_preds;
obj_hashtable<app> apps; obj_hashtable<app> apps;
for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) { for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) {
app* application = r.get_tail(i); app* t = r.get_tail(i);
if (!is_recursive_app(r, application) && has_recursive_premise(application)) { if (!is_recursive(r, *t) && has_recursive_premise(t)) {
apps.insert(application); apps.insert(t);
} }
} }
if (apps.size() < 2) { if (apps.size() < 2) return;
return; for (auto *a : apps) non_recursive_preds.push_back(a);
}
for (obj_hashtable<app>::iterator it = apps.begin(); it != apps.end(); it++) { item_set_vector merged_decls = add_merged_decls(non_recursive_preds);
non_recursive_applications.push_back(*it);
}
ptr_vector<rule_stratifier::item_set> merged_decls = add_merged_decls(non_recursive_applications); unsigned n = non_recursive_preds.size();
unsigned n = non_recursive_applications.size();
ptr_vector<func_decl> decls_buf; ptr_vector<func_decl> decls_buf;
decls_buf.resize(n); decls_buf.resize(n);
bool was_added = false; bool was_added = false;
@ -348,7 +348,7 @@ namespace datalog {
merge_rules(0, rules_buf, renamed_rules, rules); merge_rules(0, rules_buf, renamed_rules, rules);
} }
replace_applications(r, rules, non_recursive_applications); replace_applications(r, rules, non_recursive_preds);
m_deps->populate(rules); m_deps->populate(rules);
m_stratifier = alloc(rule_stratifier, *m_deps); m_stratifier = alloc(rule_stratifier, *m_deps);
} }
@ -357,10 +357,7 @@ namespace datalog {
rule_set* rules = alloc(rule_set, m_ctx); rule_set* rules = alloc(rule_set, m_ctx);
rules->inherit_predicates(source); rules->inherit_predicates(source);
rule_set::iterator it = source.begin(), end = source.end(); for (auto *r : source) { rules->add_rule(r); }
for (; it != end; ++it) {
rules->add_rule(*it);
}
m_deps = alloc(rule_dependencies, m_ctx); m_deps = alloc(rule_dependencies, m_ctx);
m_deps->populate(*rules); m_deps->populate(*rules);
@ -372,6 +369,7 @@ namespace datalog {
merge_applications(*r, *rules); merge_applications(*r, *rules);
++current_rule; ++current_rule;
} }
return rules; return rules;
} }

30
src/muz/transforms/dl_mk_synchronize.h
View file

@ -52,6 +52,9 @@ namespace datalog {
\brief Implements a synchronous product transformation. \brief Implements a synchronous product transformation.
*/ */
class mk_synchronize : public rule_transformer::plugin { class mk_synchronize : public rule_transformer::plugin {
public:
typedef ptr_vector<rule_stratifier::item_set> item_set_vector;
private:
context& m_ctx; context& m_ctx;
ast_manager& m; ast_manager& m;
rule_manager& rm; rule_manager& rm;
@ -59,25 +62,30 @@ namespace datalog {
scoped_ptr<rule_dependencies> m_deps; scoped_ptr<rule_dependencies> m_deps;
scoped_ptr<rule_stratifier> m_stratifier; scoped_ptr<rule_stratifier> m_stratifier;
map<symbol, func_decl*, symbol_hash_proc, symbol_eq_proc> cache; map<symbol, func_decl*, symbol_hash_proc, symbol_eq_proc> cache;
bool is_recursive(rule &r, func_decl &decl) const;
bool is_recursive(rule &r, expr &e) const;
bool is_recursive_app(rule & r, app * app) const;
bool has_recursive_premise(app * app) const; bool has_recursive_premise(app * app) const;
ptr_vector<rule_stratifier::item_set> add_merged_decls(ptr_vector<app> & apps); item_set_vector add_merged_decls(ptr_vector<app> & apps);
void add_new_rel_symbols(unsigned idx, ptr_vector<rule_stratifier::item_set> const & decls, void add_new_rel_symbols(unsigned idx, item_set_vector const & decls,
ptr_vector<func_decl> & buf, bool & was_added); ptr_vector<func_decl> & buf, bool & was_added);
void replace_applications(rule & r, rule_set & rules, ptr_vector<app> & apps); void replace_applications(rule & r, rule_set & rules,
ptr_vector<app> & apps);
rule_ref rename_bound_vars_in_rule(rule * r, unsigned & var_idx); rule_ref rename_bound_vars_in_rule(rule * r, unsigned & var_idx);
vector<rule_ref_vector> rename_bound_vars(ptr_vector<rule_stratifier::item_set> const & heads, rule_set & rules); vector<rule_ref_vector> rename_bound_vars(item_set_vector const & heads,
rule_set & rules);
void add_rec_tail(vector< ptr_vector<app> > & recursive_calls, ptr_vector<app> & new_tail, void add_rec_tail(vector< ptr_vector<app> > & recursive_calls,
svector<bool> & new_tail_neg, unsigned & tail_idx); app_ref_vector & new_tail,
void add_non_rec_tail(rule & r, ptr_vector<app> & new_tail, svector<bool> & new_tail_neg, svector<bool> & new_tail_neg, unsigned & tail_idx);
unsigned & tail_idx); void add_non_rec_tail(rule & r, app_ref_vector & new_tail,
svector<bool> & new_tail_neg,
unsigned & tail_idx);
app* product_application(ptr_vector<app> const & apps); app_ref product_application(ptr_vector<app> const & apps);
rule_ref product_rule(rule_ref_vector const & rules); rule_ref product_rule(rule_ref_vector const & rules);
void merge_rules(unsigned idx, rule_ref_vector & buf, void merge_rules(unsigned idx, rule_ref_vector & buf,