mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

Replace cone-of-influence filter with generalized dataflow-engine

Browse source 
Signed-off-by: Henning Guenther <t-hennig@microsoft.com>
This commit is contained in:
Henning Guenther 2015-06-29 10:49:34 +01:00
parent 3104d2954c
commit c7e96d897a
5 changed files with 424 additions and 159 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_project.py
View file

@ -59,7 +59,8 @@ def init_project_def():
add_lib('qe', ['smt','sat'], 'qe')
add_lib('duality', ['smt', 'interp', 'qe'])
add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base')
add_lib('transforms', ['muz', 'hilbert'], 'muz/transforms')
add_lib('dataflow', ['muz'], 'muz/dataflow')
add_lib('transforms', ['muz', 'hilbert', 'dataflow'], 'muz/transforms')
add_lib('rel', ['muz', 'transforms'], 'muz/rel')
add_lib('pdr', ['muz', 'transforms', 'arith_tactics', 'core_tactics', 'smt_tactic'], 'muz/pdr')
add_lib('clp', ['muz', 'transforms'], 'muz/clp')

269
src/muz/dataflow/dataflow.h Executable file
View file

@ -0,0 +1,269 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
dataflow.h
Abstract:
Generic bottom-up and top-down data-flow engine for analysis
of rule sets.
Author:
Henning Guenther (t-hennig)
--*/
#ifndef DATAFLOW_H_
#define DATAFLOW_H_
#include "dl_rule.h"
#include "dl_rule_set.h"
#include "hashtable.h"
#include "vector.h"
namespace datalog {
template <typename Fact> class fact_reader;
template <typename Fact> class fact_writer;
/* The structure of fact classes:
class fact {
public:
typedef ... ctx_t;
// Empty fact
static fact null_fact;
fact(); -- bottom
// Init (Top down)
void init_down(ctx_t& ctx, const rule* r);
// Init (Bottom up)
bool init_up(ctx_t& ctx, const rule* r);
// Step (Bottom up)
bool propagate_up(ctx_t& ctx, const rule* r, const fact_reader<fact>& tail_facts);
// Step (Top down)
void propagate_down(ctx_t& ctx, const rule* r, fact_writer<fact>& tail_facts) const;
// Debugging
void dump(ctx_t& ctx, std::ostream& outp) const;
// Union
void join(ctx_t& ctx, const Fact& oth);
// Intersection
void intersect(ctx_t& ctx, const Fact& oth);
}; */
template <typename Fact> class dataflow_engine {
public:
typedef map<func_decl*, Fact, obj_ptr_hash<func_decl>, ptr_eq<func_decl> > fact_db;
typedef hashtable<func_decl*, obj_ptr_hash<func_decl>, ptr_eq<func_decl> > todo_set;
typedef typename fact_db::iterator iterator;
private:
const rule_set& m_rules;
fact_db m_facts;
todo_set m_todo[2];
unsigned m_todo_idx;
typename Fact::ctx_t& m_context;
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 (unsigned i = 0; i < cur->get_uninterpreted_tail_size(); ++i) {
func_decl *d = cur->get_tail(i)->get_decl();
rule_set::decl2rules::obj_map_entry *e = m_body2rules.insert_if_not_there2(d, 0);
if (!e->get_data().m_value) {
e->get_data().m_value = alloc(ptr_vector<rule>);
}
e->get_data().m_value->push_back(cur);
}
if (cur->get_uninterpreted_tail_size() == 0) {
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);
if (new_info) {
m_todo[m_todo_idx].insert(sym);
}
}
}
}
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;
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]);
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) {
ptr_vector<rule> * rules;
if (!m_body2rules.find(*I, rules))
continue;
for (ptr_vector<rule>::iterator I2 = rules->begin(),
E2 = rules->end(); I2 != E2; ++I2) {
func_decl* head_sym = (*I2)->get_head()->get_decl();
fact_reader<Fact> 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);
if (new_info) {
m_todo[!m_todo_idx].insert(head_sym);
}
}
}
// Update todo list
m_todo[m_todo_idx].reset();
m_todo_idx = !m_todo_idx;
}
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;
// 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];
const unsigned tail_size = trg_rule->get_uninterpreted_tail_size();
fact_writer<Fact> writer(m_facts, trg_rule, m_todo[!m_todo_idx]);
// Generate new facts
head_fact.propagate_down(m_context, trg_rule, writer);
}
}
// Update todo list
m_todo[m_todo_idx].reset();
m_todo_idx = !m_todo_idx;
}
bool done() const {
return m_todo[m_todo_idx].empty();
}
public:
dataflow_engine(typename Fact::ctx_t& ctx, const rule_set& rules) : m_rules(rules), m_context(ctx), m_todo_idx(0) {}
~dataflow_engine() {
for (rule_set::decl2rules::iterator it = m_body2rules.begin(); it != m_body2rules.end(); ++it) {
dealloc(it->m_value);
}
}
void dump(std::ostream& outp) {
obj_hashtable<func_decl> visited;
for (rule_set::iterator I = m_rules.begin(),
E = m_rules.end(); I != E; ++I) {
const rule* r = *I;
func_decl* head_decl = r->get_decl();
obj_hashtable<func_decl>::entry *dummy;
if (visited.insert_if_not_there_core(head_decl, dummy)) {
const Fact& fact = m_facts.get(head_decl, Fact::null_fact);
outp << head_decl->get_name() << " -> ";
fact.dump(m_context, outp);
outp << "\n";
}
for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
func_decl* tail_decl = r->get_tail(i)->get_decl();
if (visited.insert_if_not_there_core(tail_decl, dummy)) {
const Fact& fact = m_facts.get(tail_decl, Fact::null_fact);
outp << tail_decl->get_name() << " -> ";
fact.dump(m_context, outp);
outp << "\n";
}
}
}
}
void run_bottom_up() {
init_bottom_up();
while (!done()) step_bottom_up();
}
void run_top_down() {
init_top_down();
while (!done()) step_top_down();
}
const Fact& get_fact(func_decl* decl) const {
return m_facts.get(decl, Fact::null_fact);
}
iterator begin() const { return m_facts.begin(); }
iterator end() const { return m_facts.end(); }
void join(const dataflow_engine<Fact>& oth) {
for (typename fact_db::iterator I = oth.m_facts.begin(),
E = oth.m_facts.end(); I != E; ++I) {
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;
} else {
entry->get_data().m_value.join(m_context, I->m_value);
}
}
}
void intersect(const dataflow_engine<Fact>& oth) {
vector<func_decl*> to_delete;
for (typename fact_db::iterator I = m_facts.begin(),
E = m_facts.end(); I != E; ++I) {
typename fact_db::entry* entry;
if (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);
}
}
for (unsigned i = 0; i < to_delete.size(); ++i) {
m_facts.erase(to_delete[i]);
}
}
};
// This helper-class is used to look up facts for rule tails
template <typename Fact> class fact_reader {
typedef typename dataflow_engine<Fact>::fact_db fact_db;
const fact_db& m_facts;
const rule* m_rule;
public:
fact_reader(const fact_db& facts, const rule* r)
: m_facts(facts), m_rule(r) {
}
const Fact& get(unsigned idx) const {
return m_facts.get(m_rule->get_tail(idx)->get_decl(), Fact::null_fact);
}
unsigned size() const {
return m_rule->get_uninterpreted_tail_size();
}
};
template <typename Fact> class fact_writer {
friend class dataflow_engine<Fact>;
typedef typename dataflow_engine<Fact>::fact_db fact_db;
fact_db& m_facts;
const rule* m_rule;
typename dataflow_engine<Fact>::todo_set& m_todo;
public:
fact_writer(fact_db& facts, const rule* r, typename dataflow_engine<Fact>::todo_set& todo)
: m_facts(facts), m_rule(r), m_todo(todo) {}
Fact& get(unsigned idx) {
func_decl* sym = m_rule->get_tail(idx)->get_decl();
return m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value;
}
void set_changed(unsigned idx) {
m_todo.insert(m_rule->get_tail(idx)->get_decl());
}
unsigned size() const {
return m_rule->get_uninterpreted_tail_size();
}
};
}
#endif

82
src/muz/dataflow/reachability.h Executable file
View file

@ -0,0 +1,82 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
reachability.h
Abstract:
Abstract domain for tracking rule reachability.
Author:
Henning Guenther (t-hennig)
--*/
#ifndef REACHABILITY_H_
#define REACHABILITY_H_
#include "dataflow.h"
namespace datalog {
class reachability_info {
bool m_reachable;
reachability_info(bool r) : m_reachable(r) {}
public:
typedef ast_manager ctx_t;
static const reachability_info null_fact;
reachability_info() : m_reachable(false) {}
void init_down(const ctx_t& m, const rule* r) {
m_reachable = true;
}
bool init_up(const ctx_t& m, const rule* r) {
if (m_reachable)
return false;
else {
m_reachable = true;
return true;
}
}
void propagate_down(const ctx_t& manager, const rule* r, fact_writer<reachability_info>& tail_facts) const {
SASSERT(m_reachable);
for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
reachability_info& tail_fact = tail_facts.get(i);
if (!tail_fact.m_reachable) {
tail_fact.m_reachable = true;
tail_facts.set_changed(i);
}
}
}
bool propagate_up(const ctx_t& manager, const rule* r, const fact_reader<reachability_info>& tail_facts) {
if (m_reachable)
return false;
for (unsigned i = 0; i < r->get_positive_tail_size(); ++i) {
if (!tail_facts.get(i).m_reachable) {
return false;
}
}
m_reachable = true;
return true;
}
void join(const ctx_t& manager, const reachability_info& oth) {
m_reachable |= oth.m_reachable;
}
void dump(const ctx_t& manager, std::ostream& outp) const {
outp << (m_reachable ? "reachable" : "unreachable");
}
bool is_reachable() const { return m_reachable; }
};
typedef dataflow_engine<reachability_info> reachability;
}
#endif

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

@ -1,5 +1,5 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Copyright (c) 2006-2015 Microsoft Corporation
Module Name:
@ -7,181 +7,100 @@ Module Name:
Abstract:
Rule transformer which removes relations which are out of the cone of
Rule transformer which removes relations which are out of the cone of
influence of output relations
Author:
Krystof Hoder (t-khoder) 2011-10-01.
Revision History:
Andrey Rybalchenko (rybal) 2013-8-8
Added bottom_up pruning.
Krystof Hoder (t-khoder)
Andrey Rybalchenko (rybal)
Henning Guenther (t-hennig)
--*/
#include <sstream>
#include"ast_pp.h"
#include"dl_mk_coi_filter.h"
#include"extension_model_converter.h"
#include "dl_mk_coi_filter.h"
#include "dataflow.h"
#include "reachability.h"
#include "ast_pp.h"
#include "extension_model_converter.h"
namespace datalog {
// -----------------------------------
//
// mk_coi_filter
//
// -----------------------------------
const reachability_info reachability_info::null_fact;
rule_set * mk_coi_filter::operator()(rule_set const & source) {
if (!m_context.xform_coi()) {
return 0;
}
if (source.empty()) {
return 0;
}
scoped_ptr<rule_set> result1 = top_down(source);
scoped_ptr<rule_set> result2 = bottom_up(result1?*result1:source);
if (!result2) {
result2 = result1.detach();
}
return result2.detach();
scoped_ptr<rule_set> result2 = bottom_up(result1 ? *result1 : source);
return result2 ? result2.detach() : result1.detach();
}
rule_set * mk_coi_filter::bottom_up(rule_set const & source) {
func_decl_set all, reached;
ptr_vector<func_decl> todo;
rule_set::decl2rules body2rules;
// initialization for reachability
for (rule_set::iterator it = source.begin(); it != source.end(); ++it) {
rule * r = *it;
all.insert(r->get_decl());
if (r->get_uninterpreted_tail_size() == 0) {
if (!reached.contains(r->get_decl())) {
reached.insert(r->get_decl());
todo.insert(r->get_decl());
}
}
else {
for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
func_decl * d = r->get_tail(i)->get_decl();
all.insert(d);
rule_set::decl2rules::obj_map_entry * e = body2rules.insert_if_not_there2(d, 0);
if (!e->get_data().m_value) {
e->get_data().m_value = alloc(ptr_vector<rule>);
}
e->get_data().m_value->push_back(r);
if (r->is_neg_tail(i)) {
// don't try COI on rule with negation.
return 0;
}
}
}
}
rel_context_base* rc = m_context.get_rel_context();
if (rc) {
func_decl_set::iterator fit = all.begin(), fend = all.end();
for (; fit != fend; ++fit) {
if (!rc->is_empty_relation(*fit) &&
!reached.contains(*fit)) {
reached.insert(*fit);
todo.insert(*fit);
}
}
}
// reachability computation
while (!todo.empty()) {
func_decl * d = todo.back();
todo.pop_back();
ptr_vector<rule> * rules;
if (!body2rules.find(d, rules)) continue;
for (ptr_vector<rule>::iterator it = rules->begin(); it != rules->end(); ++it) {
rule * r = *it;
if (reached.contains(r->get_decl())) continue;
bool contained = true;
for (unsigned i = 0; contained && i < r->get_uninterpreted_tail_size(); ++i) {
contained = reached.contains(r->get_tail(i)->get_decl());
}
if (!contained) continue;
reached.insert(r->get_decl());
todo.insert(r->get_decl());
}
}
// eliminate each rule when some body predicate is not reached
dataflow_engine<reachability_info> engine(source.get_manager(), source);
engine.run_bottom_up();
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
res->inherit_predicates(source);
for (rule_set::iterator it = source.begin(); it != source.end(); ++it) {
rule * r = *it;
bool new_tail = false;
bool contained = true;
for (unsigned i = 0; contained && i < r->get_uninterpreted_tail_size(); ++i) {
contained = reached.contains(r->get_tail(i)->get_decl());
for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
if (r->is_neg_tail(i)) {
if (!engine.get_fact(r->get_tail(i)->get_decl()).is_reachable()) {
if (!new_tail) {
for (unsigned j = 0; j < i; ++j) {
m_new_tail.push_back(r->get_tail(j));
m_new_tail_neg.push_back(r->is_neg_tail(j));
}
new_tail = true;
}
} else if (new_tail) {
m_new_tail.push_back(r->get_tail(i));
m_new_tail_neg.push_back(true);
}
} else {
SASSERT(!new_tail);
if (!engine.get_fact(r->get_tail(i)->get_decl()).is_reachable()) {
contained = false;
break;
}
}
}
if (contained) {
res->add_rule(r);
if (new_tail) {
rule* new_r = m_context.get_rule_manager().mk(r->get_head(), m_new_tail.size(),
m_new_tail.c_ptr(), m_new_tail_neg.c_ptr(), symbol::null, false);
res->add_rule(new_r);
} else {
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()) {
extension_model_converter* mc0 = alloc(extension_model_converter, m);
for (func_decl_set::iterator it = all.begin(); it != all.end(); ++it) {
if (!reached.contains(*it)) {
mc0->insert(*it, m.mk_false());
for (dataflow_engine<reachability_info>::iterator it = engine.begin(); it != engine.end(); it++) {
if (!it->m_value.is_reachable()) {
mc0->insert(it->m_key, m.mk_false());
}
}
}
m_context.add_model_converter(mc0);
}
// clean up body2rules range resources
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();
}
rule_set * mk_coi_filter::top_down(rule_set const & source) {
func_decl_set interesting_preds;
func_decl_set pruned_preds;
ptr_vector<func_decl> todo;
{
const func_decl_set& output_preds = source.get_output_predicates();
func_decl_set::iterator oend = output_preds.end();
for (func_decl_set::iterator it = output_preds.begin(); it!=oend; ++it) {
todo.push_back(*it);
interesting_preds.insert(*it);
}
}
const rule_dependencies& deps = source.get_dependencies();
while (!todo.empty()) {
func_decl * curr = todo.back();
todo.pop_back();
interesting_preds.insert(curr);
const rule_dependencies::item_set& cdeps = deps.get_deps(curr);
rule_dependencies::item_set::iterator dend = cdeps.end();
for (rule_dependencies::item_set::iterator it = cdeps.begin(); it != dend; ++it) {
func_decl * dep_pred = *it;
if (!interesting_preds.contains(dep_pred)) {
interesting_preds.insert(dep_pred);
todo.push_back(dep_pred);
}
}
}
dataflow_engine<reachability_info> engine(source.get_manager(), source);
engine.run_top_down();
scoped_ptr<rule_set> res = alloc(rule_set, m_context);
res->inherit_predicates(source);
@ -189,10 +108,9 @@ namespace datalog {
for (rule_set::iterator rit = source.begin(); rit != rend; ++rit) {
rule * r = *rit;
func_decl * pred = r->get_decl();
if (interesting_preds.contains(pred)) {
if (engine.get_fact(pred).is_reachable()) {
res->add_rule(r);
}
else if (m_context.get_model_converter()) {
} else if (m_context.get_model_converter()) {
pruned_preds.insert(pred);
}
}
@ -201,7 +119,6 @@ namespace datalog {
TRACE("dl", tout << "No transformation\n";);
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();
@ -217,18 +134,16 @@ namespace datalog {
if (!is_var(arg)) {
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()));
}
expr_ref fml(m);
fml = m.mk_or(fmls.size(), fmls.c_ptr());
mc0->insert(*it, fml);
}
}
m_context.add_model_converter(mc0);
}
CTRACE("dl", 0 != res, res->display(tout););
return res.detach();
}
};
}

