mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Datalog: fix bug in compilation of negated queries that referenced vars not in the head.

Browse source 
We will now first add unbounded columns for negation and for filtering
do filter_negation, and finally filter_interpret(_project)
This commit is contained in:
Nuno Lopes 2015-01-27 14:21:34 +00:00
parent 83bae6c8aa
commit 9e447281ed
1 changed files with 49 additions and 46 deletions
Download patch file Download diff file Expand all files Collapse all files

95
src/muz/rel/dl_compiler.cpp
View file

@ -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<expr> 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<sort> 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; i<ut_len; i++) {
app * neg_tail = r->get_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; i<neg_len; i++) {
expr * e = neg_tail->get_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; i<ut_len; i++) {
app * neg_tail = r->get_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; i<neg_len; i++) {
expr * e = neg_tail->get_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