From 08eb85fe3def5ab5d2ded01d1a14192119bf6996 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 23 Apr 2013 10:02:44 -0700 Subject: [PATCH 1/5] minor cleanup Signed-off-by: Nuno Lopes --- src/muz_qe/dl_compiler.h | 1 - src/muz_qe/dl_rule_transformer.cpp | 3 --- src/muz_qe/fixedpoint_params.pyg | 1 - src/muz_qe/rel_context.cpp | 2 -- 4 files changed, 7 deletions(-) diff --git a/src/muz_qe/dl_compiler.h b/src/muz_qe/dl_compiler.h index 8f40f814a..78b4623de 100644 --- a/src/muz_qe/dl_compiler.h +++ b/src/muz_qe/dl_compiler.h @@ -42,7 +42,6 @@ namespace datalog { typedef u_map int2int; typedef u_map int2ints; typedef obj_map pred2idx; -// typedef map,ptr_eq > pred2idx; typedef unsigned_vector var_vector; typedef ptr_vector func_decl_vector; diff --git a/src/muz_qe/dl_rule_transformer.cpp b/src/muz_qe/dl_rule_transformer.cpp index 21021ca43..0cad08cb4 100644 --- a/src/muz_qe/dl_rule_transformer.cpp +++ b/src/muz_qe/dl_rule_transformer.cpp @@ -107,9 +107,6 @@ namespace datalog { tout << typeid(p).name()<<":\n"; new_rules->display(tout); ); - IF_VERBOSE(1, new_rules->get_rule(0)->display(m_context, verbose_stream() << typeid(p).name() <<"\n");); - IF_VERBOSE(1, verbose_stream() << new_rules->get_dependencies().begin()->m_key->get_name() << "\n";); - } if (modified) { rules.replace_rules(*new_rules); diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index fd7dbdcae..774559cdb 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -13,7 +13,6 @@ def_module_params('fixedpoint', ('unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables in rule heads"), ('similarity_compressor', BOOL, True, "(DATALOG) rules that differ only in values of constants will be merged into a single rule"), ('similarity_compressor_threshold', UINT, 11, "(DATALOG) if similarity_compressor is on, this value determines how many similar rules there must be in order for them to be merged"), - ('filter_rules', BOOL, True, "(DATALOG) apply filter compression on rules"), ('all_or_nothing_deltas', BOOL, False, "(DATALOG) compile rules so that it is enough for the delta relation in union and widening operations to determine only whether the updated relation was modified or not"), ('compile_with_widening', BOOL, False, "(DATALOG) widening will be used to compile recursive rules"), ('eager_emptiness_checking', BOOL, True, "(DATALOG) emptiness of affected relations will be checked after each instruction, so that we may ommit unnecessary instructions"), diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index be6d999b6..ef5639279 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -113,12 +113,10 @@ namespace datalog { TRACE("dl", m_context.display(tout);); while (true) { - m_ectx.reset(); m_code.reset(); termination_code.reset(); m_context.ensure_closed(); - IF_VERBOSE(1, verbose_stream() << "num rules: " << m_context.get_rules().get_num_rules() << "\n";); m_context.transform_rules(); if (m_context.canceled()) { result = l_undef; From 12b092c45fdde206bbc12e2446cb786d021ef1a3 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 23 Apr 2013 11:27:27 -0700 Subject: [PATCH 2/5] [datalog] restore the old (linear) cycle breaker force the compiler to use all preds as global deltas for correctness. This is a temporary fix. Signed-off-by: Nuno Lopes --- src/muz_qe/dl_compiler.cpp | 58 +- src/muz_qe/dl_compiler.cpp.orig | 1245 +++++++++++++++++++++++++++++++ 2 files changed, 1263 insertions(+), 40 deletions(-) create mode 100644 src/muz_qe/dl_compiler.cpp.orig diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index e4528426a..57d9880c0 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -832,19 +832,19 @@ 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 m_stack; + ast_mark m_stack_content; ast_mark m_visited; void traverse(T v) { - SASSERT(!m_visited.is_marked(v)); - if (m_removed.contains(v)) { + SASSERT(!m_stack_content.is_marked(v)); + if(m_visited.is_marked(v) || m_removed.contains(v)) { return; } m_stack.push_back(v); + m_stack_content.mark(v, true); m_visited.mark(v, true); const item_set & deps = m_deps.get_deps(v); @@ -852,49 +852,22 @@ namespace datalog { item_set::iterator end = deps.end(); for(; it!=end; ++it) { T d = *it; - if (m_visited.is_marked(d)) { + if(m_stack_content.is_marked(d)) { //TODO: find the best vertex to remove in the cycle - remove_from_stack(); - continue; + m_removed.insert(v); + break; } traverse(d); } SASSERT(m_stack.back()==v); m_stack.pop_back(); - m_visited.mark(v, false); - } - - void remove_from_stack() { - for (unsigned i = 0; i < m_stack.size(); ++i) { - func_decl* p = m_stack[i]; - if (m_context.has_facts(p)) { - m_removed.insert(p); - return; - } - - rule_vector const& rules = m_rules.get_predicate_rules(p); - unsigned stratum = m_rules.get_predicate_strat(p); - 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()); + m_stack_content.mark(v, false); } public: - 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()); } + cycle_breaker(rule_dependencies & deps, item_set & removed) + : m_deps(deps), m_removed(removed) { SASSERT(removed.empty()); } void operator()() { rule_dependencies::iterator it = m_deps.begin(); @@ -916,7 +889,7 @@ namespace datalog { rule_dependencies deps(m_rule_set.get_dependencies()); deps.restrict(preds); - cycle_breaker(deps, m_rule_set, m_context, global_deltas)(); + cycle_breaker(deps, global_deltas)(); VERIFY( deps.sort_deps(ordered_preds) ); //the predicates that were removed to get acyclic induced subgraph are put last @@ -1052,12 +1025,17 @@ namespace datalog { } func_decl_vector preds_vector; - func_decl_set global_deltas; + func_decl_set global_deltas_dummy; - detect_chains(head_preds, preds_vector, global_deltas); + detect_chains(head_preds, preds_vector, global_deltas_dummy); + /* + FIXME: right now we use all preds as global deltas for correctness purposes func_decl_set local_deltas(head_preds); set_difference(local_deltas, global_deltas); + */ + func_decl_set local_deltas; + func_decl_set global_deltas(head_preds); pred2idx d_global_src; //these deltas serve as sources of tuples for rule evaluation inside the loop get_fresh_registers(global_deltas, d_global_src); diff --git a/src/muz_qe/dl_compiler.cpp.orig b/src/muz_qe/dl_compiler.cpp.orig new file mode 100644 index 000000000..e4528426a --- /dev/null +++ b/src/muz_qe/dl_compiler.cpp.orig @@ -0,0 +1,1245 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + dl_compiler.cpp + +Abstract: + + + +Author: + + Krystof Hoder (t-khoder) 2010-09-14. + +Revision History: + +--*/ + + +#include +#include"ref_vector.h" +#include"dl_context.h" +#include"dl_rule.h" +#include"dl_util.h" +#include"dl_compiler.h" +#include"ast_pp.h" +#include"ast_smt2_pp.h" + + +namespace datalog { + + void compiler::reset() { + m_pred_regs.reset(); + m_new_reg = 0; + } + + void compiler::ensure_predicate_loaded(func_decl * pred, instruction_block & acc) { + pred2idx::obj_map_entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX); + if(e->get_data().m_value!=UINT_MAX) { + //predicate is already loaded + return; + } + relation_signature sig; + m_context.get_rel_context().get_rmanager().from_predicate(pred, sig); + reg_idx reg = get_fresh_register(sig); + e->get_data().m_value=reg; + + acc.push_back(instruction::mk_load(m_context.get_manager(), pred, reg)); + } + + void compiler::make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result, + instruction_block & acc) { + relation_signature res_sig; + relation_signature::from_join(m_reg_signatures[t1], m_reg_signatures[t2], vars.size(), + vars.get_cols1(), vars.get_cols2(), res_sig); + result = get_fresh_register(res_sig); + acc.push_back(instruction::mk_join(t1, t2, vars.size(), vars.get_cols1(), vars.get_cols2(), result)); + } + + void compiler::make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, + const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) { + relation_signature aux_sig; + relation_signature sig1 = m_reg_signatures[t1]; + relation_signature sig2 = m_reg_signatures[t2]; + relation_signature::from_join(sig1, sig2, vars.size(), vars.get_cols1(), vars.get_cols2(), aux_sig); + relation_signature res_sig; + relation_signature::from_project(aux_sig, removed_cols.size(), removed_cols.c_ptr(), + res_sig); + result = get_fresh_register(res_sig); + + acc.push_back(instruction::mk_join_project(t1, t2, vars.size(), vars.get_cols1(), + vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result)); + } + + void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, + reg_idx & result, instruction_block & acc) { + relation_signature res_sig; + relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig); + result = get_fresh_register(res_sig); + acc.push_back(instruction::mk_select_equal_and_project(m_context.get_manager(), + src, val, col, result)); + } + + void compiler::make_clone(reg_idx src, reg_idx & result, instruction_block & acc) { + relation_signature sig = m_reg_signatures[src]; + result = get_fresh_register(sig); + acc.push_back(instruction::mk_clone(src, result)); + } + + void compiler::make_union(reg_idx src, reg_idx tgt, reg_idx delta, bool use_widening, + instruction_block & acc) { + SASSERT(m_reg_signatures[src]==m_reg_signatures[tgt]); + SASSERT(delta==execution_context::void_register || m_reg_signatures[src]==m_reg_signatures[delta]); + + if (use_widening) { + acc.push_back(instruction::mk_widen(src, tgt, delta)); + } + else { + acc.push_back(instruction::mk_union(src, tgt, delta)); + } + } + + void compiler::make_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, + reg_idx & result, instruction_block & acc) { + SASSERT(col_cnt>0); + + relation_signature res_sig; + relation_signature::from_project(m_reg_signatures[src], col_cnt, removed_cols, res_sig); + result = get_fresh_register(res_sig); + acc.push_back(instruction::mk_projection(src, col_cnt, removed_cols, result)); + } + + compiler::reg_idx compiler::get_fresh_register(const relation_signature & sig) { + //since we might be resizing the m_reg_signatures vector, the argument must not point inside it + SASSERT((&sig>=m_reg_signatures.end()) || (&sigto_formula(e); + verbose_stream() << "Compiling unsafe rule column " << col_idx << "\n" + << mk_ismt2_pp(e, m_context.get_manager()) << "\n"; + }); + reg_idx total_table; + if (!m_total_registers.find(s, pred, total_table)) { + total_table = get_single_column_register(s); + relation_signature sig; + sig.push_back(s); + m_top_level_code.push_back(instruction::mk_total(sig, pred, total_table)); + m_total_registers.insert(s, pred, total_table); + } + if(src == execution_context::void_register) { + result = total_table; + dealloc = false; + } + else { + variable_intersection empty_vars(m_context.get_manager()); + make_join(src, total_table, empty_vars, result, acc); + dealloc = true; + } + } + + void compiler::make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, + instruction_block & acc) { + SASSERT(sig.empty()); + TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";); + if (m_empty_tables_registers.find(pred, result)) + return; + + result = get_fresh_register(sig); + m_top_level_code.push_back(instruction::mk_total(sig, pred, result)); + m_empty_tables_registers.insert(pred, result); + } + + + void compiler::make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, + instruction_block & acc) { + + relation_signature & src_sig = m_reg_signatures[src]; + reg_idx single_col_reg; + unsigned src_col_cnt = src_sig.size(); + if(src_col_cnt==1) { + single_col_reg = src; + } + else { + unsigned_vector removed_cols; + for(unsigned i=0; i & acis0, + reg_idx & result, + bool & dealloc, + instruction_block & acc) { + + TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";); + + unsigned col_cnt = acis0.size(); + reg_idx curr = src; + + relation_signature empty_signature; + + relation_signature * curr_sig; + if(curr!=execution_context::void_register) { + curr_sig = & m_reg_signatures[curr]; + } + else { + curr_sig = & empty_signature; + } + unsigned src_col_cnt=curr_sig->size(); + + svector acis(acis0); + int2int handled_unbound; + + //first remove unused source columns + int_set referenced_src_cols; + for(unsigned i=0; isize(); + if(acis[i].kind==ACK_CONSTANT) { + make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, new_curr, new_dealloc, acc); + } + else { + SASSERT(acis[i].kind==ACK_UNBOUND_VAR); + make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, new_curr, new_dealloc, acc); + handled_unbound.insert(acis[i].var_index,bound_column_index); + } + if (dealloc) + make_dealloc_non_void(curr, acc); + dealloc = new_dealloc; + curr=new_curr; + curr_sig = & m_reg_signatures[curr]; + SASSERT(bound_column_index==curr_sig->size()-1); + } + SASSERT((*curr_sig)[bound_column_index]==acis[i].domain); + acis[i].kind=ACK_BOUND_VAR; + acis[i].source_column=bound_column_index; + } + + //duplicate needed source columns + int_set used_cols; + for(unsigned i=0; isize()-1; + SASSERT((*curr_sig)[bound_column_index]==acis[i].domain); + acis[i].source_column=bound_column_index; + } + + //reorder source columns to match target + SASSERT(curr_sig->size()==col_cnt); //now the intermediate table is a permutation + for(unsigned i=0; i=i); //columns below i are already reordered + SASSERT(nextget_num_args(); + for(unsigned i = 0; iget_arg(i); + if(!is_var(e) || globals.get(to_var(e)->get_idx())!=0) { + continue; + } + res.push_back(i+ofs); + } + } + + void compiler::get_local_indexes_for_projection(rule * r, unsigned_vector & res) { + SASSERT(r->get_positive_tail_size()==2); + ast_manager & m = m_context.get_manager(); + rule_counter counter; + counter.count_rule_vars(m, r); + app * t1 = r->get_tail(0); + app * t2 = r->get_tail(1); + counter.count_vars(m, t1, -1); + counter.count_vars(m, t2, -1); + get_local_indexes_for_projection(t1, counter, 0, res); + get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res); + } + + void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs, + reg_idx delta_reg, bool use_widening, instruction_block & acc) { + + ast_manager & m = m_context.get_manager(); + m_instruction_observer.start_rule(r); + + const app * h = r->get_head(); + unsigned head_len = h->get_num_args(); + func_decl * head_pred = h->get_decl(); + + TRACE("dl", r->display(m_context, tout); ); + + unsigned pt_len = r->get_positive_tail_size(); + SASSERT(pt_len<=2); //we require rules to be processed by the mk_simple_joins rule transformer plugin + + reg_idx single_res; + expr_ref_vector single_res_expr(m); + + //used to save on filter_identical instructions where the check is already done + //by the join operation + unsigned second_tail_arg_ofs; + + // whether to dealloc the previous result + bool dealloc = true; + + if(pt_len == 2) { + reg_idx t1_reg=tail_regs[0]; + reg_idx t2_reg=tail_regs[1]; + app * a1 = r->get_tail(0); + app * a2 = r->get_tail(1); + SASSERT(m_reg_signatures[t1_reg].size()==a1->get_num_args()); + SASSERT(m_reg_signatures[t2_reg].size()==a2->get_num_args()); + + variable_intersection a1a2(m_context.get_manager()); + a1a2.populate(a1,a2); + + unsigned_vector removed_cols; + get_local_indexes_for_projection(r, removed_cols); + + if(removed_cols.empty()) { + make_join(t1_reg, t2_reg, a1a2, single_res, acc); + } + else { + make_join_project(t1_reg, t2_reg, a1a2, removed_cols, single_res, acc); + } + + unsigned rem_index = 0; + unsigned rem_sz = removed_cols.size(); + unsigned a1len=a1->get_num_args(); + for(unsigned i=0; i=i); + if(rem_indexget_arg(i)); + } + second_tail_arg_ofs = single_res_expr.size(); + unsigned a2len=a2->get_num_args(); + for(unsigned i=0; i=i+a1len); + if(rem_indexget_arg(i)); + } + SASSERT(rem_index==rem_sz); + } + else if(pt_len==1) { + reg_idx t_reg=tail_regs[0]; + app * a = r->get_tail(0); + SASSERT(m_reg_signatures[t_reg].size()==a->get_num_args()); + + single_res = t_reg; + + unsigned n=a->get_num_args(); + for(unsigned i=0; iget_arg(i); + if(is_app(arg)) { + app * c = to_app(arg); //argument is a constant + SASSERT(c->get_num_args()==0); + SASSERT(m_context.get_decl_util().is_numeral_ext(arg)); + reg_idx new_reg; + make_select_equal_and_project(single_res, c, single_res_expr.size(), new_reg, acc); + if(single_res!=t_reg) { + //since single_res is a local register, we deallocate it + make_dealloc_non_void(single_res, acc); + } + single_res = new_reg; + } + else { + SASSERT(is_var(arg)); + single_res_expr.push_back(arg); + } + } + if(single_res==t_reg) { + dealloc = false; + } + + } + else { + SASSERT(pt_len==0); + + //single_res register should never be used in this case + single_res=execution_context::void_register; + } + + add_unbound_columns_for_negation(r, head_pred, single_res, single_res_expr, dealloc, acc); + + int2ints var_indexes; + + reg_idx filtered_res = single_res; + + { + //enforce equality to constants + unsigned srlen=single_res_expr.size(); + SASSERT((single_res==execution_context::void_register) ? (srlen==0) : (srlen==m_reg_signatures[single_res].size())); + for(unsigned i=0; iget_idx(); + int2ints::entry * e = var_indexes.insert_if_not_there2(var_num, unsigned_vector()); + e->get_data().m_value.push_back(i); + } + } + } + + //enforce equality of columns + int2ints::iterator vit=var_indexes.begin(); + int2ints::iterator vend=var_indexes.end(); + for(; vit!=vend; ++vit) { + int2ints::key_data & k = *vit; + unsigned_vector & indexes = k.m_value; + if(indexes.size()==1) { + continue; + } + SASSERT(indexes.size()>1); + if(pt_len==2 && indexes[0]=second_tail_arg_ofs) { + //If variable appears in multiple tails, the identicity will already be enforced by join. + //(If behavior the join changes so that it is not enforced anymore, remove this + //condition!) + continue; + } + if (!dealloc) + make_clone(filtered_res, filtered_res, acc); + acc.push_back(instruction::mk_filter_identical(filtered_res, indexes.size(), indexes.c_ptr())); + dealloc = true; + } + + //enforce negative predicates + unsigned ut_len=r->get_uninterpreted_tail_size(); + for(unsigned i=pt_len; iget_tail(i); + func_decl * neg_pred = neg_tail->get_decl(); + variable_intersection neg_intersection(m_context.get_manager()); + neg_intersection.populate(single_res_expr, neg_tail); + unsigned_vector t_cols(neg_intersection.size(), neg_intersection.get_cols1()); + unsigned_vector neg_cols(neg_intersection.size(), neg_intersection.get_cols2()); + + unsigned neg_len = neg_tail->get_num_args(); + for(unsigned i=0; iget_arg(i); + if(is_var(e)) { + continue; + } + SASSERT(is_app(e)); + relation_sort arg_sort; + m_context.get_rel_context().get_rmanager().from_predicate(neg_pred, i, arg_sort); + reg_idx new_reg; + bool new_dealloc; + make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc); + + if (dealloc) + make_dealloc_non_void(filtered_res, acc); + dealloc = new_dealloc; + filtered_res = new_reg; // here filtered_res value gets changed !! + + t_cols.push_back(single_res_expr.size()); + neg_cols.push_back(i); + single_res_expr.push_back(e); + } + SASSERT(t_cols.size()==neg_cols.size()); + + reg_idx neg_reg = m_pred_regs.find(neg_pred); + if (!dealloc) + make_clone(filtered_res, filtered_res, acc); + acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(), + t_cols.c_ptr(), neg_cols.c_ptr())); + dealloc = true; + } + + // enforce interpreted tail predicates + unsigned ft_len=r->get_tail_size(); //full tail + for(unsigned tail_index=ut_len; tail_indexget_tail(tail_index); + ptr_vector t_vars; + ::get_free_vars(t, t_vars); + + if(t_vars.empty()) { + expr_ref simplified(m); + m_context.get_rewriter()(t, simplified); + if(m.is_true(simplified)) { + //this tail element is always true + continue; + } + //the tail of this rule is never satisfied + SASSERT(m.is_false(simplified)); + goto finish; + } + + //determine binding size + while (!t_vars.back()) { + t_vars.pop_back(); + } + unsigned max_var = t_vars.size(); + + //create binding + expr_ref_vector binding(m); + binding.resize(max_var+1); + + for(unsigned v = 0; v < t_vars.size(); ++v) { + if (!t_vars[v]) { + continue; + } + int2ints::entry * e = var_indexes.find_core(v); + if(!e) { + //we have an unbound variable, so we add an unbound column for it + relation_sort unbound_sort = t_vars[v]; + + reg_idx new_reg; + TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";); + bool new_dealloc; + make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, new_dealloc, acc); + + if (dealloc) + make_dealloc_non_void(filtered_res, acc); + dealloc = new_dealloc; + filtered_res = new_reg; // here filtered_res value gets changed !! + + unsigned unbound_column_index = single_res_expr.size(); + single_res_expr.push_back(m.mk_var(v, unbound_sort)); + + e = var_indexes.insert_if_not_there2(v, unsigned_vector()); + e->get_data().m_value.push_back(unbound_column_index); + } + unsigned src_col=e->get_data().m_value.back(); + relation_sort var_sort = m_reg_signatures[filtered_res][src_col]; + binding[max_var-v]=m.mk_var(src_col, var_sort); + } + + + expr_ref renamed(m); + m_context.get_var_subst()(t, binding.size(), binding.c_ptr(), renamed); + app_ref app_renamed(to_app(renamed), m); + if (!dealloc) + make_clone(filtered_res, filtered_res, acc); + acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed)); + dealloc = true; + } + + { + //put together the columns of head relation + relation_signature & head_sig = m_reg_signatures[head_reg]; + svector head_acis; + unsigned_vector head_src_cols; + for(unsigned i=0; iget_arg(i); + if(is_var(exp)) { + unsigned var_num=to_var(exp)->get_idx(); + int2ints::entry * e = var_indexes.find_core(var_num); + if(e) { + unsigned_vector & binding_indexes = e->get_data().m_value; + aci.kind=ACK_BOUND_VAR; + aci.source_column=binding_indexes.back(); + SASSERT(aci.source_column1) { + //if possible, we do not want multiple head columns + //point to a single column in the intermediate table, + //since then we would have to duplicate the column + //(and remove columns we did not point to at all) + binding_indexes.pop_back(); + } + } + else { + aci.kind=ACK_UNBOUND_VAR; + aci.var_index=var_num; + } + } + else { + SASSERT(is_app(exp)); + SASSERT(m_context.get_decl_util().is_numeral_ext(exp)); + aci.kind=ACK_CONSTANT; + aci.constant=to_app(exp); + } + head_acis.push_back(aci); + } + SASSERT(head_acis.size()==head_len); + + reg_idx new_head_reg; + make_assembling_code(r, head_pred, filtered_res, head_acis, new_head_reg, dealloc, acc); + + //update the head relation + make_union(new_head_reg, head_reg, delta_reg, use_widening, acc); + if (dealloc) + make_dealloc_non_void(new_head_reg, acc); + } + + finish: + m_instruction_observer.finish_rule(); + } + + void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr, + bool & dealloc, instruction_block & acc) { + uint_set pos_vars; + u_map neg_vars; + ast_manager& m = m_context.get_manager(); + unsigned pt_len = r->get_positive_tail_size(); + unsigned ut_len = r->get_uninterpreted_tail_size(); + if (pt_len == ut_len || pt_len == 0) { + return; + } + // populate negative variables: + for (unsigned i = pt_len; i < ut_len; ++i) { + app * neg_tail = r->get_tail(i); + unsigned neg_len = neg_tail->get_num_args(); + for (unsigned j = 0; j < neg_len; ++j) { + expr * e = neg_tail->get_arg(j); + if (is_var(e)) { + neg_vars.insert(to_var(e)->get_idx(), e); + } + } + } + // populate positive variables: + for (unsigned i = 0; i < single_res_expr.size(); ++i) { + expr* e = single_res_expr[i].get(); + if (is_var(e)) { + pos_vars.insert(to_var(e)->get_idx()); + } + } + // add negative variables that are not in positive: + u_map::iterator it = neg_vars.begin(), end = neg_vars.end(); + for (; it != end; ++it) { + unsigned v = it->m_key; + expr* e = it->m_value; + if (!pos_vars.contains(v)) { + single_res_expr.push_back(e); + reg_idx new_single_res; + bool new_dealloc; + make_add_unbound_column(r, v, pred, single_res, m.get_sort(e), new_single_res, new_dealloc, acc); + if (dealloc) + make_dealloc_non_void(single_res, acc); + dealloc = new_dealloc; + single_res = new_single_res; + TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m) << "\n";); + } + } + } + + void compiler::compile_rule_evaluation(rule * r, const pred2idx * input_deltas, + reg_idx output_delta, bool use_widening, instruction_block & acc) { + typedef std::pair tail_delta_info; //(delta register, tail index) + typedef svector tail_delta_infos; + + unsigned rule_len = r->get_uninterpreted_tail_size(); + reg_idx head_reg = m_pred_regs.find(r->get_decl()); + + svector tail_regs; + tail_delta_infos tail_deltas; + for(unsigned j=0;jget_tail(j)->get_decl(); + reg_idx tail_reg = m_pred_regs.find(tail_pred); + tail_regs.push_back(tail_reg); + + if(input_deltas && !all_or_nothing_deltas()) { + reg_idx tail_delta_idx; + if(input_deltas->find(tail_pred, tail_delta_idx)) { + tail_deltas.push_back(tail_delta_info(tail_delta_idx, j)); + } + } + } + + if(!input_deltas || all_or_nothing_deltas()) { + compile_rule_evaluation_run(r, head_reg, tail_regs.c_ptr(), output_delta, use_widening, acc); + } + else { + tail_delta_infos::iterator tdit = tail_deltas.begin(); + tail_delta_infos::iterator tdend = tail_deltas.end(); + for(; tdit!=tdend; ++tdit) { + tail_delta_info tdinfo = *tdit; + flet flet_tail_reg(tail_regs[tdinfo.second], tdinfo.first); + compile_rule_evaluation_run(r, head_reg, tail_regs.c_ptr(), output_delta, use_widening, acc); + } + } + } + + class cycle_breaker + { + typedef func_decl * T; + 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 m_stack; + ast_mark m_visited; + + void traverse(T v) { + SASSERT(!m_visited.is_marked(v)); + if (m_removed.contains(v)) { + return; + } + + m_stack.push_back(v); + m_visited.mark(v, true); + + const item_set & deps = m_deps.get_deps(v); + item_set::iterator it = deps.begin(); + item_set::iterator end = deps.end(); + for(; it!=end; ++it) { + T d = *it; + if (m_visited.is_marked(d)) { + //TODO: find the best vertex to remove in the cycle + remove_from_stack(); + continue; + } + traverse(d); + } + SASSERT(m_stack.back()==v); + + m_stack.pop_back(); + m_visited.mark(v, false); + } + + void remove_from_stack() { + for (unsigned i = 0; i < m_stack.size(); ++i) { + func_decl* p = m_stack[i]; + if (m_context.has_facts(p)) { + m_removed.insert(p); + return; + } + + rule_vector const& rules = m_rules.get_predicate_rules(p); + unsigned stratum = m_rules.get_predicate_strat(p); + 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, 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(); + rule_dependencies::iterator end = m_deps.end(); + for(; it!=end; ++it) { + T v = it->m_key; + traverse(v); + } + m_deps.remove(m_removed); + } + }; + + void compiler::detect_chains(const func_decl_set & preds, func_decl_vector & ordered_preds, + func_decl_set & global_deltas) { + typedef obj_map pred2pred; + + SASSERT(ordered_preds.empty()); + SASSERT(global_deltas.empty()); + + rule_dependencies deps(m_rule_set.get_dependencies()); + deps.restrict(preds); + 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 + //so that all their local input deltas are already populated + func_decl_set::iterator gdit = global_deltas.begin(); + func_decl_set::iterator gend = global_deltas.end(); + for(; gdit!=gend; ++gdit) { + ordered_preds.push_back(*gdit); + } + } + + void compiler::compile_preds(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(); + for(; hpit!=hpend; ++hpit) { + func_decl * head_pred = *hpit; + + bool widen_predicate_in_loop = widened_preds.contains(head_pred); + + reg_idx d_head_reg; //output delta for the initial rule execution + if(!output_deltas.find(head_pred, d_head_reg)) { + d_head_reg = execution_context::void_register; + } + + 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(); + for(; rit!=rend; ++rit) { + rule * r = *rit; + 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 + pred2idx::iterator gdit = global_head_deltas.begin(); + pred2idx::iterator gend = global_head_deltas.end(); + for(; gdit!=gend; ++gdit) { + func_decl * pred = gdit->m_key; + reg_idx head_reg = gdit->m_value; + reg_idx tail_reg = global_tail_deltas.find(pred); + acc.push_back(instruction::mk_move(head_reg, tail_reg)); + } + //empty local deltas + pred2idx::iterator lit = local_deltas.begin(); + pred2idx::iterator lend = local_deltas.end(); + for(; lit!=lend; ++lit) { + acc.push_back(instruction::mk_dealloc(lit->m_value)); + } + } + + void compiler::compile_loop(const func_decl_vector & head_preds, const func_decl_set & widened_preds, + const pred2idx & global_head_deltas, const pred2idx & global_tail_deltas, + const pred2idx & local_deltas, instruction_block & acc) { + instruction_block * loop_body = alloc(instruction_block); + loop_body->set_observer(&m_instruction_observer); + + pred2idx all_head_deltas(global_head_deltas); + unite_disjoint_maps(all_head_deltas, local_deltas); + pred2idx all_tail_deltas(global_tail_deltas); + unite_disjoint_maps(all_tail_deltas, local_deltas); + + //generate code for the iterative fixpoint search + //The order in which we iterate the preds_vector matters, since rules can depend on + //deltas generated earlier in the same iteration. + compile_preds(head_preds, widened_preds, &all_tail_deltas, all_head_deltas, *loop_body); + + svector loop_control_regs; //loop is controlled by global src regs + collect_map_range(loop_control_regs, global_tail_deltas); + //move target deltas into source deltas at the end of the loop + //and clear local deltas + make_inloop_delta_transition(global_head_deltas, global_tail_deltas, local_deltas, *loop_body); + + loop_body->set_observer(0); + acc.push_back(instruction::mk_while_loop(loop_control_regs.size(), + loop_control_regs.c_ptr(), loop_body)); + } + + void compiler::compile_dependent_rules(const func_decl_set & head_preds, + const pred2idx * input_deltas, const pred2idx & output_deltas, + bool add_saturation_marks, instruction_block & acc) { + + if (!output_deltas.empty()) { + func_decl_set::iterator hpit = head_preds.begin(); + func_decl_set::iterator hpend = head_preds.end(); + for(; hpit!=hpend; ++hpit) { + if(output_deltas.contains(*hpit)) { + //we do not support retrieving deltas for rules that are inside a recursive + //stratum, since we would have to maintain this 'global' delta through the loop + //iterations + NOT_IMPLEMENTED_YET(); + } + } + } + + func_decl_vector preds_vector; + func_decl_set global_deltas; + + detect_chains(head_preds, preds_vector, global_deltas); + + func_decl_set local_deltas(head_preds); + set_difference(local_deltas, global_deltas); + + pred2idx d_global_src; //these deltas serve as sources of tuples for rule evaluation inside the loop + get_fresh_registers(global_deltas, d_global_src); + pred2idx d_global_tgt; //these deltas are targets for new tuples in rule evaluation inside the loop + get_fresh_registers(global_deltas, d_global_tgt); + pred2idx d_local; + get_fresh_registers(local_deltas, d_local); + + pred2idx d_all_src(d_global_src); //src together with local deltas + unite_disjoint_maps(d_all_src, d_local); + pred2idx d_all_tgt(d_global_tgt); //tgt together with local deltas + unite_disjoint_maps(d_all_tgt, d_local); + + + 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_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); + } + else { + compile_loop(preds_vector, empty_func_decl_set, d_global_tgt, d_global_src, d_local, acc); + } + + + if(add_saturation_marks) { + //after the loop finishes, all predicates in the group are saturated, + //so we may mark them as such + func_decl_set::iterator fdit = head_preds.begin(); + func_decl_set::iterator fdend = head_preds.end(); + for(; fdit!=fdend; ++fdit) { + acc.push_back(instruction::mk_mark_saturated(m_context.get_manager(), *fdit)); + } + } + } + + bool compiler::is_nonrecursive_stratum(const func_decl_set & preds) const { + SASSERT(preds.size()>0); + if(preds.size()>1) { + return false; + } + func_decl * head_pred = *preds.begin(); + const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred); + rule_vector::const_iterator it = rules.begin(); + rule_vector::const_iterator end = rules.end(); + for(; it!=end; ++it) { + //it is sufficient to check just for presence of the first head predicate, + //since if the rules are recursive and their heads are strongly connected by dependence, + //this predicate must appear in some tail + if((*it)->is_in_tail(head_pred)) { + return false; + } + } + return true; + } + + void compiler::compile_nonrecursive_stratum(const func_decl_set & preds, + const pred2idx * input_deltas, const pred2idx & output_deltas, + bool add_saturation_marks, instruction_block & acc) { + //non-recursive stratum always has just one head predicate + SASSERT(preds.size()==1); + SASSERT(is_nonrecursive_stratum(preds)); + func_decl * head_pred = *preds.begin(); + const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred); + + + + reg_idx output_delta; + if (!output_deltas.find(head_pred, output_delta)) { + output_delta = execution_context::void_register; + } + + rule_vector::const_iterator it = rules.begin(); + rule_vector::const_iterator end = rules.end(); + for (; it != end; ++it) { + rule * r = *it; + SASSERT(r->get_decl()==head_pred); + + compile_rule_evaluation(r, input_deltas, output_delta, false, acc); + } + + if (add_saturation_marks) { + //now the predicate is saturated, so we may mark it as such + acc.push_back(instruction::mk_mark_saturated(m_context.get_manager(), head_pred)); + } + } + + bool compiler::all_saturated(const func_decl_set & preds) const { + func_decl_set::iterator fdit = preds.begin(); + func_decl_set::iterator fdend = preds.end(); + for(; fdit!=fdend; ++fdit) { + if(!m_context.get_rel_context().get_rmanager().is_saturated(*fdit)) { + return false; + } + } + return true; + } + + void compiler::compile_strats(const rule_stratifier & stratifier, + const pred2idx * input_deltas, const pred2idx & output_deltas, + bool add_saturation_marks, instruction_block & acc) { + rule_set::pred_set_vector strats = stratifier.get_strats(); + rule_set::pred_set_vector::const_iterator sit = strats.begin(); + rule_set::pred_set_vector::const_iterator send = strats.end(); + for(; sit!=send; ++sit) { + func_decl_set & strat_preds = **sit; + + if (all_saturated(strat_preds)) { + //all predicates in stratum are saturated, so no need to compile rules for them + continue; + } + + TRACE("dl", + tout << "Stratum: "; + func_decl_set::iterator pit = strat_preds.begin(); + func_decl_set::iterator pend = strat_preds.end(); + for(; pit!=pend; ++pit) { + func_decl * pred = *pit; + tout << pred->get_name() << " "; + } + tout << "\n"; + ); + + if (is_nonrecursive_stratum(strat_preds)) { + //this stratum contains just a single non-recursive rule + compile_nonrecursive_stratum(strat_preds, input_deltas, output_deltas, add_saturation_marks, acc); + } + else { + compile_dependent_rules(strat_preds, input_deltas, output_deltas, + add_saturation_marks, acc); + } + } + } + + void compiler::do_compilation(instruction_block & execution_code, + instruction_block & termination_code) { + + unsigned rule_cnt=m_rule_set.get_num_rules(); + if(rule_cnt==0) { + return; + } + + instruction_block & acc = execution_code; + acc.set_observer(&m_instruction_observer); + + + //load predicate data + for(unsigned i=0;iget_decl(), acc); + + unsigned rule_len = r->get_uninterpreted_tail_size(); + for(unsigned j=0;jget_tail(j)->get_decl(), acc); + } + } + + pred2idx empty_pred2idx_map; + + compile_strats(m_rule_set.get_stratifier(), static_cast(0), + empty_pred2idx_map, true, execution_code); + + + + //store predicate data + pred2idx::iterator pit = m_pred_regs.begin(); + pred2idx::iterator pend = m_pred_regs.end(); + for(; pit!=pend; ++pit) { + pred2idx::key_data & e = *pit; + func_decl * pred = e.m_key; + reg_idx reg = e.m_value; + termination_code.push_back(instruction::mk_store(m_context.get_manager(), pred, reg)); + } + + acc.set_observer(0); + + TRACE("dl", execution_code.display(m_context.get_rel_context(), tout);); + } + + +} + From 1917c909d8ba44a15d6e06b3e13541751bff6d9c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 23 Apr 2013 11:28:09 -0700 Subject: [PATCH 3/5] delete garbage Signed-off-by: Nuno Lopes --- src/muz_qe/dl_compiler.cpp.orig | 1245 ------------------------------- 1 file changed, 1245 deletions(-) delete mode 100644 src/muz_qe/dl_compiler.cpp.orig diff --git a/src/muz_qe/dl_compiler.cpp.orig b/src/muz_qe/dl_compiler.cpp.orig deleted file mode 100644 index e4528426a..000000000 --- a/src/muz_qe/dl_compiler.cpp.orig +++ /dev/null @@ -1,1245 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - dl_compiler.cpp - -Abstract: - - - -Author: - - Krystof Hoder (t-khoder) 2010-09-14. - -Revision History: - ---*/ - - -#include -#include"ref_vector.h" -#include"dl_context.h" -#include"dl_rule.h" -#include"dl_util.h" -#include"dl_compiler.h" -#include"ast_pp.h" -#include"ast_smt2_pp.h" - - -namespace datalog { - - void compiler::reset() { - m_pred_regs.reset(); - m_new_reg = 0; - } - - void compiler::ensure_predicate_loaded(func_decl * pred, instruction_block & acc) { - pred2idx::obj_map_entry * e = m_pred_regs.insert_if_not_there2(pred, UINT_MAX); - if(e->get_data().m_value!=UINT_MAX) { - //predicate is already loaded - return; - } - relation_signature sig; - m_context.get_rel_context().get_rmanager().from_predicate(pred, sig); - reg_idx reg = get_fresh_register(sig); - e->get_data().m_value=reg; - - acc.push_back(instruction::mk_load(m_context.get_manager(), pred, reg)); - } - - void compiler::make_join(reg_idx t1, reg_idx t2, const variable_intersection & vars, reg_idx & result, - instruction_block & acc) { - relation_signature res_sig; - relation_signature::from_join(m_reg_signatures[t1], m_reg_signatures[t2], vars.size(), - vars.get_cols1(), vars.get_cols2(), res_sig); - result = get_fresh_register(res_sig); - acc.push_back(instruction::mk_join(t1, t2, vars.size(), vars.get_cols1(), vars.get_cols2(), result)); - } - - void compiler::make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars, - const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) { - relation_signature aux_sig; - relation_signature sig1 = m_reg_signatures[t1]; - relation_signature sig2 = m_reg_signatures[t2]; - relation_signature::from_join(sig1, sig2, vars.size(), vars.get_cols1(), vars.get_cols2(), aux_sig); - relation_signature res_sig; - relation_signature::from_project(aux_sig, removed_cols.size(), removed_cols.c_ptr(), - res_sig); - result = get_fresh_register(res_sig); - - acc.push_back(instruction::mk_join_project(t1, t2, vars.size(), vars.get_cols1(), - vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result)); - } - - void compiler::make_select_equal_and_project(reg_idx src, const relation_element & val, unsigned col, - reg_idx & result, instruction_block & acc) { - relation_signature res_sig; - relation_signature::from_project(m_reg_signatures[src], 1, &col, res_sig); - result = get_fresh_register(res_sig); - acc.push_back(instruction::mk_select_equal_and_project(m_context.get_manager(), - src, val, col, result)); - } - - void compiler::make_clone(reg_idx src, reg_idx & result, instruction_block & acc) { - relation_signature sig = m_reg_signatures[src]; - result = get_fresh_register(sig); - acc.push_back(instruction::mk_clone(src, result)); - } - - void compiler::make_union(reg_idx src, reg_idx tgt, reg_idx delta, bool use_widening, - instruction_block & acc) { - SASSERT(m_reg_signatures[src]==m_reg_signatures[tgt]); - SASSERT(delta==execution_context::void_register || m_reg_signatures[src]==m_reg_signatures[delta]); - - if (use_widening) { - acc.push_back(instruction::mk_widen(src, tgt, delta)); - } - else { - acc.push_back(instruction::mk_union(src, tgt, delta)); - } - } - - void compiler::make_projection(reg_idx src, unsigned col_cnt, const unsigned * removed_cols, - reg_idx & result, instruction_block & acc) { - SASSERT(col_cnt>0); - - relation_signature res_sig; - relation_signature::from_project(m_reg_signatures[src], col_cnt, removed_cols, res_sig); - result = get_fresh_register(res_sig); - acc.push_back(instruction::mk_projection(src, col_cnt, removed_cols, result)); - } - - compiler::reg_idx compiler::get_fresh_register(const relation_signature & sig) { - //since we might be resizing the m_reg_signatures vector, the argument must not point inside it - SASSERT((&sig>=m_reg_signatures.end()) || (&sigto_formula(e); - verbose_stream() << "Compiling unsafe rule column " << col_idx << "\n" - << mk_ismt2_pp(e, m_context.get_manager()) << "\n"; - }); - reg_idx total_table; - if (!m_total_registers.find(s, pred, total_table)) { - total_table = get_single_column_register(s); - relation_signature sig; - sig.push_back(s); - m_top_level_code.push_back(instruction::mk_total(sig, pred, total_table)); - m_total_registers.insert(s, pred, total_table); - } - if(src == execution_context::void_register) { - result = total_table; - dealloc = false; - } - else { - variable_intersection empty_vars(m_context.get_manager()); - make_join(src, total_table, empty_vars, result, acc); - dealloc = true; - } - } - - void compiler::make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, - instruction_block & acc) { - SASSERT(sig.empty()); - TRACE("dl", tout << "Adding unbound column " << mk_pp(pred, m_context.get_manager()) << "\n";); - if (m_empty_tables_registers.find(pred, result)) - return; - - result = get_fresh_register(sig); - m_top_level_code.push_back(instruction::mk_total(sig, pred, result)); - m_empty_tables_registers.insert(pred, result); - } - - - void compiler::make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, - instruction_block & acc) { - - relation_signature & src_sig = m_reg_signatures[src]; - reg_idx single_col_reg; - unsigned src_col_cnt = src_sig.size(); - if(src_col_cnt==1) { - single_col_reg = src; - } - else { - unsigned_vector removed_cols; - for(unsigned i=0; i & acis0, - reg_idx & result, - bool & dealloc, - instruction_block & acc) { - - TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";); - - unsigned col_cnt = acis0.size(); - reg_idx curr = src; - - relation_signature empty_signature; - - relation_signature * curr_sig; - if(curr!=execution_context::void_register) { - curr_sig = & m_reg_signatures[curr]; - } - else { - curr_sig = & empty_signature; - } - unsigned src_col_cnt=curr_sig->size(); - - svector acis(acis0); - int2int handled_unbound; - - //first remove unused source columns - int_set referenced_src_cols; - for(unsigned i=0; isize(); - if(acis[i].kind==ACK_CONSTANT) { - make_add_constant_column(head_pred, curr, acis[i].domain, acis[i].constant, new_curr, new_dealloc, acc); - } - else { - SASSERT(acis[i].kind==ACK_UNBOUND_VAR); - make_add_unbound_column(compiled_rule, i, head_pred, curr, acis[i].domain, new_curr, new_dealloc, acc); - handled_unbound.insert(acis[i].var_index,bound_column_index); - } - if (dealloc) - make_dealloc_non_void(curr, acc); - dealloc = new_dealloc; - curr=new_curr; - curr_sig = & m_reg_signatures[curr]; - SASSERT(bound_column_index==curr_sig->size()-1); - } - SASSERT((*curr_sig)[bound_column_index]==acis[i].domain); - acis[i].kind=ACK_BOUND_VAR; - acis[i].source_column=bound_column_index; - } - - //duplicate needed source columns - int_set used_cols; - for(unsigned i=0; isize()-1; - SASSERT((*curr_sig)[bound_column_index]==acis[i].domain); - acis[i].source_column=bound_column_index; - } - - //reorder source columns to match target - SASSERT(curr_sig->size()==col_cnt); //now the intermediate table is a permutation - for(unsigned i=0; i=i); //columns below i are already reordered - SASSERT(nextget_num_args(); - for(unsigned i = 0; iget_arg(i); - if(!is_var(e) || globals.get(to_var(e)->get_idx())!=0) { - continue; - } - res.push_back(i+ofs); - } - } - - void compiler::get_local_indexes_for_projection(rule * r, unsigned_vector & res) { - SASSERT(r->get_positive_tail_size()==2); - ast_manager & m = m_context.get_manager(); - rule_counter counter; - counter.count_rule_vars(m, r); - app * t1 = r->get_tail(0); - app * t2 = r->get_tail(1); - counter.count_vars(m, t1, -1); - counter.count_vars(m, t2, -1); - get_local_indexes_for_projection(t1, counter, 0, res); - get_local_indexes_for_projection(t2, counter, t1->get_num_args(), res); - } - - void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs, - reg_idx delta_reg, bool use_widening, instruction_block & acc) { - - ast_manager & m = m_context.get_manager(); - m_instruction_observer.start_rule(r); - - const app * h = r->get_head(); - unsigned head_len = h->get_num_args(); - func_decl * head_pred = h->get_decl(); - - TRACE("dl", r->display(m_context, tout); ); - - unsigned pt_len = r->get_positive_tail_size(); - SASSERT(pt_len<=2); //we require rules to be processed by the mk_simple_joins rule transformer plugin - - reg_idx single_res; - expr_ref_vector single_res_expr(m); - - //used to save on filter_identical instructions where the check is already done - //by the join operation - unsigned second_tail_arg_ofs; - - // whether to dealloc the previous result - bool dealloc = true; - - if(pt_len == 2) { - reg_idx t1_reg=tail_regs[0]; - reg_idx t2_reg=tail_regs[1]; - app * a1 = r->get_tail(0); - app * a2 = r->get_tail(1); - SASSERT(m_reg_signatures[t1_reg].size()==a1->get_num_args()); - SASSERT(m_reg_signatures[t2_reg].size()==a2->get_num_args()); - - variable_intersection a1a2(m_context.get_manager()); - a1a2.populate(a1,a2); - - unsigned_vector removed_cols; - get_local_indexes_for_projection(r, removed_cols); - - if(removed_cols.empty()) { - make_join(t1_reg, t2_reg, a1a2, single_res, acc); - } - else { - make_join_project(t1_reg, t2_reg, a1a2, removed_cols, single_res, acc); - } - - unsigned rem_index = 0; - unsigned rem_sz = removed_cols.size(); - unsigned a1len=a1->get_num_args(); - for(unsigned i=0; i=i); - if(rem_indexget_arg(i)); - } - second_tail_arg_ofs = single_res_expr.size(); - unsigned a2len=a2->get_num_args(); - for(unsigned i=0; i=i+a1len); - if(rem_indexget_arg(i)); - } - SASSERT(rem_index==rem_sz); - } - else if(pt_len==1) { - reg_idx t_reg=tail_regs[0]; - app * a = r->get_tail(0); - SASSERT(m_reg_signatures[t_reg].size()==a->get_num_args()); - - single_res = t_reg; - - unsigned n=a->get_num_args(); - for(unsigned i=0; iget_arg(i); - if(is_app(arg)) { - app * c = to_app(arg); //argument is a constant - SASSERT(c->get_num_args()==0); - SASSERT(m_context.get_decl_util().is_numeral_ext(arg)); - reg_idx new_reg; - make_select_equal_and_project(single_res, c, single_res_expr.size(), new_reg, acc); - if(single_res!=t_reg) { - //since single_res is a local register, we deallocate it - make_dealloc_non_void(single_res, acc); - } - single_res = new_reg; - } - else { - SASSERT(is_var(arg)); - single_res_expr.push_back(arg); - } - } - if(single_res==t_reg) { - dealloc = false; - } - - } - else { - SASSERT(pt_len==0); - - //single_res register should never be used in this case - single_res=execution_context::void_register; - } - - add_unbound_columns_for_negation(r, head_pred, single_res, single_res_expr, dealloc, acc); - - int2ints var_indexes; - - reg_idx filtered_res = single_res; - - { - //enforce equality to constants - unsigned srlen=single_res_expr.size(); - SASSERT((single_res==execution_context::void_register) ? (srlen==0) : (srlen==m_reg_signatures[single_res].size())); - for(unsigned i=0; iget_idx(); - int2ints::entry * e = var_indexes.insert_if_not_there2(var_num, unsigned_vector()); - e->get_data().m_value.push_back(i); - } - } - } - - //enforce equality of columns - int2ints::iterator vit=var_indexes.begin(); - int2ints::iterator vend=var_indexes.end(); - for(; vit!=vend; ++vit) { - int2ints::key_data & k = *vit; - unsigned_vector & indexes = k.m_value; - if(indexes.size()==1) { - continue; - } - SASSERT(indexes.size()>1); - if(pt_len==2 && indexes[0]=second_tail_arg_ofs) { - //If variable appears in multiple tails, the identicity will already be enforced by join. - //(If behavior the join changes so that it is not enforced anymore, remove this - //condition!) - continue; - } - if (!dealloc) - make_clone(filtered_res, filtered_res, acc); - acc.push_back(instruction::mk_filter_identical(filtered_res, indexes.size(), indexes.c_ptr())); - dealloc = true; - } - - //enforce negative predicates - unsigned ut_len=r->get_uninterpreted_tail_size(); - for(unsigned i=pt_len; iget_tail(i); - func_decl * neg_pred = neg_tail->get_decl(); - variable_intersection neg_intersection(m_context.get_manager()); - neg_intersection.populate(single_res_expr, neg_tail); - unsigned_vector t_cols(neg_intersection.size(), neg_intersection.get_cols1()); - unsigned_vector neg_cols(neg_intersection.size(), neg_intersection.get_cols2()); - - unsigned neg_len = neg_tail->get_num_args(); - for(unsigned i=0; iget_arg(i); - if(is_var(e)) { - continue; - } - SASSERT(is_app(e)); - relation_sort arg_sort; - m_context.get_rel_context().get_rmanager().from_predicate(neg_pred, i, arg_sort); - reg_idx new_reg; - bool new_dealloc; - make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, new_dealloc, acc); - - if (dealloc) - make_dealloc_non_void(filtered_res, acc); - dealloc = new_dealloc; - filtered_res = new_reg; // here filtered_res value gets changed !! - - t_cols.push_back(single_res_expr.size()); - neg_cols.push_back(i); - single_res_expr.push_back(e); - } - SASSERT(t_cols.size()==neg_cols.size()); - - reg_idx neg_reg = m_pred_regs.find(neg_pred); - if (!dealloc) - make_clone(filtered_res, filtered_res, acc); - acc.push_back(instruction::mk_filter_by_negation(filtered_res, neg_reg, t_cols.size(), - t_cols.c_ptr(), neg_cols.c_ptr())); - dealloc = true; - } - - // enforce interpreted tail predicates - unsigned ft_len=r->get_tail_size(); //full tail - for(unsigned tail_index=ut_len; tail_indexget_tail(tail_index); - ptr_vector t_vars; - ::get_free_vars(t, t_vars); - - if(t_vars.empty()) { - expr_ref simplified(m); - m_context.get_rewriter()(t, simplified); - if(m.is_true(simplified)) { - //this tail element is always true - continue; - } - //the tail of this rule is never satisfied - SASSERT(m.is_false(simplified)); - goto finish; - } - - //determine binding size - while (!t_vars.back()) { - t_vars.pop_back(); - } - unsigned max_var = t_vars.size(); - - //create binding - expr_ref_vector binding(m); - binding.resize(max_var+1); - - for(unsigned v = 0; v < t_vars.size(); ++v) { - if (!t_vars[v]) { - continue; - } - int2ints::entry * e = var_indexes.find_core(v); - if(!e) { - //we have an unbound variable, so we add an unbound column for it - relation_sort unbound_sort = t_vars[v]; - - reg_idx new_reg; - TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";); - bool new_dealloc; - make_add_unbound_column(r, 0, head_pred, filtered_res, unbound_sort, new_reg, new_dealloc, acc); - - if (dealloc) - make_dealloc_non_void(filtered_res, acc); - dealloc = new_dealloc; - filtered_res = new_reg; // here filtered_res value gets changed !! - - unsigned unbound_column_index = single_res_expr.size(); - single_res_expr.push_back(m.mk_var(v, unbound_sort)); - - e = var_indexes.insert_if_not_there2(v, unsigned_vector()); - e->get_data().m_value.push_back(unbound_column_index); - } - unsigned src_col=e->get_data().m_value.back(); - relation_sort var_sort = m_reg_signatures[filtered_res][src_col]; - binding[max_var-v]=m.mk_var(src_col, var_sort); - } - - - expr_ref renamed(m); - m_context.get_var_subst()(t, binding.size(), binding.c_ptr(), renamed); - app_ref app_renamed(to_app(renamed), m); - if (!dealloc) - make_clone(filtered_res, filtered_res, acc); - acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed)); - dealloc = true; - } - - { - //put together the columns of head relation - relation_signature & head_sig = m_reg_signatures[head_reg]; - svector head_acis; - unsigned_vector head_src_cols; - for(unsigned i=0; iget_arg(i); - if(is_var(exp)) { - unsigned var_num=to_var(exp)->get_idx(); - int2ints::entry * e = var_indexes.find_core(var_num); - if(e) { - unsigned_vector & binding_indexes = e->get_data().m_value; - aci.kind=ACK_BOUND_VAR; - aci.source_column=binding_indexes.back(); - SASSERT(aci.source_column1) { - //if possible, we do not want multiple head columns - //point to a single column in the intermediate table, - //since then we would have to duplicate the column - //(and remove columns we did not point to at all) - binding_indexes.pop_back(); - } - } - else { - aci.kind=ACK_UNBOUND_VAR; - aci.var_index=var_num; - } - } - else { - SASSERT(is_app(exp)); - SASSERT(m_context.get_decl_util().is_numeral_ext(exp)); - aci.kind=ACK_CONSTANT; - aci.constant=to_app(exp); - } - head_acis.push_back(aci); - } - SASSERT(head_acis.size()==head_len); - - reg_idx new_head_reg; - make_assembling_code(r, head_pred, filtered_res, head_acis, new_head_reg, dealloc, acc); - - //update the head relation - make_union(new_head_reg, head_reg, delta_reg, use_widening, acc); - if (dealloc) - make_dealloc_non_void(new_head_reg, acc); - } - - finish: - m_instruction_observer.finish_rule(); - } - - void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr, - bool & dealloc, instruction_block & acc) { - uint_set pos_vars; - u_map neg_vars; - ast_manager& m = m_context.get_manager(); - unsigned pt_len = r->get_positive_tail_size(); - unsigned ut_len = r->get_uninterpreted_tail_size(); - if (pt_len == ut_len || pt_len == 0) { - return; - } - // populate negative variables: - for (unsigned i = pt_len; i < ut_len; ++i) { - app * neg_tail = r->get_tail(i); - unsigned neg_len = neg_tail->get_num_args(); - for (unsigned j = 0; j < neg_len; ++j) { - expr * e = neg_tail->get_arg(j); - if (is_var(e)) { - neg_vars.insert(to_var(e)->get_idx(), e); - } - } - } - // populate positive variables: - for (unsigned i = 0; i < single_res_expr.size(); ++i) { - expr* e = single_res_expr[i].get(); - if (is_var(e)) { - pos_vars.insert(to_var(e)->get_idx()); - } - } - // add negative variables that are not in positive: - u_map::iterator it = neg_vars.begin(), end = neg_vars.end(); - for (; it != end; ++it) { - unsigned v = it->m_key; - expr* e = it->m_value; - if (!pos_vars.contains(v)) { - single_res_expr.push_back(e); - reg_idx new_single_res; - bool new_dealloc; - make_add_unbound_column(r, v, pred, single_res, m.get_sort(e), new_single_res, new_dealloc, acc); - if (dealloc) - make_dealloc_non_void(single_res, acc); - dealloc = new_dealloc; - single_res = new_single_res; - TRACE("dl", tout << "Adding unbound column: " << mk_pp(e, m) << "\n";); - } - } - } - - void compiler::compile_rule_evaluation(rule * r, const pred2idx * input_deltas, - reg_idx output_delta, bool use_widening, instruction_block & acc) { - typedef std::pair tail_delta_info; //(delta register, tail index) - typedef svector tail_delta_infos; - - unsigned rule_len = r->get_uninterpreted_tail_size(); - reg_idx head_reg = m_pred_regs.find(r->get_decl()); - - svector tail_regs; - tail_delta_infos tail_deltas; - for(unsigned j=0;jget_tail(j)->get_decl(); - reg_idx tail_reg = m_pred_regs.find(tail_pred); - tail_regs.push_back(tail_reg); - - if(input_deltas && !all_or_nothing_deltas()) { - reg_idx tail_delta_idx; - if(input_deltas->find(tail_pred, tail_delta_idx)) { - tail_deltas.push_back(tail_delta_info(tail_delta_idx, j)); - } - } - } - - if(!input_deltas || all_or_nothing_deltas()) { - compile_rule_evaluation_run(r, head_reg, tail_regs.c_ptr(), output_delta, use_widening, acc); - } - else { - tail_delta_infos::iterator tdit = tail_deltas.begin(); - tail_delta_infos::iterator tdend = tail_deltas.end(); - for(; tdit!=tdend; ++tdit) { - tail_delta_info tdinfo = *tdit; - flet flet_tail_reg(tail_regs[tdinfo.second], tdinfo.first); - compile_rule_evaluation_run(r, head_reg, tail_regs.c_ptr(), output_delta, use_widening, acc); - } - } - } - - class cycle_breaker - { - typedef func_decl * T; - 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 m_stack; - ast_mark m_visited; - - void traverse(T v) { - SASSERT(!m_visited.is_marked(v)); - if (m_removed.contains(v)) { - return; - } - - m_stack.push_back(v); - m_visited.mark(v, true); - - const item_set & deps = m_deps.get_deps(v); - item_set::iterator it = deps.begin(); - item_set::iterator end = deps.end(); - for(; it!=end; ++it) { - T d = *it; - if (m_visited.is_marked(d)) { - //TODO: find the best vertex to remove in the cycle - remove_from_stack(); - continue; - } - traverse(d); - } - SASSERT(m_stack.back()==v); - - m_stack.pop_back(); - m_visited.mark(v, false); - } - - void remove_from_stack() { - for (unsigned i = 0; i < m_stack.size(); ++i) { - func_decl* p = m_stack[i]; - if (m_context.has_facts(p)) { - m_removed.insert(p); - return; - } - - rule_vector const& rules = m_rules.get_predicate_rules(p); - unsigned stratum = m_rules.get_predicate_strat(p); - 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, 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(); - rule_dependencies::iterator end = m_deps.end(); - for(; it!=end; ++it) { - T v = it->m_key; - traverse(v); - } - m_deps.remove(m_removed); - } - }; - - void compiler::detect_chains(const func_decl_set & preds, func_decl_vector & ordered_preds, - func_decl_set & global_deltas) { - typedef obj_map pred2pred; - - SASSERT(ordered_preds.empty()); - SASSERT(global_deltas.empty()); - - rule_dependencies deps(m_rule_set.get_dependencies()); - deps.restrict(preds); - 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 - //so that all their local input deltas are already populated - func_decl_set::iterator gdit = global_deltas.begin(); - func_decl_set::iterator gend = global_deltas.end(); - for(; gdit!=gend; ++gdit) { - ordered_preds.push_back(*gdit); - } - } - - void compiler::compile_preds(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(); - for(; hpit!=hpend; ++hpit) { - func_decl * head_pred = *hpit; - - bool widen_predicate_in_loop = widened_preds.contains(head_pred); - - reg_idx d_head_reg; //output delta for the initial rule execution - if(!output_deltas.find(head_pred, d_head_reg)) { - d_head_reg = execution_context::void_register; - } - - 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(); - for(; rit!=rend; ++rit) { - rule * r = *rit; - 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 - pred2idx::iterator gdit = global_head_deltas.begin(); - pred2idx::iterator gend = global_head_deltas.end(); - for(; gdit!=gend; ++gdit) { - func_decl * pred = gdit->m_key; - reg_idx head_reg = gdit->m_value; - reg_idx tail_reg = global_tail_deltas.find(pred); - acc.push_back(instruction::mk_move(head_reg, tail_reg)); - } - //empty local deltas - pred2idx::iterator lit = local_deltas.begin(); - pred2idx::iterator lend = local_deltas.end(); - for(; lit!=lend; ++lit) { - acc.push_back(instruction::mk_dealloc(lit->m_value)); - } - } - - void compiler::compile_loop(const func_decl_vector & head_preds, const func_decl_set & widened_preds, - const pred2idx & global_head_deltas, const pred2idx & global_tail_deltas, - const pred2idx & local_deltas, instruction_block & acc) { - instruction_block * loop_body = alloc(instruction_block); - loop_body->set_observer(&m_instruction_observer); - - pred2idx all_head_deltas(global_head_deltas); - unite_disjoint_maps(all_head_deltas, local_deltas); - pred2idx all_tail_deltas(global_tail_deltas); - unite_disjoint_maps(all_tail_deltas, local_deltas); - - //generate code for the iterative fixpoint search - //The order in which we iterate the preds_vector matters, since rules can depend on - //deltas generated earlier in the same iteration. - compile_preds(head_preds, widened_preds, &all_tail_deltas, all_head_deltas, *loop_body); - - svector loop_control_regs; //loop is controlled by global src regs - collect_map_range(loop_control_regs, global_tail_deltas); - //move target deltas into source deltas at the end of the loop - //and clear local deltas - make_inloop_delta_transition(global_head_deltas, global_tail_deltas, local_deltas, *loop_body); - - loop_body->set_observer(0); - acc.push_back(instruction::mk_while_loop(loop_control_regs.size(), - loop_control_regs.c_ptr(), loop_body)); - } - - void compiler::compile_dependent_rules(const func_decl_set & head_preds, - const pred2idx * input_deltas, const pred2idx & output_deltas, - bool add_saturation_marks, instruction_block & acc) { - - if (!output_deltas.empty()) { - func_decl_set::iterator hpit = head_preds.begin(); - func_decl_set::iterator hpend = head_preds.end(); - for(; hpit!=hpend; ++hpit) { - if(output_deltas.contains(*hpit)) { - //we do not support retrieving deltas for rules that are inside a recursive - //stratum, since we would have to maintain this 'global' delta through the loop - //iterations - NOT_IMPLEMENTED_YET(); - } - } - } - - func_decl_vector preds_vector; - func_decl_set global_deltas; - - detect_chains(head_preds, preds_vector, global_deltas); - - func_decl_set local_deltas(head_preds); - set_difference(local_deltas, global_deltas); - - pred2idx d_global_src; //these deltas serve as sources of tuples for rule evaluation inside the loop - get_fresh_registers(global_deltas, d_global_src); - pred2idx d_global_tgt; //these deltas are targets for new tuples in rule evaluation inside the loop - get_fresh_registers(global_deltas, d_global_tgt); - pred2idx d_local; - get_fresh_registers(local_deltas, d_local); - - pred2idx d_all_src(d_global_src); //src together with local deltas - unite_disjoint_maps(d_all_src, d_local); - pred2idx d_all_tgt(d_global_tgt); //tgt together with local deltas - unite_disjoint_maps(d_all_tgt, d_local); - - - 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_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); - } - else { - compile_loop(preds_vector, empty_func_decl_set, d_global_tgt, d_global_src, d_local, acc); - } - - - if(add_saturation_marks) { - //after the loop finishes, all predicates in the group are saturated, - //so we may mark them as such - func_decl_set::iterator fdit = head_preds.begin(); - func_decl_set::iterator fdend = head_preds.end(); - for(; fdit!=fdend; ++fdit) { - acc.push_back(instruction::mk_mark_saturated(m_context.get_manager(), *fdit)); - } - } - } - - bool compiler::is_nonrecursive_stratum(const func_decl_set & preds) const { - SASSERT(preds.size()>0); - if(preds.size()>1) { - return false; - } - func_decl * head_pred = *preds.begin(); - const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred); - rule_vector::const_iterator it = rules.begin(); - rule_vector::const_iterator end = rules.end(); - for(; it!=end; ++it) { - //it is sufficient to check just for presence of the first head predicate, - //since if the rules are recursive and their heads are strongly connected by dependence, - //this predicate must appear in some tail - if((*it)->is_in_tail(head_pred)) { - return false; - } - } - return true; - } - - void compiler::compile_nonrecursive_stratum(const func_decl_set & preds, - const pred2idx * input_deltas, const pred2idx & output_deltas, - bool add_saturation_marks, instruction_block & acc) { - //non-recursive stratum always has just one head predicate - SASSERT(preds.size()==1); - SASSERT(is_nonrecursive_stratum(preds)); - func_decl * head_pred = *preds.begin(); - const rule_vector & rules = m_rule_set.get_predicate_rules(head_pred); - - - - reg_idx output_delta; - if (!output_deltas.find(head_pred, output_delta)) { - output_delta = execution_context::void_register; - } - - rule_vector::const_iterator it = rules.begin(); - rule_vector::const_iterator end = rules.end(); - for (; it != end; ++it) { - rule * r = *it; - SASSERT(r->get_decl()==head_pred); - - compile_rule_evaluation(r, input_deltas, output_delta, false, acc); - } - - if (add_saturation_marks) { - //now the predicate is saturated, so we may mark it as such - acc.push_back(instruction::mk_mark_saturated(m_context.get_manager(), head_pred)); - } - } - - bool compiler::all_saturated(const func_decl_set & preds) const { - func_decl_set::iterator fdit = preds.begin(); - func_decl_set::iterator fdend = preds.end(); - for(; fdit!=fdend; ++fdit) { - if(!m_context.get_rel_context().get_rmanager().is_saturated(*fdit)) { - return false; - } - } - return true; - } - - void compiler::compile_strats(const rule_stratifier & stratifier, - const pred2idx * input_deltas, const pred2idx & output_deltas, - bool add_saturation_marks, instruction_block & acc) { - rule_set::pred_set_vector strats = stratifier.get_strats(); - rule_set::pred_set_vector::const_iterator sit = strats.begin(); - rule_set::pred_set_vector::const_iterator send = strats.end(); - for(; sit!=send; ++sit) { - func_decl_set & strat_preds = **sit; - - if (all_saturated(strat_preds)) { - //all predicates in stratum are saturated, so no need to compile rules for them - continue; - } - - TRACE("dl", - tout << "Stratum: "; - func_decl_set::iterator pit = strat_preds.begin(); - func_decl_set::iterator pend = strat_preds.end(); - for(; pit!=pend; ++pit) { - func_decl * pred = *pit; - tout << pred->get_name() << " "; - } - tout << "\n"; - ); - - if (is_nonrecursive_stratum(strat_preds)) { - //this stratum contains just a single non-recursive rule - compile_nonrecursive_stratum(strat_preds, input_deltas, output_deltas, add_saturation_marks, acc); - } - else { - compile_dependent_rules(strat_preds, input_deltas, output_deltas, - add_saturation_marks, acc); - } - } - } - - void compiler::do_compilation(instruction_block & execution_code, - instruction_block & termination_code) { - - unsigned rule_cnt=m_rule_set.get_num_rules(); - if(rule_cnt==0) { - return; - } - - instruction_block & acc = execution_code; - acc.set_observer(&m_instruction_observer); - - - //load predicate data - for(unsigned i=0;iget_decl(), acc); - - unsigned rule_len = r->get_uninterpreted_tail_size(); - for(unsigned j=0;jget_tail(j)->get_decl(), acc); - } - } - - pred2idx empty_pred2idx_map; - - compile_strats(m_rule_set.get_stratifier(), static_cast(0), - empty_pred2idx_map, true, execution_code); - - - - //store predicate data - pred2idx::iterator pit = m_pred_regs.begin(); - pred2idx::iterator pend = m_pred_regs.end(); - for(; pit!=pend; ++pit) { - pred2idx::key_data & e = *pit; - func_decl * pred = e.m_key; - reg_idx reg = e.m_value; - termination_code.push_back(instruction::mk_store(m_context.get_manager(), pred, reg)); - } - - acc.set_observer(0); - - TRACE("dl", execution_code.display(m_context.get_rel_context(), tout);); - } - - -} - From 9c230941cc4179ec5aa9a73b3b928bce16f47d4d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 23 Apr 2013 12:01:50 -0700 Subject: [PATCH 4/5] [datalog] improve performance of smt2 frontend - delay calls to make_annotations and process_costs untill needed - remove debug exception handler in join() Signed-off-by: Nuno Lopes --- src/muz_qe/dl_instruction.cpp | 16 +--------------- src/muz_qe/rel_context.cpp | 9 +++++---- src/muz_qe/rel_context.h | 2 +- 3 files changed, 7 insertions(+), 20 deletions(-) diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp index 296fa95f3..b103d743e 100644 --- a/src/muz_qe/dl_instruction.cpp +++ b/src/muz_qe/dl_instruction.cpp @@ -359,21 +359,7 @@ namespace datalog { r2.get_signature().output(ctx.get_rel_context().get_manager(), tout); tout<<":"<\n";); - try { - ctx.set_reg(m_res, (*fn)(r1, r2)); - } - catch(...) - { - std::string annotation; - unsigned sz; - ctx.get_register_annotation(m_rel1, annotation); - sz = ctx.reg(m_rel1)?ctx.reg(m_rel1)->get_size_estimate_rows():0; - std::cout << m_rel1 << "\t" << sz << "\t" << annotation << "\n"; - ctx.get_register_annotation(m_rel2, annotation); - sz = ctx.reg(m_rel2)?ctx.reg(m_rel2)->get_size_estimate_rows():0; - std::cout << m_rel2 << "\t" << sz << "\t" << annotation << "\n"; - throw; - } + ctx.set_reg(m_res, (*fn)(r1, r2)); TRACE("dl", ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout); diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp index ef5639279..731ab8b63 100644 --- a/src/muz_qe/rel_context.cpp +++ b/src/muz_qe/rel_context.cpp @@ -179,9 +179,7 @@ namespace datalog { scoped_query.reset(); } m_context.record_transformed_rules(); - TRACE("dl", m_ectx.report_big_relations(100, tout);); - m_code.process_all_costs(); - m_code.make_annotations(m_ectx); + TRACE("dl", display_profile(tout);); return result; } @@ -480,7 +478,10 @@ namespace datalog { get_rmanager().display(out); } - void rel_context::display_profile(std::ostream& out) const { + void rel_context::display_profile(std::ostream& out) { + m_code.make_annotations(m_ectx); + m_code.process_all_costs(); + out << "\n--------------\n"; out << "Instructions\n"; m_code.display(*this, out); diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h index 3e019cb50..8e4c6f2de 100644 --- a/src/muz_qe/rel_context.h +++ b/src/muz_qe/rel_context.h @@ -105,7 +105,7 @@ namespace datalog { void display_output_facts(rule_set const& rules, std::ostream & out) const; void display_facts(std::ostream & out) const; - void display_profile(std::ostream& out) const; + void display_profile(std::ostream& out); lbool saturate(); From f58e8e961dfd09181407d7be90c8498678c04859 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 23 Apr 2013 14:59:19 -0700 Subject: [PATCH 5/5] fix the build Signed-off-by: Nuno Lopes --- src/muz_qe/dl_mk_filter_rules.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/muz_qe/dl_mk_filter_rules.cpp b/src/muz_qe/dl_mk_filter_rules.cpp index 8ab8412c0..932a644ab 100644 --- a/src/muz_qe/dl_mk_filter_rules.cpp +++ b/src/muz_qe/dl_mk_filter_rules.cpp @@ -152,9 +152,6 @@ namespace datalog { } rule_set * mk_filter_rules::operator()(rule_set const & source) { - if (!m_context.get_params().filter_rules()) { - return 0; - } m_tail2filter.reset(); m_result = alloc(rule_set, m_context); m_modified = false;