diff --git a/src/muz/transforms/dl_mk_synchronize.cpp b/src/muz/transforms/dl_mk_synchronize.cpp index af2a6f8d3..348c9b5de 100644 --- a/src/muz/transforms/dl_mk_synchronize.cpp +++ b/src/muz/transforms/dl_mk_synchronize.cpp @@ -19,6 +19,7 @@ Revision History: --*/ #include "muz/transforms/dl_mk_synchronize.h" +#include namespace datalog { @@ -39,9 +40,6 @@ namespace datalog { unsigned num_of_stratum = m_stratifier->get_predicate_strat(hdecl); return strata[num_of_stratum]->contains(&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 { func_decl* app_decl = app->get_decl(); @@ -83,7 +81,6 @@ namespace datalog { if (!m_cache.contains(new_name)) { was_added = true; func_decl* orig = decls_buf[0]; - // AG : is this ref counted func_decl* product_pred = m_ctx.mk_fresh_head_predicate(new_name, symbol::null, domain.size(), domain.c_ptr(), orig); m_cache.insert(new_name, product_pred); @@ -91,7 +88,8 @@ namespace datalog { return; } - // AG: why recursive? + // -- compute Cartesian product of decls, and create a new + // -- predicate for each element of the product for (auto &p : *decls[idx]) { decls_buf[idx] = p; add_new_rel_symbols(idx + 1, decls, decls_buf, was_added); @@ -180,20 +178,20 @@ namespace datalog { app_ref_vector & new_tail, svector & new_tail_neg, unsigned & tail_idx) { - int max_size = 0; + unsigned max_sz = 0; + for (auto &rc : recursive_calls) + max_sz= std::max(rc.size(), max_sz); + unsigned n = recursive_calls.size(); - for (unsigned i = 0; i < n; ++i) { - if (recursive_calls[i].size() > max_size) { - max_size = recursive_calls[i].size(); - } - } - for (unsigned j = 0; j < max_size; ++j) { - ptr_vector merged_recursive_calls; + ptr_vector merged_recursive_calls; + + for (unsigned j = 0; j < max_sz; ++j) { + merged_recursive_calls.reset(); merged_recursive_calls.resize(n); for (unsigned i = 0; i < n; ++i) { - unsigned cur_size = recursive_calls[i].size(); - j < cur_size ? merged_recursive_calls[i] = recursive_calls[i][j]: - merged_recursive_calls[i] = recursive_calls[i][cur_size - 1]; + unsigned sz = recursive_calls[i].size(); + merged_recursive_calls[i] = + j < sz ? recursive_calls[i][j] : recursive_calls[i][sz - 1]; } ++tail_idx; new_tail[tail_idx] = product_application(merged_recursive_calls); @@ -204,7 +202,7 @@ namespace datalog { void mk_synchronize::add_non_rec_tail(rule & r, app_ref_vector & new_tail, svector & new_tail_neg, unsigned & tail_idx) { - for (unsigned i = 0; i < r.get_positive_tail_size(); ++i) { + for (unsigned i = 0, sz = r.get_positive_tail_size(); i < sz; ++i) { app* tail = r.get_tail(i); if (!is_recursive(r, *tail)) { ++tail_idx; @@ -212,12 +210,14 @@ namespace datalog { new_tail_neg[tail_idx] = false; } } - for (unsigned i = r.get_positive_tail_size(); i < r.get_uninterpreted_tail_size(); ++i) { + for (unsigned i = r.get_positive_tail_size(), + sz = r.get_uninterpreted_tail_size() ; i < sz; ++i) { ++tail_idx; new_tail[tail_idx] = r.get_tail(i); new_tail_neg[tail_idx] = true; } - for (unsigned i = r.get_uninterpreted_tail_size(); i < r.get_tail_size(); ++i) { + for (unsigned i = r.get_uninterpreted_tail_size(), + sz = r.get_tail_size(); i < sz; ++i) { ++tail_idx; new_tail[tail_idx] = r.get_tail(i); new_tail_neg[tail_idx] = r.is_neg_tail(i); @@ -254,7 +254,7 @@ namespace datalog { string_buffer<> buffer; bool first_rule = true; - for (rule_ref_vector::iterator it = rules.begin(); it != rules.end(); ++it, first_rule = false) { + for (auto it = rules.begin(); it != rules.end(); ++it, first_rule = false) { if (!first_rule) { buffer << "+"; } diff --git a/src/muz/transforms/dl_mk_synchronize.h b/src/muz/transforms/dl_mk_synchronize.h index 50d748bfa..6f4b3ca40 100644 --- a/src/muz/transforms/dl_mk_synchronize.h +++ b/src/muz/transforms/dl_mk_synchronize.h @@ -61,16 +61,45 @@ namespace datalog { scoped_ptr m_deps; scoped_ptr m_stratifier; - map m_cache; - bool is_recursive(rule &r, func_decl &decl) const; - bool is_recursive(rule &r, expr &e) const; + // symbol table that maps new predicate names to corresponding + // func_decl + map m_cache; + + /// returns true if decl is recursive in the given rule + /// requires that decl appears in the tail of r + bool is_recursive(rule &r, func_decl &decl) const; + bool is_recursive(rule &r, expr &e) const { + SASSERT(is_app(&e)); + return is_app(&e) && is_recursive(r, *to_app(&e)->get_decl()); + } + + /// returns true if the top-level predicate of app is recursive bool has_recursive_premise(app * app) const; item_set_vector add_merged_decls(ptr_vector & apps); + + /** + Compute Cartesian product of decls and create a new + predicate for each element. For example, if decls is + + ( (a, b), (c, d) ) ) + + create new predicates: a!!c, a!!d, b!!c, and b!!d + */ void add_new_rel_symbols(unsigned idx, item_set_vector const & decls, ptr_vector & buf, bool & was_added); + /** + Convert vector of predicate apps into a single app. For example, + (Foo a) (Bar b) becomes (Foo!!Bar a b) + */ + app_ref product_application(ptr_vector const & apps); + + /** + Replace a given rule by a rule in which conjunction of + predicates is replaced by a single product predicate + */ void replace_applications(rule & r, rule_set & rules, ptr_vector & apps); @@ -85,7 +114,6 @@ namespace datalog { svector & new_tail_neg, unsigned & tail_idx); - app_ref product_application(ptr_vector const & apps); rule_ref product_rule(rule_ref_vector const & rules); void merge_rules(unsigned idx, rule_ref_vector & buf,