From e8d4804dbb726b8b13cc996cc33bd57d6acc893a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 21 Feb 2022 04:33:52 -0800 Subject: [PATCH] Revert "use horn_subsume_model_converter in coi filter (#5844)" (#5859) This reverts commit 09da87dc85560312fe5c6dbfa4929e82a420f8e8. --- src/muz/transforms/dl_mk_coi_filter.cpp | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index d3f6555aa..841ab4637 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -139,12 +139,24 @@ namespace datalog { res = nullptr; } if (res && m_context.get_model_converter()) { - horn_subsume_model_converter* mc0 = alloc(horn_subsume_model_converter, m); + generic_model_converter* mc0 = alloc(generic_model_converter, m, "dl_coi"); for (func_decl* f : pruned_preds) { const rule_vector& rules = source.get_predicate_rules(f); + expr_ref_vector fmls(m); for (rule * r : rules) { - datalog::del_rule(mc0, *r, false); + 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)); } + expr_ref fml(m); + fml = m.mk_or(fmls.size(), fmls.data()); + mc0->add(f, fml); } m_context.add_model_converter(mc0); }