From 9828b26379013990df2702ebdf15ccfd1c9514e7 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 2 Oct 2014 09:56:06 +0100 Subject: [PATCH 1/3] DoC: fix slow path of filter_by_negation when columns are repeated in tgt relation Signed-off-by: Nuno Lopes --- src/muz/rel/check_relation.cpp | 2 +- src/muz/rel/udoc_relation.cpp | 25 ++++++++++++++++++------- src/test/udoc_relation.cpp | 34 ++++++++++++++++++++++++++++++++++ 3 files changed, 53 insertions(+), 8 deletions(-) diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index a526ffc1b..46d1171d0 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -661,7 +661,7 @@ namespace datalog { expr_ref_vector eqs(m); dst.to_formula(dstf); std::cout << mk_pp(dstf, m) << "\n"; - dst.to_formula(negf); + neg.to_formula(negf); std::cout << mk_pp(negf, m) << "\n"; eqs.push_back(negf); for (unsigned i = 0; i < cols1.size(); ++i) { diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 10c01ccdd..269780a94 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -1110,11 +1110,16 @@ namespace datalog { for (unsigned i = 0; i < neg.size(); ++i) { doc& neg_i = neg[i]; doc_ref newD(dmt, dmt.allocateX()); - copy_columns(newD->pos(), neg_i.pos(), t, n); + if (!copy_columns(newD->pos(), neg_i.pos(), t, n)) + continue; + bool is_empty = false; for (unsigned j = 0; !is_empty && j < neg_i.neg().size(); ++j) { tbv_ref newT(dmt.tbvm(), dmt.tbvm().allocateX()); - copy_columns(*newT, neg_i.neg()[j], t, n); + 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; } @@ -1139,17 +1144,19 @@ namespace datalog { renamed_neg.reset(dmt); IF_VERBOSE(3, tb.display(verbose_stream() << "slow case:");); } - void copy_columns( + 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) { - copy_column(dst, src, m_t_cols[i], m_neg_cols[i], dstt, srct); + if (!copy_column(dst, src, m_t_cols[i], m_neg_cols[i], dstt, srct)) + return false; } + return true; } - void copy_column( + bool copy_column( tbv& dst, tbv const& src, unsigned col_dst, unsigned col_src, udoc_relation const& dstt, @@ -1162,8 +1169,12 @@ namespace datalog { IF_VERBOSE(3, verbose_stream() << "copy column " << idx_src << " to " << idx_dst << " " << num_tbits << "\n";); for (unsigned i = 0; i < num_tbits; ++i) { - dm.set(dst, idx_dst + i, src[idx_src + 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; } }; diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 9824c481d..26858c12c 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -149,6 +149,7 @@ public: test_rename(); test_filter_neg(); test_filter_neg2(); + test_filter_neg3(); // empty @@ -601,6 +602,39 @@ public: t2->deallocate(); } + void test_filter_neg3() { + // filter_by_negation + relation_signature sig; + sig.push_back(bv.mk_sort(1)); + sig.push_back(bv.mk_sort(1)); + sig.push_back(bv.mk_sort(1)); + unsigned_vector cols1, cols2; + + cols1.push_back(0); + cols1.push_back(0); + cols2.push_back(0); + cols2.push_back(1); + + /// 1xx + udoc_relation* t1 = mk_full(sig); + { + doc& d = t1->get_udoc()[0]; + t1->get_dm().set(d, 0, BIT_1); + } + + /// 10x + udoc_relation* t2 = mk_full(sig); + { + doc& d = t2->get_udoc()[0]; + t1->get_dm().set(d, 0, BIT_1); + t1->get_dm().set(d, 1, BIT_0); + } + + apply_filter_neg(*t1, *t2, cols1, cols2); + t1->deallocate(); + t2->deallocate(); + } + 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()); From 7d599fa047e20172cdcba36d6d4049b11c20bb86 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 2 Oct 2014 11:54:53 +0100 Subject: [PATCH 2/3] DoC: fix bug I previously introduced in insert Signed-off-by: Nuno Lopes --- src/muz/rel/doc.h | 1 - 1 file changed, 1 deletion(-) diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h index 75b4e9499..5fdfe6297 100644 --- a/src/muz/rel/doc.h +++ b/src/muz/rel/doc.h @@ -174,7 +174,6 @@ public: for ( ; i < sz; ++i, ++j) { if (m.contains(*m_elems[i], *t)) { found = true; - break; } if (m.contains(*t, *m_elems[i])) { m.deallocate(m_elems[i]); From e778f3e65b0d91712dc3e4c2069e32aa20ec8d2a Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 2 Oct 2014 12:49:38 +0100 Subject: [PATCH 3/3] DoC: fix bug in insertion when inserting an element equal to on on the disjunction already Signed-off-by: Nuno Lopes --- src/muz/rel/doc.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h index 5fdfe6297..2a4b3ead7 100644 --- a/src/muz/rel/doc.h +++ b/src/muz/rel/doc.h @@ -175,17 +175,17 @@ public: if (m.contains(*m_elems[i], *t)) { found = true; } - if (m.contains(*t, *m_elems[i])) { + else if (m.contains(*t, *m_elems[i])) { m.deallocate(m_elems[i]); --j; + continue; } - else if (i != j) { + if (i != j) { m_elems[j] = m_elems[i]; } } if (j != sz) m_elems.resize(j); if (found) { - SASSERT(j == i); m.deallocate(t); } else {