mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

Merge pull request #1091 from agurfinkel/dl

Browse source 
preserve rule names during dl transforms
This commit is contained in:
Nikolaj Bjorner 2017-06-20 21:31:21 -05:00 • committed by GitHub
commit a9990e3a0b
10 changed files with 21 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz/base/dl_rule.cpp
View file

@ -784,7 +784,7 @@ namespace datalog {
SASSERT(tail.size()==tail_neg.size());
rule_ref old_r = r;
r = mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
r = mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), old_r->name());
r->set_accounting_parent_object(m_ctx, old_r);
}
@ -1003,6 +1003,7 @@ namespace datalog {
void rule::display(context & ctx, std::ostream & out) const {
ast_manager & m = ctx.get_manager();
out << m_name.str () << ":\n";
//out << mk_pp(m_head, m);
output_predicate(ctx, m_head, out);
if (m_tail_size == 0) {

9
src/muz/base/dl_rule.h
View file

@ -298,7 +298,7 @@ namespace datalog {
static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); }
rule() : m_ref_cnt(0) {}
rule() : m_ref_cnt(0), m_name(symbol::null) {}
~rule() {}
void deallocate(ast_manager & m);
@ -355,7 +355,12 @@ namespace datalog {
void display(context & ctx, std::ostream & out) const;
symbol const& name() const { return m_name; }
/**
\brief Return the name(s) associated with this rule. Plural for preprocessed (e.g. obtained by inlining) rules.
This possibly returns a ";"-separated list of names.
*/
symbol const& name() const { return m_name; } ;
unsigned hash() const;

2
src/muz/transforms/dl_mk_filter_rules.cpp
View file

@ -140,7 +140,7 @@ namespace datalog {
if (rule_modified) {
remove_duplicate_tails(new_tail, new_is_negated);
SASSERT(new_tail.size() == new_is_negated.size());
rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr());
rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr(), r->name());
new_rule->set_accounting_parent_object(m_context, m_current);
m_result->add_rule(new_rule);
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule);

4
src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
View file

@ -84,7 +84,7 @@ namespace datalog {
mk_rule_inliner::remove_duplicate_tails(m_tail, m_neg);
SASSERT(m_tail.size() == m_neg.size());
res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr());
res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr(),m_rule->name());
res->set_accounting_parent_object(m_context, m_rule);
res->norm_vars(res.get_manager());
}
@ -557,7 +557,7 @@ namespace datalog {
}
SASSERT(m_tail.size() == m_tail_neg.size());
res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr());
res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr(), r->name());
res->set_accounting_parent_object(m_context, r);
}
else {

2
src/muz/transforms/dl_mk_magic_sets.cpp
View file

@ -280,7 +280,7 @@ namespace datalog {
new_tail.push_back(create_magic_literal(new_head));
negations.push_back(false);
rule * nr = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), negations.c_ptr());
rule * nr = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), negations.c_ptr(), r->name());
result.add_rule(nr);
nr->set_accounting_parent_object(m_context, r);
}

2
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
View file

@ -341,7 +341,7 @@ namespace datalog {
head = mk_head(source, *result, r.get_head(), cnt);
fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head);
proof_ref pr(m);
rm.mk_rule(fml, pr, *result);
rm.mk_rule(fml, pr, *result, r.name());
TRACE("dl", result->last()->display(m_ctx, tout););
}

2
src/muz/transforms/dl_mk_quantifier_instantiation.cpp
View file

@ -232,7 +232,7 @@ namespace datalog {
rule_set added_rules(m_ctx);
proof_ref pr(m);
rm.mk_rule(fml, pr, added_rules);
rm.mk_rule(fml, pr, added_rules, r.name());
if (r.get_proof()) {
// use def-axiom to encode that new rule is a weakening of the original.
proof* p1 = r.get_proof();

5
src/muz/transforms/dl_mk_rule_inliner.cpp
View file

@ -114,7 +114,10 @@ namespace datalog {
apply(src, false, UINT_MAX, tail, tail_neg);
mk_rule_inliner::remove_duplicate_tails(tail, tail_neg);
SASSERT(tail.size()==tail_neg.size());
res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), tgt.name(), m_normalize);
std::ostringstream comb_name;
comb_name << tgt.name().str() << ";" << src.name().str();
symbol combined_rule_name = symbol(comb_name.str().c_str());
res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), combined_rule_name, m_normalize);
res->set_accounting_parent_object(m_context, const_cast<rule*>(&tgt));
TRACE("dl",
tgt.display(m_context, tout << "tgt (" << tail_index << "): \n");

2
src/muz/transforms/dl_mk_slice.cpp
View file

@ -22,7 +22,7 @@ Revision History:
input: x, z
output: x, y
Let x_i, y_i, z_i be incides into the vectors x, y, z.
Let x_i, y_i, z_i be indices into the vectors x, y, z.
Suppose that positions in P and R are annotated with what is
slicable.

2
src/muz/transforms/dl_mk_subsumption_checker.cpp
View file

@ -159,7 +159,7 @@ namespace datalog {
}
SASSERT(tail.size()==tail_neg.size());
res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), r->name());
res->set_accounting_parent_object(m_context, r);
m_context.get_rule_manager().fix_unbound_vars(res, true);
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *res.get());