From 9e447281ed6b3eefe3e6a03f961222d274742243 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 27 Jan 2015 14:21:34 +0000 Subject: [PATCH] Datalog: fix bug in compilation of negated queries that referenced vars not in the head. We will now first add unbounded columns for negation and for filtering do filter_negation, and finally filter_interpret(_project) --- src/muz/rel/dl_compiler.cpp | 95 +++++++++++++++++++------------------ 1 file changed, 49 insertions(+), 46 deletions(-) diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index d3d0501e7..d73f8c4ad 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -609,7 +609,8 @@ namespace datalog { dealloc = true; } - // enforce interpreted tail predicates + + // add unbounded columns for interpreted filter unsigned ut_len = r->get_uninterpreted_tail_size(); unsigned ft_len = r->get_tail_size(); // full tail ptr_vector tail; @@ -617,15 +618,12 @@ namespace datalog { tail.push_back(r->get_tail(tail_index)); } + expr_ref_vector binding(m); if (!tail.empty()) { app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail.size(), tail.c_ptr()), m); - ptr_vector filter_vars; m_free_vars(filter_cond); - // create binding - expr_ref_vector binding(m); binding.resize(m_free_vars.size()+1); - for (unsigned v = 0; v < m_free_vars.size(); ++v) { if (!m_free_vars[v]) continue; @@ -655,6 +653,52 @@ namespace datalog { relation_sort var_sort = m_reg_signatures[filtered_res][src_col]; binding[m_free_vars.size()-v] = m.mk_var(src_col, var_sort); } + } + + //enforce negative predicates + 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; + + 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 + if (!tail.empty()) { + app_ref filter_cond(tail.size() == 1 ? to_app(tail.back()) : m.mk_and(tail.size(), tail.c_ptr()), m); // check if there are any columns to remove unsigned_vector remove_columns; @@ -716,47 +760,6 @@ namespace datalog { dealloc = true; } - //enforce negative predicates - 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; - } - #if 0 // this version is potentially better for non-symbolic tables, // since it constraints each unbound column at a time (reducing the