From db653a6e686da6cd0ca8bf7f291a099c976ccced Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 22 Apr 2013 09:05:27 -0700 Subject: [PATCH] [datalog] merge changes from the hassel branch Signed-off-by: Nuno Lopes --- src/muz_qe/dl_check_table.h | 9 ----- src/muz_qe/dl_compiler.cpp | 53 ++++++++++-------------------- src/muz_qe/dl_compiler.h | 2 +- src/muz_qe/dl_context.cpp | 9 ++++- src/muz_qe/dl_relation_manager.cpp | 1 - src/muz_qe/dl_util.h | 2 ++ 6 files changed, 29 insertions(+), 47 deletions(-) diff --git a/src/muz_qe/dl_check_table.h b/src/muz_qe/dl_check_table.h index 7126bde66..40a3d5207 100644 --- a/src/muz_qe/dl_check_table.h +++ b/src/muz_qe/dl_check_table.h @@ -89,15 +89,6 @@ namespace datalog { class check_table : public table_base { friend class check_table_plugin; - friend class check_table_plugin::join_fn; - friend class check_table_plugin::union_fn; - friend class check_table_plugin::transformer_fn; - friend class check_table_plugin::rename_fn; - friend class check_table_plugin::project_fn; - friend class check_table_plugin::filter_equal_fn; - friend class check_table_plugin::filter_identical_fn; - friend class check_table_plugin::filter_interpreted_fn; - friend class check_table_plugin::filter_by_negation_fn; table_base* m_checker; table_base* m_tocheck; diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp index 80b9dee5a..34dd94214 100644 --- a/src/muz_qe/dl_compiler.cpp +++ b/src/muz_qe/dl_compiler.cpp @@ -421,6 +421,7 @@ namespace datalog { 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(); @@ -433,7 +434,7 @@ namespace datalog { SASSERT(pt_len<=2); //we require rules to be processed by the mk_simple_joins rule transformer plugin reg_idx single_res; - ptr_vector single_res_expr; + expr_ref_vector single_res_expr(m); //used to save on filter_identical instructions where the check is already done //by the join operation @@ -536,7 +537,7 @@ namespace datalog { 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_tail_size(); //full tail for(unsigned tail_index=ut_len; tail_indexget_tail(tail_index); - var_idx_set t_vars; - ast_manager & m = m_context.get_manager(); - collect_vars(m, t, t_vars); - + ptr_vector t_vars; + ::get_free_vars(t, t_vars); + if(t_vars.empty()) { expr_ref simplified(m); m_context.get_rewriter()(t, simplified); @@ -639,40 +639,23 @@ namespace datalog { } //determine binding size - unsigned max_var=0; - var_idx_set::iterator vit = t_vars.begin(); - var_idx_set::iterator vend = t_vars.end(); - for(; vit!=vend; ++vit) { - unsigned v = *vit; - if(v>max_var) { max_var = v; } + 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); - vit = t_vars.begin(); - for(; vit!=vend; ++vit) { - unsigned v = *vit; + + 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 = 0; - - for(unsigned hindex = 0; hindexget_arg(hindex); - if(!is_var(harg) || to_var(harg)->get_idx()!=v) { - continue; - } - unbound_sort = to_var(harg)->get_sort(); - } - if(!unbound_sort) { - // the variable in the interpreted tail is neither bound in the - // uninterpreted tail nor present in the head - std::stringstream sstm; - sstm << "rule with unbound variable #" << v << " in interpreted tail: "; - r->display(m_context, sstm); - throw default_exception(sstm.str()); - } + relation_sort unbound_sort = t_vars[v]; reg_idx new_reg; TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";); @@ -759,7 +742,7 @@ namespace datalog { m_instruction_observer.finish_rule(); } - void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, ptr_vector& single_res_expr, + 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; @@ -782,7 +765,7 @@ namespace datalog { } // populate positive variables: for (unsigned i = 0; i < single_res_expr.size(); ++i) { - expr* e = single_res_expr[i]; + expr* e = single_res_expr[i].get(); if (is_var(e)) { pos_vars.insert(to_var(e)->get_idx()); } diff --git a/src/muz_qe/dl_compiler.h b/src/muz_qe/dl_compiler.h index 1dfb7c7d8..e5b62f54b 100644 --- a/src/muz_qe/dl_compiler.h +++ b/src/muz_qe/dl_compiler.h @@ -177,7 +177,7 @@ namespace datalog { void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, instruction_block & acc); - void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, ptr_vector& single_res_expr, + void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr, bool & dealloc, instruction_block& acc); void make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, instruction_block & acc); diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index df293aeba..8ac32f4a7 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -823,7 +823,14 @@ namespace datalog { if (similarity_compressor()) { m_transf.register_plugin(alloc(mk_similarity_compressor, *this)); } - m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this)); + m_transf.register_plugin(alloc(mk_partial_equivalence_transformer, *this)); + m_transf.register_plugin(alloc(mk_rule_inliner, *this)); + m_transf.register_plugin(alloc(mk_interp_tail_simplifier, *this)); + + if (get_params().bit_blast()) { + m_transf.register_plugin(alloc(mk_bit_blast, *this, 22000)); + m_transf.register_plugin(alloc(mk_interp_tail_simplifier, *this, 21000)); + } transform_rules(m_transf); } diff --git a/src/muz_qe/dl_relation_manager.cpp b/src/muz_qe/dl_relation_manager.cpp index ef8e6ddd4..986a1f2c4 100644 --- a/src/muz_qe/dl_relation_manager.cpp +++ b/src/muz_qe/dl_relation_manager.cpp @@ -740,7 +740,6 @@ namespace datalog { relation_transformer_fn * relation_manager::mk_select_equal_and_project_fn(const relation_base & t, const relation_element & value, unsigned col) { relation_transformer_fn * res = t.get_plugin().mk_select_equal_and_project_fn(t, value, col); - TRACE("dl", tout << t.get_plugin().get_name() << " " << value << " " << col << "\n";); if(!res) { relation_mutator_fn * selector = mk_filter_equal_fn(t, value, col); if(selector) { diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index 974ab5862..2da0463e8 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -207,7 +207,9 @@ namespace datalog { static unsigned expr_cont_get_size(app * a) { return a->get_num_args(); } static expr * expr_cont_get(app * a, unsigned i) { return a->get_arg(i); } static unsigned expr_cont_get_size(const ptr_vector & v) { return v.size(); } + static unsigned expr_cont_get_size(const expr_ref_vector & v) { return v.size(); } static expr * expr_cont_get(const ptr_vector & v, unsigned i) { return v[i]; } + static expr * expr_cont_get(const expr_ref_vector & v, unsigned i) { return v[i]; } public: variable_intersection(ast_manager & m) : m_consts(m) {}