From 09da87dc85560312fe5c6dbfa4929e82a420f8e8 Mon Sep 17 00:00:00 2001 From: Valentine Sobol Date: Thu, 17 Feb 2022 00:35:58 +0300 Subject: [PATCH] use horn_subsume_model_converter in coi filter (#5844) --- src/muz/transforms/dl_mk_coi_filter.cpp | 16 ++-------------- 1 file changed, 2 insertions(+), 14 deletions(-) diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 841ab4637..d3f6555aa 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -139,24 +139,12 @@ namespace datalog { res = nullptr; } if (res && m_context.get_model_converter()) { - generic_model_converter* mc0 = alloc(generic_model_converter, m, "dl_coi"); + horn_subsume_model_converter* mc0 = alloc(horn_subsume_model_converter, 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)); + datalog::del_rule(mc0, *r, false); } - expr_ref fml(m); - fml = m.mk_or(fmls.size(), fmls.data()); - mc0->add(f, fml); } m_context.add_model_converter(mc0); }