mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 18:06:15 +00:00
Code Activity

refining model update rules for del_rule #5865 #5866

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-02-25 08:03:46 -08:00
parent 30a2f2fd9d
commit 7f149a36d7
3 changed files with 19 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/muz/base/dl_util.cpp
View file

@ -281,14 +281,19 @@ namespace datalog {
return get_max_var(has_var); return get_max_var(has_var);
} }
void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable) { void del_rule(horn_subsume_model_converter* mc, rule& r, lbool unreachable) {
if (mc) { if (mc) {
ast_manager& m = mc->get_manager(); ast_manager& m = mc->get_manager();
expr_ref_vector body(m); expr_ref_vector body(m);
if (unreachable) { TRACE("dl", tout << "unreachable: " << unreachable << " " << r.get_decl()->get_name() << "\n");
switch (unreachable) {
case l_true:
body.push_back(m.mk_true()); body.push_back(m.mk_true());
} break;
else { case l_false:
body.push_back(m.mk_false());
break;
default:
for (unsigned i = 0; i < r.get_tail_size(); ++i) { for (unsigned i = 0; i < r.get_tail_size(); ++i) {
if (r.is_neg_tail(i)) { if (r.is_neg_tail(i)) {
body.push_back(m.mk_not(r.get_tail(i))); body.push_back(m.mk_not(r.get_tail(i)));
@ -297,11 +302,12 @@ namespace datalog {
body.push_back(r.get_tail(i)); body.push_back(r.get_tail(i));
} }
} }
break;
} }
TRACE("dl_dr", TRACE("dl",
tout << mk_pp(r.get_head(), m) << " :- \n"; tout << mk_pp(r.get_head(), m) << " :- \n";
for (unsigned i = 0; i < body.size(); ++i) { for (unsigned i = 0; i < body.size(); ++i) {
tout << mk_pp(body[i].get(), m) << "\n"; tout << mk_pp(body.get(i), m) << "\n";
}); });
mc->insert(r.get_head(), body.size(), body.data()); mc->insert(r.get_head(), body.size(), body.data());

2
src/muz/base/dl_util.h
View file

@ -353,7 +353,7 @@ namespace datalog {
unsigned get_max_rule_var(const rule& r); unsigned get_max_rule_var(const rule& r);
}; };
void del_rule(horn_subsume_model_converter* mc, rule& r, bool unreachable); void del_rule(horn_subsume_model_converter* mc, rule& r, lbool unreachable);
void resolve_rule(rule_manager& rm, void resolve_rule(rule_manager& rm,
replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx,

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

@ -410,7 +410,7 @@ namespace datalog {
TRACE("dl", tout << "inlined rules after mutual inlining:\n" << m_inlined_rules; ); TRACE("dl", tout << "inlined rules after mutual inlining:\n" << m_inlined_rules; );
for (rule * r : m_inlined_rules) { for (rule * r : m_inlined_rules) {
datalog::del_rule(m_mc, *r, false); datalog::del_rule(m_mc, *r, l_undef);
} }
} }
@ -449,7 +449,7 @@ namespace datalog {
} }
} }
if (modified) { if (modified) {
datalog::del_rule(m_mc, *r0, true); datalog::del_rule(m_mc, *r0, l_false);
} }
return modified; return modified;
@ -473,7 +473,7 @@ namespace datalog {
if (something_done && m_mc) { if (something_done && m_mc) {
for (rule* r : orig) { for (rule* r : orig) {
if (inlining_allowed(orig, r->get_decl())) { if (inlining_allowed(orig, r->get_decl())) {
datalog::del_rule(m_mc, *r, true); datalog::del_rule(m_mc, *r, l_undef);
} }
} }
} }
@ -558,7 +558,7 @@ namespace datalog {
// nothing unifies with the tail atom, therefore the rule is unsatisfiable // 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) // (we can say this because relation pred doesn't have any ground facts either)
res = nullptr; res = nullptr;
datalog::del_rule(m_mc, *r, false); datalog::del_rule(m_mc, *r, l_false);
return true; return true;
} }
if (!is_oriented_rewriter(inlining_candidate, strat)) { if (!is_oriented_rewriter(inlining_candidate, strat)) {
@ -568,7 +568,7 @@ namespace datalog {
goto process_next_tail; goto process_next_tail;
} }
if (!try_to_inline_rule(*r, *inlining_candidate, ti, res)) { if (!try_to_inline_rule(*r, *inlining_candidate, ti, res)) {
datalog::del_rule(m_mc, *r, false); datalog::del_rule(m_mc, *r, l_false);
res = nullptr; res = nullptr;
} }
return true; return true;
@ -801,7 +801,7 @@ namespace datalog {
if (num_tail_unifiers == 1) { if (num_tail_unifiers == 1) {
TRACE("dl", tout << "setting invalid: " << j << "\n";); TRACE("dl", tout << "setting invalid: " << j << "\n";);
valid.set(j, false); valid.set(j, false);
datalog::del_rule(m_mc, *r2, true); datalog::del_rule(m_mc, *r2, l_true);
del_rule(r2, j); del_rule(r2, j);
} }