diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp index adc7e959a..e87143482 100644 --- a/src/muz/rel/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -187,7 +187,14 @@ unsigned doc_manager::diff_by_012(tbv const& pos, tbv const& neg, unsigned& inde void doc_manager::set(doc& d, unsigned idx, tbit value) { m.set(d.pos(), idx, value); for (unsigned i = 0; i < d.neg().size(); ++i) { - m.set(d.neg()[i], idx, value); + tbit b = d.neg()[i][idx]; + if (b != BIT_x && value != BIT_x && value != b) { + d.neg().erase(tbvm(), i); + --i; + } + else { + m.set(d.neg()[i], idx, value); + } } } @@ -234,6 +241,7 @@ bool doc_manager::merge(doc& d, unsigned idx, subset_ints const& equalities, } while (idx != root); + TRACE("doc", tout << "num_x: " << num_x << " value: " << value << "\n";); if (num_x == 0) { // nothing to do. } @@ -248,7 +256,7 @@ bool doc_manager::merge(doc& d, unsigned idx, subset_ints const& equalities, } else { do { - if (!discard_cols.get(idx) && idx != root1) { + if (/*!discard_cols.get(idx) &&*/ idx != root1) { tbv* t = m.allocate(d.pos()); m.set(*t, idx, BIT_0); m.set(*t, root1, BIT_1); @@ -281,10 +289,10 @@ bool doc_manager::intersect(doc const& A, doc const& B, doc& result) { // indices where BIT_0 is set are positive. // -doc* doc_manager::project(doc_manager& dstm, unsigned n, bit_vector const& to_delete, doc const& src) { +doc* doc_manager::project(doc_manager& dstm, bit_vector const& to_delete, doc const& src) { tbv_manager& dstt = dstm.m; tbv_ref t(dstt); - t = dstt.project(n, to_delete, src.pos()); + t = dstt.project(to_delete, src.pos()); doc* r = dstm.allocate(t.detach()); SASSERT(r); @@ -368,7 +376,7 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bit_vector const& to_de } case project_done: { for (unsigned i = 0; i < todo.size(); ++i) { - t = dstt.project(n, to_delete, *todo[i]); + t = dstt.project(to_delete, *todo[i]); if (dstt.equals(r->pos(), *t)) { r->neg().reset(dstt); r->neg().push_back(t.detach()); diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h index 2a4b3ead7..f78ce94ff 100644 --- a/src/muz/rel/doc.h +++ b/src/muz/rel/doc.h @@ -87,7 +87,7 @@ public: std::ostream& display(std::ostream& out, doc const& b) const; std::ostream& display(std::ostream& out, doc const& b, unsigned hi, unsigned lo) const; unsigned num_tbits() const { return m.num_tbits(); } - doc* project(doc_manager& dstm, unsigned n, bit_vector const& to_delete, doc const& src); + doc* project(doc_manager& dstm, bit_vector const& to_delete, doc const& src); bool well_formed(doc const& d) const; bool merge(doc& d, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols); void set(doc& d, unsigned idx, tbit value); diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 9c71b826c..fc3c32390 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -99,9 +99,10 @@ tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) { } return r; } -tbv* tbv_manager::project(unsigned n, bit_vector const& to_delete, tbv const& src) { +tbv* tbv_manager::project(bit_vector const& to_delete, tbv const& src) { tbv* r = allocate(); unsigned i, j; + unsigned n = to_delete.size(); for (i = 0, j = 0; i < n; ++i) { if (!to_delete.get(i)) { set(*r, j, src[i]); diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h index 941853a1b..d667ccaa2 100644 --- a/src/muz/rel/tbv.h +++ b/src/muz/rel/tbv.h @@ -75,7 +75,7 @@ public: bool intersect(tbv const& a, tbv const& b, tbv& result); std::ostream& display(std::ostream& out, tbv const& b) const; std::ostream& display(std::ostream& out, tbv const& b, unsigned hi, unsigned lo) const; - tbv* project(unsigned n, bit_vector const& to_delete, tbv const& src); + tbv* project(bit_vector const& to_delete, tbv const& src); bool is_well_formed(tbv const& b) const; // - does not contain BIT_z; void set(tbv& dst, uint64 n, unsigned hi, unsigned lo); void set(tbv& dst, rational const& r, unsigned hi, unsigned lo); diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 7f0a61da9..b3abf7998 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -460,7 +460,7 @@ namespace datalog { udoc const& ud1 = t.get_udoc(); udoc& ud2 = r->get_udoc(); for (unsigned i = 0; i < ud1.size(); ++i) { - d2 = dm1.project(dm2, m_to_delete.size(), m_to_delete, ud1[i]); + d2 = dm1.project(dm2, m_to_delete, ud1[i]); ud2.push_back(d2.detach()); } TRACE("doc", tout << "final size: " << r->get_size_estimate_rows() << '\n';); @@ -1071,7 +1071,7 @@ namespace datalog { // TBD: replace this by "join" given below. virtual relation_base* operator()(relation_base const& t1, relation_base const& t2) { -#if 0 +#if 1 return join(get(t1), get(t2)); #else udoc_relation *joined = get(m_joiner(t1, t2)); @@ -1097,6 +1097,7 @@ namespace datalog { udoc const& d1 = t1.get_udoc(); udoc const& d2 = t2.get_udoc(); doc_manager& dm1 = t1.get_dm(); + doc_manager& dm2 = t2.get_dm(); udoc_plugin& p = t1.get_plugin(); doc_manager& dm_prod = p.dm(prod_signature); udoc_relation* result = get(p.mk_empty(get_result_signature())); @@ -1104,17 +1105,21 @@ namespace datalog { doc_manager& dm_res = result->get_dm(); for (unsigned i = 0; i < d1.size(); ++i) { for (unsigned j = 0; j < d2.size(); ++j) { - prod.push_back(xprod(dm_prod, dm1, d1[i], d2[j])); + prod.push_back(xprod(dm_prod, dm1, dm2, d1[i], d2[j])); } } + TRACE("doc", prod.display(dm_prod, tout) << "\n";); prod.merge(dm_prod, m_roots, m_equalities, m_to_delete); + TRACE("doc", prod.display(dm_prod, tout) << "\n";); for (unsigned i = 0; i < prod.size(); ++i) { - res.insert(dm_res, dm_prod.project(dm_res, m_to_delete.size(), m_to_delete, prod[i])); + res.insert(dm_res, dm_prod.project(dm_res, m_to_delete, prod[i])); } + TRACE("doc", result->display(tout);); prod.reset(dm_prod); return result; } - doc* xprod(doc_manager& dm, doc_manager& dm1, doc const& d1, doc const& d2) { + doc* xprod(doc_manager& dm, doc_manager& dm1, doc_manager& dm2, + doc const& d1, doc const& d2) { tbv_manager& tbm = dm.tbvm(); doc_ref d(dm); tbv_ref t(tbm); @@ -1138,6 +1143,10 @@ namespace datalog { neg.push_back(t.detach()); } SASSERT(dm.well_formed(*d)); + TRACE("doc", + dm1.display(tout, d1) << "\n"; + dm2.display(tout, d2) << "\n"; + dm.display(tout, *d) << "\n";); return d.detach(); } @@ -1181,24 +1190,24 @@ namespace datalog { bool m_is_subtract; bool m_is_aliased; public: - negation_filter_fn(const udoc_relation & r, 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) : m_t_cols(joined_col_cnt, t_cols), m_neg_cols(joined_col_cnt, neg_cols), - m_mk_remove_cols(r, neg, m_remove_cols), - m_join_project(r, neg, joined_col_cnt, t_cols, neg_cols, + m_mk_remove_cols(t, neg, m_remove_cols), + m_join_project(t, neg, joined_col_cnt, t_cols, neg_cols, m_remove_cols.size(), m_remove_cols.c_ptr()), m_is_subtract(false), m_is_aliased(true) { SASSERT(joined_col_cnt > 0); - m_is_subtract = (joined_col_cnt == r.get_signature().size()); + m_is_subtract = (joined_col_cnt == t.get_signature().size()); m_is_subtract &= (joined_col_cnt == neg.get_signature().size()); svector found(joined_col_cnt, false); for (unsigned i = 0; m_is_subtract && i < joined_col_cnt; ++i) { m_is_subtract = !found[t_cols[i]] && (t_cols[i] == neg_cols[i]); found[t_cols[i]] = true; } - r.expand_column_vector(m_t_cols); + t.expand_column_vector(m_t_cols); neg.expand_column_vector(m_neg_cols); } @@ -1316,7 +1325,7 @@ namespace datalog { udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature())); doc_manager& dm2 = r->get_dm(); for (unsigned i = 0; i < m_udoc2.size(); ++i) { - doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete, m_udoc2[i]); + doc* d = dm.project(dm2, m_to_delete, m_udoc2[i]); r->get_udoc().insert(dm2, d); SASSERT(r->get_udoc().well_formed(dm2)); } diff --git a/src/test/doc.cpp b/src/test/doc.cpp index 731bc100f..593d09cfe 100644 --- a/src/test/doc.cpp +++ b/src/test/doc.cpp @@ -78,19 +78,19 @@ static void tst_doc1(unsigned n) { to_delete.set(1); to_delete.set(3); doc_manager m1(n-2); - doc_ref d1_1(m1, m.project(m1, n, to_delete, *d1)); + doc_ref d1_1(m1, m.project(m1, to_delete, *d1)); doc_ref d1_2(m1, m1.allocate1()); m.display(std::cout, *d1) << " -> "; m1.display(std::cout, *d1_1) << "\n"; SASSERT(m1.equals(*d1_1,*d1_2)); m.set(*d1,2,BIT_x); m.set(*d1,4,BIT_x); - d1_1 = m.project(m1, n, to_delete, *d1); + d1_1 = m.project(m1, to_delete, *d1); m.display(std::cout, *d1) << " -> "; m1.display(std::cout, *d1_1) << "\n"; d1->neg().push_back(m.tbvm().allocate1()); SASSERT(m.well_formed(*d1)); - d1_1 = m.project(m1, n, to_delete, *d1); + d1_1 = m.project(m1, to_delete, *d1); m.display(std::cout, *d1) << " -> "; m1.display(std::cout, *d1_1) << "\n"; } @@ -218,7 +218,7 @@ class test_doc_cls { } void project(doc const& d, doc_manager& m2, const bit_vector& to_delete, doc_ref& result) { - result = dm.project(m2, m_vars.size(), to_delete, d); + result = dm.project(m2, to_delete, d); TRACE("doc", for (unsigned i = 0; i < m_vars.size(); ++i) { tout << (to_delete.get(i)?"0":"1"); diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp index dc2867f58..c53eb3671 100644 --- a/src/test/tbv.cpp +++ b/src/test/tbv.cpp @@ -32,7 +32,7 @@ static void tst1(unsigned num_bits) { to_delete.set(3); m.set(*b1, 2, BIT_0); m.set(*b1, 4, BIT_x); - tbv_ref b2(m2, m2.project(num_bits, to_delete, *b1)); + tbv_ref b2(m2, m2.project(to_delete, *b1)); m.display(std::cout, *b1) << " -> "; m2.display(std::cout, *b2) << "\n"; m.deallocate(b0); diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index af80a6d5c..8b9fa3a80 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -76,20 +76,32 @@ class udoc_tester { doc* mk_rand_doc(doc_manager& dm, unsigned num_diff) { tbv_ref t(dm.tbvm()); + doc_ref result(dm); t = mk_rand_tbv(dm); - doc* result = dm.allocate(*t); + result = dm.allocate(*t); SASSERT(dm.tbvm().equals(*t, result->pos())); for (unsigned i = 0; i < num_diff; ++i) { - result->neg().push_back(mk_rand_tbv(dm, result->pos())); + t = mk_rand_tbv(dm, result->pos()); + if (dm.tbvm().equals(*t, result->pos())) { + return 0; + } + if (!result->neg().is_empty() && + dm.tbvm().equals(*t, result->neg()[0])) { + continue; + } + result->neg().push_back(t.detach()); } SASSERT(dm.well_formed(*result)); - return result; + return result.detach(); } void mk_rand_udoc(doc_manager& dm, unsigned num_elems, unsigned num_diff, udoc& result) { result.reset(dm); for (unsigned i = 0; i < num_elems; ++i) { - result.push_back(mk_rand_doc(dm, num_diff)); + doc* d = mk_rand_doc(dm, num_diff); + if (d) { + result.push_back(d); + } } } @@ -144,6 +156,8 @@ public: udoc_relation* t1, *t2, *t3; expr_ref fml(m); + test_filter_neg2(); + test_join_project(); test_filter_neg4(false); @@ -152,7 +166,6 @@ public: test_filter_neg5(true); test_filter_neg(); - test_filter_neg2(); test_filter_neg3(); test_join(1000); @@ -408,27 +421,34 @@ public: } + // {11xx \ {111x}, x011 \ {x011}, 0111} + // {xx11 \ {0011, 1111, x111}} + // 0111 + // {1x1x \ {1x1x}, 1111 \ {1111}, x1x1 \ {x1x1}} + void test_join_project() { datalog::relation_signature sig; - sig.push_back(bv.mk_sort(3)); - sig.push_back(bv.mk_sort(3)); - sig.push_back(bv.mk_sort(3)); + sig.push_back(bv.mk_sort(2)); + sig.push_back(bv.mk_sort(2)); + //sig.push_back(bv.mk_sort(3)); unsigned_vector jc1, jc2, pc; jc1.push_back(0); jc2.push_back(0); pc.push_back(1); pc.push_back(3); - pc.push_back(4); + //pc.push_back(4); udoc_relation* t1, *t2; relation_base* t; scoped_ptr join_project_fn; - for (unsigned i = 0; i < 20; ++i) { + for (unsigned i = 0; i < 200; ++i) { t1 = mk_rand(sig); t2 = mk_rand(sig); + t1->display(std::cout); + t2->display(std::cout); join_project_fn = p.mk_join_project_fn(*t1, *t2, jc1.size(), jc1.c_ptr(), jc2.c_ptr(), pc.size(), pc.c_ptr()); t = (*join_project_fn)(*t1, *t2); t->display(std::cout); @@ -612,6 +632,8 @@ public: apply_filter_neg(*t2, *neg, allcols, allcols); neg->deallocate(); } + t1->display(std::cout); + t2->display(std::cout); apply_filter_neg(*t2, *t1, cols, cols); t1->deallocate();