mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-26 14:07:54 +00:00
Code Activity

compiler optimization and fixes to unit tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-04-11 13:44:23 -07:00
commit 18ea547cea
85 changed files with 1156 additions and 11585 deletions
Download patch file Download diff file Expand all files Collapse all files

85
src/muz_qe/dl_compiler.cpp
View file

@ -708,6 +708,7 @@ namespace datalog {
//update the head relation
make_union(new_head_reg, head_reg, delta_reg, use_widening, acc);
make_dealloc_non_void(new_head_reg, acc);
}
finish:
@ -761,7 +762,7 @@ namespace datalog {
typedef svector<tail_delta_info> tail_delta_infos;
unsigned rule_len = r->get_uninterpreted_tail_size();
reg_idx head_reg = m_pred_regs.find(r->get_head()->get_decl());
reg_idx head_reg = m_pred_regs.find(r->get_decl());
svector<reg_idx> tail_regs;
tail_delta_infos tail_deltas;
@ -798,6 +799,8 @@ namespace datalog {
typedef rule_dependencies::item_set item_set; //set of T
rule_dependencies & m_deps;
rule_set const& m_rules;
context& m_context;
item_set & m_removed;
svector<T> m_stack;
ast_mark m_stack_content;
@ -820,7 +823,7 @@ namespace datalog {
T d = *it;
if(m_stack_content.is_marked(d)) {
//TODO: find the best vertex to remove in the cycle
m_removed.insert(v);
remove_from_stack();
break;
}
traverse(d);
@ -830,9 +833,36 @@ namespace datalog {
m_stack.pop_back();
m_stack_content.mark(v, false);
}
void remove_from_stack() {
for (unsigned i = 0; i < m_stack.size(); ++i) {
func_decl* p = m_stack[i];
rule_vector const& rules = m_rules.get_predicate_rules(p);
unsigned stratum = m_rules.get_predicate_strat(p);
if (m_context.has_facts(p)) {
m_removed.insert(p);
return;
}
for (unsigned j = 0; j < rules.size(); ++j) {
rule const& r = *rules[j];
bool ok = true;
for (unsigned k = 0; ok && k < r.get_uninterpreted_tail_size(); ++k) {
ok &= m_rules.get_predicate_strat(r.get_decl(k)) < stratum;
}
if (ok) {
m_removed.insert(p);
return;
}
}
}
// nothing was found.
m_removed.insert(m_stack.back());
}
public:
cycle_breaker(rule_dependencies & deps, item_set & removed)
: m_deps(deps), m_removed(removed) { SASSERT(removed.empty()); }
cycle_breaker(rule_dependencies & deps, rule_set const& rules, context& ctx, item_set & removed)
: m_deps(deps), m_rules(rules), m_context(ctx), m_removed(removed) { SASSERT(removed.empty()); }
void operator()() {
rule_dependencies::iterator it = m_deps.begin();
@ -854,7 +884,7 @@ namespace datalog {
rule_dependencies deps(m_rule_set.get_dependencies());
deps.restrict(preds);
cycle_breaker(deps, global_deltas)();
cycle_breaker(deps, m_rule_set, m_context, global_deltas)();
VERIFY( deps.sort_deps(ordered_preds) );
//the predicates that were removed to get acyclic induced subgraph are put last
@ -885,13 +915,47 @@ namespace datalog {
rule_vector::const_iterator rend = pred_rules.end();
for(; rit!=rend; ++rit) {
rule * r = *rit;
SASSERT(head_pred==r->get_head()->get_decl());
SASSERT(head_pred==r->get_decl());
compile_rule_evaluation(r, input_deltas, d_head_reg, widen_predicate_in_loop, acc);
}
}
}
void compiler::compile_preds_init(const func_decl_vector & head_preds, const func_decl_set & widened_preds,
const pred2idx * input_deltas, const pred2idx & output_deltas, instruction_block & acc) {
func_decl_vector::const_iterator hpit = head_preds.begin();
func_decl_vector::const_iterator hpend = head_preds.end();
reg_idx void_reg = execution_context::void_register;
for(; hpit!=hpend; ++hpit) {
func_decl * head_pred = *hpit;
const rule_vector & pred_rules = m_rule_set.get_predicate_rules(head_pred);
rule_vector::const_iterator rit = pred_rules.begin();
rule_vector::const_iterator rend = pred_rules.end();
unsigned stratum = m_rule_set.get_predicate_strat(head_pred);
for(; rit != rend; ++rit) {
rule * r = *rit;
SASSERT(head_pred==r->get_decl());
for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) {
unsigned stratum1 = m_rule_set.get_predicate_strat(r->get_decl(i));
if (stratum1 >= stratum) {
goto next_loop;
}
}
compile_rule_evaluation(r, input_deltas, void_reg, false, acc);
next_loop:
;
}
reg_idx d_head_reg;
if (output_deltas.find(head_pred, d_head_reg)) {
acc.push_back(instruction::mk_clone(m_pred_regs.find(head_pred), d_head_reg));
}
}
}
void compiler::make_inloop_delta_transition(const pred2idx & global_head_deltas,
const pred2idx & global_tail_deltas, const pred2idx & local_deltas, instruction_block & acc) {
//move global head deltas into tail ones
@ -942,7 +1006,7 @@ namespace datalog {
const pred2idx * input_deltas, const pred2idx & output_deltas,
bool add_saturation_marks, instruction_block & acc) {
if(!output_deltas.empty()) {
if (!output_deltas.empty()) {
func_decl_set::iterator hpit = head_preds.begin();
func_decl_set::iterator hpend = head_preds.end();
for(; hpit!=hpend; ++hpit) {
@ -979,7 +1043,8 @@ namespace datalog {
func_decl_set empty_func_decl_set;
//generate code for the initial run
compile_preds(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc);
// compile_preds(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc);
compile_preds_init(preds_vector, empty_func_decl_set, input_deltas, d_global_src, acc);
if (compile_with_widening()) {
compile_loop(preds_vector, global_deltas, d_global_tgt, d_global_src, d_local, acc);
@ -1040,7 +1105,7 @@ namespace datalog {
rule_vector::const_iterator end = rules.end();
for (; it != end; ++it) {
rule * r = *it;
SASSERT(r->get_head()->get_decl()==head_pred);
SASSERT(r->get_decl()==head_pred);
compile_rule_evaluation(r, input_deltas, output_delta, false, acc);
}
@ -1113,7 +1178,7 @@ namespace datalog {
//load predicate data
for(unsigned i=0;i<rule_cnt;i++) {
const rule * r = m_rule_set.get_rule(i);
ensure_predicate_loaded(r->get_head()->get_decl(), acc);
ensure_predicate_loaded(r->get_decl(), acc);
unsigned rule_len = r->get_uninterpreted_tail_size();
for(unsigned j=0;j<rule_len;j++) {