mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix #6793, disable unbound_compressor when used in context of a moel converter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-13 14:03:40 -07:00
parent 08599177d0
commit d1482287d4
2 changed files with 15 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -102,14 +102,11 @@ namespace datalog {
// set to false each unreached predicate
if (res && m_context.get_model_converter()) {
generic_model_converter* mc0 = alloc(generic_model_converter, m, "dl_coi");
for (auto const& kv : engine) {
if (!kv.m_value.is_reachable()) {
for (auto const& kv : engine)
if (!kv.m_value.is_reachable())
unreachable.insert(kv.m_key);
}
}
for (func_decl* f : unreachable) {
for (func_decl* f : unreachable)
mc0->add(f, m.mk_false());
}
m_context.add_model_converter(mc0);
TRACE("dl", m_context.get_model_converter()->display(tout););
}

25
src/muz/transforms/dl_mk_unbound_compressor.cpp
View file

@ -294,13 +294,11 @@ namespace datalog {
replace_original_rule = true;
replace_by_decompression_rule(source, rule_index, tail_index, arg_index);
// NB. arg_indices becomes stale after original rule is replaced.
if (is_negated_predicate && !can_remove_orig_rule) {
if (is_negated_predicate && !can_remove_orig_rule)
break;
}
}
else {
else
add_decompression_rule(source, r, tail_index, arg_index);
}
}
return replace_original_rule;
}
@ -343,20 +341,19 @@ namespace datalog {
}
rule_set * mk_unbound_compressor::operator()(rule_set const & source) {
// TODO mc
if (!m_context.compress_unbound()) {
if (!m_context.compress_unbound() || m_context.get_model_converter())
return nullptr;
}
m_modified = false;
SASSERT(m_rules.empty());
rel_context_base* rel = m_context.get_rel_context();
if (rel) {
if (rel)
rel->collect_non_empty_predicates(m_non_empty_rels);
}
unsigned init_rule_cnt = source.get_num_rules();
for (unsigned i = 0; i < init_rule_cnt; i++) {
rule * r = source.get_rule(i);
@ -390,13 +387,15 @@ namespace datalog {
scoped_ptr<rule_set> result;
if (m_modified) {
result = alloc(rule_set, m_context);
unsigned fin_rule_cnt = m_rules.size();
for (unsigned i=0; i<fin_rule_cnt; i++) {
result->add_rule(m_rules.get(i));
}
for (auto* r : m_rules)
result->add_rule(r);
result->inherit_predicates(source);
}
if (result && m_context.get_model_converter()) {
// TODO mc
}
reset();
return result.detach();
}