From 061e94d723422b240e23743c8ef3f99739f1ac23 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Feb 2022 17:45:00 -0800 Subject: [PATCH] #5858 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. --- src/muz/transforms/dl_mk_coi_filter.cpp | 55 +++++++++++++-------- src/tactic/horn_subsume_model_converter.cpp | 17 +++---- 2 files changed, 42 insertions(+), 30 deletions(-) diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 841ab4637..389f0abab 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -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 engine(source.get_manager(), source); engine.run_top_down(); scoped_ptr 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); } diff --git a/src/tactic/horn_subsume_model_converter.cpp b/src/tactic/horn_subsume_model_converter.cpp index 79b9a038f..979359a46 100644 --- a/src/tactic/horn_subsume_model_converter.cpp +++ b/src/tactic/horn_subsume_model_converter.cpp @@ -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));