mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
include information whether rule is reachable in del_rule model converter for simpler model presentation #1241
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2cab1cccc9
commit
2c97eb1393
|
@ -277,16 +277,21 @@ namespace datalog {
|
|||
return get_max_var(has_var);
|
||||
}
|
||||
|
||||
void del_rule(horn_subsume_model_converter* mc, rule& r) {
|
||||
void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable) {
|
||||
if (mc) {
|
||||
ast_manager& m = mc->get_manager();
|
||||
expr_ref_vector body(m);
|
||||
for (unsigned i = 0; i < r.get_tail_size(); ++i) {
|
||||
if (r.is_neg_tail(i)) {
|
||||
body.push_back(m.mk_not(r.get_tail(i)));
|
||||
}
|
||||
else {
|
||||
body.push_back(r.get_tail(i));
|
||||
if (unreachable) {
|
||||
body.push_back(m.mk_false());
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < r.get_tail_size(); ++i) {
|
||||
if (r.is_neg_tail(i)) {
|
||||
body.push_back(m.mk_not(r.get_tail(i)));
|
||||
}
|
||||
else {
|
||||
body.push_back(r.get_tail(i));
|
||||
}
|
||||
}
|
||||
}
|
||||
TRACE("dl_dr",
|
||||
|
|
|
@ -354,7 +354,7 @@ namespace datalog {
|
|||
unsigned get_max_rule_var(const rule& r);
|
||||
};
|
||||
|
||||
void del_rule(horn_subsume_model_converter* mc, rule& r);
|
||||
void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable);
|
||||
|
||||
void resolve_rule(rule_manager& rm,
|
||||
replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx,
|
||||
|
|
|
@ -426,7 +426,7 @@ namespace datalog {
|
|||
|
||||
for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) {
|
||||
rule* r = m_inlined_rules.get_rule(i);
|
||||
datalog::del_rule(m_mc, *r);
|
||||
datalog::del_rule(m_mc, *r, true);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -465,7 +465,7 @@ namespace datalog {
|
|||
}
|
||||
}
|
||||
if (modified) {
|
||||
datalog::del_rule(m_mc, *r0);
|
||||
datalog::del_rule(m_mc, *r0, true);
|
||||
}
|
||||
|
||||
return modified;
|
||||
|
@ -488,9 +488,9 @@ namespace datalog {
|
|||
}
|
||||
|
||||
if (something_done && m_mc) {
|
||||
for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {
|
||||
if (inlining_allowed(orig, (*rit)->get_decl())) {
|
||||
datalog::del_rule(m_mc, **rit);
|
||||
for (rule* r : orig) {
|
||||
if (inlining_allowed(orig, r->get_decl())) {
|
||||
datalog::del_rule(m_mc, *r, true);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -580,7 +580,7 @@ namespace datalog {
|
|||
// nothing unifies with the tail atom, therefore the rule is unsatisfiable
|
||||
// (we can say this because relation pred doesn't have any ground facts either)
|
||||
res = 0;
|
||||
datalog::del_rule(m_mc, *r);
|
||||
datalog::del_rule(m_mc, *r, false);
|
||||
return true;
|
||||
}
|
||||
if (!is_oriented_rewriter(inlining_candidate, strat)) {
|
||||
|
@ -590,7 +590,7 @@ namespace datalog {
|
|||
goto process_next_tail;
|
||||
}
|
||||
if (!try_to_inline_rule(*r, *inlining_candidate, ti, res)) {
|
||||
datalog::del_rule(m_mc, *r);
|
||||
datalog::del_rule(m_mc, *r, false);
|
||||
res = 0;
|
||||
}
|
||||
return true;
|
||||
|
@ -823,7 +823,7 @@ namespace datalog {
|
|||
if (num_tail_unifiers == 1) {
|
||||
TRACE("dl", tout << "setting invalid: " << j << "\n";);
|
||||
valid.set(j, false);
|
||||
datalog::del_rule(m_mc, *r2);
|
||||
datalog::del_rule(m_mc, *r2, true);
|
||||
del_rule(r2, j);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue