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: optimize previous commit

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

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

@ -633,12 +633,8 @@ 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);
}
relation_signature empty_signature;
make_full_relation(head_pred, empty_signature, filtered_res, acc);
}
//enforce negative predicates