From 44e8833369a7674f77164c194ab8d807bb0ea634 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Sep 2014 17:06:05 -0700 Subject: [PATCH] more udoc Signed-off-by: Nikolaj Bjorner --- src/muz/ddnf/doc.h | 17 +++- src/muz/ddnf/tbv.h | 16 +++ src/muz/ddnf/udoc_relation.cpp | 172 ++++++++++++++++++++++++++++++++- src/muz/ddnf/udoc_relation.h | 13 ++- 4 files changed, 208 insertions(+), 10 deletions(-) diff --git a/src/muz/ddnf/doc.h b/src/muz/ddnf/doc.h index 22f9ecf7b..b311a9ef0 100644 --- a/src/muz/ddnf/doc.h +++ b/src/muz/ddnf/doc.h @@ -117,13 +117,19 @@ public: } return !found; } - bool intersect(M& m, T& t) { + void intersect(M& m, T& t) { unsigned sz = size(); - for (unsigned i = 0; i < sz; ++i) { - if (!m.set_and(m_elems[i], t)) - return false; + unsigned j = 0; + for (unsigned i = 0; i < sz; ++i, ++j) { + if (!m.set_and(*m_elems[i], t)) { + m.deallocate(m_elems[i]); + --j; + } + else if (i != j) { + m_elems[i] = m_elems[j]; + } } - return true; + if (j != sz) m_elems.resize(j); } void insert(M& m, union_bvec const& other) { for (unsigned i = 0; i < other.size(); ++i) { @@ -163,6 +169,7 @@ public: for (unsigned i = 0; i < length; ++i) { unsigned k = 0; for (unsigned j = 0; j < size(); ++j, ++k) { + NOT_IMPLEMENTED_YET(); #if 0 T *eqBV = BV ? const_cast(BV) : &*I; diff --git a/src/muz/ddnf/tbv.h b/src/muz/ddnf/tbv.h index c583dd3f1..2ae79a10d 100644 --- a/src/muz/ddnf/tbv.h +++ b/src/muz/ddnf/tbv.h @@ -106,5 +106,21 @@ private: } }; +class tbv_ref { + tbv_manager& mgr; + tbv* d; +public: + tbv_ref(tbv_manager& mgr):mgr(mgr),d(0) {} + tbv_ref(tbv_manager& mgr, tbv* d):mgr(mgr),d(d) {} + ~tbv_ref() { + if (d) mgr.deallocate(d); + } + tbv_ref& operator=(tbv* d2) { + if (d) mgr.deallocate(d); + d = d2; + } + tbv& operator*() { return *d; } +}; + #endif /* _TBV_H_ */ diff --git a/src/muz/ddnf/udoc_relation.cpp b/src/muz/ddnf/udoc_relation.cpp index 83b6c28fb..8f422e77a 100644 --- a/src/muz/ddnf/udoc_relation.cpp +++ b/src/muz/ddnf/udoc_relation.cpp @@ -358,14 +358,178 @@ namespace datalog { return 0; return alloc(filter_identical_fn, t, col_cnt, identical_cols); } + class udoc_plugin::filter_equal_fn : public relation_mutator_fn { + doc_manager& dm; + doc* m_filter; + public: + filter_equal_fn(udoc_plugin& p, const udoc_relation & t, const relation_element val, unsigned col): + dm(p.dm(t.get_signature())) { + rational r; + unsigned num_bits; + VERIFY(p.bv.is_numeral(val, r, num_bits)); + m_filter = dm.allocateX(); + unsigned lo = t.column_idx(col); + unsigned hi = t.column_idx(col+1); + SASSERT(num_bits == hi - lo); + m_filter->pos().set(r, hi-1, lo); + } + virtual ~filter_equal_fn() { + dm.deallocate(m_filter); + } + virtual void operator()(relation_base & tb) { + udoc_relation & t = get(tb); + t.get_udoc().intersect(dm, *m_filter); + } + }; relation_mutator_fn * udoc_plugin::mk_filter_equal_fn( const relation_base & t, const relation_element & value, unsigned col) { - NOT_IMPLEMENTED_YET(); - return 0; + if (!check_kind(t)) + return 0; + return alloc(filter_equal_fn, *this, get(t), value, col); } +#if 0 + static bool cond_is_guard(const expr *e, const table_information& t) { + switch (e->get_kind()) { + case AST_APP: { + const app *app = to_app(e); + switch (app->get_decl_kind()) { + case OP_AND: + case OP_OR: + case OP_NOT: + for (unsigned i = 0; i < app->get_num_args(); ++i) { + if (!cond_is_guard(app->get_arg(i), t)) + return false; + } + return true; + + case OP_EQ: { + const expr *a = app->get_arg(0), *b = app->get_arg(1); + + // column equality is not succinctly representable with TBVs + if (is_var(a) && is_var(b)) + return false; + + // (= var (concat var foo)) + if (t.get_bv_util().is_concat(b)) + return false; + + return true;} + + case OP_FALSE: + case OP_TRUE: + return true; + + default: + return false; + } + break;} + + case AST_VAR: + return true; + + default: + break; + } + return false; + } + + static void split_cond_guard(app *cond, expr_ref& guard, expr_ref& leftover, const table_information& t) { + expr_ref_vector guards(guard.m()); + expr_ref_vector leftovers(leftover.m()); + + if (is_app(cond) && to_app(cond)->get_decl_kind() == OP_AND) { + app *a = to_app(cond); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr *arg = a->get_arg(i); + if (cond_is_guard(arg, t)) { + guards.push_back(arg); + } else { + leftovers.push_back(arg); + } + } + } else if (cond_is_guard(cond, t)) { + guard = cond; + return; + } else { + leftover = cond; + return; + } + + if (guards.size() > 1) { + guard = guard.m().mk_and(guards.size(), guards.c_ptr()); + } else if (guards.size() == 1) { + guard = guards.get(0); + } + + if (leftovers.size() > 1) { + leftover = leftover.m().mk_and(leftovers.size(), leftovers.c_ptr()); + } else if (leftovers.size() == 1) { + leftover = leftovers.get(0); + } + } +#endif + class udoc_plugin::filter_interpreted_fn : public relation_mutator_fn { + expr_ref m_condition; + //typename T::bitset_t m_filter; + //bit_vector m_empty_bv; + public: + filter_interpreted_fn(const udoc_relation & t, ast_manager& m, app *condition) : + m_condition(m) { + NOT_IMPLEMENTED_YET(); + //m_filter(t.get_num_bits(), true); + //m_empty_bv.resize(t.get_num_bits(), false); + + //expr_ref guard(m); + //split_cond_guard(condition, guard, m_condition, t); + //if (guard) + // m_filter.filter(guard, m_empty_bv, t); + } + + virtual void operator()(relation_base & tb) { + udoc_relation & t = get(tb); + // first apply guard and then run the interpreter on the leftover + //t.m_bitsets = m_filter.band(t.m_bitsets); + //if (m_condition) + // t.m_bitsets.filter(m_condition, m_empty_bv, t); + TRACE("dl", tout << "final size: " << t.get_size_estimate_rows() << '\n';); + } + }; + + + relation_mutator_fn * udoc_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) { - NOT_IMPLEMENTED_YET(); - return 0; + if (!check_kind(t)) + return 0; + TRACE("dl", tout << mk_pp(condition, get_ast_manager()) << '\n';); + return alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition); } + class udoc_plugin::negation_filter_fn : public relation_intersection_filter_fn { + const unsigned_vector m_t_cols; + const unsigned_vector m_neg_cols; + public: + negation_filter_fn(const udoc_relation & r, 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) { + SASSERT(joined_col_cnt > 0); + } + + virtual void operator()(relation_base& tb, const relation_base& negb) { + udoc_relation& t = get(tb); + udoc_relation const& neg = get(negb); + NOT_IMPLEMENTED_YET(); + // t.m_bitsets.filter_negate(t, neg.m_bitsets, neg, m_t_cols, m_neg_cols); + } + }; + + relation_intersection_filter_fn * udoc_plugin::mk_filter_by_negation_fn( + const relation_base& t, + const relation_base& neg, unsigned joined_col_cnt, const unsigned *t_cols, + const unsigned *negated_cols) { + if (!check_kind(t) || !check_kind(neg)) + return 0; + return alloc(negation_filter_fn, get(t), get(neg), joined_col_cnt, t_cols, negated_cols); + } + + } diff --git a/src/muz/ddnf/udoc_relation.h b/src/muz/ddnf/udoc_relation.h index 27035dd53..4e9c9c308 100644 --- a/src/muz/ddnf/udoc_relation.h +++ b/src/muz/ddnf/udoc_relation.h @@ -49,6 +49,7 @@ namespace datalog { virtual bool empty() const { return m_elems.empty(); } virtual void display(std::ostream& out) const; virtual bool is_precise() const { return true; } + virtual unsigned get_size_estimate_rows() const { return m_elems.size(); } doc_manager& get_dm() const { return dm; } udoc const& get_udoc() const { return m_elems; } @@ -67,11 +68,13 @@ namespace datalog { class project_fn; class union_fn; class rename_fn; - class filter_mask_fn; + class filter_equal_fn; class filter_identical_fn; class filter_interpreted_fn; class filter_by_negation_fn; class filter_by_union_fn; + class filter_proj_fn; + class negation_filter_fn; ast_manager& m; bv_util bv; u_map m_dms; @@ -103,6 +106,14 @@ namespace datalog { virtual relation_mutator_fn * mk_filter_equal_fn(const relation_base & t, const relation_element & value, unsigned col); virtual relation_mutator_fn * mk_filter_interpreted_fn(const relation_base & t, app * condition); + virtual relation_intersection_filter_fn * udoc_plugin::mk_filter_by_negation_fn( + const relation_base& t, + const relation_base& neg, unsigned joined_col_cnt, const unsigned *t_cols, + const unsigned *negated_cols); + virtual relation_transformer_fn * mk_filter_interpreted_and_project_fn( + const relation_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols); + // project join select }; };