Revert "use horn_subsume_model_converter in coi filter (#5844)" (#5859)

This reverts commit 09da87d.
Z3Prover · Feb 21, 2022 · e8d4804 · e8d4804
1 parent 456b8ee
commit e8d4804
Showing 1 changed file with 14 additions and 2 deletions.
diff --git 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);
         }