From 9cea3a1c021ec580c76eaac36232d77731f9488d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 Sep 2014 22:08:49 -0700 Subject: [PATCH] last? bug-fix to new udoc_relation for feature parity Signed-off-by: Nikolaj Bjorner --- src/muz/rel/check_relation.cpp | 110 +++++++++++++++++++++++++++------ src/muz/rel/check_relation.h | 13 ++-- src/muz/rel/doc.cpp | 26 +++++++- src/muz/rel/doc.h | 13 +++- src/muz/rel/tbv.cpp | 27 +++++++- src/muz/rel/tbv.h | 4 ++ src/muz/rel/udoc_relation.cpp | 110 ++++++++++++++++++++++----------- 7 files changed, 240 insertions(+), 63 deletions(-) diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index f67c5be3c..e779a42c4 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -3,6 +3,7 @@ #include "qe_util.h" #include "ast_util.h" #include "smt_kernel.h" +#include namespace datalog { @@ -343,6 +344,12 @@ namespace datalog { check_equiv("filter", fml1, fml2); } + void check_relation_plugin::check_contains(char const* objective, expr* fml1, expr* fml2) { + expr_ref fml0(m); + fml0 = m.mk_and(fml1, fml2); + check_equiv(objective, fml0, fml2); + } + void check_relation_plugin::check_equiv(char const* objective, expr* fml1, expr* fml2) { TRACE("doc", tout << mk_pp(fml1, m) << "\n"; tout << mk_pp(fml2, m) << "\n";); @@ -358,16 +365,20 @@ namespace datalog { else { IF_VERBOSE(3, verbose_stream() << "NOT verified " << res << "\n"; verbose_stream() << mk_pp(fml1, m) << "\n"; - verbose_stream() << mk_pp(fml2, m) << "\n";); + verbose_stream() << mk_pp(fml2, m) << "\n"; + verbose_stream().flush(); + ); throw 0; } } - void check_relation_plugin::verify_union(expr* fml0, relation_base const& src, relation_base const& dst, relation_base const* delta) { - expr_ref fml1(m), fml2(m), fml3(m); + void check_relation_plugin::verify_union(expr* dst0, relation_base const& src, + relation_base const& dst, + expr* delta0, relation_base const* delta) { + expr_ref fml1(m), fml2(m); src.to_formula(fml1); dst.to_formula(fml2); - fml1 = m.mk_or(fml1, fml0); + fml1 = m.mk_or(fml1, dst0); relation_signature const& sig = dst.get_signature(); expr_ref_vector vars(m); var_subst sub(m, false); @@ -382,21 +393,30 @@ namespace datalog { check_equiv("union", fml1, fml2); if (delta) { - delta->to_formula(fml3); - IF_VERBOSE(3, verbose_stream() << "verify delta\n"; - verbose_stream() << fml3 << "\n";); - // delta >= dst \ fml0 - // dst \ fml0 == delta & dst & \ fml0 + expr_ref d0(m), d(m); + delta->to_formula(d); + IF_VERBOSE(3, verbose_stream() << "verify delta " << d << "\n";); + // delta >= dst \ dst0 + // dst \ dst0 == delta & dst & \ dst0 expr_ref fml4(m), fml5(m); - fml4 = m.mk_and(fml2, m.mk_not(fml0)); - fml5 = m.mk_and(fml3, fml4); + fml4 = m.mk_and(fml2, m.mk_not(dst0)); + sub(fml4, vars.size(), vars.c_ptr(), fml4); + sub(d, vars.size(), vars.c_ptr(), d); + check_contains("union_delta low", d, fml4); + // + // delta >= delta0 + // + sub(delta0, vars.size(), vars.c_ptr(), d0); + check_contains("union delta0", d, d0); + + // + // dst u delta0 = delta u dst0 + // + fml4 = m.mk_or(fml2, delta0); + fml5 = m.mk_or(d, dst0); sub(fml4, vars.size(), vars.c_ptr(), fml4); sub(fml5, vars.size(), vars.c_ptr(), fml5); - check_equiv("union delta low", fml4, fml5); - //fml4 = m.mk_and(fml3, fml2); - //sub(fml3, vars.size(), vars.c_ptr(), fml3); - //sub(fml4, vars.size(), vars.c_ptr(), fml4); - //check_equiv("union delta high", fml3, fml4); + check_equiv("union no overflow", fml4, fml5); } } @@ -411,8 +431,10 @@ namespace datalog { check_relation const& src = get(_src); check_relation* d = get(_delta); expr_ref fml0 = r.m_fml; + expr_ref delta0(r.m_fml.get_manager()); + if (d) d->to_formula(delta0); (*m_union)(r.rb(), src.rb(), d?(&d->rb()):0); - r.get_plugin().verify_union(fml0, src.rb(), r.rb(), d?(&d->rb()):0); + r.get_plugin().verify_union(fml0, src.rb(), r.rb(), delta0, d?(&d->rb()):0); r.rb().to_formula(r.m_fml); if (d) d->rb().to_formula(d->m_fml); } @@ -595,12 +617,15 @@ namespace datalog { } virtual void operator()(relation_base& tb, const relation_base& negb) { - IF_VERBOSE(0, verbose_stream() << "TBD: verify filter_negation\n";); check_relation& t = get(tb); check_relation const& n = get(negb); check_relation_plugin& p = t.get_plugin(); + ast_manager& m = p.get_ast_manager(); + expr_ref dst0(m); + t.to_formula(dst0); (*m_filter)(t.rb(), n.rb()); t.rb().to_formula(t.m_fml); + p.verify_filter_by_negation(dst0, t, n, m_t_cols, m_neg_cols); } }; @@ -608,10 +633,57 @@ namespace datalog { const relation_base& t, const relation_base& neg, unsigned joined_col_cnt, const unsigned *t_cols, const unsigned *negated_cols) { - relation_intersection_filter_fn* f = mk_filter_by_negation_fn(get(t).rb(), get(neg).rb(), joined_col_cnt, t_cols, negated_cols); + relation_intersection_filter_fn* f = m_base->mk_filter_by_negation_fn(get(t).rb(), get(neg).rb(), joined_col_cnt, t_cols, negated_cols); return f?alloc(negation_filter_fn, f, joined_col_cnt, t_cols, negated_cols):0; } + /* + 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 check_relation_plugin::verify_filter_by_negation( + expr* dst0, + check_relation const& dst, + check_relation const& neg, + unsigned_vector const& cols1, + unsigned_vector const& cols2) { + relation_signature const& sig1 = dst.get_signature(); + relation_signature const& sig2 = neg.get_signature(); + expr_ref dstf(m), negf(m); + std::cout << mk_pp(dst0, m) << "\n"; + expr_ref_vector eqs(m); + dst.to_formula(dstf); + std::cout << mk_pp(dstf, m) << "\n"; + dst.to_formula(negf); + std::cout << mk_pp(negf, m) << "\n"; + eqs.push_back(negf); + for (unsigned i = 0; i < cols1.size(); ++i) { + var_ref v1(m), v2(m); + unsigned c1 = cols1[i]; + unsigned c2 = cols2[i]; + SASSERT(sig1[c1] == sig2[c2]); + v1 = m.mk_var(sig2.size() + c1, sig1[c1]); + v2 = m.mk_var(c2, sig2[c2]); + eqs.push_back(m.mk_eq(v1, v2)); + } + negf = mk_and(m, eqs.size(), eqs.c_ptr()); + ptr_vector rev_sig2(sig2.size(), sig2.c_ptr()); + rev_sig2.reverse(); + svector names; + for (unsigned i = 0; i < sig2.size(); ++i) { + names.push_back(symbol(i)); + } + negf = m.mk_exists(rev_sig2.size(), rev_sig2.c_ptr(), names.c_ptr(), negf); + negf = m.mk_and(dst0, m.mk_not(negf)); + negf = dst.ground(negf); + dstf = dst.ground(dstf); + std::cout << negf << "\n"; + std::cout << dstf << "\n"; + check_equiv("filter by negation", dstf, negf); + } class check_relation_plugin::filter_proj_fn : public convenient_relation_project_fn { app_ref m_cond; diff --git a/src/muz/rel/check_relation.h b/src/muz/rel/check_relation.h index 9a59772ef..016751184 100644 --- a/src/muz/rel/check_relation.h +++ b/src/muz/rel/check_relation.h @@ -115,7 +115,7 @@ namespace datalog { void verify_filter(expr* fml0, relation_base const& t, expr* cond); void verify_union(expr* fml0, relation_base const& src, relation_base const& dst, - relation_base const* delta); + expr* delta0, relation_base const* delta); void verify_permutation( relation_base const& src, relation_base const& dst, @@ -135,11 +135,16 @@ namespace datalog { relation_base const& src, relation_base const& dst, app* cond, unsigned_vector const& removed_cols); - - void check_equiv(char const* objective, expr* f1, expr* f2); - + void check_contains(char const* objective, expr* f1, expr* f2); + + void verify_filter_by_negation( + expr* dst0, + check_relation const& dst, + check_relation const& neg, + unsigned_vector const& dst_eq, + unsigned_vector const& neg_eq); }; }; diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp index 938f39aed..e2c0ab162 100644 --- a/src/muz/rel/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -552,11 +552,33 @@ bool doc_manager::contains(doc const& a, doc const& b) const { } return true; } + +bool doc_manager::contains( + unsigned offset_a, doc const& a, + doc_manager const& dm_b, + unsigned offset_b, doc const& b, + unsigned length) const { + if (!m.contains(offset_a, a.pos(), dm_b.tbvm(), offset_b, b.pos(), length)) return false; + for (unsigned i = 0; i < a.neg().size(); ++i) { + bool found = false; + for (unsigned j = 0; !found && j < b.neg().size(); ++j) { + found = dm_b.tbvm().contains(offset_b, b.neg()[j], tbvm(), offset_a, a.neg()[i], length); + } + if (!found) return false; + } + return true; +} + std::ostream& doc_manager::display(std::ostream& out, doc const& b) const { - m.display(out, b.pos()); + if (num_tbits() == 0) return out << "[]"; + return display(out, b, num_tbits()-1, 0); +} + +std::ostream& doc_manager::display(std::ostream& out, doc const& b, unsigned hi, unsigned lo) const { + m.display(out, b.pos(), hi, lo); if (b.neg().is_empty()) return out; out << " \\ "; - b.neg().display(m, out); + b.neg().display(m, out, hi, lo); return out; } diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h index 3be31ead7..16e7c5f28 100644 --- a/src/muz/rel/doc.h +++ b/src/muz/rel/doc.h @@ -53,6 +53,7 @@ public: doc_manager(unsigned num_bits); ~doc_manager(); tbv_manager& tbvm() { return m; } + tbv_manager const& tbvm() const { return m; } doc* allocate(); doc* allocate1(); doc* allocate0(); @@ -81,7 +82,11 @@ public: bool equals(doc const& a, doc const& b) const; unsigned hash(doc const& src) const; bool contains(doc const& a, doc const& b) const; + bool contains(unsigned offset_a, doc const& a, + doc_manager const& dm_b, unsigned offset_b, doc const& b, + unsigned length) const; std::ostream& display(std::ostream& out, doc const& b) const; + std::ostream& display(std::ostream& out, doc const& b, unsigned hi, unsigned lo) const; 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; @@ -123,10 +128,16 @@ public: return false; } std::ostream& display(M const& m, std::ostream& out) const { + if (m.num_tbits() == 0) return out << "[]"; + return display(m, out, m.num_tbits()-1, 0); + } + std::ostream& display(M const& m, std::ostream& out, unsigned hi, unsigned lo) const { out << "{"; + if (size() + m.num_tbits() > 10) out << "\n "; for (unsigned i = 0; i < size(); ++i) { - m.display(out, *m_elems[i]); + m.display(out, *m_elems[i], hi, lo); if (i + 1 < size()) out << ", "; + if (i + 1 < size() && m.num_tbits() > 10) out << "\n "; } return out << "}"; } diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 391445215..739443ea0 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -244,13 +244,31 @@ unsigned tbv_manager::hash(tbv const& src) const { bool tbv_manager::contains(tbv const& a, tbv const& b) const { return m.contains(a, b); } + +bool tbv_manager::contains(unsigned offset_a, tbv const& a, + tbv_manager const& dm_b, unsigned offset_b, tbv const& b, + unsigned length) const { + if (this == &dm_b && length == num_tbits()) { + SASSERT(offset_a == 0); + SASSERT(offset_b == 0); + return m.contains(a, b); + } + for (unsigned i = 0; i < length; ++i) { + tbit bit_a = a[offset_a + i]; + if (bit_a == BIT_x) continue; + if (bit_a != b[offset_b + i]) return false; + } + return true; +} + bool tbv_manager::intersect(tbv const& a, tbv const& b, tbv& result) { copy(result, a); return set_and(result, b); } -std::ostream& tbv_manager::display(std::ostream& out, tbv const& b) const { - for (unsigned i = 0; i < num_tbits(); ++i) { +std::ostream& tbv_manager::display(std::ostream& out, tbv const& b, unsigned hi, unsigned lo) const { + SASSERT(lo <= hi && hi < num_tbits()); + for (unsigned i = lo; i <= hi; ++i) { switch (b.get(i)) { case BIT_0: out << '0'; @@ -271,6 +289,11 @@ std::ostream& tbv_manager::display(std::ostream& out, tbv const& b) const { return out; } +std::ostream& tbv_manager::display(std::ostream& out, tbv const& b) const { + if (num_tbits() == 0) return out << "[]"; + return display(out, b, num_tbits()-1, 0); +} + expr_ref tbv_manager::to_formula(ast_manager& m, tbv const& src) { expr_ref result(m); expr_ref_vector conj(m); diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h index 454cbae37..9663f7d04 100644 --- a/src/muz/rel/tbv.h +++ b/src/muz/rel/tbv.h @@ -70,8 +70,12 @@ public: bool equals(tbv const& a, tbv const& b) const; unsigned hash(tbv const& src) const; bool contains(tbv const& a, tbv const& b) const; + bool contains(unsigned offset_a, tbv const& a, + tbv_manager const& dm_b, unsigned offset_b, tbv const& b, + unsigned length) const; bool intersect(tbv const& a, tbv const& b, tbv& result); std::ostream& display(std::ostream& out, tbv const& b) const; + std::ostream& display(std::ostream& out, tbv const& b, unsigned hi, unsigned lo) const; tbv* project(unsigned n, bool const* to_delete, tbv const& src); bool is_well_formed(tbv const& b) const; // - does not contain BIT_z; void set(tbv& dst, uint64 n, unsigned hi, unsigned lo); diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 5f3d6288d..b862781b7 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -1003,9 +1003,18 @@ namespace datalog { return check_kind(t)?alloc(filter_interpreted_fn, get(t), get_ast_manager(), condition):0; } + // + // Notes: + // 1. this code could use some cleanup and simplification. + // 2. It is also not very efficient in the copy routines. + // They fall back to copying each bit instead of a chunk. + // 3. Argument about correctness is needed as comments. + // 4. Unit/stress test cases are needed. + // 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) @@ -1018,72 +1027,103 @@ namespace datalog { udoc_relation const& n = get(negb); udoc & dst = t.get_udoc(); udoc const & neg = n.get_udoc(); - doc_manager& dm = t.get_dm(); + doc_manager& dmt = t.get_dm(); + doc_manager& dmn = n.get_dm(); + IF_VERBOSE(3, t.display(verbose_stream() << "dst:");); + IF_VERBOSE(3, n.display(verbose_stream() << "neg:");); + 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_j && c < m_t_cols.size(); ++c) { + for (unsigned j = 0; j < neg.size(); ++j) { + for (unsigned c = 0; 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); + bool cont = dmn.contains(n_idx, neg[j], dmt, t_idx, dst[i], num_bits); + IF_VERBOSE( + 3, + dmt.display(verbose_stream() << "dst:", dst[i], t_idx+num_bits-1,t_idx) << "\n"; + dmn.display(verbose_stream() << "neg:", neg[j], n_idx+num_bits-1,n_idx) << "\n"; + verbose_stream() << "contains: " << (cont?"true":"false") << "\n";); + if (!cont) { + goto next_neg_disj; } } - if (done_j) { - result.push_back(&dst[i]); - done_i = true; - } - } - if (!done_i) { - dm.deallocate(&dst[i]); + dmt.deallocate(&dst[i]); + goto next_disj; + next_neg_disj:; } + result.push_back(&dst[i]); + next_disj:; } std::swap(dst, result); if (dst.is_empty()) { - IF_VERBOSE(3, tb.display(verbose_stream());); + IF_VERBOSE(3, tb.display(verbose_stream() << "fast 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); + doc& neg_i = neg[i]; + doc_ref newD(dmt, dmt.allocateX()); + copy_columns(newD->pos(), neg_i.pos(), t, n); + bool is_empty = false; + for (unsigned j = 0; !is_empty && j < neg_i.neg().size(); ++j) { + tbv_ref newT(dmt.tbvm(), dmt.tbvm().allocateX()); + copy_columns(*newT, neg_i.neg()[j], t, n); + if (dmt.tbvm().equals(newD->pos(), *newT)) { + is_empty = true; + } + else { + newD->neg().push_back(newT.detach()); + } + } + if (!is_empty) { + IF_VERBOSE(3, + dmn.display(verbose_stream() << "copy neg: ", neg_i) << "\n"; + dmt.display(verbose_stream() << "to dst: ", *newD) << "\n";); + renamed_neg.push_back(newD.detach()); } - renamed_neg.push_back(newD.detach()); } - TRACE("doc", dst.display(dm, tout) << "\n"; - renamed_neg.display(dm, tout) << "\n"; + TRACE("doc", dst.display(dmt, tout) << "\n"; + renamed_neg.display(dmt, tout) << "\n"; ); - dst.subtract(dm, renamed_neg); - TRACE("doc", dst.display(dm, tout) << "\n";); - SASSERT(dst.well_formed(dm)); - renamed_neg.reset(t.get_dm()); - IF_VERBOSE(3, tb.display(verbose_stream());); + dst.subtract(dmt, renamed_neg); + // TBD: double check semantics + TRACE("doc", dst.display(dmt, tout) << "\n";); + SASSERT(dst.well_formed(dmt)); + renamed_neg.reset(dmt); + IF_VERBOSE(3, tb.display(verbose_stream() << "slow case:");); + } + void copy_columns( + tbv& dst, tbv const& src, + udoc_relation const& dstt, + udoc_relation const& srct) + { + unsigned num_cols = m_t_cols.size(); + for (unsigned i = 0; i < num_cols; ++i) { + copy_column(dst, src, m_t_cols[i], m_neg_cols[i], dstt, srct); + } } void copy_column( - doc& dst, doc const& src, + tbv& dst, tbv const& src, unsigned col_dst, unsigned col_src, udoc_relation const& dstt, udoc_relation const& srct) { - doc_manager& dm = dstt.get_dm(); + tbv_manager& dm = dstt.get_dm().tbvm(); 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); + unsigned num_tbits = 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]); - } + IF_VERBOSE(3, verbose_stream() << "copy column " << idx_src + << " to " << idx_dst << " " << num_tbits << "\n";); + for (unsigned i = 0; i < num_tbits; ++i) { + dm.set(dst, idx_dst + i, src[idx_src + i]); + } } };