From 3a01fd791b0b06ccf2439eaab8bce828dbbd7dbc Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 12 Jul 2018 22:38:29 +0300 Subject: [PATCH] Replace rule API --- src/muz/base/dl_rule_set.cpp | 59 +++++++++++++++++++++++------------- src/muz/base/dl_rule_set.h | 13 +++++--- 2 files changed, 46 insertions(+), 26 deletions(-) diff --git a/src/muz/base/dl_rule_set.cpp b/src/muz/base/dl_rule_set.cpp index 5114fdca4..80af80266 100644 --- a/src/muz/base/dl_rule_set.cpp +++ b/src/muz/base/dl_rule_set.cpp @@ -31,7 +31,7 @@ namespace datalog { rule_dependencies::rule_dependencies(const rule_dependencies & o, bool reversed): m_context(o.m_context) { if (reversed) { - for (auto & kv : o) { + for (auto & kv : o) { func_decl * pred = kv.m_key; item_set & orig_items = *kv.get_value(); @@ -114,8 +114,8 @@ namespace datalog { app* a = to_app(e); d = a->get_decl(); if (m_context.is_predicate(d)) { - // insert d and ensure the invariant - // that every predicate is present as + // insert d and ensure the invariant + // that every predicate is present as // a key in m_data s.insert(d); ensure_key(d); @@ -148,7 +148,7 @@ namespace datalog { item_set& itms = *kv.get_value(); set_intersection(itms, allowed); } - for (func_decl* f : to_remove) + for (func_decl* f : to_remove) remove_m_data_entry(f); } @@ -253,18 +253,18 @@ namespace datalog { // // ----------------------------------- - rule_set::rule_set(context & ctx) - : m_context(ctx), - m_rule_manager(ctx.get_rule_manager()), - m_rules(m_rule_manager), + rule_set::rule_set(context & ctx) + : m_context(ctx), + m_rule_manager(ctx.get_rule_manager()), + m_rules(m_rule_manager), m_deps(ctx), m_stratifier(nullptr), m_refs(ctx.get_manager()) { } - rule_set::rule_set(const rule_set & other) - : m_context(other.m_context), - m_rule_manager(other.m_rule_manager), + rule_set::rule_set(const rule_set & other) + : m_context(other.m_context), + m_rule_manager(other.m_rule_manager), m_rules(m_rule_manager), m_deps(other.m_context), m_stratifier(nullptr), @@ -353,10 +353,27 @@ namespace datalog { break; \ } \ } \ - + DEL_VECTOR(*rules); DEL_VECTOR(m_rules); - } + } + + void rule_set::replace_rule(rule * r, rule * other) { + TRACE("dl", r->display(m_context, tout << "replace:");); + func_decl* d = r->get_decl(); + rule_vector* rules = m_head2rules.find(d); +#define REPLACE_VECTOR(_v) \ + for (unsigned i = (_v).size(); i > 0; ) { \ + --i; \ + if ((_v)[i] == r) { \ + (_v)[i] = other; \ + break; \ + } \ + } \ + + REPLACE_VECTOR(*rules); + REPLACE_VECTOR(m_rules); + } void rule_set::ensure_closed() { if (!is_closed()) { @@ -365,7 +382,7 @@ namespace datalog { } bool rule_set::close() { - SASSERT(!is_closed()); //the rule_set is not already closed + SASSERT(!is_closed()); //the rule_set is not already closed m_deps.populate(*this); m_stratifier = alloc(rule_stratifier, m_deps); if (!stratified_negation()) { @@ -426,7 +443,7 @@ namespace datalog { inherit_predicates(src); } - const rule_vector & rule_set::get_predicate_rules(func_decl * pred) const { + const rule_vector & rule_set::get_predicate_rules(func_decl * pred) const { decl2rules::obj_map_entry * e = m_head2rules.find_core(pred); if (!e) { return m_empty_rule_vector; @@ -519,7 +536,7 @@ namespace datalog { out << "\n"; non_empty = false; } - + for (func_decl * first : *strat) { const func_decl_set & deps = m_deps.get_deps(first); for (func_decl * dep : deps) { @@ -545,8 +562,8 @@ namespace datalog { unsigned rule_stratifier::get_predicate_strat(func_decl * pred) const { unsigned num; if (!m_pred_strat_nums.find(pred, num)) { - //the number of the predicate is not stored, therefore it did not appear - //in the algorithm and therefore it does not depend on anything and nothing + //the number of the predicate is not stored, therefore it did not appear + //in the algorithm and therefore it does not depend on anything and nothing //depends on it. So it is safe to assign zero strate to it, although it is //not strictly true. num = 0; @@ -641,7 +658,7 @@ namespace datalog { } - // We put components whose indegree is zero to m_strats and assign its + // We put components whose indegree is zero to m_strats and assign its // m_components entry to zero. unsigned comp_cnt = m_components.size(); for (unsigned i = 0; i < comp_cnt; i++) { @@ -680,7 +697,7 @@ namespace datalog { strats_index++; } //we have managed to topologicaly order all the components - SASSERT(std::find_if(m_components.begin(), m_components.end(), + SASSERT(std::find_if(m_components.begin(), m_components.end(), std::bind1st(std::not_equal_to(), (item_set*)0)) == m_components.end()); //reverse the strats array, so that the only the later components would depend on earlier ones @@ -713,7 +730,7 @@ namespace datalog { } out << "\n"; } - + } }; diff --git a/src/muz/base/dl_rule_set.h b/src/muz/base/dl_rule_set.h index 736dd8888..e870e369c 100644 --- a/src/muz/base/dl_rule_set.h +++ b/src/muz/base/dl_rule_set.h @@ -77,7 +77,7 @@ namespace datalog { \brief Number of predicates that depend on \c f. */ unsigned out_degree(func_decl * f) const; - + /** \brief If the rependency graph is acyclic, put all elements into \c res ordered so that elements can depend only on elements that are before them. @@ -131,7 +131,7 @@ namespace datalog { it must exist for the whole lifetime of the \c stratifier object. */ rule_stratifier(const rule_dependencies & deps) - : m_deps(deps), m_next_preorder(0) + : m_deps(deps), m_next_preorder(0) { process(); } @@ -145,7 +145,7 @@ namespace datalog { const comp_vector & get_strats() const { return m_strats; } unsigned get_predicate_strat(func_decl * pred) const; - + void display( std::ostream & out ) const; }; @@ -203,6 +203,10 @@ namespace datalog { \brief Remove rule \c r from the rule set. */ void del_rule(rule * r); + /** + \brief Replace a rule \c r with the rule \c other + */ + void replace_rule(rule * r, rule * other); /** \brief Add all rules from a different rule_set. @@ -276,8 +280,7 @@ namespace datalog { inline std::ostream& operator<<(std::ostream& out, rule_set const& r) { r.display(out); return out; } - + }; #endif /* DL_RULE_SET_H_ */ -