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

preserve dl rule names during xforms

Browse source
This commit is contained in:
Arie Gurfinkel 2017-06-20 22:04:35 -04:00
parent 50f794c4f5
commit af28057980
8 changed files with 13 additions and 9 deletions
Show stats 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()); SASSERT(tail.size()==tail_neg.size());
rule_ref old_r = r; 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); r->set_accounting_parent_object(m_ctx, old_r);
} }
@ -1003,6 +1003,7 @@ namespace datalog {
void rule::display(context & ctx, std::ostream & out) const { void rule::display(context & ctx, std::ostream & out) const {
ast_manager & m = ctx.get_manager(); ast_manager & m = ctx.get_manager();
out << m_name.str () << ":\n";
//out << mk_pp(m_head, m); //out << mk_pp(m_head, m);
output_predicate(ctx, m_head, out); output_predicate(ctx, m_head, out);
if (m_tail_size == 0) { if (m_tail_size == 0) {

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

@ -140,7 +140,7 @@ namespace datalog {
if (rule_modified) { if (rule_modified) {
remove_duplicate_tails(new_tail, new_is_negated); remove_duplicate_tails(new_tail, new_is_negated);
SASSERT(new_tail.size() == new_is_negated.size()); 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); new_rule->set_accounting_parent_object(m_context, m_current);
m_result->add_rule(new_rule); m_result->add_rule(new_rule);
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *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); mk_rule_inliner::remove_duplicate_tails(m_tail, m_neg);
SASSERT(m_tail.size() == m_neg.size()); 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->set_accounting_parent_object(m_context, m_rule);
res->norm_vars(res.get_manager()); res->norm_vars(res.get_manager());
} }
@ -557,7 +557,7 @@ namespace datalog {
} }
SASSERT(m_tail.size() == m_tail_neg.size()); 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); res->set_accounting_parent_object(m_context, r);
} }
else { 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)); new_tail.push_back(create_magic_literal(new_head));
negations.push_back(false); 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); result.add_rule(nr);
nr->set_accounting_parent_object(m_context, r); 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); head = mk_head(source, *result, r.get_head(), cnt);
fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head); fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head);
proof_ref pr(m); 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);); 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); rule_set added_rules(m_ctx);
proof_ref pr(m); proof_ref pr(m);
rm.mk_rule(fml, pr, added_rules); rm.mk_rule(fml, pr, added_rules, r.name());
if (r.get_proof()) { if (r.get_proof()) {
// use def-axiom to encode that new rule is a weakening of the original. // use def-axiom to encode that new rule is a weakening of the original.
proof* p1 = r.get_proof(); 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); apply(src, false, UINT_MAX, tail, tail_neg);
mk_rule_inliner::remove_duplicate_tails(tail, tail_neg); mk_rule_inliner::remove_duplicate_tails(tail, tail_neg);
SASSERT(tail.size()==tail_neg.size()); 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)); res->set_accounting_parent_object(m_context, const_cast<rule*>(&tgt));
TRACE("dl", TRACE("dl",
tgt.display(m_context, tout << "tgt (" << tail_index << "): \n"); tgt.display(m_context, tout << "tgt (" << tail_index << "): \n");

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

@ -159,7 +159,7 @@ namespace datalog {
} }
SASSERT(tail.size()==tail_neg.size()); 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); res->set_accounting_parent_object(m_context, r);
m_context.get_rule_manager().fix_unbound_vars(res, true); m_context.get_rule_manager().fix_unbound_vars(res, true);
m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *res.get()); m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *res.get());