mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 11:41:22 +00:00
Code Activity

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

Browse source 
This reverts commit 09da87dc85.
This commit is contained in:
Nikolaj Bjorner 2022-02-21 04:33:52 -08:00 • committed by GitHub
parent 456b8ee682
commit e8d4804dbb
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/muz/transforms/dl_mk_coi_filter.cpp
View file

@ -139,12 +139,24 @@ namespace datalog {
res = nullptr; res = nullptr;
} }
if (res && m_context.get_model_converter()) { 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) { for (func_decl* f : pruned_preds) {
const rule_vector& rules = source.get_predicate_rules(f); const rule_vector& rules = source.get_predicate_rules(f);
expr_ref_vector fmls(m);
for (rule * r : rules) { 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); m_context.add_model_converter(mc0);
} }