From 2552c1530b09fca4480196467a35ab58d31f3bae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Sep 2014 10:19:54 -0700 Subject: [PATCH] doc unit tests pass Signed-off-by: Nikolaj Bjorner --- src/muz/rel/doc.cpp | 5 +- src/muz/rel/doc.h | 15 ++-- src/muz/rel/udoc_relation.cpp | 154 ++++++++++++++++++++++------------ src/muz/rel/udoc_relation.h | 6 +- src/test/udoc_relation.cpp | 84 +++++++++++-------- 5 files changed, 166 insertions(+), 98 deletions(-) diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp index 6cf719fd2..1db1ac2b7 100644 --- a/src/muz/rel/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -192,14 +192,15 @@ void doc_manager::set(doc& d, unsigned idx, tbit value) { // bool doc_manager::merge( doc& d, unsigned lo, unsigned length, - subset_ints& equalities, bit_vector const& discard_cols) { + subset_ints const& equalities, bit_vector const& discard_cols) { for (unsigned i = 0; i < length; ++i) { unsigned idx = lo + i; if (!merge(d, lo + i, equalities, discard_cols)) return false; } return true; } -bool doc_manager::merge(doc& d, unsigned idx, subset_ints& equalities, bit_vector const& discard_cols) { +bool doc_manager::merge(doc& d, unsigned idx, subset_ints const& equalities, + bit_vector const& discard_cols) { unsigned root = equalities.find(idx); idx = root; unsigned num_x = 0; diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h index 510ee8bef..e56196026 100644 --- a/src/muz/rel/doc.h +++ b/src/muz/rel/doc.h @@ -69,11 +69,11 @@ public: unsigned num_tbits() const { return m.num_tbits(); } doc* project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src); bool well_formed(doc const& d) const; - bool merge(doc& d, unsigned lo, unsigned length, subset_ints& equalities, bit_vector const& discard_cols); + 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); private: unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index); - bool merge(doc& d, unsigned idx, subset_ints& equalities, bit_vector const& discard_cols); + bool merge(doc& d, unsigned idx, subset_ints const& equalities, bit_vector const& discard_cols); bool can_project_neg(tbv const& pos, unsigned n, bool const* to_delete, tbv const& neg); }; @@ -233,7 +233,7 @@ public: std::swap(*this, result); } - void merge(M& m, unsigned lo, unsigned length, subset_ints & equalities, bit_vector const& discard_cols) { + void merge(M& m, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols) { for (unsigned i = 0; i < size(); ++i) { if (!m.merge(*m_elems[i], lo, length, equalities, discard_cols)) { erase(m, i); @@ -254,9 +254,12 @@ public: merge(m, lo1, length, equalities, discard_cols); } - -private: - + void merge(M& m, unsigned_vector const& roots, subset_ints const& equalities, + bit_vector const& discard_cols) { + for (unsigned i = 0; i < roots.size(); ++i) { + merge(m, roots[i], equalities, discard_cols); + } + } }; diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index ebebe4063..874885e5f 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -116,6 +116,7 @@ namespace datalog { break; case BIT_x: if (!is_x) { + SASSERT(p.bv.is_bv_sort(get_signature()[i])); conjs.push_back(m.mk_eq(p.bv.mk_extract(j-1-lo,lo1-lo,v), p.bv.mk_numeral(r,j-lo1))); } @@ -185,6 +186,23 @@ namespace datalog { } return *r; } + bool udoc_relation::is_var_range(expr* e, unsigned& hi, unsigned& lo, unsigned& v) const { + udoc_plugin& p = get_plugin(); + if (is_var(e)) { + v = to_var(e)->get_idx(); + hi = p.num_sort_bits(e)-1; + lo = 0; + return true; + } + expr* e2; + if (p.bv.is_extract(e, lo, hi, e2) && is_var(e2)) { + v = to_var(e2)->get_idx(); + SASSERT(lo <= hi); + return true; + } + return false; + } + expr* udoc_plugin::mk_numeral(rational const& r, sort* s) { if (bv.is_bv_sort(s)) { return bv.mk_numeral(r, s); @@ -576,16 +594,14 @@ namespace datalog { udoc_plugin& p = get_plugin(); ast_manager& m = p.get_ast_manager(); bv_util& bv = p.bv; - expr* e1, *e2, *e3; - unsigned hi, lo; + expr* e1, *e2; + unsigned hi, lo, v; if (m.is_and(g) || m.is_or(g) || m.is_not(g) || m.is_true(g) || m.is_false(g)) { return is_guard(to_app(g)->get_num_args(), to_app(g)->get_args()); } if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) { - if (is_var(e1) && is_ground(e2)) return true; - if (is_var(e2) && is_ground(e1)) return true; - if (bv.is_extract(e1, lo, hi, e3) && is_var(e3) && is_ground(e2)) return true; - if (bv.is_extract(e2, lo, hi, e3) && is_var(e3) && is_ground(e1)) return true; + if (is_var_range(e1, hi, lo, v) && is_ground(e2)) return true; + if (is_var_range(e2, hi, lo, v) && is_ground(e1)) return true; } if (is_var(g)) { return true; @@ -611,6 +627,37 @@ namespace datalog { guard = mk_and(m, guards.size(), guards.c_ptr()); rest = mk_and(m, rests.size(), rests.c_ptr()); } + void udoc_relation::extract_equalities(expr* g, expr_ref& rest, subset_ints& equalities, + unsigned_vector& roots) const { + rest.reset(); + ast_manager& m = get_plugin().get_ast_manager(); + expr_ref_vector conds(m); + conds.push_back(g); + qe::flatten_and(conds); + expr* e1, *e2; + unsigned v1, v2, lo1, lo2, hi1, hi2; + for (unsigned i = 0; i < conds.size(); ++i) { + expr* g = conds[i].get(); + if (m.is_eq(g, e1, e2) && + is_var_range(e1, hi1, lo1, v1) && + is_var_range(e2, hi2, lo2, v2)) { + unsigned col1 = column_idx(v1); + lo1 += col1; + hi1 += col1; + unsigned col2 = column_idx(v2); + lo2 += col2; + hi2 += col2; + for (unsigned j = 0; j <= hi1-lo1; ++j) { + roots.push_back(lo1 + j); + equalities.merge(lo1 + j, lo2 + j); + } + conds[i] = conds.back(); + conds.pop_back(); + --i; + } + } + rest = mk_and(m, conds.size(), conds.c_ptr()); + } void udoc_relation::compile_guard(expr* g, udoc& d, bit_vector const& discard_cols) const { d.reset(dm); d.push_back(dm.allocateX()); @@ -625,12 +672,11 @@ namespace datalog { } apply_guard(g, result, equalities, discard_cols); } - bool udoc_relation::apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c) const { + bool udoc_relation::apply_eq(expr* g, udoc& result, unsigned v, unsigned hi, unsigned lo, expr* c) const { udoc_plugin& p = get_plugin(); unsigned num_bits; rational r; - unsigned idx = v->get_idx(); - unsigned col = column_idx(idx); + unsigned col = column_idx(v); lo += col; hi += col; if (p.is_numeral(c, r, num_bits)) { @@ -644,7 +690,7 @@ namespace datalog { } void udoc_relation::apply_guard( - expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols) const { + expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const { ast_manager& m = get_plugin().get_ast_manager(); bv_util& bv = get_plugin().bv; expr* e1, *e2; @@ -660,16 +706,16 @@ namespace datalog { // the equivalence class to collapse. // It seems the current organization with fix_eq_bits // will merge the equivalence class as a side-effect. - TRACE("doc", result.display(dm, tout << "result0:") << "\n";); udoc sub; sub.push_back(dm.allocateX()); apply_guard(e1, sub, equalities, discard_cols); - TRACE("doc", sub.display(dm, tout << "sub:") << "\n";); + TRACE("doc", + result.display(dm, tout << "result0:") << "\n"; + sub.display(dm, tout << "sub:") << "\n";); result.subtract(dm, sub); result.simplify(dm); sub.reset(dm); TRACE("doc", result.display(dm, tout << "result:") << "\n";); - } else if (m.is_or(g)) { udoc sub; @@ -717,36 +763,20 @@ namespace datalog { diff2.reset(dm); } else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) { - unsigned hi, lo, lo1, lo2, hi1, hi2; - expr* e3, *e4; - if (is_var(e1) && is_ground(e2) && - apply_eq(g, result, to_var(e1), bv.get_bv_size(e1)-1, 0, e2)) { + unsigned hi, lo, lo1, lo2, hi1, hi2, v, v1, v2; + if (is_var_range(e1, hi, lo, v) && is_ground(e2) && + apply_eq(g, result, v, hi, lo, e2)) { } - else if (is_var(e2) && is_ground(e1) && - apply_eq(g, result, to_var(e2), bv.get_bv_size(e2)-1, 0, e1)) { + else if (is_var_range(e2, hi, lo, v) && is_ground(e1) && + apply_eq(g, result, v, hi, lo, e1)) { } - else if (bv.is_extract(e1, lo, hi, e3) && is_var(e3) && is_ground(e2) && - apply_eq(g, result, to_var(e3), hi, lo, e2)) { - } - else if (bv.is_extract(e2, lo, hi, e3) && is_var(e3) && is_ground(e1) && - apply_eq(g, result, to_var(e3), hi, lo, e1)) { - } - else if (is_var(e1) && is_var(e2)) { - var* v1 = to_var(e1); - var* v2 = to_var(e2); - unsigned idx1 = column_idx(v1->get_idx()); - unsigned idx2 = column_idx(v2->get_idx()); - unsigned length = column_num_bits(v1->get_idx()); + else if (is_var_range(e1, hi1, lo1, v1) && + is_var_range(e2, hi2, lo2, v2)) { + unsigned idx1 = lo1 + column_idx(v1); + unsigned idx2 = lo2 + column_idx(v2); + unsigned length = hi1-lo1+1; result.merge(dm, idx1, idx2, length, discard_cols); } - else if (bv.is_extract(e1, lo1, hi1, e3) && is_var(e3) && - bv.is_extract(e2, lo2, hi2, e4) && is_var(e4)) { - var* v1 = to_var(e3); - var* v2 = to_var(e4); - unsigned idx1 = lo1 + column_idx(v1->get_idx()); - unsigned idx2 = lo2 + column_idx(v2->get_idx()); - result.merge(dm, idx1, idx2, hi1-lo1+1, discard_cols); - } else { goto failure_case; } @@ -760,16 +790,24 @@ namespace datalog { } class udoc_plugin::filter_interpreted_fn : public relation_mutator_fn { + union_find_default_ctx union_ctx; doc_manager& dm; expr_ref m_condition; udoc m_udoc; bit_vector m_empty_bv; + subset_ints m_equalities; + public: filter_interpreted_fn(const udoc_relation & t, ast_manager& m, app *condition) : dm(t.get_dm()), - m_condition(m) { - m_empty_bv.resize(t.get_num_bits(), false); - expr_ref guard(m), rest(m); + m_condition(m), + m_equalities(union_ctx) { + unsigned num_bits = t.get_num_bits(); + m_empty_bv.resize(num_bits, false); + expr_ref guard(m); + for (unsigned i = 0; i < num_bits; ++i) { + m_equalities.mk_var(); + } t.extract_guard(condition, guard, m_condition); t.compile_guard(guard, m_udoc, m_empty_bv); if (m.is_true(m_condition)) { @@ -790,7 +828,7 @@ namespace datalog { udoc& u = t.get_udoc(); u.intersect(dm, m_udoc); if (m_condition && !u.is_empty()) { - t.apply_guard(m_condition, u, m_empty_bv); + t.apply_guard(m_condition, u, m_equalities, m_empty_bv); } u.simplify(dm); TRACE("doc", tout << "final size: " << t.get_size_estimate_rows() << '\n';); @@ -821,7 +859,7 @@ namespace datalog { bool done_i = false; for (unsigned j = 0; !done_i && j < neg.size(); ++j) { bool done_j = false; - for (unsigned c = 0; !done_i && !done_j && c < m_t_cols.size(); ++c) { + for (unsigned c = 0; !done_j && c < m_t_cols.size(); ++c) { unsigned t_col = m_t_cols[c]; unsigned n_col = m_neg_cols[c]; unsigned num_bits = t.column_num_bits(t_col); @@ -837,12 +875,12 @@ namespace datalog { } if (done_j) { result.push_back(&dst[i]); - } - else { - dm.deallocate(&dst[i]); done_i = true; } } + if (!done_i) { + dm.deallocate(&dst[i]); + } } std::swap(dst, result); if (dst.is_empty()) { @@ -859,6 +897,7 @@ namespace datalog { renamed_neg.push_back(newD.detach()); } dst.subtract(t.get_dm(), renamed_neg); + renamed_neg.reset(t.get_dm()); } void copy_column( doc& dst, doc const& src, @@ -886,19 +925,28 @@ namespace datalog { } class udoc_plugin::filter_proj_fn : public convenient_relation_project_fn { + union_find_default_ctx union_ctx; doc_manager& dm; expr_ref m_condition; udoc m_udoc; bit_vector m_col_list; // map: col idx -> bool (whether the column is to be removed) svector m_to_delete; // same + subset_ints m_equalities; + unsigned_vector m_roots; + public: filter_proj_fn(const udoc_relation & t, ast_manager& m, app *condition, unsigned col_cnt, const unsigned * removed_cols) : convenient_relation_project_fn(t.get_signature(), col_cnt, removed_cols), dm(t.get_dm()), - m_condition(m) { + m_condition(m), + m_equalities(union_ctx) { t.expand_column_vector(m_removed_cols); - m_col_list.resize(t.get_num_bits(), false); + unsigned num_bits = t.get_num_bits(); + m_col_list.resize(num_bits, false); + for (unsigned i = 0; i < num_bits; ++i) { + m_equalities.mk_var(); + } for (unsigned i = 0; i < m_removed_cols.size(); ++i) { m_col_list.set(m_removed_cols[i], true); } @@ -906,8 +954,9 @@ namespace datalog { for (unsigned i = 0; i < m_removed_cols.size(); ++i) { m_to_delete[m_removed_cols[i]] = true; } - expr_ref guard(m), rest(m); - t.extract_guard(condition, guard, m_condition); + expr_ref guard(m), non_eq_cond(m); + t.extract_equalities(condition, non_eq_cond, m_equalities, m_roots); + t.extract_guard(non_eq_cond, guard, m_condition); t.compile_guard(guard, m_udoc, m_col_list); if (m.is_true(m_condition)) { m_condition = 0; @@ -924,8 +973,9 @@ namespace datalog { udoc u2; u2.copy(dm, u1); u2.intersect(dm, m_udoc); + u2.merge(dm, m_roots, m_equalities, m_col_list); if (m_condition && !u2.is_empty()) { - t.apply_guard(m_condition, u2, m_col_list); + t.apply_guard(m_condition, u2, m_equalities, m_col_list); } udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature())); doc_manager& dm2 = r->get_dm(); diff --git a/src/muz/rel/udoc_relation.h b/src/muz/rel/udoc_relation.h index 4befa228a..697928d60 100644 --- a/src/muz/rel/udoc_relation.h +++ b/src/muz/rel/udoc_relation.h @@ -65,9 +65,11 @@ namespace datalog { bool is_guard(expr* g) const; bool is_guard(unsigned n, expr* const *g) const; void compile_guard(expr* g, udoc& result, bit_vector const& discard_cols) const; + void extract_equalities(expr* g, expr_ref& rest, subset_ints& equalities, unsigned_vector& roots) const; void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const; - void apply_guard(expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols) const; - bool apply_eq(expr* g, udoc& result, var* v, unsigned hi, unsigned lo, expr* c) const; + void apply_guard(expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const; + bool apply_eq(expr* g, udoc& result, unsigned v, unsigned hi, unsigned lo, expr* c) const; + bool is_var_range(expr* e, unsigned& hi, unsigned& lo, unsigned& v) const; }; class udoc_plugin : public relation_plugin { diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 67a008688..13623aeeb 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -88,41 +88,7 @@ public: udoc_relation* t1, *t2, *t3; expr_ref fml(m); - // filter_by_negation - - /* - The filter_by_negation postcondition: - filter_by_negation(tgt, neg, columns in tgt: c1,...,cN, - corresponding columns in neg: d1,...,dN): - tgt_1:={x: x\in tgt_0 && ! \exists y: ( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) } - */ - { - relation_signature sig4; - sig4.push_back(bv.mk_sort(1)); - sig4.push_back(bv.mk_sort(1)); - sig4.push_back(bv.mk_sort(1)); - t1 = mk_empty(sig4); - t2 = mk_empty(sig4); - unsigned_vector cols1, cols2; - unsigned num_bits = t1->get_dm().num_tbits(); - - cols1.push_back(0); - cols2.push_back(1); - for (unsigned i = 0; i < 100; ++i) { - set_random(*t1, 2*num_bits/3); - set_random(*t2, 2*num_bits/3); - apply_filter_neg(*t1,*t2, cols1, cols2); - } - cols1.push_back(1); - cols2.push_back(2); - for (unsigned i = 0; i < 100; ++i) { - set_random(*t1, 2*num_bits/3); - set_random(*t2, 2*num_bits/3); - apply_filter_neg(*t1,*t2, cols1, cols2); - } - t1->deallocate(); - t2->deallocate(); - } + test_filter_neg(); // empty { @@ -328,6 +294,7 @@ public: cond1 = m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)); conds.push_back(cond1); conds.push_back(m.mk_or(cond1,m.mk_eq(v3,v4))); + conds.push_back(m.mk_eq(ex(2,1,v3),ex(1,0,v4))); conds.push_back(m.mk_or(cond1,m.mk_eq(ex(2,1,v3),ex(1,0,v4)))); conds.push_back(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v0,v4))); conds.push_back(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v3,v4))); @@ -375,6 +342,43 @@ public: } + /* + The filter_by_negation postcondition: + filter_by_negation(tgt, neg, columns in tgt: c1,...,cN, + corresponding columns in neg: d1,...,dN): + tgt_1:={x: x\in tgt_0 && ! \exists y: ( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) } + */ + + void test_filter_neg() { + // filter_by_negation + + relation_signature sig4; + sig4.push_back(bv.mk_sort(1)); + sig4.push_back(bv.mk_sort(1)); + sig4.push_back(bv.mk_sort(1)); + udoc_relation* t1 = mk_empty(sig4); + udoc_relation* t2 = mk_empty(sig4); + unsigned_vector cols1, cols2; + unsigned num_bits = t1->get_dm().num_tbits(); + + cols1.push_back(0); + cols2.push_back(1); + for (unsigned i = 0; i < 100; ++i) { + set_random(*t1, 2*num_bits/3); + set_random(*t2, 2*num_bits/3); + apply_filter_neg(*t1,*t2, cols1, cols2); + } + cols1.push_back(1); + cols2.push_back(2); + for (unsigned i = 0; i < 200; ++i) { + set_random(*t1, 2*num_bits/3); + set_random(*t2, 2*num_bits/3); + 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()); @@ -390,6 +394,7 @@ public: tbit b = (val == 0)?BIT_0:BIT_1; dm.set(d0, idx, b); } + full->deallocate(); } void apply_filter_neg(udoc_relation& t1, udoc_relation& t2, @@ -401,7 +406,14 @@ public: expr_ref fml1(m), fml2(m), fml3(m); t1.to_formula(fml1); t2.to_formula(fml2); + for (unsigned i = 0; i < cols1.size(); ++i) { + std::cout << cols1[i] << " = " << cols2[i] << " "; + } + std::cout << "\n"; + t1.display(std::cout); std::cout << "\n"; + t2.display(std::cout); std::cout << "\n"; (*negf)(t1, t2); + t1.display(std::cout); std::cout << "\n"; t1.to_formula(fml3); std::cout << fml1 << "\n"; std::cout << fml2 << "\n"; @@ -426,7 +438,7 @@ public: for (unsigned i = 0; i < sub.size(); ++i) { project_var(sig.size() + i, m.get_sort(sub[i].get()), fml2); } - fml1 = m.mk_and(fml1, fml2); + fml1 = m.mk_and(fml1, m.mk_not(fml2)); expr_ref_vector vars(m); for (unsigned i = 0; i < sig.size(); ++i) {