mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

update unit tests to use filter_by_negation verifier from check_relation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-01 15:21:42 -07:00
parent d8e62cac94
commit bb15ddbf15
3 changed files with 19 additions and 58 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/muz/rel/check_relation.cpp
View file

@ -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);

5
src/muz/rel/check_relation.h
View file

@ -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);
};

56
src/test/udoc_relation.cpp
View file

@ -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<datalog::relation_intersection_filter_fn> 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: