From 5548ecc853eaf1b1ea6a09e6bea10f47500d08da Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 2 Feb 2015 11:29:49 +0000 Subject: [PATCH] Datalog: fix bug with the following 2 scenarios: A(#x00) :- not B(). A() :- not B(). The first case can be further optimized, but committing this for correctness Signed-off-by: Nuno Lopes --- src/muz/rel/dl_compiler.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 42805d1a4..860add434 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -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 for (unsigned i = pt_len; iget_tail(i);