diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h index 01772543a..510ee8bef 100644 --- a/src/muz/rel/doc.h +++ b/src/muz/rel/doc.h @@ -220,6 +220,18 @@ public: push_back(m.allocate(other[i])); } } + void simplify(M& m) { + union_bvec result; + for (unsigned i = 0; i < size(); ++i) { + if (m.fold_neg(*m_elems[i])) { + result.insert(m, m_elems[i]); + } + else { + m.deallocate(m_elems[i]); + } + } + std::swap(*this, result); + } void merge(M& m, unsigned lo, unsigned length, subset_ints & equalities, bit_vector const& discard_cols) { for (unsigned i = 0; i < size(); ++i) { diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index f1f919ec7..fb1d1c9e8 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -739,6 +739,7 @@ namespace datalog { if (m_condition && !u.is_empty()) { t.apply_guard(m_condition, u, m_empty_bv); } + u.simplify(dm); TRACE("dl", tout << "final size: " << t.get_size_estimate_rows() << '\n';); } }; diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 2c5540fe2..7a616fdd0 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -21,6 +21,9 @@ class udoc_tester { typedef datalog::udoc_relation udoc_relation; typedef datalog::udoc_plugin udoc_plugin; typedef datalog::relation_signature relation_signature; + typedef datalog::relation_fact relation_fact; + typedef scoped_ptr rel_mut; + typedef scoped_ptr rel_union; struct init { init(ast_manager& m) { @@ -61,6 +64,7 @@ public: 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)); @@ -73,7 +77,15 @@ public: fact3.push_back(bv.mk_numeral(rational(16), 6)); fact3.push_back(bv.mk_numeral(rational(4), 12)); + relation_signature sig2; + sig2.push_back(bv.mk_sort(3)); + sig2.push_back(bv.mk_sort(6)); + sig2.push_back(bv.mk_sort(3)); + sig2.push_back(bv.mk_sort(3)); + sig2.push_back(bv.mk_sort(3)); + relation_base* t; + udoc_relation* t1, *t2, *t3; expr_ref fml(m); // empty { @@ -97,9 +109,9 @@ public: // join { - udoc_relation* t1 = mk_full(sig); - udoc_relation* t2 = mk_full(sig); - udoc_relation* t3 = mk_empty(sig); + t1 = mk_full(sig); + t2 = mk_full(sig); + t3 = mk_empty(sig); unsigned_vector jc1, jc2; jc1.push_back(1); jc2.push_back(1); @@ -128,7 +140,7 @@ public: // project { std::cout << "project\n"; - udoc_relation* t1 = mk_full(sig); + 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()); @@ -155,7 +167,7 @@ public: // rename { - udoc_relation* t1 = mk_empty(sig); + t1 = mk_empty(sig); unsigned_vector cycle; cycle.push_back(0); cycle.push_back(2); @@ -175,14 +187,14 @@ public: // union { - udoc_relation* t1 = mk_empty(sig); - udoc_relation* t2 = mk_empty(sig); + t1 = mk_empty(sig); + 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); + rel_union union_fn = p.mk_union_fn(*t1, *t2, 0); t1->display(std::cout << "t1 before:"); std::cout << "\n"; (*union_fn)(*t1, *t2, delta); @@ -195,9 +207,69 @@ public: } // filter_identical + { + t1 = mk_empty(sig2); + unsigned_vector id; + 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()); + relation_fact f1(m); + f1.push_back(bv.mk_numeral(rational(1),3)); + f1.push_back(bv.mk_numeral(rational(1),6)); + f1.push_back(bv.mk_numeral(rational(1),3)); + f1.push_back(bv.mk_numeral(rational(1),3)); + f1.push_back(bv.mk_numeral(rational(1),3)); + t1->add_fact(f1); + f1[4] = bv.mk_numeral(rational(2),3); + t1->add_fact(f1); + t1->display(std::cout); std::cout << "\n"; + (*filter_id)(*t1); + t1->display(std::cout); std::cout << "\n"; + t1->deallocate(); + dealloc(filter_id); + } // 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); + var_ref v3(m.mk_var(3, bv.mk_sort(3)),m); + var_ref v4(m.mk_var(4, bv.mk_sort(3)),m); + app_ref cond1(m), cond2(m), cond3(m), cond4(m); + app_ref cond5(m), cond6(m), cond7(m), cond8(m); + cond1 = m.mk_true(); + cond2 = m.mk_false(); + cond3 = m.mk_eq(v0, v2); + 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"; + t1->deallocate(); + t2->deallocate(); + + } // filter_by_negation // filter_interpreted_project