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

Datalog: fix bug with the following 2 scenarios:

Browse source 
A(#x00) :- not B().
A() :- not B().

The first case can be further optimized, but committing this for correctness

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-02-02 11:29:49 +00:00
parent 2444440edc
commit 5548ecc853
1 changed files with 10 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -631,6 +631,16 @@ namespace datalog {
} }
} }
// add at least one column for the negative filter
if (pt_len != ut_len && filtered_res == execution_context::void_register) {
relation_signature & head_sig = m_reg_signatures[head_reg];
if (head_sig.empty()) {
make_full_relation(head_pred, m_reg_signatures[head_reg], filtered_res, acc);
} else {
make_add_unbound_column(r, 0, head_pred, filtered_res, head_sig[0], filtered_res, dealloc, acc);
}
}
//enforce negative predicates //enforce negative predicates
for (unsigned i = pt_len; i<ut_len; i++) { for (unsigned i = pt_len; i<ut_len; i++) {
app * neg_tail = r->get_tail(i); app * neg_tail = r->get_tail(i);