diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index ffb964f47..27d62538e 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -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) { diff --git a/src/muz/transforms/dl_mk_filter_rules.cpp b/src/muz/transforms/dl_mk_filter_rules.cpp index b112f4c99..0d118a589 100644 --- a/src/muz/transforms/dl_mk_filter_rules.cpp +++ b/src/muz/transforms/dl_mk_filter_rules.cpp @@ -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); diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 455b06d3d..3c1d1b924 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -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 { diff --git a/src/muz/transforms/dl_mk_magic_sets.cpp b/src/muz/transforms/dl_mk_magic_sets.cpp index 048decaf9..19dccf417 100644 --- a/src/muz/transforms/dl_mk_magic_sets.cpp +++ b/src/muz/transforms/dl_mk_magic_sets.cpp @@ -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); } diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index caff79d2e..5c0d442df 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -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);); } diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index 5d36d26cc..586c52cd6 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -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(); diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 7dabece2f..c6b3e8be7 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -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(&tgt)); TRACE("dl", tgt.display(m_context, tout << "tgt (" << tail_index << "): \n"); diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index 1967fdc93..8fae4ee35 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -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());