mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
COI model converter has to use constraints from the body and work in disjunctive mode. It needs a pre-condition that the body does not depend on other rules, in the case that it is used in a different pre-processing step for in-lining. The in-lined occurrence of the predicate has to correspond to the model construction version.
This commit is contained in:
parent
e8d4804dbb
commit
061e94d723
|
@ -118,7 +118,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
rule_set * mk_coi_filter::top_down(rule_set const & source) {
|
||||
func_decl_set pruned_preds;
|
||||
func_decl_set pruned_preds, seen;
|
||||
dataflow_engine<reachability_info> engine(source.get_manager(), source);
|
||||
engine.run_top_down();
|
||||
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
|
||||
|
@ -126,37 +126,50 @@ namespace datalog {
|
|||
|
||||
for (rule * r : source) {
|
||||
func_decl * pred = r->get_decl();
|
||||
if (engine.get_fact(pred).is_reachable()) {
|
||||
res->add_rule(r);
|
||||
}
|
||||
bool should_keep = false;
|
||||
if (seen.contains(pred))
|
||||
continue;
|
||||
seen.insert(pred);
|
||||
if (engine.get_fact(pred).is_reachable())
|
||||
should_keep = true;
|
||||
else if (m_context.get_model_converter()) {
|
||||
pruned_preds.insert(pred);
|
||||
bool should_keep = false;
|
||||
for (rule* pr : source.get_predicate_rules(pred))
|
||||
for (unsigned i = 0; i < pr->get_uninterpreted_tail_size(); ++i)
|
||||
should_keep |= pr->get_tail(i)->get_decl() != pred;
|
||||
}
|
||||
else
|
||||
continue;
|
||||
|
||||
if (should_keep)
|
||||
for (rule* pr : source.get_predicate_rules(pred))
|
||||
res->add_rule(pr);
|
||||
else
|
||||
pruned_preds.insert(pred);
|
||||
}
|
||||
|
||||
if (res->get_num_rules() == source.get_num_rules()) {
|
||||
TRACE("dl", tout << "No transformation\n";);
|
||||
res = nullptr;
|
||||
}
|
||||
if (res && m_context.get_model_converter()) {
|
||||
generic_model_converter* mc0 = alloc(generic_model_converter, m, "dl_coi");
|
||||
for (func_decl* f : pruned_preds) {
|
||||
if (res && m_context.get_model_converter() && !pruned_preds.empty()) {
|
||||
auto* mc0 = alloc(generic_model_converter, m, "dl_coi");
|
||||
horn_subsume_model_converter hmc(m);
|
||||
|
||||
for (func_decl* f : pruned_preds) {
|
||||
const rule_vector& rules = source.get_predicate_rules(f);
|
||||
expr_ref_vector fmls(m);
|
||||
for (rule * r : rules) {
|
||||
app* head = r->get_head();
|
||||
expr_ref_vector conj(m);
|
||||
for (unsigned j = 0; j < head->get_num_args(); ++j) {
|
||||
expr* arg = head->get_arg(j);
|
||||
if (!is_var(arg)) {
|
||||
conj.push_back(m.mk_eq(m.mk_var(j, arg->get_sort()), arg));
|
||||
}
|
||||
}
|
||||
fmls.push_back(mk_and(conj));
|
||||
for (rule* r : rules) {
|
||||
expr_ref_vector constraints(m);
|
||||
expr_ref body_res(m);
|
||||
func_decl_ref pred(m);
|
||||
for (unsigned i = r->get_uninterpreted_tail_size(); i < r->get_tail_size(); ++i)
|
||||
constraints.push_back(r->get_tail(i));
|
||||
expr_ref body = mk_and(constraints);
|
||||
VERIFY(hmc.mk_horn(r->get_head(), body, pred, body_res));
|
||||
fmls.push_back(body_res);
|
||||
}
|
||||
expr_ref fml(m);
|
||||
fml = m.mk_or(fmls.size(), fmls.data());
|
||||
mc0->add(f, fml);
|
||||
mc0->add(f, mk_or(fmls));
|
||||
}
|
||||
m_context.add_model_converter(mc0);
|
||||
}
|
||||
|
|
|
@ -80,8 +80,8 @@ bool horn_subsume_model_converter::mk_horn(
|
|||
if (w >= subst.size()) {
|
||||
subst.resize(w+1);
|
||||
}
|
||||
if (subst[w].get()) {
|
||||
conjs.push_back(m.mk_eq(v, subst[w].get()));
|
||||
if (subst.get(w)) {
|
||||
conjs.push_back(m.mk_eq(v, subst.get(w)));
|
||||
}
|
||||
else {
|
||||
subst[w] = v;
|
||||
|
@ -92,11 +92,11 @@ bool horn_subsume_model_converter::mk_horn(
|
|||
}
|
||||
}
|
||||
expr_ref body_expr(m);
|
||||
body_expr = m.mk_and(conjs.size(), conjs.data());
|
||||
body_expr = m.mk_and(conjs);
|
||||
|
||||
// substitute variables directly.
|
||||
if (!subst.empty()) {
|
||||
body_expr = vs(body_expr, subst.size(), subst.data());
|
||||
body_expr = vs(body_expr, subst);
|
||||
}
|
||||
|
||||
if (fv.empty()) {
|
||||
|
@ -174,17 +174,16 @@ void horn_subsume_model_converter::operator()(model_ref& mr) {
|
|||
func_decl_ref pred(m);
|
||||
expr_ref body_res(m);
|
||||
for (unsigned i = 0; i < m_delay_head.size(); ++i) {
|
||||
VERIFY(mk_horn(m_delay_head[i].get(), m_delay_body[i].get(), pred, body_res));
|
||||
VERIFY(mk_horn(m_delay_head.get(i), m_delay_body.get(i), pred, body_res));
|
||||
insert(pred.get(), body_res.get());
|
||||
}
|
||||
m_delay_head.reset();
|
||||
m_delay_body.reset();
|
||||
|
||||
TRACE("mc", tout << m_funcs.size() << "\n"; model_smt2_pp(tout, m, *mr, 0););
|
||||
for (unsigned i = m_funcs.size(); i > 0; ) {
|
||||
--i;
|
||||
func_decl* h = m_funcs[i].get();
|
||||
expr_ref body(m_bodies[i].get(), m);
|
||||
for (unsigned i = m_funcs.size(); i-- > 0; ) {
|
||||
func_decl* h = m_funcs.get(i);
|
||||
expr_ref body(m_bodies.get(i), m);
|
||||
unsigned arity = h->get_arity();
|
||||
add_default_false_interpretation(body, mr);
|
||||
SASSERT(m.is_bool(body));
|
||||
|
|
Loading…
Reference in a new issue