diff --git a/src/muz/ddnf/udoc_relation.cpp b/src/muz/ddnf/udoc_relation.cpp index 817909f14..dce993e87 100644 --- a/src/muz/ddnf/udoc_relation.cpp +++ b/src/muz/ddnf/udoc_relation.cpp @@ -146,7 +146,7 @@ namespace datalog { } void udoc_relation::display(std::ostream& out) const { - m_elems.display(dm, out); + m_elems.display(dm, out << "{") << "}"; } // ------------- diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index f5795df0c..a4c254272 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -206,6 +206,7 @@ namespace datalog { } void relation_manager::register_relation_plugin_impl(relation_plugin * plugin) { + TRACE("dl", tout << "register: " << plugin->get_name() << "\n";); m_relation_plugins.push_back(plugin); plugin->initialize(get_next_relation_fid(*plugin)); if (plugin->get_name() == get_context().default_relation()) { diff --git a/src/muz/ddnf/doc.cpp b/src/muz/rel/doc.cpp similarity index 97% rename from src/muz/ddnf/doc.cpp rename to src/muz/rel/doc.cpp index 4292aac05..cf27f3751 100644 --- a/src/muz/ddnf/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -193,7 +193,6 @@ 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) { - std::cout << "merge\n"; for (unsigned i = 0; i < length; ++i) { unsigned idx = lo + i; if (!merge(d, lo + i, equalities, discard_cols)) return false; @@ -245,12 +244,10 @@ bool doc_manager::merge(doc& d, unsigned idx, subset_ints& equalities, bit_vecto do { if (!discard_cols.get(idx) && idx != root1) { tbv* t = tbvm().allocate(d.pos()); - std::cout << "insert " << t << "\n"; t->set(idx, BIT_0); t->set(root1, BIT_1); d.neg().insert(tbvm(), t); t = tbvm().allocate(d.pos()); - std::cout << "insert " << t << "\n"; t->set(idx, BIT_1); t->set(root1, BIT_0); d.neg().insert(tbvm(), t); @@ -262,6 +259,11 @@ bool doc_manager::merge(doc& d, unsigned idx, subset_ints& equalities, bit_vecto return true; } +bool doc_manager::intersect(doc const& A, doc const& B, doc& result) { + copy(result, A); + return set_and(result, B); +} + // // 1. If n = 0,1: can project directly. // 2. If tbv_i uses X in all positions with vars or constant where tbv is constant: can project directly. @@ -454,11 +456,8 @@ bool doc_manager::contains(doc const& a, doc const& b) const { std::ostream& doc_manager::display(std::ostream& out, doc const& b) const { m.display(out, b.pos()); if (b.neg().is_empty()) return out; - out << " \\ {"; - for (unsigned i = 0; i < b.neg().size(); ++i) { - m.display(out, b.neg()[i]); - if (i + 1 < b.neg().size()) out << ", "; - } - return out << "}"; + out << " \\ "; + b.neg().display(m, out); + return out; } diff --git a/src/muz/ddnf/doc.h b/src/muz/rel/doc.h similarity index 98% rename from src/muz/ddnf/doc.h rename to src/muz/rel/doc.h index e3d36019b..01772543a 100644 --- a/src/muz/ddnf/doc.h +++ b/src/muz/rel/doc.h @@ -59,7 +59,7 @@ public: bool is_full(doc const& src) const; bool set_and(doc& dst, doc const& src); bool fold_neg(doc& dst); - bool intersect(doc const& A, doc const& B, doc& result) const; + bool intersect(doc const& A, doc const& B, doc& result); 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; @@ -101,12 +101,13 @@ public: } return false; } - std::ostream& display(M& m, std::ostream& out) const { + std::ostream& display(M const& m, std::ostream& out) const { + out << "{"; for (unsigned i = 0; i < size(); ++i) { m.display(out, *m_elems[i]); if (i + 1 < size()) out << ", "; } - return out << "\n"; + return out << "}"; } void push_back(T* t) { diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 742930b5c..920a0924a 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -32,6 +32,7 @@ Revision History: #include"karr_relation.h" #include"dl_finite_product_relation.h" #include"product_set.h" +#include"udoc_relation.h" #include"dl_lazy_table.h" #include"dl_sparse_table.h" #include"dl_table.h" @@ -114,6 +115,7 @@ namespace datalog { rm.register_plugin(alloc(interval_relation_plugin, rm)); rm.register_plugin(alloc(karr_relation_plugin, rm)); rm.register_plugin(alloc(product_set_plugin, rm)); + rm.register_plugin(alloc(udoc_plugin, rm)); } rel_context::~rel_context() { diff --git a/src/muz/ddnf/tbv.cpp b/src/muz/rel/tbv.cpp similarity index 100% rename from src/muz/ddnf/tbv.cpp rename to src/muz/rel/tbv.cpp diff --git a/src/muz/ddnf/tbv.h b/src/muz/rel/tbv.h similarity index 100% rename from src/muz/ddnf/tbv.h rename to src/muz/rel/tbv.h diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp new file mode 100644 index 000000000..f1f919ec7 --- /dev/null +++ b/src/muz/rel/udoc_relation.cpp @@ -0,0 +1,893 @@ +#include "udoc_relation.h" +#include "dl_relation_manager.h" +#include "qe_util.h" +#include "ast_util.h" + +namespace datalog { + + udoc_relation::udoc_relation(udoc_plugin& p, relation_signature const& sig): + relation_base(p, sig), + dm(p.dm(p.num_signature_bits(sig))) { + unsigned column = 0; + for (unsigned i = 0; i < sig.size(); ++i) { + m_column_info.push_back(column); + column += p.num_sort_bits(sig[i]); + } + m_column_info.push_back(column); + } + udoc_relation::~udoc_relation() { + reset(); + } + void udoc_relation::reset() { + m_elems.reset(dm); + } + void udoc_relation::expand_column_vector(unsigned_vector& v, udoc_relation* other) const { + unsigned_vector orig; + orig.swap(v); + for (unsigned i = 0; i < orig.size(); ++i) { + unsigned col, limit; + if (orig[i] < get_num_cols()) { + col = column_idx(orig[i]); + limit = col + column_num_bits(orig[i]); + } else { + unsigned idx = orig[i] - get_num_cols(); + col = get_num_bits() + other->column_idx(idx); + limit = col + other->column_num_bits(idx); + } + for (; col < limit; ++col) { + v.push_back(col); + } + } + } + + doc* udoc_relation::fact2doc(const relation_fact & f) const { + doc* d = dm.allocate0(); + for (unsigned i = 0; i < f.size(); ++i) { + unsigned bv_size; + rational val; + VERIFY(get_plugin().is_numeral(f[i], val, bv_size)); + SASSERT(bv_size == column_num_bits(i)); + unsigned lo = column_idx(i); + unsigned hi = column_idx(i + 1); + d->pos().set(val, hi, lo); + } + return d; + } + void udoc_relation::add_fact(const relation_fact & f) { + doc* d = fact2doc(f); + m_elems.insert(dm, d); + } + bool udoc_relation::contains_fact(const relation_fact & f) const { + doc_ref d(dm, fact2doc(f)); + return m_elems.contains(dm, *d); + } + udoc_relation * udoc_relation::clone() const { + udoc_relation* result = udoc_plugin::get(get_plugin().mk_empty(get_signature())); + for (unsigned i = 0; i < m_elems.size(); ++i) { + result->m_elems.push_back(dm.allocate(m_elems[i])); + } + return result; + } + udoc_relation * udoc_relation::complement(func_decl* f) const { + udoc_relation* result = udoc_plugin::get(get_plugin().mk_empty(get_signature())); + m_elems.complement(dm, result->m_elems); + return result; + } + void udoc_relation::to_formula(expr_ref& fml) const { + ast_manager& m = fml.get_manager(); + expr_ref_vector disj(m); + for (unsigned i = 0; i < m_elems.size(); ++i) { + disj.push_back(to_formula(m_elems[i])); + } + fml = mk_or(m, disj.size(), disj.c_ptr()); + } + expr_ref udoc_relation::to_formula(doc const& d) const { + ast_manager& m = get_plugin().get_ast_manager(); + expr_ref result(m); + expr_ref_vector conjs(m); + conjs.push_back(to_formula(d.pos())); + for (unsigned i = 0; i < d.neg().size(); ++i) { + conjs.push_back(m.mk_not(to_formula(d.neg()[i]))); + } + result = mk_and(m, conjs.size(), conjs.c_ptr()); + return result; + } + expr_ref udoc_relation::to_formula(tbv const& t) const { + udoc_plugin& p = get_plugin(); + ast_manager& m = p.get_ast_manager(); + expr_ref result(m); + expr_ref_vector conjs(m); + for (unsigned i = 0; i < get_num_cols(); ++i) { + var_ref v(m); + v = m.mk_var(i, get_signature()[i]); + unsigned lo = column_idx(i); + unsigned hi = column_idx(i+1); + rational r(0); + unsigned lo0 = lo; + bool is_x = true; + for (unsigned j = lo; j < hi; ++j) { + switch(t[j]) { + case BIT_0: + if (is_x) is_x = false, lo0 = j, r.reset(); + break; + case BIT_1: + if (is_x) is_x = false, lo0 = j, r.reset(); + r += rational::power_of_two(j - lo0); + break; + case BIT_x: + if (!is_x) { + conjs.push_back(m.mk_eq(p.bv.mk_extract(j-1,lo0,v), + p.bv.mk_numeral(r,j-lo0))); + } + is_x = true; + break; + default: + UNREACHABLE(); + } + } + if (!is_x) { + expr_ref num(m); + if (lo0 == lo) { + num = p.mk_numeral(r, get_signature()[i]); + conjs.push_back(m.mk_eq(v, num)); + } + else { + num = p.bv.mk_numeral(r, hi-lo0); + conjs.push_back(m.mk_eq(p.bv.mk_extract(hi-1,lo0,v), num)); + } + } + } + result = mk_and(m, conjs.size(), conjs.c_ptr()); + return result; + } + + udoc_plugin& udoc_relation::get_plugin() const { + return static_cast(relation_base::get_plugin()); + } + + void udoc_relation::display(std::ostream& out) const { + m_elems.display(dm, out); + } + + // ------------- + + udoc_plugin::udoc_plugin(relation_manager& rm): + relation_plugin(udoc_plugin::get_name(), rm), + m(rm.get_context().get_manager()), + bv(m), + dl(m) { + } + udoc_plugin::~udoc_plugin() { + u_map::iterator it = m_dms.begin(), end = m_dms.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } + } + udoc_relation& udoc_plugin::get(relation_base& r) { + return dynamic_cast(r); + } + udoc_relation* udoc_plugin::get(relation_base* r) { + return r?dynamic_cast(r):0; + } + udoc_relation const & udoc_plugin::get(relation_base const& r) { + return dynamic_cast(r); + } + + doc_manager& udoc_plugin::dm(relation_signature const& sig) { + return dm(num_signature_bits(sig)); + } + + doc_manager& udoc_plugin::dm(unsigned n) { + doc_manager* r; + if (!m_dms.find(n, r)) { + r = alloc(doc_manager, n); + m_dms.insert(n, r); + } + return *r; + } + expr* udoc_plugin::mk_numeral(rational const& r, sort* s) { + if (bv.is_bv_sort(s)) { + return bv.mk_numeral(r, s); + } + SASSERT(dl.is_finite_sort(s)); + return dl.mk_numeral(r.get_uint64(), s); + } + bool udoc_plugin::is_numeral(expr* e, rational& r, unsigned& num_bits) { + if (bv.is_numeral(e, r, num_bits)) return true; + uint64 n, sz; + ast_manager& m = get_ast_manager(); + if (dl.is_numeral(e, n) && dl.try_get_size(m.get_sort(e), sz)) { + num_bits = 0; + while (sz > 0) ++num_bits, sz = sz/2; + r = rational(n, rational::ui64()); + return true; + } + return false; + } + unsigned udoc_plugin::num_sort_bits(sort* s) const { + unsigned num_bits = 0; + if (bv.is_bv_sort(s)) + return bv.get_bv_size(s); + uint64 sz; + if (dl.try_get_size(s, sz)) { + while (sz > 0) ++num_bits, sz /= 2; + return num_bits; + } + UNREACHABLE(); + return 0; + } + unsigned udoc_plugin::num_signature_bits(relation_signature const& sig) { + unsigned result = 0; + for (unsigned i = 0; i < sig.size(); ++i) { + result += num_sort_bits(sig[i]); + } + return result; + } + + bool udoc_plugin::is_finite_sort(sort* s) const { + return bv.is_bv_sort(s) || dl.is_finite_sort(s); + } + + + bool udoc_plugin::can_handle_signature(const relation_signature & sig) { + for (unsigned i = 0; i < sig.size(); ++i) { + if (!is_finite_sort(sig[i])) + return false; + } + return true; + } + relation_base * udoc_plugin::mk_empty(const relation_signature & sig) { + return alloc(udoc_relation, *this, sig); + } + relation_base * udoc_plugin::mk_full(func_decl* p, const relation_signature & s) { + udoc_relation* r = get(mk_empty(s)); + r->get_udoc().push_back(dm(s).allocateX()); + return r; + } + class udoc_plugin::join_fn : public convenient_relation_join_fn { + doc_manager& dm; + doc_manager& dm1; + doc_manager& dm2; + public: + join_fn(udoc_plugin& p, udoc_relation const& t1, udoc_relation const& t2, unsigned col_cnt, + const unsigned * cols1, const unsigned * cols2) + : convenient_relation_join_fn(t1.get_signature(), t2.get_signature(), col_cnt, cols1, cols2), + dm(p.dm(get_result_signature())), + dm1(t1.get_dm()), + dm2(t2.get_dm()) { + t1.expand_column_vector(m_cols1); + t2.expand_column_vector(m_cols2); + } + + void join(doc const& d1, doc const& d2, udoc& result) { + doc* 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); + // first fix bits + for (unsigned i = 0; i < m_cols1.size(); ++i) { + unsigned idx1 = m_cols1[i]; + unsigned idx2 = mid + m_cols2[i]; + tbit v1 = pos[idx1]; + tbit v2 = pos[idx2]; + + if (v1 == BIT_x) { + if (v2 != BIT_x) + pos.set(idx1, v2); + } else if (v2 == BIT_x) { + pos.set(idx2, v1); + } else if (v1 != v2) { + dm.deallocate(d); + // columns don't match + return; + } + } + // fix equality of don't care columns + for (unsigned i = 0; i < m_cols1.size(); ++i) { + unsigned idx1 = m_cols1[i]; + unsigned idx2 = mid + m_cols2[i]; + unsigned v1 = pos[idx1]; + unsigned v2 = pos[idx2]; + + 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); + } + } + + // 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); + } + for (unsigned i = 0; i < d2.neg().size(); ++i) { + tbv* t = dm.tbvm().allocate(); + t->set(d1.pos(), mid-1, 0); + t->set(d2.neg()[i], hi - 1, mid); + neg.push_back(t); + } + result.insert(dm, d); + } + + virtual relation_base * operator()(const relation_base & _r1, const relation_base & _r2) { + udoc_relation const& r1 = get(_r1); + udoc_relation const& r2 = get(_r2); + TRACE("dl", r1.display(tout << "r1:\n"); r2.display(tout << "r2:\n");); + udoc_plugin& p = r1.get_plugin(); + relation_signature const& sig = get_result_signature(); + udoc_relation * result = alloc(udoc_relation, p, sig); + udoc const& d1 = r1.get_udoc(); + udoc const& d2 = r2.get_udoc(); + udoc& r = result->get_udoc(); + for (unsigned i = 0; i < d1.size(); ++i) { + for (unsigned j = 0; j < d2.size(); ++j) { + join(d1[i], d2[j], r); + } + } + TRACE("dl", result->display(tout << "result:\n");); + return result; + } + }; + relation_join_fn * udoc_plugin::mk_join_fn( + const relation_base & t1, const relation_base & t2, + unsigned col_cnt, const unsigned * cols1, const unsigned * cols2) { + if (!check_kind(t1) || !check_kind(t2)) { + return 0; + } + return alloc(join_fn, *this, get(t1), get(t2), col_cnt, cols1, cols2); + } + class udoc_plugin::project_fn : public convenient_relation_project_fn { + svector m_to_delete; + public: + project_fn(udoc_relation const & t, unsigned removed_col_cnt, const unsigned * removed_cols) + : convenient_relation_project_fn(t.get_signature(), removed_col_cnt, removed_cols) { + t.expand_column_vector(m_removed_cols); + unsigned n = t.get_dm().num_tbits(); + m_to_delete.resize(n, false); + for (unsigned i = 0; i < m_removed_cols.size(); ++i) { + m_to_delete[m_removed_cols[i]] = true; + } + } + + virtual relation_base * operator()(const relation_base & tb) { + TRACE("dl", tb.display(tout << "src:\n");); + udoc_relation const& t = get(tb); + udoc_plugin& p = t.get_plugin(); + udoc_relation* r = udoc_plugin::get(p.mk_empty(get_result_signature())); + doc_manager& dm1 = t.get_dm(); + doc_manager& dm2 = r->get_dm(); + doc_ref d2(dm2); + udoc const& ud1 = t.get_udoc(); + udoc& ud2 = r->get_udoc(); + for (unsigned i = 0; i < ud1.size(); ++i) { + d2 = dm1.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), ud1[i]); + ud2.push_back(d2.detach()); + } + TRACE("dl", tout << "final size: " << r->get_size_estimate_rows() << '\n';); + return r; + } + }; + + + relation_transformer_fn * udoc_plugin::mk_project_fn( + const relation_base & t, unsigned col_cnt, + const unsigned * removed_cols) { + if (!check_kind(t)) + return 0; + return alloc(project_fn, get(t), col_cnt, removed_cols); + } + + class udoc_plugin::rename_fn : public convenient_relation_rename_fn { + unsigned_vector m_permutation; + public: + rename_fn(udoc_relation const& t, unsigned cycle_len, const unsigned * cycle) + : convenient_relation_rename_fn(t.get_signature(), cycle_len, cycle) { + udoc_plugin& p = t.get_plugin(); + for (unsigned i = 0; i < t.get_num_bits(); ++i) { + m_permutation.push_back(i); + } + unsigned len = t.column_num_bits(cycle[0]); + for (unsigned i = 0; i < cycle_len; ++i) { + unsigned j = (i + 1)%cycle_len; + unsigned col1 = cycle[i]; + unsigned col2 = cycle[j]; + unsigned lo1 = t.column_idx(col1); + unsigned lo2 = t.column_idx(col2); + for (unsigned k = 0; k < len; ++k) { + m_permutation[k + lo1] = k + lo2; + } + SASSERT(t.column_num_bits(col1) == t.column_num_bits(col2)); + } + } + + virtual relation_base * operator()(const relation_base & _r) { + udoc_relation const& r = get(_r); + TRACE("dl", r.display(tout << "r:\n");); + udoc_plugin& p = r.get_plugin(); + relation_signature const& sig = get_result_signature(); + udoc_relation* result = alloc(udoc_relation, p, sig); + udoc const& src = r.get_udoc(); + udoc& dst = result->get_udoc(); + doc_manager& dm = r.get_dm(); + for (unsigned i = 0; i < src.size(); ++i) { + dst.push_back(dm.allocate(src[i], m_permutation.c_ptr())); + } + TRACE("dl", result->display(tout << "result:\n");); + return result; + } + }; + relation_transformer_fn * udoc_plugin::mk_rename_fn( + const relation_base & r, + unsigned cycle_len, const unsigned * permutation_cycle) { + if (check_kind(r)) { + return alloc(rename_fn, get(r), cycle_len, permutation_cycle); + } + else { + return 0; + } + } + class udoc_plugin::union_fn : public relation_union_fn { + public: + union_fn() {} + + virtual void operator()(relation_base & _r, const relation_base & _src, relation_base * _delta) { + TRACE("dl", _r.display(tout << "dst:\n"); _src.display(tout << "src:\n");); + udoc_relation& r = get(_r); + udoc_relation const& src = get(_src); + udoc_relation* d = get(_delta); + doc_manager& dm = r.get_dm(); + udoc* d1 = 0; + if (d) d1 = &d->get_udoc(); + if (d1) d1->reset(dm); + r.get_plugin().mk_union(dm, r.get_udoc(), src.get_udoc(), d1); + TRACE("dl", _r.display(tout << "dst':\n");); + } + }; + void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) { + for (unsigned i = 0; i < src.size(); ++i) { + doc* d = dm.allocate(src[i]); + if (dst.insert(dm, d)) { + if (delta) { + delta->insert(dm, dm.allocate(src[i])); + } + } + } + } + relation_union_fn * udoc_plugin::mk_union_fn( + const relation_base & tgt, const relation_base & src, + const relation_base * delta) { + if (!check_kind(tgt) || !check_kind(src) || (delta && !check_kind(*delta))) { + return 0; + } + return alloc(union_fn); + } + relation_union_fn * udoc_plugin::mk_widen_fn( + const relation_base & tgt, const relation_base & src, + const relation_base * delta) { + return mk_union_fn(tgt, src, delta); + } + + class udoc_plugin::filter_identical_fn : public relation_mutator_fn { + unsigned_vector m_cols; + unsigned m_size; + bit_vector m_empty_bv; + union_find_default_ctx union_ctx; + union_find<> m_equalities; + public: + filter_identical_fn(const relation_base & _r, unsigned col_cnt, const unsigned *identical_cols) + : m_cols(col_cnt), m_equalities(union_ctx) { + udoc_relation const& r = get(_r); + doc_manager& dm = r.get_dm(); + unsigned num_bits = dm.num_tbits(); + m_size = r.column_num_bits(identical_cols[0]); + m_empty_bv.resize(r.get_num_bits(), false); + for (unsigned i = 0; i < col_cnt; ++i) { + m_cols[i] = r.column_idx(identical_cols[i]); + } + for (unsigned i = 0, e = m_empty_bv.size(); i < e; ++i) { + m_equalities.mk_var(); + } + for (unsigned i = 1; i < col_cnt; ++i) { + for (unsigned j = 0; j < m_size; ++j) { + m_equalities.merge(m_cols[0]+j ,m_cols[i]+j); + } + } + } + + virtual void operator()(relation_base & _r) { + udoc_relation& r = get(_r); + udoc& d = r.get_udoc(); + doc_manager& dm = r.get_dm(); + d.merge(dm, m_cols[0], m_size, m_equalities, m_empty_bv); + TRACE("dl", tout << "final size: " << r.get_size_estimate_rows() << '\n';); + } + }; + relation_mutator_fn * udoc_plugin::mk_filter_identical_fn( + const relation_base & t, unsigned col_cnt, const unsigned * identical_cols) { + return check_kind(t)?alloc(filter_identical_fn, t, col_cnt, identical_cols):0; + } + 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.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) { + if (!check_kind(t)) + 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 { + udoc_plugin& p = get_plugin(); + ast_manager& m = p.get_ast_manager(); + bv_util& bv = p.bv; + expr* e1, *e2, *e3; + unsigned hi, lo; + 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(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, bit_vector const& discard_cols) const { + d.reset(dm); + d.push_back(dm.allocateX()); + apply_guard(g, d, discard_cols); + } + void udoc_relation::apply_guard(expr* g, udoc& result, bit_vector const& discard_cols) const { + // 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); + } + bool udoc_relation::apply_eq(expr* g, udoc& result, var* 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); + lo += col; + hi += col; + if (p.is_numeral(c, r, num_bits)) { + doc_ref d(dm, dm.allocateX()); + d->pos().set(r, hi, lo); + result.intersect(dm, *d); + return true; + } + // other cases? + return false; + } + + void udoc_relation::apply_guard( + expr* g, udoc& result, subset_ints& equalities, bit_vector const& discard_cols) const { + ast_manager& m = get_plugin().get_ast_manager(); + bv_util& bv = get_plugin().bv; + expr* e1, *e2; + if (result.is_empty()) { + } + else if (m.is_and(g)) { + for (unsigned i = 0; !result.is_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)) { + // REVIEW: (not (= x y)) should not cause + // the equivalence class to collapse. + // It seems the current organization with fix_eq_bits + // will merge the equivalence class as a side-effect. + udoc sub; + sub.push_back(dm.allocateX()); + apply_guard(e1, sub, equalities, discard_cols); + result.subtract(dm, sub); + } + else if (m.is_or(g)) { + udoc sub; + sub.push_back(dm.allocateX()); + for (unsigned i = 0; !sub.is_empty() && i < to_app(g)->get_num_args(); ++i) { + expr_ref arg(m); + arg = mk_not(m, to_app(g)->get_arg(i)); + apply_guard(arg, result, equalities, discard_cols); + } + 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_ref d(dm); + d = dm.allocateX(); + dm.set(*d, idx, BIT_1); + result.intersect(dm, *d); + } + else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) { + unsigned hi, lo; + expr* e3; + if (is_var(e1) && is_ground(e2) && + apply_eq(g, result, to_var(e1), bv.get_bv_size(e1)-1, 0, 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 (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()); + result.merge(dm, idx1, idx2, length, discard_cols); + } + else { + goto failure_case; + } + } + else { + failure_case: + std::ostringstream strm; + strm << "Guard expression is not handled" << mk_pp(g, m); + throw default_exception(strm.str()); + } + } + + class udoc_plugin::filter_interpreted_fn : public relation_mutator_fn { + 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) { + 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, m_empty_bv); + if (m.is_true(m_condition)) { + m_condition = 0; + } + TRACE("dl", + tout << "condition: " << mk_pp(condition, m) << "\n"; + tout << m_condition << "\n"; m_udoc.display(dm, tout) << "\n";); + } + + virtual ~filter_interpreted_fn() { + m_udoc.reset(dm); + } + + virtual void operator()(relation_base & tb) { + udoc_relation & t = get(tb); + 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); + } + 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) { + return check_kind(t)?alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition):0; + } + + 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& n = get(negb); + udoc & dst = t.get_udoc(); + udoc const & neg = n.get_udoc(); + doc_manager& dm = t.get_dm(); + udoc result; + for (unsigned i = 0; i < dst.size(); ++i) { + 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) { + unsigned t_col = m_t_cols[c]; + unsigned n_col = m_neg_cols[c]; + unsigned num_bits = t.column_num_bits(t_col); + SASSERT(num_bits == n.column_num_bits(n_col)); + unsigned t_idx = t.column_idx(t_col); + unsigned n_idx = n.column_idx(n_col); + for (unsigned k = 0; !done_j && k < num_bits; ++k) { + tbit n_bit = neg[j][n_idx + k]; + tbit d_bit = dst[i][t_idx + k]; + // neg does not contain dst. + done_j = (n_bit != BIT_x && n_bit != d_bit); + } + } + if (done_j) { + result.push_back(&dst[i]); + } + else { + dm.deallocate(&dst[i]); + done_i = true; + } + } + } + std::swap(dst, result); + if (dst.is_empty()) { + return; + } + + // slow case + udoc renamed_neg; + for (unsigned i = 0; i < neg.size(); ++i) { + doc_ref newD(dm, dm.allocateX()); + for (unsigned j = 0; j < m_neg_cols.size(); ++j) { + copy_column(*newD, neg[i], m_t_cols[j], m_neg_cols[j], t, n); + } + renamed_neg.push_back(newD.detach()); + } + dst.subtract(t.get_dm(), renamed_neg); + } + void copy_column( + doc& dst, doc const& src, + unsigned col_dst, unsigned col_src, + udoc_relation const& dstt, + udoc_relation const& srct) { + doc_manager& dm = dstt.get_dm(); + unsigned idx_dst = dstt.column_idx(col_dst); + unsigned idx_src = srct.column_idx(col_src); + unsigned num_bits = dstt.column_num_bits(col_dst); + SASSERT(num_bits == srct.column_num_bits(col_src)); + for (unsigned i = 0; i < num_bits; ++i) { + dm.set(dst, idx_dst+i, src[idx_src+i]); + } + } + }; + + 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); + } + + class udoc_plugin::filter_proj_fn : public convenient_relation_project_fn { + 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 + 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) { + t.expand_column_vector(m_removed_cols); + m_col_list.resize(t.get_num_bits(), false); + for (unsigned i = 0; i < m_removed_cols.size(); ++i) { + m_col_list.set(m_removed_cols[i], true); + } + m_to_delete.resize(m_removed_cols.size(), false); + 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); + t.compile_guard(guard, m_udoc, m_col_list); + if (m.is_true(m_condition)) { + m_condition = 0; + } + } + + virtual ~filter_proj_fn() { + m_udoc.reset(dm); + } + virtual relation_base* operator()(const relation_base & tb) { + udoc_relation const & t = get(tb); + udoc const& u1 = t.get_udoc(); + doc_manager& dm = t.get_dm(); + udoc u2; + u2.copy(dm, u1); + u2.intersect(dm, m_udoc); + if (m_condition && !u2.is_empty()) { + t.apply_guard(m_condition, u2, m_col_list); + } + udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature())); + doc_manager& dm2 = r->get_dm(); + for (unsigned i = 0; i < u2.size(); ++i) { + doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), u2[i]); + r->get_udoc().insert(dm2, d); + } + u2.reset(dm); + return r; + } + }; + relation_transformer_fn * udoc_plugin::mk_filter_interpreted_and_project_fn( + const relation_base & t, app * condition, + unsigned removed_col_cnt, const unsigned * removed_cols) { + return check_kind(t)?alloc(filter_proj_fn, get(t), get_ast_manager(), condition, removed_col_cnt, removed_cols):0; + } + + +} diff --git a/src/muz/ddnf/udoc_relation.h b/src/muz/rel/udoc_relation.h similarity index 98% rename from src/muz/ddnf/udoc_relation.h rename to src/muz/rel/udoc_relation.h index 5205a9547..4befa228a 100644 --- a/src/muz/ddnf/udoc_relation.h +++ b/src/muz/rel/udoc_relation.h @@ -121,7 +121,7 @@ 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( + virtual relation_intersection_filter_fn * 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); diff --git a/src/test/doc.cpp b/src/test/doc.cpp index 2747ef35d..890ce4204 100644 --- a/src/test/doc.cpp +++ b/src/test/doc.cpp @@ -224,7 +224,7 @@ class test_doc_cls { void test_merge(unsigned num_clauses) { doc_ref d(dm, dm.allocateX()); - expr_ref_vector fmls(m); + expr_ref_vector fmls(m), eqs(m); th_rewriter rw(m); unsigned N = m_vars.size(); expr_ref fml1(m), fml2(m), fml3(m), tmp1(m), tmp2(m), fml(m); @@ -251,15 +251,26 @@ class test_doc_cls { for (unsigned i = 0; i < N; ++i) { if (to_merge[i] && i != lo) { equalities.merge(i, lo); + eqs.push_back(m.mk_eq(m_vars[i].get(), m_vars[lo].get())); } } - fml1 = to_formula(*d, dm, to_delete.c_ptr()); + eqs.push_back(to_formula(*d, dm, to_delete.c_ptr())); + fml1 = mk_and(m, eqs.size(), eqs.c_ptr()); if (dm.merge(*d, lo, 1, equalities, discard_cols)) { fml2 = to_formula(*d, dm, to_delete.c_ptr()); - std::cout << fml1 << "\n"; - std::cout << fml2 << "\n"; } - // ... + else { + fml2 = m.mk_false(); + } + rw(fml1); + rw(fml2); + smt_params fp; + smt::kernel solver(m, fp); + TRACE("doc", tout << "manual project:\n" << fml1 << "\nautomatic project: \n" << fml2 << "\n";); + fml = m.mk_not(m.mk_eq(fml1, fml2)); + solver.assert_expr(fml); + lbool res = solver.check(); + SASSERT(res == l_false); } public: diff --git a/src/test/main.cpp b/src/test/main.cpp index f613402b8..d5608a7d4 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -143,6 +143,7 @@ int main(int argc, char ** argv) { TST(fixed_bit_vector); TST(tbv); TST(doc); + TST(udoc_relation); TST(string_buffer); TST(map); TST(diff_logic); diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp new file mode 100644 index 000000000..2c5540fe2 --- /dev/null +++ b/src/test/udoc_relation.cpp @@ -0,0 +1,211 @@ +#include "udoc_relation.h" +#include "trace.h" +#include "vector.h" +#include "ast.h" +#include "ast_pp.h" +#include "reg_decl_plugins.h" +#include "sorting_network.h" +#include "smt_kernel.h" +#include "model_smt2_pp.h" +#include "smt_params.h" +#include "ast_util.h" +#include "expr_safe_replace.h" +#include "th_rewriter.h" +#include "dl_relation_manager.h" +#include "dl_register_engine.h" +#include "rel_context.h" +#include "bv_decl_plugin.h" + +class udoc_tester { + typedef datalog::relation_base relation_base; + typedef datalog::udoc_relation udoc_relation; + typedef datalog::udoc_plugin udoc_plugin; + typedef datalog::relation_signature relation_signature; + + struct init { + init(ast_manager& m) { + reg_decl_plugins(m); + } + }; + random_gen m_rand; + ast_manager m; + init m_init; + bv_util bv; + expr_ref_vector m_vars; + smt_params m_smt_params; + datalog::register_engine m_reg; + datalog::context m_ctx; + datalog::rel_context rc; + udoc_plugin& p; +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")))) + { + } + + udoc_relation* mk_empty(relation_signature const& sig) { + SASSERT(p.can_handle_signature(sig)); + relation_base* empty = p.mk_empty(sig); + return dynamic_cast(empty); + } + + udoc_relation* mk_full(relation_signature const& sig) { + func_decl_ref fn(m); + fn = m.mk_func_decl(symbol("full"), sig.size(), sig.c_ptr(), m.mk_bool_sort()); + relation_base* full = p.mk_full(fn, sig); + return dynamic_cast(full); + } + + void test1() { + datalog::relation_signature sig; + sig.push_back(bv.mk_sort(12)); + sig.push_back(bv.mk_sort(6)); + sig.push_back(bv.mk_sort(12)); + + datalog::relation_fact fact1(m), fact2(m), fact3(m); + fact1.push_back(bv.mk_numeral(rational(1), 12)); + fact1.push_back(bv.mk_numeral(rational(6), 6)); + fact1.push_back(bv.mk_numeral(rational(56), 12)); + fact2.push_back(bv.mk_numeral(rational(8), 12)); + fact2.push_back(bv.mk_numeral(rational(16), 6)); + fact2.push_back(bv.mk_numeral(rational(32), 12)); + fact3.push_back(bv.mk_numeral(rational(32), 12)); + fact3.push_back(bv.mk_numeral(rational(16), 6)); + fact3.push_back(bv.mk_numeral(rational(4), 12)); + + relation_base* t; + expr_ref fml(m); + // empty + { + std::cout << "empty\n"; + t = mk_empty(sig); + t->display(std::cout); std::cout << "\n"; + t->to_formula(fml); + std::cout << fml << "\n"; + t->deallocate(); + } + + // full + { + std::cout << "full\n"; + t = mk_full(sig); + t->display(std::cout); std::cout << "\n"; + t->to_formula(fml); + std::cout << fml << "\n"; + t->deallocate(); + } + + // join + { + udoc_relation* t1 = mk_full(sig); + udoc_relation* t2 = mk_full(sig); + udoc_relation* t3 = mk_empty(sig); + unsigned_vector jc1, jc2; + jc1.push_back(1); + jc2.push_back(1); + datalog::relation_join_fn* join_fn = p.mk_join_fn(*t1, *t2, jc1.size(), jc1.c_ptr(), jc2.c_ptr()); + SASSERT(join_fn); + t = (*join_fn)(*t1, *t2); + t->display(std::cout); std::cout << "\n"; + t->deallocate(); + + t = (*join_fn)(*t1, *t3); + SASSERT(t->empty()); + t->display(std::cout); std::cout << "\n"; + t->deallocate(); + + t = (*join_fn)(*t3, *t3); + SASSERT(t->empty()); + t->display(std::cout); std::cout << "\n"; + t->deallocate(); + + dealloc(join_fn); + t1->deallocate(); + t2->deallocate(); + t3->deallocate(); + } + + // project + { + std::cout << "project\n"; + udoc_relation* t1 = mk_full(sig); + unsigned_vector pc; + pc.push_back(0); + datalog::relation_transformer_fn* proj_fn = p.mk_project_fn(*t1, pc.size(), pc.c_ptr()); + t = (*proj_fn)(*t1); + t->display(std::cout); std::cout << "\n"; + t->deallocate(); + + t1->reset(); + t = (*proj_fn)(*t1); + t->display(std::cout); std::cout << "\n"; + t->deallocate(); + + t1->add_fact(fact1); + t1->add_fact(fact2); + t1->add_fact(fact3); + t = (*proj_fn)(*t1); + t1->display(std::cout); std::cout << "\n"; + t->display(std::cout); std::cout << "\n"; + t->deallocate(); + + dealloc(proj_fn); + t1->deallocate(); + } + + // rename + { + udoc_relation* t1 = mk_empty(sig); + unsigned_vector cycle; + cycle.push_back(0); + cycle.push_back(2); + datalog::relation_transformer_fn* rename = p.mk_rename_fn(*t1, cycle.size(), cycle.c_ptr()); + + t1->add_fact(fact1); + t1->add_fact(fact2); + t1->add_fact(fact3); + t = (*rename)(*t1); + t1->display(std::cout); std::cout << "\n"; + t->display(std::cout); std::cout << "\n"; + t->deallocate(); + + dealloc(rename); + t1->deallocate(); + } + + // union + { + udoc_relation* t1 = mk_empty(sig); + udoc_relation* t2 = mk_empty(sig); + udoc_relation* delta = mk_full(sig); + t2->add_fact(fact1); + t2->add_fact(fact2); + t1->add_fact(fact3); + + datalog::relation_union_fn* union_fn = p.mk_union_fn(*t1, *t2, 0); + + t1->display(std::cout << "t1 before:"); std::cout << "\n"; + (*union_fn)(*t1, *t2, delta); + t1->display(std::cout << "t1 after:"); std::cout << "\n"; + delta->display(std::cout << "delta:"); std::cout << "\n"; + + t1->deallocate(); + t2->deallocate(); + delta->deallocate(); + } + + // filter_identical + + // filter_interpreted + + // filter_by_negation + + // filter_interpreted_project + } +}; + +void tst_udoc_relation() { + udoc_tester tester; + + tester.test1(); +}