mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix coi filter to consider 0 cases

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-08-08 15:01:35 -07:00
parent dc58bce052
commit a0d79c8dd7
1 changed files with 16 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/muz_qe/dl_mk_coi_filter.cpp
View file

@ -36,11 +36,16 @@ namespace datalog {
// -----------------------------------
rule_set * mk_coi_filter::operator()(rule_set const & source) {
TRACE("dl", tout << "Hello";);
if (source.empty()) {
return 0;
}
scoped_ptr<rule_set> result = top_down(source);
return bottom_up(result?*result:source);
scoped_ptr<rule_set> result1 = top_down(source);
scoped_ptr<rule_set> result2 = bottom_up(result1?*result1:source);
if (!result2) {
result2 = result1;
}
return result2.detach();
}
rule_set * mk_coi_filter::bottom_up(rule_set const & source) {
@ -102,11 +107,13 @@ namespace datalog {
res->add_rule(r);
}
}
if (res->get_num_rules() == source.get_num_rules()) {
return 0;
}
res->close();
TRACE("dl", tout << "No transformation\n";);
res = 0;
}
else {
res->close();
}
// set to false each unreached predicate
if (m_context.get_model_converter()) {
@ -122,6 +129,7 @@ namespace datalog {
for (rule_set::decl2rules::iterator it = body2rules.begin(); it != body2rules.end(); ++it) {
dealloc(it->m_value);
}
CTRACE("dl", 0 != res, res->display(tout););
return res.detach();
}
@ -173,6 +181,7 @@ namespace datalog {
}
if (res->get_num_rules() == source.get_num_rules()) {
TRACE("dl", tout << "No transformation\n";);
res = 0;
}
@ -185,7 +194,7 @@ namespace datalog {
}
m_context.add_model_converter(mc0);
}
CTRACE("dl", 0 != res, res->display(tout););
return res.detach();
}