mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 12:58:44 +00:00
Code Activity

Replace rule API

Browse source
This commit is contained in:
Arie Gurfinkel 2018-07-12 22:38:29 +03:00
parent 0035d9b8cb
commit 3a01fd791b
2 changed files with 46 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

59
src/muz/base/dl_rule_set.cpp
View file

@ -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*>(), (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";
}
}
};

13
src/muz/base/dl_rule_set.h
View file

@ -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_ */