diff --git a/src/muz/dataflow/dataflow.h b/src/muz/dataflow/dataflow.h index 5e91a0149..e9e543b2d 100644 --- a/src/muz/dataflow/dataflow.h +++ b/src/muz/dataflow/dataflow.h @@ -62,8 +62,7 @@ namespace datalog { rule_set::decl2rules m_body2rules; void init_bottom_up() { - for (rule_set::iterator it = m_rules.begin(); it != m_rules.end(); ++it) { - rule* cur = *it; + for (rule* cur : m_rules) { for (unsigned i = 0; i < cur->get_uninterpreted_tail_size(); ++i) { func_decl *d = cur->get_decl(i); rule_set::decl2rules::obj_map_entry *e = m_body2rules.insert_if_not_there2(d, 0); @@ -83,31 +82,25 @@ namespace datalog { } void init_top_down() { - const func_decl_set& output_preds = m_rules.get_output_predicates(); - for (func_decl_set::iterator I = output_preds.begin(), - E = output_preds.end(); I != E; ++I) { - func_decl* sym = *I; + for (func_decl* sym : m_rules.get_output_predicates()) { TRACE("dl", tout << sym->get_name() << "\n";); const rule_vector& output_rules = m_rules.get_predicate_rules(sym); - for (unsigned i = 0; i < output_rules.size(); ++i) { - m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, output_rules[i]); + for (rule* r : output_rules) { + m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, r); m_todo[m_todo_idx].insert(sym); } } } void step_bottom_up() { - for(todo_set::iterator I = m_todo[m_todo_idx].begin(), - E = m_todo[m_todo_idx].end(); I!=E; ++I) { + for (func_decl* f : m_todo[m_todo_idx]) { ptr_vector * rules; - if (!m_body2rules.find(*I, rules)) + if (!m_body2rules.find(f, rules)) continue; - - for (ptr_vector::iterator I2 = rules->begin(), - E2 = rules->end(); I2 != E2; ++I2) { - func_decl* head_sym = (*I2)->get_head()->get_decl(); - fact_reader tail_facts(m_facts, *I2); - bool new_info = m_facts.insert_if_not_there2(head_sym, Fact())->get_data().m_value.propagate_up(m_context, *I2, tail_facts); + for (rule* r : *rules) { + func_decl* head_sym = r->get_head()->get_decl(); + fact_reader tail_facts(m_facts, r); + bool new_info = m_facts.insert_if_not_there2(head_sym, Fact())->get_data().m_value.propagate_up(m_context, r, tail_facts); if (new_info) { m_todo[!m_todo_idx].insert(head_sym); } @@ -119,15 +112,11 @@ namespace datalog { } void step_top_down() { - for(todo_set::iterator I = m_todo[m_todo_idx].begin(), - E = m_todo[m_todo_idx].end(); I!=E; ++I) { - func_decl* head_sym = *I; + for (func_decl* head_sym : m_todo[m_todo_idx]) { // We can't use a reference here because we are changing the map while using the reference const Fact head_fact = m_facts.get(head_sym, Fact::null_fact); const rule_vector& deps = m_rules.get_predicate_rules(head_sym); - const unsigned deps_size = deps.size(); - for (unsigned i = 0; i < deps_size; ++i) { - rule *trg_rule = deps[i]; + for (rule* trg_rule : deps) { fact_writer writer(m_facts, trg_rule, m_todo[!m_todo_idx]); // Generate new facts head_fact.propagate_down(m_context, trg_rule, writer); @@ -146,16 +135,13 @@ namespace datalog { dataflow_engine(typename Fact::ctx_t& ctx, const rule_set& rules) : m_rules(rules), m_todo_idx(0), m_context(ctx) {} ~dataflow_engine() { - for (rule_set::decl2rules::iterator it = m_body2rules.begin(); it != m_body2rules.end(); ++it) { - dealloc(it->m_value); - } + for (auto & kv : m_body2rules) + dealloc(kv.m_value); } void dump(std::ostream& outp) { obj_hashtable visited; - for (rule_set::iterator I = m_rules.begin(), - E = m_rules.end(); I != E; ++I) { - const rule* r = *I; + for (rule const* r : m_rules) { func_decl* head_decl = r->get_decl(); obj_hashtable::entry *dummy; if (visited.insert_if_not_there_core(head_decl, dummy)) { @@ -194,30 +180,29 @@ namespace datalog { iterator end() const { return m_facts.end(); } void join(const dataflow_engine& oth) { - for (typename fact_db::iterator I = oth.m_facts.begin(), - E = oth.m_facts.end(); I != E; ++I) { + for (auto const& kv : oth.m_facts) { typename fact_db::entry* entry; - if (m_facts.insert_if_not_there_core(I->m_key, entry)) { - entry->get_data().m_value = I->m_value; + if (m_facts.insert_if_not_there_core(kv.m_key, entry)) { + entry->get_data().m_value = kv.m_value; } else { - entry->get_data().m_value.join(m_context, I->m_value); + entry->get_data().m_value.join(m_context, kv.m_value); } } } void intersect(const dataflow_engine& oth) { vector to_delete; - for (typename fact_db::iterator I = m_facts.begin(), - E = m_facts.end(); I != E; ++I) { + for (auto const& kv : m_facts) { - if (typename fact_db::entry *entry = oth.m_facts.find_core(I->m_key)) { - I->m_value.intersect(m_context, entry->get_data().m_value); - } else { - to_delete.push_back(I->m_key); + if (typename fact_db::entry *entry = oth.m_facts.find_core(kv.m_key)) { + kv.m_value.intersect(m_context, entry->get_data().m_value); + } + else { + to_delete.push_back(kvm_key); } } - for (unsigned i = 0; i < to_delete.size(); ++i) { - m_facts.erase(to_delete[i]); + for (func_decl* f : to_delete) { + m_facts.erase(f); } } }; diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 31188bf43..3ea0e305a 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -21,6 +21,7 @@ Author: #include "muz/dataflow/dataflow.h" #include "muz/dataflow/reachability.h" #include "ast/ast_pp.h" +#include "ast/ast_util.h" #include "tactic/extension_model_converter.h" namespace datalog { @@ -33,20 +34,28 @@ namespace datalog { rule_set * mk_coi_filter::bottom_up(rule_set const & source) { dataflow_engine engine(source.get_manager(), source); engine.run_bottom_up(); + func_decl_set unreachable; scoped_ptr res = alloc(rule_set, m_context); res->inherit_predicates(source); - for (rule_set::iterator it = source.begin(); it != source.end(); ++it) { - rule * r = *it; - + for (rule* r : source) { bool new_tail = false; bool contained = true; + m_new_tail.reset(); + m_new_tail_neg.reset(); for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) { - if (m_context.has_facts(r->get_decl(i))) { + func_decl* decl_i = r->get_decl(i); + if (m_context.has_facts(decl_i)) { return 0; } + bool reachable = engine.get_fact(decl_i).is_reachable(); + + if (!reachable) { + unreachable.insert(decl_i); + } + if (r->is_neg_tail(i)) { - if (!engine.get_fact(r->get_decl(i)).is_reachable()) { + if (!reachable) { if (!new_tail) { for (unsigned j = 0; j < i; ++j) { m_new_tail.push_back(r->get_tail(j)); @@ -60,10 +69,9 @@ namespace datalog { m_new_tail_neg.push_back(true); } } - else { SASSERT(!new_tail); - if (!engine.get_fact(r->get_decl(i)).is_reachable()) { + if (!reachable) { contained = false; break; } @@ -78,24 +86,26 @@ namespace datalog { res->add_rule(r); } } - m_new_tail.reset(); - m_new_tail_neg.reset(); } if (res->get_num_rules() == source.get_num_rules()) { TRACE("dl", tout << "No transformation\n";); res = 0; - } else { + } + else { res->close(); } - + // set to false each unreached predicate - if (m_context.get_model_converter()) { + if (res && m_context.get_model_converter()) { extension_model_converter* mc0 = alloc(extension_model_converter, m); - for (dataflow_engine::iterator it = engine.begin(); it != engine.end(); it++) { - if (!it->m_value.is_reachable()) { - mc0->insert(it->m_key, m.mk_false()); + for (auto const& kv : engine) { + if (!kv.m_value.is_reachable()) { + mc0->insert(kv.m_key, m.mk_false()); } } + for (func_decl* f : unreachable) { + mc0->insert(f, m.mk_false()); + } m_context.add_model_converter(mc0); } CTRACE("dl", 0 != res, res->display(tout);); @@ -109,9 +119,7 @@ namespace datalog { scoped_ptr res = alloc(rule_set, m_context); res->inherit_predicates(source); - rule_set::iterator rend = source.end(); - for (rule_set::iterator rit = source.begin(); rit != rend; ++rit) { - rule * r = *rit; + for (rule * r : source) { func_decl * pred = r->get_decl(); if (engine.get_fact(pred).is_reachable()) { res->add_rule(r); @@ -125,14 +133,12 @@ namespace datalog { res = 0; } if (res && m_context.get_model_converter()) { - func_decl_set::iterator end = pruned_preds.end(); - func_decl_set::iterator it = pruned_preds.begin(); extension_model_converter* mc0 = alloc(extension_model_converter, m); - for (; it != end; ++it) { - const rule_vector& rules = source.get_predicate_rules(*it); + for (func_decl* f : pruned_preds) { + const rule_vector& rules = source.get_predicate_rules(f); expr_ref_vector fmls(m); - for (unsigned i = 0; i < rules.size(); ++i) { - app* head = rules[i]->get_head(); + for (rule * r : rules) { + 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); @@ -140,11 +146,9 @@ namespace datalog { conj.push_back(m.mk_eq(m.mk_var(j, m.get_sort(arg)), arg)); } } - fmls.push_back(m.mk_and(conj.size(), conj.c_ptr())); + fmls.push_back(mk_and(conj)); } - expr_ref fml(m); - fml = m.mk_or(fmls.size(), fmls.c_ptr()); - mc0->insert(*it, fml); + mc0->insert(f, mk_or(fmls)); } m_context.add_model_converter(mc0); }