From e32448d7ea197178b87d043a09965a9d9b8a3720 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 16 Sep 2014 21:46:39 -0700 Subject: [PATCH] more fun with docs Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 7 - src/ast/ast.h | 1 - src/muz/ddnf/doc.cpp | 3 + src/muz/ddnf/doc.h | 10 +- src/muz/ddnf/tbv.h | 2 + src/muz/ddnf/udoc_relation.cpp | 318 +++++++++++++++++++++++---------- src/muz/ddnf/udoc_relation.h | 6 + 7 files changed, 244 insertions(+), 103 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 0915ae1b6..95d47dc03 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2066,13 +2066,6 @@ expr* ast_manager::mk_or_reduced(unsigned n, expr* const* args) { } } -expr* ast_manager::mk_and_reduced(unsigned n, expr* const* args) { - switch (n) { - case 0: return mk_true(); - case 1: return args[0]; - default: return mk_and(n, args); - } -} func_decl * ast_manager::mk_fresh_func_decl(symbol const & prefix, symbol const & suffix, unsigned arity, sort * const * domain, sort * range) { diff --git a/src/ast/ast.h b/src/ast/ast.h index f8ba43554..1c4771e7f 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2005,7 +2005,6 @@ public: app * mk_false() { return m_false; } app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); } expr * mk_or_reduced(unsigned num_args, expr * const * args); - expr * mk_and_reduced(unsigned num_args, expr * const * args); func_decl* mk_and_decl() { diff --git a/src/muz/ddnf/doc.cpp b/src/muz/ddnf/doc.cpp index 5dd3d0eb1..2c6b4696e 100644 --- a/src/muz/ddnf/doc.cpp +++ b/src/muz/ddnf/doc.cpp @@ -73,6 +73,9 @@ void doc_manager::subtract(doc const& A, doc const& B, ptr_vector& result) bool doc_manager::equals(doc const& a, doc const& b) const { return false; } +bool doc_manager::is_full(doc const& src) const { + return false; +} unsigned doc_manager::hash(doc const& src) const { return 0; } diff --git a/src/muz/ddnf/doc.h b/src/muz/ddnf/doc.h index b311a9ef0..074045c95 100644 --- a/src/muz/ddnf/doc.h +++ b/src/muz/ddnf/doc.h @@ -51,7 +51,9 @@ public: doc& fill0(doc& src) const; doc& fill1(doc& src) const; doc& fillX(doc& src) const; + bool is_full(doc const& src) const; bool set_and(doc& dst, doc const& src) const; + bool intersect(doc const& A, doc const& B, doc& result) const; void complement(doc const& src, ptr_vector& result); void subtract(doc const& A, doc const& B, ptr_vector& result); bool equals(doc const& a, doc const& b) const; @@ -61,6 +63,8 @@ public: unsigned num_tbits() const { return m.num_tbits(); } }; +typedef union_find<> subset_ints; + // union of tbv*, union of doc* template class union_bvec { @@ -72,12 +76,12 @@ class union_bvec { e_fixed }; - typedef union_find<> subset_ints; public: unsigned size() const { return m_elems.size(); } T& operator[](unsigned idx) const { return *m_elems[idx]; } bool empty() const { return m_elems.empty(); } + bool is_full(M& m) const { return size() == 1 && m.is_full(*m_elems[0]); } bool contains(M& m, T& t) const { for (unsigned i = 0; i < m_elems.size(); ++i) { if (m.contains(*m_elems[i], t)) return true; @@ -143,7 +147,7 @@ public: T* inter = m.allocate(); for (unsigned i = 0; i < sz1; ++i) { for (unsigned j = 0; j < sz2; ++j) { - if (m.intesect(*m_elems[i], other[j], *inter)) { + if (m.intersect(*m_elems[i], other[j], *inter)) { result.push_back(inter); inter = m.allocate(); } @@ -151,7 +155,7 @@ public: } m.deallocate(inter); std::swap(result, *this); - result.reset(); + result.reset(m); } void complement(M& m, union_bvec& result) { union_bvec negated; diff --git a/src/muz/ddnf/tbv.h b/src/muz/ddnf/tbv.h index 2ae79a10d..c8b9b5c96 100644 --- a/src/muz/ddnf/tbv.h +++ b/src/muz/ddnf/tbv.h @@ -118,8 +118,10 @@ public: tbv_ref& operator=(tbv* d2) { if (d) mgr.deallocate(d); d = d2; + return *this; } tbv& operator*() { return *d; } + tbv* get() { return d; } }; diff --git a/src/muz/ddnf/udoc_relation.cpp b/src/muz/ddnf/udoc_relation.cpp index 8f422e77a..e14e5b98c 100644 --- a/src/muz/ddnf/udoc_relation.cpp +++ b/src/muz/ddnf/udoc_relation.cpp @@ -1,5 +1,7 @@ #include "udoc_relation.h" #include "dl_relation_manager.h" +#include "qe_util.h" +#include "ast_util.h" namespace datalog { @@ -387,110 +389,171 @@ namespace datalog { return 0; return alloc(filter_equal_fn, *this, get(t), value, col); } + + bool udoc_relation::is_guard(unsigned n, expr* const* gs) const { + for (unsigned i = 0; i < n; ++i) { + if (!is_guard(gs[i])) return false; + } + return true; + } + bool udoc_relation::is_guard(expr* g) const { + ast_manager& m = get_plugin().get_ast_manager(); + expr* e1, *e2; + 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)) { + if (is_var(e1) && is_var(e2)) return false; + NOT_IMPLEMENTED_YET(); + // TBD + } + if (is_var(g)) { + return true; + } + return false; + } + + void udoc_relation::extract_guard(expr* cond, expr_ref& guard, expr_ref& rest) const { + rest.reset(); + ast_manager& m = get_plugin().get_ast_manager(); + expr_ref_vector conds(m), guards(m), rests(m); + conds.push_back(cond); + qe::flatten_and(conds); + for (unsigned i = 0; i < conds.size(); ++i) { + expr* g = conds[i].get(); + if (is_guard(g)) { + guards.push_back(g); + } + else { + rests.push_back(g); + } + } + guard = mk_and(m, guards.size(), guards.c_ptr()); + rest = mk_and(m, rests.size(), rests.c_ptr()); + } + void udoc_relation::compile_guard(expr* g, udoc& d) const { + NOT_IMPLEMENTED_YET(); + } + void udoc_relation::apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) { + // datastructure to store equalities with columns that will be projected out + union_find_default_ctx union_ctx; + subset_ints equalities(union_ctx); + for (unsigned i = 0, e = discard_cols.size(); i < e; ++i) { + equalities.mk_var(); + } + apply_guard(g, result, equalities, discard_cols); + } + void udoc_relation::apply_guard( + expr* g, udoc& result, subset_ints& equalities, + bit_vector const& discard_cols) { + ast_manager& m = get_plugin().get_ast_manager(); + expr* e1, *e2; + if (result.empty()) { + } + else if (m.is_and(g)) { + for (unsigned i = 0; !result.empty() && i < to_app(g)->get_num_args(); ++i) { + apply_guard(to_app(g)->get_arg(i), result, equalities, discard_cols); + } + } + else if (m.is_not(g, e1)) { + udoc sub; + sub.push_back(dm.allocateX()); + apply_guard(e1, sub, equalities, discard_cols); + // TBD: result.subtract(dm, sub); + } + else if (m.is_or(g)) { + udoc sub; + sub.push_back(dm.allocateX()); + for (unsigned i = 0; !sub.empty() && i < to_app(g)->get_num_args(); ++i) { + expr_ref arg(m); + arg = to_app(g)->get_arg(i); + if (m.is_not(arg, e1)) { + arg = e1; + } + else { + arg = m.mk_not(arg); + } + apply_guard(arg, result, equalities, discard_cols); + } + // TBD: result.subtract(dm, sub); + } + else if (m.is_true(g)) { + } + else if (m.is_false(g)) { + result.reset(dm); + } + else if (is_var(g)) { + SASSERT(m.is_bool(g)); + unsigned v = to_var(g)->get_idx(); + unsigned idx = column_idx(v); + doc_manager& dm1 = get_plugin().dm(1); + tbv_ref bit1(dm1.tbv()); + bit1 = dm1.tbv().allocate1(); + result.fix_eq_bits(idx, bit1.get(), 0, 1, equalities, discard_cols); + } + else if (m.is_eq(g, e1, e2)) { #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; + const var *v; + unsigned vidx = 0; + unsigned length; + + unsigned low, high; + expr *e2; + if (is_var(e1)) { + v = to_var(e1); + length = column_num_bits(v->get_idx()); + } else if (bv.is_extract(e1, low, high, e11)) { + vidx = bv.get_bv_size(e11) - high - 1; + length = high - low + 1; + SASSERT(is_var(e11)); + v = to_var(e11); } else { - leftover = cond; - return; + NOT_IMPLEMENTED_YET(); } - - 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); - } - } + vidx += t.column_idx(v->get_idx()); + + unsigned final_idx = fix_eq_bits(vidx, e2, 0, length, t, equalities, discard_cols); + SASSERT(final_idx == vidx + length); + (void)final_idx; #endif + } + else { + // std::ostringstream strm; + // strm << "Guard expression is not handled" << mk_pp(g, m); + // throw default_exception(strm.str()); + throw 0; + } + } + 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; + doc_manager& dm; + expr_ref m_condition; + udoc m_udoc; + bit_vector m_empty_bv; public: filter_interpreted_fn(const udoc_relation & t, ast_manager& m, app *condition) : + dm(t.get_dm()), 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); + m_empty_bv.resize(t.get_num_bits(), false); + expr_ref guard(m), rest(m); + t.extract_guard(condition, guard, m_condition); + t.compile_guard(guard, m_udoc); + if (m.is_true(m_condition)) { + m_condition = 0; + } + } + + virtual ~filter_interpreted_fn() { + m_udoc.reset(dm); } 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); + udoc& u = t.get_udoc(); + u.intersect(dm, m_udoc); + if (m_condition && !u.empty()) { + t.apply_guard(m_condition, u, m_empty_bv); + } TRACE("dl", tout << "final size: " << t.get_size_estimate_rows() << '\n';); } }; @@ -531,5 +594,76 @@ namespace datalog { return alloc(negation_filter_fn, get(t), get(neg), joined_col_cnt, t_cols, negated_cols); } +#if 0 + /// make bits of table [idx,idx+max_length] equal to e sliced starting at idx2 + unsigned fix_eq_bits(unsigned idx, expr *e, unsigned idx2, unsigned max_length, + const table_information& t, subset_ints& equalities, + const bit_vector & discard_cols) { + const bv_util& bvu = t.get_bv_util(); + const dl_decl_util& dutil = t.get_decl_util(); + + rational n; + unsigned bv_size; + if (bvu.is_numeral(e, n, bv_size)) { + SASSERT(idx2 < bv_size); + max_length = std::min(max_length, bv_size - idx2); + T num(n, max_length); + fix_eq_bits(idx, &num, idx2, max_length, equalities, discard_cols); + return idx + max_length; + } + + uint64 num; + if (dutil.is_numeral(e, num)) { + T num_bv(rational(num,rational::ui64()), max_length); + fix_eq_bits(idx, &num_bv, idx2, max_length, equalities, discard_cols); + return idx + max_length; + } + + if (bvu.is_concat(e)) { + const app *a = to_app(e); + + // skip the first elements of the concat if e.g. we have a top level extract + unsigned i = 0; + for (; i < a->get_num_args(); ++i) { + unsigned arg_size = bvu.get_bv_size(a->get_arg(i)); + if (idx2 < arg_size) + break; + idx2 -= arg_size; + } + + SASSERT(i < a->get_num_args()); + for (; max_length > 0 && i < a->get_num_args(); ++i) { + unsigned idx0 = idx; + idx = fix_eq_bits(idx, a->get_arg(i), idx2, max_length, t, equalities, discard_cols); + idx2 = 0; + SASSERT((idx - idx0) <= max_length); + max_length = max_length - (idx - idx0); + } + return idx; + } + + unsigned low, high; + expr *e2; + if (bvu.is_extract(e, low, high, e2)) { + SASSERT(low <= high); + unsigned size = bvu.get_bv_size(e2); + unsigned offset = size - (high+1) + idx2; + SASSERT(idx2 < (high-low+1)); + max_length = std::min(max_length, high - low + 1 - idx2); + return fix_eq_bits(idx, e2, offset, max_length, t, equalities, discard_cols); + } + + if (e->get_kind() == AST_VAR) { + unsigned idx_var = idx2 + t.column_idx(to_var(e)->get_idx()); + SASSERT(idx2 < t.column_num_bits(to_var(e)->get_idx())); + max_length = std::min(max_length, t.column_num_bits(to_var(e)->get_idx()) - idx2); + fix_eq_bits(idx, 0, idx_var, max_length, equalities, discard_cols); + return idx + max_length; + } + + NOT_IMPLEMENTED_YET(); + return 0; + } +#endif } diff --git a/src/muz/ddnf/udoc_relation.h b/src/muz/ddnf/udoc_relation.h index 4e9c9c308..6c10a62bb 100644 --- a/src/muz/ddnf/udoc_relation.h +++ b/src/muz/ddnf/udoc_relation.h @@ -60,6 +60,12 @@ namespace datalog { unsigned column_idx(unsigned col) const { return m_column_info[col]; } unsigned column_num_bits(unsigned col) const { return m_column_info[col+1] - m_column_info[col]; } void expand_column_vector(unsigned_vector& v, udoc_relation* other = 0) const; + void extract_guard(expr* condition, expr_ref& guard, expr_ref& rest) const; + bool is_guard(expr* g) const; + bool is_guard(unsigned n, expr* const *g) const; + void compile_guard(expr* g, udoc& d) const; + void apply_guard(expr* g, udoc& result, bit_vector const& discard_cols); + void apply_guard(expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols); }; class udoc_plugin : public relation_plugin {