diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp index cf27f3751..baff1f504 100644 --- a/src/muz/rel/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -441,12 +441,13 @@ unsigned doc_manager::hash(doc const& src) const { // A \ (A1 u A2) contains B \ (B1 u B2) // if // A contains B -// B1 contains A1 or A2 +// B1 contains A1 or B2 contains A1 +// B1 contains A2 or B2 contains A2 bool doc_manager::contains(doc const& a, doc const& b) const { if (!m.contains(a.pos(), b.pos())) return false; - for (unsigned i = 0; i < b.neg().size(); ++i) { + for (unsigned i = 0; i < a.neg().size(); ++i) { bool found = false; - for (unsigned j = 0; !found && j < a.neg().size(); ++j) { + for (unsigned j = 0; !found && j < b.neg().size(); ++j) { found = m.contains(b.neg()[i],a.neg()[j]); } if (!found) return false; diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index fb1d1c9e8..a9a858c43 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -103,21 +103,21 @@ namespace datalog { unsigned lo = column_idx(i); unsigned hi = column_idx(i+1); rational r(0); - unsigned lo0 = lo; + unsigned lo1 = 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(); + if (is_x) is_x = false, lo1 = j, r.reset(); break; case BIT_1: - if (is_x) is_x = false, lo0 = j, r.reset(); - r += rational::power_of_two(j - lo0); + if (is_x) is_x = false, lo1 = j, r.reset(); + r += rational::power_of_two(j - lo1); 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))); + conjs.push_back(m.mk_eq(p.bv.mk_extract(j-1-lo,lo1-lo,v), + p.bv.mk_numeral(r,j-lo1))); } is_x = true; break; @@ -127,13 +127,13 @@ namespace datalog { } if (!is_x) { expr_ref num(m); - if (lo0 == lo) { + if (lo1 == 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)); + num = p.bv.mk_numeral(r, hi-lo1); + conjs.push_back(m.mk_eq(p.bv.mk_extract(hi-1-lo,lo1-lo,v), num)); } } } @@ -146,7 +146,7 @@ namespace datalog { } void udoc_relation::display(std::ostream& out) const { - m_elems.display(dm, out); + m_elems.display(dm, out); out << "\n"; } // ------------- @@ -189,11 +189,25 @@ namespace datalog { if (bv.is_bv_sort(s)) { return bv.mk_numeral(r, s); } + if (m.is_bool(s)) { + if (r.is_zero()) return m.mk_false(); + return m.mk_true(); + } 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; + if (m.is_true(e)) { + r = rational(1); + num_bits = 1; + return true; + } + if (m.is_false(e)) { + r = rational(0); + num_bits = 1; + 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)) { @@ -208,6 +222,9 @@ namespace datalog { unsigned num_bits = 0; if (bv.is_bv_sort(s)) return bv.get_bv_size(s); + if (m.is_bool(s)) { + return 1; + } uint64 sz; if (dl.try_get_size(s, sz)) { while (sz > 0) ++num_bits, sz /= 2; @@ -325,7 +342,7 @@ namespace datalog { 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");); + TRACE("doc", 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); @@ -337,7 +354,7 @@ namespace datalog { join(d1[i], d2[j], r); } } - TRACE("dl", result->display(tout << "result:\n");); + TRACE("doc", result->display(tout << "result:\n");); return result; } }; @@ -363,7 +380,7 @@ namespace datalog { } virtual relation_base * operator()(const relation_base & tb) { - TRACE("dl", tb.display(tout << "src:\n");); + TRACE("doc", 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())); @@ -376,7 +393,7 @@ namespace datalog { 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';); + TRACE("doc", tout << "final size: " << r->get_size_estimate_rows() << '\n';); return r; } }; @@ -415,7 +432,7 @@ namespace datalog { virtual relation_base * operator()(const relation_base & _r) { udoc_relation const& r = get(_r); - TRACE("dl", r.display(tout << "r:\n");); + TRACE("doc", 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); @@ -425,7 +442,7 @@ namespace datalog { 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");); + TRACE("doc", result->display(tout << "result:\n");); return result; } }; @@ -444,7 +461,7 @@ namespace datalog { 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");); + TRACE("doc", _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); @@ -453,7 +470,7 @@ namespace datalog { 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");); + TRACE("doc", _r.display(tout << "dst':\n"); ); } }; void udoc_plugin::mk_union(doc_manager& dm, udoc& dst, udoc const& src, udoc* delta) { @@ -512,7 +529,7 @@ namespace datalog { 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';); + TRACE("doc", tout << "final size: " << r.get_size_estimate_rows() << '\n';); } }; relation_mutator_fn * udoc_plugin::mk_filter_identical_fn( @@ -643,10 +660,15 @@ 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";); result.subtract(dm, sub); + result.simplify(dm); + TRACE("doc", result.display(dm, tout << "result:") << "\n";); + } else if (m.is_or(g)) { udoc sub; @@ -654,9 +676,10 @@ namespace datalog { 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); + apply_guard(arg, sub, equalities, discard_cols); } result.subtract(dm, sub); + sub.reset(dm); } else if (m.is_true(g)) { } @@ -672,9 +695,25 @@ namespace datalog { dm.set(*d, idx, BIT_1); result.intersect(dm, *d); } + else if ((m.is_eq(g, e1, e2) || m.is_iff(g, e1, e2)) && m.is_bool(e1)) { + udoc diff1, diff2; + diff1.push_back(dm.allocateX()); + diff2.push_back(dm.allocateX()); + expr_ref f1(m), f2(m); + f1 = mk_not(m, e1); + f2 = mk_not(m, e2); + apply_guard(e1, diff1, equalities, discard_cols); + apply_guard(f2, diff1, equalities, discard_cols); + result.subtract(dm, diff1); + diff1.reset(dm); + apply_guard(f1, diff2, equalities, discard_cols); + apply_guard(e2, diff2, equalities, discard_cols); + result.subtract(dm, diff2); + diff2.reset(dm); + } else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) { - unsigned hi, lo; - expr* e3; + 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)) { } @@ -695,6 +734,14 @@ namespace datalog { unsigned length = column_num_bits(v1->get_idx()); 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; } @@ -723,9 +770,10 @@ namespace datalog { if (m.is_true(m_condition)) { m_condition = 0; } - TRACE("dl", + TRACE("doc", tout << "condition: " << mk_pp(condition, m) << "\n"; - tout << m_condition << "\n"; m_udoc.display(dm, tout) << "\n";); + if (m_condition) tout << m_condition << "\n"; + m_udoc.display(dm, tout) << "\n";); } virtual ~filter_interpreted_fn() { @@ -740,7 +788,7 @@ namespace datalog { t.apply_guard(m_condition, u, m_empty_bv); } u.simplify(dm); - TRACE("dl", tout << "final size: " << t.get_size_estimate_rows() << '\n';); + TRACE("doc", tout << "final size: " << t.get_size_estimate_rows() << '\n';); } }; relation_mutator_fn * udoc_plugin::mk_filter_interpreted_fn(const relation_base & t, app * condition) { diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 7a616fdd0..e307455cc 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -213,7 +213,7 @@ public: id.push_back(0); id.push_back(2); id.push_back(4); - datalog::relation_mutator_fn* filter_id = p.mk_filter_identical_fn(*t1, id.size(), id.c_ptr()); + rel_mut filter_id = p.mk_filter_identical_fn(*t1, id.size(), id.c_ptr()); relation_fact f1(m); f1.push_back(bv.mk_numeral(rational(1),3)); f1.push_back(bv.mk_numeral(rational(1),6)); @@ -227,14 +227,42 @@ public: (*filter_id)(*t1); t1->display(std::cout); std::cout << "\n"; t1->deallocate(); - dealloc(filter_id); + } + + { + relation_signature sig3; + sig3.push_back(m.mk_bool_sort()); + sig3.push_back(m.mk_bool_sort()); + sig3.push_back(m.mk_bool_sort()); + var_ref v0(m.mk_var(0, m.mk_bool_sort()),m); + var_ref v1(m.mk_var(1, m.mk_bool_sort()),m); + var_ref v2(m.mk_var(2, m.mk_bool_sort()),m); + app_ref cond1(m); + cond1 = m.mk_or(m.mk_eq(v0,v1),m.mk_eq(v0,v2)); + t1 = mk_full(sig3); + apply_filter(*t1, cond1); + t1->deallocate(); + } + + { + relation_signature sig3; + sig3.push_back(bv.mk_sort(1)); + sig3.push_back(bv.mk_sort(1)); + sig3.push_back(bv.mk_sort(1)); + var_ref v0(m.mk_var(0, bv.mk_sort(1)),m); + var_ref v1(m.mk_var(1, bv.mk_sort(1)),m); + var_ref v2(m.mk_var(2, bv.mk_sort(1)),m); + app_ref cond1(m); + cond1 = m.mk_or(m.mk_eq(v0,v1),m.mk_eq(v0,v2)); + t1 = mk_full(sig3); + apply_filter(*t1, cond1); + t1->deallocate(); } // filter_interpreted { std::cout << "filter interpreted\n"; t1 = mk_full(sig2); - t2 = mk_full(sig2); var_ref v0(m.mk_var(0, bv.mk_sort(3)),m); var_ref v1(m.mk_var(1, bv.mk_sort(6)),m); var_ref v2(m.mk_var(2, bv.mk_sort(3)),m); @@ -248,36 +276,112 @@ public: cond4 = m.mk_not(m.mk_eq(v0, v2)); cond5 = m.mk_eq(v0, bv.mk_numeral(rational(2), 3)); - rel_union union_fn = p.mk_union_fn(*t1, *t2, 0); - rel_mut fint1 = p.mk_filter_interpreted_fn(*t1, cond1); - rel_mut fint2 = p.mk_filter_interpreted_fn(*t1, cond2); - rel_mut fint3 = p.mk_filter_interpreted_fn(*t1, cond3); - rel_mut fint4 = p.mk_filter_interpreted_fn(*t1, cond4); - rel_mut fint5 = p.mk_filter_interpreted_fn(*t1, cond5); - (*fint1)(*t1); - t1->display(std::cout << "filter: " << cond1 << " "); std::cout << "\n"; - (*fint2)(*t1); - t1->display(std::cout << "filter: " << cond2 << " "); std::cout << "\n"; - (*union_fn)(*t1, *t2); - (*fint3)(*t1); - t1->display(std::cout << "filter: " << cond3 << " "); std::cout << "\n"; - (*fint4)(*t1); - t1->display(std::cout << "filter: " << cond4 << " "); std::cout << "\n"; - (*union_fn)(*t1, *t2); - (*fint5)(*t1); - t1->display(std::cout << "filter: " << cond5 << " "); std::cout << "\n"; + apply_filter(*t1, cond1); + apply_filter(*t1, cond2); + apply_filter(*t1, cond3); + apply_filter(*t1, cond4); + apply_filter(*t1, cond5); + + cond1 = m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)); + apply_filter(*t1, cond1); + + cond2 = m.mk_or(cond1,m.mk_eq(v3,v4)); + apply_filter(*t1, cond2); + + cond2 = m.mk_or(cond1,m.mk_eq(ex(2,1,v3),ex(1,0,v4))); + apply_filter(*t1, cond2); + + cond1 = m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v0,v4)); + apply_filter(*t1, cond1); + + cond1 = m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v3,v4)); + apply_filter(*t1, cond1); + + cond1 = m.mk_or(m.mk_eq(ex(2,1,v0),ex(1,0,v2)),m.mk_eq(v3,v4)); + apply_filter(*t1, cond1); + + cond1 = m.mk_or(m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)), + m.mk_eq(v3,v4)); + apply_filter(*t1, cond1); + + cond1 = m.mk_or(m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)), + m.mk_eq(v3,bv.mk_numeral(rational(3),5))); + apply_filter(*t1, cond1); + + cond1 = m.mk_or(m.mk_eq(v0,bv.mk_numeral(rational(5),3)), + m.mk_eq(v3,bv.mk_numeral(rational(5),3))); + apply_filter(*t1, cond1); + + cond1 = m.mk_or(m.mk_eq(v0,bv.mk_numeral(rational(7),3)), + m.mk_eq(v3,bv.mk_numeral(rational(7),3))); + apply_filter(*t1, cond1); + + cond1 = m.mk_not(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v3,v4))); + apply_filter(*t1, cond1); + + t1->deallocate(); - t2->deallocate(); } // filter_by_negation // filter_interpreted_project } + + expr_ref ex(unsigned hi, unsigned lo, expr* e) { + expr_ref result(m); + result = bv.mk_extract(hi, lo, e); + return result; + } + + void apply_filter(udoc_relation& t, app* cond) { + udoc_relation* full = mk_full(t.get_signature()); + rel_union union_fn = p.mk_union_fn(t, *full, 0); + (*union_fn)(t, *full, 0); + rel_mut fint = p.mk_filter_interpreted_fn(t, cond); + (*fint)(t); + t.display(std::cout << "filter: " << mk_pp(cond, m) << " "); std::cout << "\n"; + verify_filter(t, cond); + full->deallocate(); + } + + void verify_filter(udoc_relation& r, expr* fml2) { + expr_ref fml1(m), tmp(m); + r.to_formula(fml1); + tmp = m.mk_not(m.mk_eq(fml1, fml2)); + relation_signature const& sig = r.get_signature(); + expr_ref_vector vars(m); + var_subst sub(m, false); + for (unsigned i = 0; i < sig.size(); ++i) { + std::stringstream strm; + strm << "x" << i; + vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i])); + } + + sub(tmp, vars.size(), vars.c_ptr(), tmp); + + smt_params fp; + smt::kernel solver(m, fp); + TRACE("doc", + tout << "Original formula:\n"; + tout << mk_pp(fml2, m) << "\n"; + tout << "Filtered formula: \n"; + tout << mk_pp(fml1,m) << "\n"; + tout << tmp << "\n"; + ); + solver.assert_expr(tmp); + lbool res = solver.check(); + SASSERT(res == l_false); + } }; void tst_udoc_relation() { udoc_tester tester; - tester.test1(); + try { + tester.test1(); + } + catch (z3_exception& ex) { + std::cout << ex.msg() << "\n"; + } }