From bb15ddbf15e5abc8e8bd17c491022ddcd48047e1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Oct 2014 15:21:42 -0700 Subject: [PATCH] update unit tests to use filter_by_negation verifier from check_relation Signed-off-by: Nikolaj Bjorner --- src/muz/rel/check_relation.cpp | 16 ++++++---- src/muz/rel/check_relation.h | 5 +-- src/test/udoc_relation.cpp | 56 ++++------------------------------ 3 files changed, 19 insertions(+), 58 deletions(-) diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index e779a42c4..a526ffc1b 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -38,7 +38,11 @@ namespace datalog { } expr_ref check_relation::ground(expr* fml) const { - relation_signature const& sig = get_signature(); + return get_plugin().ground(*this, fml); + } + + expr_ref check_relation_plugin::ground(relation_base const& dst, expr* fml) const { + relation_signature const& sig = dst.get_signature(); var_subst sub(m, false); expr_ref_vector vars(m); for (unsigned i = 0; i < sig.size(); ++i) { @@ -625,7 +629,7 @@ namespace datalog { 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); + p.verify_filter_by_negation(dst0, t.rb(), n.rb(), m_t_cols, m_neg_cols); } }; @@ -646,8 +650,8 @@ namespace datalog { void check_relation_plugin::verify_filter_by_negation( expr* dst0, - check_relation const& dst, - check_relation const& neg, + relation_base const& dst, + relation_base const& neg, unsigned_vector const& cols1, unsigned_vector const& cols2) { relation_signature const& sig1 = dst.get_signature(); @@ -678,8 +682,8 @@ namespace datalog { } 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); + negf = ground(dst, negf); + dstf = ground(dst, dstf); std::cout << negf << "\n"; std::cout << dstf << "\n"; check_equiv("filter by negation", dstf, negf); diff --git a/src/muz/rel/check_relation.h b/src/muz/rel/check_relation.h index 016751184..580ce3dd4 100644 --- a/src/muz/rel/check_relation.h +++ b/src/muz/rel/check_relation.h @@ -77,6 +77,7 @@ namespace datalog { static check_relation& get(relation_base& r); static check_relation* get(relation_base* r); static check_relation const & get(relation_base const& r); + expr_ref ground(relation_base const& rb, expr* fml) const; public: check_relation_plugin(relation_manager& rm); ~check_relation_plugin(); @@ -141,8 +142,8 @@ namespace datalog { void verify_filter_by_negation( expr* dst0, - check_relation const& dst, - check_relation const& neg, + relation_base const& dst, + relation_base const& neg, unsigned_vector const& dst_eq, unsigned_vector const& neg_eq); }; diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 094e755ac..9824c481d 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -619,60 +619,16 @@ public: full->deallocate(); } - void apply_filter_neg(udoc_relation& t1, udoc_relation& t2, + void apply_filter_neg(udoc_relation& dst, udoc_relation& neg, unsigned_vector const& cols1, unsigned_vector const& cols2) { - relation_signature const& sig = t1.get_signature(); scoped_ptr negf; - negf = p.mk_filter_by_negation_fn(t1, t2, cols1.size(), cols1.c_ptr(), cols2.c_ptr()); - expr_ref fml1(m), fml2(m), fml3(m); - t1.to_formula(fml1); - t2.to_formula(fml2); - for (unsigned i = 0; i < cols1.size(); ++i) { - std::cout << cols1[i] << " = " << cols2[i] << " "; - } - std::cout << "\n"; - t1.display(std::cout); std::cout << "\n"; - t2.display(std::cout); std::cout << "\n"; - (*negf)(t1, t2); - t1.display(std::cout); std::cout << "\n"; - t1.to_formula(fml3); - std::cout << fml1 << "\n"; - std::cout << fml2 << "\n"; - std::cout << fml3 << "\n"; - expr_ref_vector eqs(m); - expr_ref_vector sub(m); - for (unsigned i = 0; i < sig.size(); ++i) { - sub.push_back(m.mk_var(i+sig.size(),sig[i])); - } - var_subst subst(m, false); - subst(fml2, sub.size(), sub.c_ptr(), fml2); - eqs.push_back(fml2); - for (unsigned i = 0; i < cols1.size(); ++i) { - var_ref v1(m), v2(m); - unsigned c1 = cols1[i]; - unsigned c2 = cols2[i]; - v1 = m.mk_var(c1, sig[c1]); - v2 = m.mk_var(sig.size() + c2, sig[c2]); - eqs.push_back(m.mk_eq(v1,v2)); - } - fml2 = mk_and(m, eqs.size(), eqs.c_ptr()); - for (unsigned i = 0; i < sub.size(); ++i) { - project_var(sig.size() + i, m.get_sort(sub[i].get()), fml2); - } - fml1 = m.mk_and(fml1, m.mk_not(fml2)); - - expr_ref_vector vars(m); - 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])); - } + negf = p.mk_filter_by_negation_fn(dst, neg, cols1.size(), cols1.c_ptr(), cols2.c_ptr()); + expr_ref dst0(m); + dst.to_formula(dst0); + (*negf)(dst, neg); + cr.verify_filter_by_negation(dst0, dst, neg, cols1, cols2); - subst(fml1, vars.size(), vars.c_ptr(), fml1); - subst(fml3, vars.size(), vars.c_ptr(), fml3); - - check_equiv(fml1, fml3); /* tgt_1:={ x: x\in tgt_0 && ! \exists y: