From 4cf8905a8f0e8be2b8396fa36430dc41e665f9e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 22 Sep 2014 11:08:23 -0700 Subject: [PATCH] fixing join Signed-off-by: Nikolaj Bjorner --- src/muz/rel/udoc_relation.cpp | 54 ++++++++------ src/test/udoc_relation.cpp | 130 ++++++++++++++++++++++++++++++++++ 2 files changed, 163 insertions(+), 21 deletions(-) diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 8abcd9050..f4b758c5e 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -304,13 +304,16 @@ namespace datalog { } void join(doc const& d1, doc const& d2, udoc& result) { - doc* d = dm.allocateX(); + doc_ref d(dm); + tbv_ref t(dm.tbvm()); + d = dm.allocateX(); tbv& pos = d->pos(); utbv& neg = d->neg(); unsigned mid = dm1.num_tbits(); unsigned hi = dm.num_tbits(); pos.set(d1.pos(), mid-1, 0); pos.set(d2.pos(), hi-1, mid); + SASSERT(dm.well_formed(*d)); // first fix bits for (unsigned i = 0; i < m_cols1.size(); ++i) { unsigned idx1 = m_cols1[i]; @@ -321,13 +324,15 @@ namespace datalog { if (v1 == BIT_x) { if (v2 != BIT_x) pos.set(idx1, v2); - } else if (v2 == BIT_x) { + } + else if (v2 == BIT_x) { pos.set(idx2, v1); - } else if (v1 != v2) { - dm.deallocate(d); + } + else if (v1 != v2) { // columns don't match return; } + SASSERT(dm.well_formed(*d)); } // fix equality of don't care columns for (unsigned i = 0; i < m_cols1.size(); ++i) { @@ -338,32 +343,39 @@ namespace datalog { if (v1 == BIT_x && v2 == BIT_x) { // add to subtracted TBVs: 1xx0 and 0xx1 - tbv* r = dm.tbvm().allocate(pos); - r->set(idx1, BIT_0); - r->set(idx2, BIT_1); - neg.push_back(r); - - r = dm.tbvm().allocate(pos); - r->set(idx1, BIT_1); - r->set(idx2, BIT_0); - neg.push_back(r); + t = dm.tbvm().allocate(pos); + t->set(idx1, BIT_0); + t->set(idx2, BIT_1); + neg.push_back(t.detach()); + t = dm.tbvm().allocate(pos); + t->set(idx1, BIT_1); + t->set(idx2, BIT_0); + neg.push_back(t.detach()); } + SASSERT(dm.well_formed(*d)); } // handle subtracted TBVs: 1010 -> 1010xxx for (unsigned i = 0; i < d1.neg().size(); ++i) { - tbv* t = dm.tbvm().allocate(); - t->set(d1.neg()[i], mid-1, 0); - t->set(d2.pos(), hi - 1, mid); - neg.push_back(t); + t = dm.tbvm().allocate(); + t->set(d1.neg()[i], mid - 1, 0); + t->set(d2.pos(), hi - 1, mid); + if (dm.tbvm().set_and(*t, pos)) { + neg.push_back(t.detach()); + } + SASSERT(dm.well_formed(*d)); } for (unsigned i = 0; i < d2.neg().size(); ++i) { - tbv* t = dm.tbvm().allocate(); - t->set(d1.pos(), mid-1, 0); + t = dm.tbvm().allocate(); + t->set(d1.pos(), mid- 1, 0); t->set(d2.neg()[i], hi - 1, mid); - neg.push_back(t); + if (dm.tbvm().set_and(*t, pos)) { + neg.push_back(t.detach()); + } + SASSERT(dm.well_formed(*d)); } - result.insert(dm, d); + SASSERT(dm.well_formed(*d)); + result.insert(dm, d.detach()); } virtual relation_base * operator()(const relation_base & _r1, const relation_base & _r2) { diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 197186bbf..4942164e2 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -16,6 +16,7 @@ #include "rel_context.h" #include "bv_decl_plugin.h" + class udoc_tester { typedef datalog::relation_base relation_base; typedef datalog::udoc_relation udoc_relation; @@ -40,6 +41,56 @@ class udoc_tester { datalog::context m_ctx; datalog::rel_context rc; udoc_plugin& p; + + + tbit choose_tbit() { + switch (m_rand(3)) { + case 0: return BIT_0; + case 1: return BIT_1; + default : return BIT_x; + } + } + + tbv* mk_rand_tbv(doc_manager& dm) { + 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(doc_manager& dm, 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(doc_manager& dm, unsigned num_diff) { + tbv_ref t(dm.tbvm()); + t = mk_rand_tbv(dm); + 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(dm, result->pos())); + } + SASSERT(dm.well_formed(*result)); + return result; + } + + 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)); + } + } + public: udoc_tester(): m_init(m), bv(m), m_vars(m), m_ctx(m, m_reg, m_smt_params), rc(m_ctx), p(dynamic_cast(*rc.get_rmanager().get_relation_plugin(symbol("doc")))) @@ -88,6 +139,8 @@ public: udoc_relation* t1, *t2, *t3; expr_ref fml(m); + test_join(1000); + test_rename(); test_filter_neg(); @@ -366,6 +419,83 @@ public: check_permutation(t1, cycle); } + void test_join(unsigned num_rounds) { + for (unsigned i = 0; i < num_rounds; ++i) { + test_join(); + } + } + + void test_join() { + relation_signature sig; + sig.push_back(bv.mk_sort(2)); + sig.push_back(bv.mk_sort(3)); + udoc_relation* t1, *t2; + relation_base* t; + + t1 = mk_rand(sig); + t2 = mk_rand(sig); + + unsigned_vector jc1, jc2; + jc1.push_back(0); + jc2.push_back(0); + scoped_ptr join_fn; + + join_fn = p.mk_join_fn(*t1, *t2, jc1.size(), jc1.c_ptr(), jc2.c_ptr()); + t = (*join_fn)(*t1, *t2); + + verify_join(*t1, *t2, *t, jc1.size(), jc1.c_ptr(), jc2.c_ptr()); + t1->display(std::cout); + t2->display(std::cout); + t->display(std::cout); + std::cout << "\n"; + t1->deallocate(); + t2->deallocate(); + t->deallocate(); + } + + udoc_relation* mk_rand(relation_signature const& sig) { + udoc_relation* t = mk_empty(sig); + mk_rand_udoc(t->get_dm(), 3, 3, t->get_udoc()); + return t; + } + + void verify_join(relation_base const& t1, relation_base& t2, relation_base& t, + unsigned sz, unsigned const* cols1, unsigned const* cols2) { + relation_signature const& sig1 = t1.get_signature(); + relation_signature const& sig2 = t2.get_signature(); + relation_signature const& sig = t.get_signature(); + expr_ref fml1(m), fml2(m), fml3(m); + var_ref var1(m), var2(m); + t1.to_formula(fml1); + t2.to_formula(fml2); + t.to_formula(fml3); + var_subst sub(m, false); + expr_ref_vector vars(m); + for (unsigned i = 0; i < sig2.size(); ++i) { + vars.push_back(m.mk_var(i + sig1.size(), sig2[i])); + } + sub(fml2, vars.size(), vars.c_ptr(), fml2); + fml1 = m.mk_and(fml1, fml2); + for (unsigned i = 0; i < sz; ++i) { + unsigned v1 = cols1[i]; + unsigned v2 = cols2[i]; + var1 = m.mk_var(v1, sig1[v1]); + var2 = m.mk_var(v2 + sig1.size(), sig2[v2]); + fml1 = m.mk_and(m.mk_eq(var1, var2), fml1); + } + vars.reset(); + for (unsigned i = 0; i < sig.size(); ++i) { + std::stringstream strm; + strm << "x" << i; + vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i])); + } + sub(fml1, vars.size(), vars.c_ptr(), fml1); + sub(fml3, vars.size(), vars.c_ptr(), fml3); + check_equiv(fml1, fml3); + } + + + void check_permutation(relation_base* t1, unsigned_vector const& cycle) { scoped_ptr rename; rename = p.mk_rename_fn(*t1, cycle.size(), cycle.c_ptr());