28
src/muz/transforms/dl_mk_coi_filter.h
View file

@ -1,5 +1,5 @@
/*++
Copyright (c) 2006 Microsoft Corporation
Copyright (c) 2006-2015 Microsoft Corporation
Module Name:
@ -7,22 +7,21 @@ Module Name:
Abstract:
Rule transformer which removes relations which are out of the cone of
Rule transformer which removes relations which are out of the cone of
influence of output relations
Author:
Krystof Hoder (t-khoder) 2011-10-01.
Revision History:
Krystof Hoder (t-khoder)
Andrey Rybalchenko (rybal)
Henning Guenther (t-hennig)
--*/
#ifndef _DL_MK_COI_FILTER_H_
#define _DL_MK_COI_FILTER_H_
#ifndef DL_MK_COI_FILTER_H_
#define DL_MK_COI_FILTER_H_
#include "dl_context.h"
#include "dl_rule_transformer.h"
#include "dl_context.h"
namespace datalog {
@ -32,20 +31,19 @@ namespace datalog {
ast_manager & m;
context & m_context;
vector<app*> m_new_tail;
svector<bool> m_new_tail_neg;
rule_set * bottom_up(rule_set const & source);
rule_set * top_down(rule_set const & source);
public:
mk_coi_filter(context & ctx, unsigned priority=45000)
mk_coi_filter(context & ctx, unsigned priority = 45000)
: plugin(priority),
m(ctx.get_manager()),
m_context(ctx) {}
rule_set * operator()(rule_set const & source);
};
}
};
#endif /* _DL_MK_COI_FILTER_H_ */
#endif