diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp index 7cad5ffe8..36717adf3 100644 --- a/src/muz/rel/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -109,7 +109,7 @@ doc& doc_manager::fillX(doc& src) { bool doc_manager::set_and(doc& dst, doc const& src) { // (A \ B) & (C \ D) = (A & C) \ (B u D) if (!m.set_and(dst.pos(), src.pos())) return false; - dst.neg().intersect(m, src.pos()); + dst.neg().intersect(m, dst.pos()); tbv_ref t(m); for (unsigned i = 0; i < src.neg().size(); ++i) { t = m.allocate(src.neg()[i]); @@ -117,6 +117,7 @@ bool doc_manager::set_and(doc& dst, doc const& src) { dst.neg().insert(m, t.detach()); } } + SASSERT(well_formed(dst)); return (src.neg().is_empty() || fold_neg(dst)); } bool doc_manager::set_and(doc& dst, tbv const& src) { @@ -150,11 +151,12 @@ bool doc_manager::fold_neg(doc& dst) { } else { // count == 1: dst.pos().set(index, neg(dst.neg()[i][index])); - dst.neg().erase(tbvm(), i); + dst.neg().intersect(tbvm(), dst.pos()); goto start_over; } } } + SASSERT(well_formed(dst)); return true; } diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h index 3c2b9091d..58850f812 100644 --- a/src/muz/rel/doc.h +++ b/src/muz/rel/doc.h @@ -175,20 +175,17 @@ public: } } void intersect(M& m, union_bvec const& other) { - union_bvec result; - unsigned sz1 = size(); - unsigned sz2 = other.size(); - T* inter = m.allocate(); - for (unsigned i = 0; i < sz1; ++i) { - for (unsigned j = 0; j < sz2; ++j) { - if (m.intersect(*m_elems[i], other[j], *inter)) { - result.push_back(inter); - inter = m.allocate(); - } + unsigned sz = other.size(); + union_bvec tmp, result; + for (unsigned i = 0; i < sz; ++i) { + tmp.copy(m, *this); + tmp.intersect(m, other[i]); + for (unsigned j = 0; j < tmp.size(); ++j) { + result.push_back(tmp.m_elems[j]); } + tmp.m_elems.reset(); } - m.deallocate(inter); - std::swap(result, *this); + std::swap(*this, result); result.reset(m); } void subtract(M& m, union_bvec const& other) { diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 1d0da90dd..8abcd9050 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -382,6 +382,7 @@ namespace datalog { } } TRACE("doc", result->display(tout << "result:\n");); + IF_VERBOSE(3, result->display(verbose_stream() << "join result:\n");); SASSERT(r.well_formed(result->get_dm())); return result; } @@ -544,6 +545,7 @@ namespace datalog { SASSERT(r.get_udoc().well_formed(dm)); SASSERT(!d1 || d1->well_formed(dm)); TRACE("doc", _r.display(tout << "dst':\n"); ); + IF_VERBOSE(3, _r.display(verbose_stream() << "union result:\n");); } }; void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) { @@ -1045,6 +1047,7 @@ namespace datalog { SASSERT(r->get_udoc().well_formed(dm2)); } u2.reset(dm); + IF_VERBOSE(3, r->display(verbose_stream() << "filter result:\n");); return r; } }; diff --git a/src/test/doc.cpp b/src/test/doc.cpp index 6bd7e50b9..45206d4ca 100644 --- a/src/test/doc.cpp +++ b/src/test/doc.cpp @@ -113,6 +113,47 @@ class test_doc_cls { default : return BIT_x; } } + + tbv* mk_rand_tbv() { + tbv* result = dm.tbvm().allocate(); + for (unsigned i = 0; i < dm.num_tbits(); ++i) { + (*result).set(i, choose_tbit()); + } + return result; + } + + tbv* mk_rand_tbv(tbv const& pos) { + tbv* result = dm.tbvm().allocate(); + for (unsigned i = 0; i < dm.num_tbits(); ++i) { + if (pos[i] == BIT_x) { + (*result).set(i, choose_tbit()); + } + else { + (*result).set(i, pos[i]); + } + } + return result; + } + + doc* mk_rand_doc(unsigned num_diff) { + tbv_ref t(dm.tbvm()); + t = mk_rand_tbv(); + doc* 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(result->pos())); + } + SASSERT(dm.well_formed(*result)); + return result; + } + + void mk_rand_udoc(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(num_diff)); + } + } + expr_ref mk_conj(tbv& t) { expr_ref result(m); expr_ref_vector conjs(m); @@ -284,6 +325,12 @@ class test_doc_cls { fml = m.mk_not(m.mk_eq(fml1, fml2)); solver.assert_expr(fml); lbool res = solver.check(); + if (res != l_false) { + TRACE("doc", + tout << mk_pp(fml1, m) << "\n"; + tout << mk_pp(fml2, m) << "\n"; + ); + } SASSERT(res == l_false); } @@ -349,6 +396,43 @@ public: ds2.reset(dm); //sub:{xxx \ {1x0, 0x1}} //result:{100} + + for (unsigned i = 0; i < 1000; ++i) { + udoc d1, d2; + mk_rand_udoc(3, 3, d1); + mk_rand_udoc(3, 3, d2); + fml1 = to_formula(d1, dm, to_delete.c_ptr()); + fml2 = to_formula(d2, dm, to_delete.c_ptr()); + d1.subtract(dm, d2); + fml3 = to_formula(d1, dm, to_delete.c_ptr()); + fml1 = m.mk_and(fml1, m.mk_not(fml2)); + check_equiv(fml1, fml3); + d1.reset(dm); + d2.reset(dm); + } + } + + void test_intersect() { + expr_ref fml1(m), fml2(m), fml3(m); + svector to_delete(m_vars.size(), false); + for (unsigned i = 0; i < 10000; ++i) { + udoc d1, d2; + mk_rand_udoc(3, 3, d1); + mk_rand_udoc(3, 3, d2); + fml1 = to_formula(d1, dm, to_delete.c_ptr()); + fml2 = to_formula(d2, dm, to_delete.c_ptr()); + TRACE("doc", + d1.display(dm, tout) << "\n"; + d2.display(dm, tout) << "\n";); + d1.intersect(dm, d2); + TRACE("doc", d1.display(dm, tout) << "\n";); + SASSERT(d1.well_formed(dm)); + fml3 = to_formula(d1, dm, to_delete.c_ptr()); + fml1 = m.mk_and(fml1, fml2); + check_equiv(fml1, fml3); + d1.reset(dm); + d2.reset(dm); + } } }; @@ -356,7 +440,8 @@ public: void tst_doc() { - test_doc_cls tp(4); + test_doc_cls tp(4); + tp.test_intersect(); tp.test_subtract(); tp.test_merge(200,7); tp.test_project(200,7);