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

cleanup warnings from new dataflow engine

Browse source 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-06-30 08:47:37 +01:00
parent 769127d531
commit 1f619fd960
4 changed files with 13 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/muz/dataflow/dataflow.cpp
View file

@ -16,10 +16,9 @@ Author:
--*/ --*/
#include "dataflow.h" #include "dataflow.h"
#include "reachability.h"
namespace datalog { namespace datalog {
void dummy_dataflow() { const reachability_info reachability_info::null_fact;
}
} }

20
src/muz/dataflow/dataflow.h Executable file → Normal file
View file

@ -65,7 +65,7 @@ namespace datalog {
for (rule_set::iterator it = m_rules.begin(); it != m_rules.end(); ++it) { for (rule_set::iterator it = m_rules.begin(); it != m_rules.end(); ++it) {
rule* cur = *it; rule* cur = *it;
for (unsigned i = 0; i < cur->get_uninterpreted_tail_size(); ++i) { for (unsigned i = 0; i < cur->get_uninterpreted_tail_size(); ++i) {
func_decl *d = cur->get_tail(i)->get_decl(); func_decl *d = cur->get_decl(i);
rule_set::decl2rules::obj_map_entry *e = m_body2rules.insert_if_not_there2(d, 0); rule_set::decl2rules::obj_map_entry *e = m_body2rules.insert_if_not_there2(d, 0);
if (!e->get_data().m_value) { if (!e->get_data().m_value) {
e->get_data().m_value = alloc(ptr_vector<rule>); e->get_data().m_value = alloc(ptr_vector<rule>);
@ -73,7 +73,7 @@ namespace datalog {
e->get_data().m_value->push_back(cur); e->get_data().m_value->push_back(cur);
} }
if (cur->get_uninterpreted_tail_size() == 0) { if (cur->get_uninterpreted_tail_size() == 0) {
func_decl* sym = cur->get_head()->get_decl(); func_decl *sym = cur->get_head()->get_decl();
bool new_info = m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_up(m_context, cur); bool new_info = m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_up(m_context, cur);
if (new_info) { if (new_info) {
m_todo[m_todo_idx].insert(sym); m_todo[m_todo_idx].insert(sym);
@ -126,8 +126,7 @@ namespace datalog {
const rule_vector& deps = m_rules.get_predicate_rules(head_sym); const rule_vector& deps = m_rules.get_predicate_rules(head_sym);
const unsigned deps_size = deps.size(); const unsigned deps_size = deps.size();
for (unsigned i = 0; i < deps_size; ++i) { for (unsigned i = 0; i < deps_size; ++i) {
rule* trg_rule = deps[i]; rule *trg_rule = deps[i];
const unsigned tail_size = trg_rule->get_uninterpreted_tail_size();
fact_writer<Fact> writer(m_facts, trg_rule, m_todo[!m_todo_idx]); fact_writer<Fact> writer(m_facts, trg_rule, m_todo[!m_todo_idx]);
// Generate new facts // Generate new facts
head_fact.propagate_down(m_context, trg_rule, writer); head_fact.propagate_down(m_context, trg_rule, writer);
@ -143,7 +142,7 @@ namespace datalog {
} }
public: public:
dataflow_engine(typename Fact::ctx_t& ctx, const rule_set& rules) : m_rules(rules), m_context(ctx), m_todo_idx(0) {} dataflow_engine(typename Fact::ctx_t& ctx, const rule_set& rules) : m_rules(rules), m_todo_idx(0), m_context(ctx) {}
~dataflow_engine() { ~dataflow_engine() {
for (rule_set::decl2rules::iterator it = m_body2rules.begin(); it != m_body2rules.end(); ++it) { for (rule_set::decl2rules::iterator it = m_body2rules.begin(); it != m_body2rules.end(); ++it) {
@ -165,7 +164,7 @@ namespace datalog {
outp << "\n"; outp << "\n";
} }
for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) { for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
func_decl* tail_decl = r->get_tail(i)->get_decl(); func_decl *tail_decl = r->get_decl(i);
if (visited.insert_if_not_there_core(tail_decl, dummy)) { if (visited.insert_if_not_there_core(tail_decl, dummy)) {
const Fact& fact = m_facts.get(tail_decl, Fact::null_fact); const Fact& fact = m_facts.get(tail_decl, Fact::null_fact);
outp << tail_decl->get_name() << " -> "; outp << tail_decl->get_name() << " -> ";
@ -210,8 +209,7 @@ namespace datalog {
for (typename fact_db::iterator I = m_facts.begin(), for (typename fact_db::iterator I = m_facts.begin(),
E = m_facts.end(); I != E; ++I) { E = m_facts.end(); I != E; ++I) {
typename fact_db::entry* entry; if (typename fact_db::entry *entry = oth.m_facts.find_core(I->m_key)) {
if (entry = oth.m_facts.find_core(I->m_key)) {
I->m_value.intersect(m_context, entry->get_data().m_value); I->m_value.intersect(m_context, entry->get_data().m_value);
} else { } else {
to_delete.push_back(I->m_key); to_delete.push_back(I->m_key);
@ -234,7 +232,7 @@ namespace datalog {
} }
const Fact& get(unsigned idx) const { const Fact& get(unsigned idx) const {
return m_facts.get(m_rule->get_tail(idx)->get_decl(), Fact::null_fact); return m_facts.get(m_rule->get_decl(idx), Fact::null_fact);
} }
unsigned size() const { unsigned size() const {
return m_rule->get_uninterpreted_tail_size(); return m_rule->get_uninterpreted_tail_size();
@ -252,12 +250,12 @@ namespace datalog {
: m_facts(facts), m_rule(r), m_todo(todo) {} : m_facts(facts), m_rule(r), m_todo(todo) {}
Fact& get(unsigned idx) { Fact& get(unsigned idx) {
func_decl* sym = m_rule->get_tail(idx)->get_decl(); func_decl *sym = m_rule->get_decl(idx);
return m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value; return m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value;
} }
void set_changed(unsigned idx) { void set_changed(unsigned idx) {
m_todo.insert(m_rule->get_tail(idx)->get_decl()); m_todo.insert(m_rule->get_decl(idx));
} }
unsigned size() const { unsigned size() const {

0
src/muz/dataflow/reachability.h Executable file → Normal file
View file

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

@ -24,8 +24,6 @@ Author:
#include "extension_model_converter.h" #include "extension_model_converter.h"
namespace datalog { namespace datalog {
const reachability_info reachability_info::null_fact;
rule_set * mk_coi_filter::operator()(rule_set const & source) { rule_set * mk_coi_filter::operator()(rule_set const & source) {
scoped_ptr<rule_set> result1 = top_down(source); scoped_ptr<rule_set> result1 = top_down(source);
scoped_ptr<rule_set> result2 = bottom_up(result1 ? *result1 : source); scoped_ptr<rule_set> result2 = bottom_up(result1 ? *result1 : source);
@ -44,7 +42,7 @@ namespace datalog {
bool contained = true; bool contained = true;
for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) { for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
if (r->is_neg_tail(i)) { if (r->is_neg_tail(i)) {
if (!engine.get_fact(r->get_tail(i)->get_decl()).is_reachable()) { if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
if (!new_tail) { if (!new_tail) {
for (unsigned j = 0; j < i; ++j) { for (unsigned j = 0; j < i; ++j) {
m_new_tail.push_back(r->get_tail(j)); m_new_tail.push_back(r->get_tail(j));
@ -58,7 +56,7 @@ namespace datalog {
} }
} else { } else {
SASSERT(!new_tail); SASSERT(!new_tail);
if (!engine.get_fact(r->get_tail(i)->get_decl()).is_reachable()) { if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
contained = false; contained = false;
break; break;
} }