mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

DoC: fix bug filter_by_negation when negation table has 0 columns

Browse source 
Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
This commit is contained in:
Nuno Lopes 2015-01-27 13:42:14 +00:00
parent 6ab167f0c7
commit 83bae6c8aa
1 changed files with 16 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/muz/rel/udoc_relation.cpp
View file

@ -1090,7 +1090,7 @@ namespace datalog {
mk_remove_cols m_mk_remove_cols; mk_remove_cols m_mk_remove_cols;
join_project_fn m_join_project; join_project_fn m_join_project;
bool m_is_subtract; bool m_is_subtract;
bool m_is_aliased; //bool m_is_aliased;
public: public:
negation_filter_fn(const udoc_relation & t, const udoc_relation & neg, unsigned joined_col_cnt, negation_filter_fn(const udoc_relation & t, const udoc_relation & neg, unsigned joined_col_cnt,
const unsigned *t_cols, const unsigned *neg_cols) const unsigned *t_cols, const unsigned *neg_cols)
@ -1099,9 +1099,9 @@ namespace datalog {
m_mk_remove_cols(t, neg, m_remove_cols), m_mk_remove_cols(t, neg, m_remove_cols),
m_join_project(t, neg, joined_col_cnt, t_cols, neg_cols, m_join_project(t, neg, joined_col_cnt, t_cols, neg_cols,
m_remove_cols.size(), m_remove_cols.c_ptr()), m_remove_cols.size(), m_remove_cols.c_ptr()),
m_is_subtract(false), m_is_subtract(false)//,
m_is_aliased(true) { /*m_is_aliased(true) */{
SASSERT(joined_col_cnt > 0); SASSERT(joined_col_cnt > 0 || neg.get_signature().size() == 0);
m_is_subtract = (joined_col_cnt == t.get_signature().size()); m_is_subtract = (joined_col_cnt == t.get_signature().size());
m_is_subtract &= (joined_col_cnt == neg.get_signature().size()); m_is_subtract &= (joined_col_cnt == neg.get_signature().size());
svector<bool> found(joined_col_cnt, false); svector<bool> found(joined_col_cnt, false);
@ -1119,20 +1119,24 @@ namespace datalog {
udoc_plugin& p = t.get_plugin(); udoc_plugin& p = t.get_plugin();
IF_VERBOSE(3, t.display(verbose_stream() << "dst:");); IF_VERBOSE(3, t.display(verbose_stream() << "dst:"););
IF_VERBOSE(3, n.display(verbose_stream() << "neg:");); IF_VERBOSE(3, n.display(verbose_stream() << "neg:"););
if (!m_is_aliased && !t.fast_empty() && !n.fast_empty() && !p.m_disable_fast_pass) { if (t.fast_empty() || n.fast_empty())
return;
/* TODO: double check
if (!m_is_aliased && !p.m_disable_fast_pass) {
// fast_pass(t, n); // fast_pass(t, n);
} }
if (m_is_subtract && !t.fast_empty() && !n.fast_empty()) { */
if (n.get_signature().size() == 0)
t.get_udoc().reset(t.get_dm());
else if (m_is_subtract)
t.get_udoc().subtract(t.get_dm(), n.get_udoc()); t.get_udoc().subtract(t.get_dm(), n.get_udoc());
return; else
}
if (!t.fast_empty() && !n.fast_empty()) {
slow_pass(t, n); slow_pass(t, n);
} }
}
private: private:
/*
void fast_pass(udoc_relation& t, const udoc_relation& n) { void fast_pass(udoc_relation& t, const udoc_relation& n) {
SASSERT(!m_is_aliased); SASSERT(!m_is_aliased);
udoc & dst = t.get_udoc(); udoc & dst = t.get_udoc();
@ -1154,6 +1158,7 @@ namespace datalog {
} }
std::swap(dst, result); std::swap(dst, result);
} }
*/
void slow_pass(udoc_relation& t, udoc_relation const& n) { void slow_pass(udoc_relation& t, udoc_relation const& n) {
doc_manager& dmt = t.get_dm(); doc_manager& dmt = t.get_dm();