diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 4d1fdf1d2..1c7a78b09 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -1067,14 +1067,23 @@ namespace datalog { class udoc_plugin::negation_filter_fn : public relation_intersection_filter_fn { unsigned_vector m_t_cols; unsigned_vector m_neg_cols; + unsigned_vector m_remove_cols; + join_fn joiner; public: negation_filter_fn(const udoc_relation & r, const udoc_relation & neg, unsigned joined_col_cnt, const unsigned *t_cols, const unsigned *neg_cols) - : m_t_cols(joined_col_cnt, t_cols), m_neg_cols(joined_col_cnt, neg_cols) { + : m_t_cols(joined_col_cnt, t_cols), m_neg_cols(joined_col_cnt, neg_cols), + joiner(r.get_plugin(), r, neg, joined_col_cnt, t_cols, neg_cols) { SASSERT(joined_col_cnt > 0); r.expand_column_vector(m_t_cols); neg.expand_column_vector(m_neg_cols); + + unsigned num_neg_cols = get(neg).get_num_cols(); + unsigned num_r_cols = get(r).get_num_cols(); + for (unsigned i = 0; i < num_neg_cols; ++i) { + m_remove_cols.push_back(num_r_cols + i); + } } virtual void operator()(relation_base& tb, const relation_base& negb) { @@ -1092,6 +1101,8 @@ namespace datalog { } void fast_pass(udoc_relation& t, const udoc_relation& n) { + /* + // FIXME: this code doesn't take aliased columns into account udoc & dst = t.get_udoc(); udoc const & neg = n.get_udoc(); doc_manager& dmt = t.get_dm(); @@ -1110,83 +1121,26 @@ namespace datalog { result.push_back(&dst[i]); } std::swap(dst, result); + */ } void slow_pass(udoc_relation& t, udoc_relation const& n) { udoc & dst = t.get_udoc(); - udoc const & neg = n.get_udoc(); doc_manager& dmt = t.get_dm(); - doc_manager& dmn = n.get_dm(); - udoc renamed_neg; - for (unsigned i = 0; i < neg.size(); ++i) { - doc& neg_i = neg[i]; - doc_ref newD(dmt, dmt.allocateX()); - if (!copy_columns(newD->pos(), neg_i.pos(), t, n)) - continue; + udoc_relation *joined = get(joiner(t, n)); + if (joined->fast_empty()) { + return; + } + + project_fn projector(*joined, m_remove_cols.size(), m_remove_cols.c_ptr()); + udoc_relation *neg_projected = get(projector(*joined)); + joined->deallocate(); - bool is_empty = false; - for (unsigned j = 0; !is_empty && j < neg_i.neg().size(); ++j) { - tbv_ref newT(dmt.tbvm(), dmt.tbvm().allocateX()); - if (!copy_columns(*newT, neg_i.neg()[j], t, n) || - !dmt.tbvm().set_and(*newT, newD->pos())) { - continue; - } - if (dmt.tbvm().equals(newD->pos(), *newT)) { - is_empty = true; - } - else { - newD->neg().push_back(newT.detach()); - } - } - if (!is_empty) { - IF_VERBOSE(3, - dmn.display(verbose_stream() << "copy neg: ", neg_i) << "\n"; - dmt.display(verbose_stream() << "to dst: ", *newD) << "\n";); - renamed_neg.push_back(newD.detach()); - } - } TRACE("doc", dst.display(dmt, tout) << "\n"; - renamed_neg.display(dmt, tout) << "\n"; + neg_projected->get_udoc().display(dmt, tout) << "\n"; ); - dst.subtract(dmt, renamed_neg); - // TBD: double check semantics - TRACE("doc", dst.display(dmt, tout) << "\n";); - SASSERT(dst.well_formed(dmt)); - renamed_neg.reset(dmt); - IF_VERBOSE(3, t.display(verbose_stream() << "slow case:");); - } - - bool copy_columns( - tbv& dst, tbv const& src, - udoc_relation const& dstt, - udoc_relation const& srct) - { - unsigned num_cols = m_t_cols.size(); - for (unsigned i = 0; i < num_cols; ++i) { - if (!copy_column(dst, src, m_t_cols[i], m_neg_cols[i], dstt, srct)) - return false; - } - return true; - } - bool copy_column( - tbv& dst, tbv const& src, - unsigned col_dst, unsigned col_src, - udoc_relation const& dstt, - udoc_relation const& srct) { - tbv_manager& dm = dstt.get_dm().tbvm(); - unsigned idx_dst = dstt.column_idx(col_dst); - unsigned idx_src = srct.column_idx(col_src); - unsigned num_tbits = dstt.column_num_bits(col_dst); - SASSERT(num_tbits == srct.column_num_bits(col_src)); - IF_VERBOSE(3, verbose_stream() << "copy column " << idx_src - << " to " << idx_dst << " " << num_tbits << "\n";); - for (unsigned i = 0; i < num_tbits; ++i) { - tbit bit = (tbit)(dst[idx_dst + i] & src[idx_src + i]); - if (bit == BIT_z) - return false; - dm.set(dst, idx_dst + i, bit); - } - return true; + dst.subtract(dmt, neg_projected->get_udoc()); + neg_projected->deallocate(); } }; diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 31908a41d..3fc727d14 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -146,8 +146,8 @@ public: test_filter_neg4(false); test_filter_neg4(true); - test_filter_neg6(false); - test_filter_neg6(true); + test_filter_neg5(false); + test_filter_neg5(true); test_filter_neg(); test_filter_neg2(); @@ -657,6 +657,10 @@ public: if (disable_fast) p.disable_fast_pass(); apply_filter_neg(*tgt, *neg, cols1, cols2); tgt->deallocate(); + + tgt = mk_full(sig1); + apply_filter_neg(*neg, *tgt, cols2, cols1); + tgt->deallocate(); neg->deallocate(); } @@ -675,7 +679,6 @@ public: cols2.push_back(2); cols3.push_back(0); cols3.push_back(1); - cols3.push_back(2); udoc_relation* tgt = mk_full(sig1); udoc_relation* neg = mk_full(sig2); rel_mut filter_id = p.mk_filter_identical_fn(*tgt, cols3.size(), cols3.c_ptr()); @@ -686,9 +689,6 @@ public: neg->deallocate(); } - // TBD: unit test to expose similar bug as projection had. - // you can't just remove columns when there are side-constraints in neg. - void set_random(udoc_relation& r, unsigned num_vals) { unsigned num_bits = r.get_dm().num_tbits(); udoc_relation* full = mk_full(r.get_signature());