From f94bdf40351efc3da868764eb3c0977908058ade Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Sep 2014 01:05:43 -0700 Subject: [PATCH] updated unit tests Signed-off-by: Nikolaj Bjorner --- src/muz/rel/doc.cpp | 2 +- src/muz/rel/tbv.cpp | 47 +++--- src/muz/rel/tbv.h | 3 + src/muz/rel/udoc_relation.cpp | 7 +- src/test/doc.cpp | 71 +++++++- src/test/udoc_relation.cpp | 300 +++++++++++++++++++++++++++------- 6 files changed, 346 insertions(+), 84 deletions(-) diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp index baff1f504..6cf719fd2 100644 --- a/src/muz/rel/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -415,8 +415,8 @@ void doc_manager::subtract(doc const& A, doc const& B, ptr_vector& result) r2 = allocate(B.neg()[i]); if (set_and(*r, *r2)) { result.push_back(r.detach()); - r = allocate(A); } + r = allocate(A); } } bool doc_manager::equals(doc const& a, doc const& b) const { diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index a83a3874e..23745f333 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -22,16 +22,20 @@ Revision History: #include "hashtable.h" -//#define _DEBUG_MEM 1 -#define _DEBUG_MEM 0 +static bool s_debug_alloc = false; + +void tbv_manager::debug_alloc() { + s_debug_alloc = true; +} tbv_manager::~tbv_manager() { -#if _DEBUG_MEM - ptr_vector::iterator it = allocated_tbvs.begin(), end = allocated_tbvs.end(); - for (; it != end; ++it) { - std::cout << "dangling: " << (*it) << "\n"; - } -#endif + DEBUG_CODE( + ptr_vector::iterator it = allocated_tbvs.begin(); + ptr_vector::iterator end = allocated_tbvs.end(); + for (; it != end; ++it) { + std::cout << "dangling: " << (*it) << "\n"; + TRACE("doc", tout << "dangling: " << (*it) << "\n";); + }); } void tbv_manager::reset() { @@ -39,10 +43,12 @@ void tbv_manager::reset() { } tbv* tbv_manager::allocate() { tbv* r = reinterpret_cast(m.allocate()); -#if _DEBUG_MEM - std::cout << allocated_tbvs.size() << " " << r << "\n"; - allocated_tbvs.insert(r); -#endif + DEBUG_CODE( + if (s_debug_alloc) { + TRACE("doc", tout << allocated_tbvs.size() << " " << r << "\n";); + } + allocated_tbvs.insert(r); + ); return r; } tbv* tbv_manager::allocate1() { @@ -145,14 +151,15 @@ tbv* tbv_manager::allocate(rational const& r) { return v; } void tbv_manager::deallocate(tbv* bv) { -#if _DEBUG_MEM - if (!allocated_tbvs.contains(bv)) { - std::cout << "double deallocate: " << bv << "\n"; - UNREACHABLE(); - } - std::cout << "deallocate: " << bv << "\n"; - allocated_tbvs.erase(bv); -#endif + DEBUG_CODE( + if (!allocated_tbvs.contains(bv)) { + std::cout << "double deallocate: " << bv << "\n"; + UNREACHABLE(); + } + if (s_debug_alloc) { + TRACE("doc", tout << "deallocate: " << bv << "\n";); + } + allocated_tbvs.erase(bv);); m.deallocate(bv); } void tbv_manager::copy(tbv& dst, tbv const& src) const { diff --git a/src/muz/rel/tbv.h b/src/muz/rel/tbv.h index f8c2d6643..90965f7d0 100644 --- a/src/muz/rel/tbv.h +++ b/src/muz/rel/tbv.h @@ -73,6 +73,8 @@ public: std::ostream& display(std::ostream& out, tbv const& b) 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; + + static void debug_alloc(); }; class tbv: private fixed_bit_vector { @@ -132,6 +134,7 @@ public: return *this; } tbv& operator*() { return *d; } + tbv* operator->() { return d; } tbv* get() { return d; } tbv* detach() { tbv* result = d; d = 0; return result; } }; diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index a9a858c43..ebebe4063 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -667,6 +667,7 @@ namespace datalog { TRACE("doc", sub.display(dm, tout << "sub:") << "\n";); result.subtract(dm, sub); result.simplify(dm); + sub.reset(dm); TRACE("doc", result.display(dm, tout << "result:") << "\n";); } @@ -678,7 +679,11 @@ namespace datalog { arg = mk_not(m, to_app(g)->get_arg(i)); apply_guard(arg, sub, equalities, discard_cols); } + TRACE("doc", result.display(dm, tout << "result0:") << "\n";); result.subtract(dm, sub); + TRACE("doc", + sub.display(dm, tout << "sub:") << "\n"; + result.display(dm, tout << "result:") << "\n";); sub.reset(dm); } else if (m.is_true(g)) { @@ -897,7 +902,7 @@ namespace datalog { for (unsigned i = 0; i < m_removed_cols.size(); ++i) { m_col_list.set(m_removed_cols[i], true); } - m_to_delete.resize(m_removed_cols.size(), false); + m_to_delete.resize(t.get_num_bits(), false); for (unsigned i = 0; i < m_removed_cols.size(); ++i) { m_to_delete[m_removed_cols[i]] = true; } diff --git a/src/test/doc.cpp b/src/test/doc.cpp index 890ce4204..6bd7e50b9 100644 --- a/src/test/doc.cpp +++ b/src/test/doc.cpp @@ -167,6 +167,16 @@ class test_doc_cls { return result; } + expr_ref to_formula(udoc const& ud, doc_manager& m2, bool const* to_delete) { + expr_ref result(m); + expr_ref_vector disjs(m); + for (unsigned i = 0; i < ud.size(); ++i) { + disjs.push_back(to_formula(ud[i], m2, to_delete)); + } + result = mk_or(m, disjs.size(), disjs.c_ptr()); + return result; + } + void project(doc const& d, doc_manager& m2, bool const* to_delete, doc_ref& result) { result = dm.project(m2, m_vars.size(), to_delete, d); TRACE("doc", @@ -264,15 +274,20 @@ class test_doc_cls { } rw(fml1); rw(fml2); + check_equiv(fml1, fml2); + } + + void check_equiv(expr* fml1, expr* fml2) { smt_params fp; smt::kernel solver(m, fp); - TRACE("doc", tout << "manual project:\n" << fml1 << "\nautomatic project: \n" << fml2 << "\n";); + expr_ref fml(m); fml = m.mk_not(m.mk_eq(fml1, fml2)); solver.assert_expr(fml); lbool res = solver.check(); SASSERT(res == l_false); } + public: test_doc_cls(unsigned num_vars): dm(num_vars), m_vars(m) { reg_decl_plugins(m); @@ -292,15 +307,61 @@ public: test_merge(num_clauses); } } + + void test_subtract() { + doc_ref d1(dm); + doc_ref d2(dm); + doc_ref d3(dm); + udoc ds1, ds2; + d1 = dm.allocateX(); + d2 = dm.allocateX(); + d3 = dm.allocateX(); + dm.set(*d1, 0, BIT_1); + dm.set(*d1, 1, BIT_0); + dm.set(*d2, 0, BIT_0); + dm.set(*d2, 1, BIT_1); + //ds1.push_back(d1.detach()); + ds1.push_back(d2.detach()); + // ds1 = {10x, 01x} + d1 = dm.allocateX(); + tbv_ref t1(dm.tbvm()); + tbv_ref t2(dm.tbvm()); + t1 = dm.tbvm().allocateX(); + t2 = dm.tbvm().allocateX(); + t1->set(0, BIT_1); + t1->set(2, BIT_0); + t2->set(0, BIT_0); + t2->set(2, BIT_1); + d1->neg().push_back(t1.detach()); + d1->neg().push_back(t2.detach()); + ds2.push_back(d1.detach()); + ds1.display(dm, std::cout) << "\n"; + ds2.display(dm, std::cout) << "\n"; + svector to_delete(m_vars.size(), false); + expr_ref fml1 = to_formula(ds1, dm, to_delete.c_ptr()); + expr_ref fml2 = to_formula(ds2, dm, to_delete.c_ptr()); + ds1.subtract(dm, ds2); + ds1.display(dm, std::cout) << "\n"; + expr_ref fml3 = to_formula(ds1, dm, to_delete.c_ptr()); + fml1 = m.mk_and(fml1, m.mk_not(fml2)); + check_equiv(fml1, fml3); + ds1.reset(dm); + ds2.reset(dm); + //sub:{xxx \ {1x0, 0x1}} + //result:{100} + } + }; void tst_doc() { + + test_doc_cls tp(4); + tp.test_subtract(); + tp.test_merge(200,7); + tp.test_project(200,7); + tst_doc1(5); tst_doc1(10); tst_doc1(70); - - test_doc_cls tp(4); - tp.test_merge(200,7); - tp.test_project(200,7); } diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index e307455cc..67a008688 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -87,6 +87,43 @@ public: relation_base* t; udoc_relation* t1, *t2, *t3; expr_ref fml(m); + + // filter_by_negation + + /* + 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) ) } + */ + { + relation_signature sig4; + sig4.push_back(bv.mk_sort(1)); + sig4.push_back(bv.mk_sort(1)); + sig4.push_back(bv.mk_sort(1)); + t1 = mk_empty(sig4); + t2 = mk_empty(sig4); + unsigned_vector cols1, cols2; + unsigned num_bits = t1->get_dm().num_tbits(); + + cols1.push_back(0); + cols2.push_back(1); + for (unsigned i = 0; i < 100; ++i) { + set_random(*t1, 2*num_bits/3); + set_random(*t2, 2*num_bits/3); + apply_filter_neg(*t1,*t2, cols1, cols2); + } + cols1.push_back(1); + cols2.push_back(2); + for (unsigned i = 0; i < 100; ++i) { + set_random(*t1, 2*num_bits/3); + set_random(*t2, 2*num_bits/3); + apply_filter_neg(*t1,*t2, cols1, cols2); + } + t1->deallocate(); + t2->deallocate(); + } + // empty { std::cout << "empty\n"; @@ -228,6 +265,22 @@ public: t1->display(std::cout); std::cout << "\n"; t1->deallocate(); } + + // tbv_manager::debug_alloc(); + { + 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); + t1 = mk_full(sig3); + cond1 = m.mk_eq(v0,v1); + apply_filter(*t1, cond1); + t1->deallocate(); + } { relation_signature sig3; @@ -238,8 +291,8 @@ public: 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); + cond1 = m.mk_or(m.mk_eq(v0,v1),m.mk_eq(v0,v2)); apply_filter(*t1, cond1); t1->deallocate(); } @@ -259,73 +312,138 @@ public: t1->deallocate(); } + + app_ref_vector conds(m); + app_ref cond1(m); + 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); + conds.push_back(m.mk_true()); + conds.push_back(m.mk_false()); + conds.push_back(m.mk_eq(v0, v2)); + conds.push_back(m.mk_not(m.mk_eq(v0, v2))); + conds.push_back(m.mk_eq(v0, bv.mk_numeral(rational(2), 3))); + cond1 = m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)); + conds.push_back(cond1); + conds.push_back(m.mk_or(cond1,m.mk_eq(v3,v4))); + conds.push_back(m.mk_or(cond1,m.mk_eq(ex(2,1,v3),ex(1,0,v4)))); + conds.push_back(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v0,v4))); + conds.push_back(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v3,v4))); + conds.push_back(m.mk_or(m.mk_eq(ex(2,1,v0),ex(1,0,v2)),m.mk_eq(v3,v4))); + conds.push_back(m.mk_or(m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)), + m.mk_eq(v3,v4))); + conds.push_back(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),3)))); + conds.push_back(m.mk_or(m.mk_eq(v0,bv.mk_numeral(rational(5),3)), + m.mk_eq(v3,bv.mk_numeral(rational(5),3)))); + conds.push_back(m.mk_or(m.mk_eq(v0,bv.mk_numeral(rational(7),3)), + m.mk_eq(v3,bv.mk_numeral(rational(7),3)))); + conds.push_back(m.mk_not(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v3,v4)))); + + // filter_interpreted { std::cout << "filter interpreted\n"; t1 = 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)); - - 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); + for (unsigned i = 0; i < conds.size(); ++i) { + apply_filter(*t1, conds[i].get()); + } t1->deallocate(); } - // filter_by_negation // filter_interpreted_project + { + unsigned_vector remove; + remove.push_back(0); + remove.push_back(2); + t1 = mk_full(sig2); + for (unsigned i = 0; i < conds.size(); ++i) { + apply_filter_project(*t1, remove, conds[i].get()); + } + remove[1] = 1; + for (unsigned i = 0; i < conds.size(); ++i) { + apply_filter_project(*t1, remove, conds[i].get()); + } + t1->deallocate(); + } + + + } + + void set_random(udoc_relation& r, unsigned num_vals) { + unsigned num_bits = r.get_dm().num_tbits(); + udoc_relation* full = mk_full(r.get_signature()); + rel_union union_fn = p.mk_union_fn(r, r, 0); + (*union_fn)(r, *full); + doc_manager& dm = r.get_dm(); + SASSERT(r.get_udoc().size() == 1); + doc& d0 = r.get_udoc()[0]; + SASSERT(dm.is_full(d0)); + for (unsigned i = 0; i < num_vals; ++i) { + unsigned idx = m_rand(num_bits); + unsigned val = m_rand(2); + tbit b = (val == 0)?BIT_0:BIT_1; + dm.set(d0, idx, b); + } + } + + void apply_filter_neg(udoc_relation& t1, udoc_relation& t2, + 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); + (*negf)(t1, t2); + 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, 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])); + } + + 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: + ( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) } + */ } expr_ref ex(unsigned hi, unsigned lo, expr* e) { @@ -334,6 +452,74 @@ public: return result; } + void apply_filter_project(udoc_relation& t, unsigned_vector const& rm, app* cond) { + scoped_ptr rt; + rt = p.mk_filter_interpreted_and_project_fn(t, cond, rm.size(), rm.c_ptr()); + udoc_relation* full = mk_full(t.get_signature()); + rel_union union_fn = p.mk_union_fn(t, *full, 0); + (*union_fn)(t, *full, 0); + datalog::relation_base* result = (*rt)(t); + + for (unsigned i = 0; i < rm.size(); ++i) { + std::cout << rm[i] << " "; + } + std::cout << mk_pp(cond, m) << "\n"; + t.display(std::cout); + result->display(std::cout); + result->deallocate(); + full->deallocate(); + } + + void verify_filter_project(udoc_relation const& r, unsigned_vector const& rm, app* cond) { + expr_ref fml(m), cfml(m); + r.to_formula(fml); + cfml = cond; + relation_signature const& sig = r.get_signature(); + expr_ref_vector vars(m); + for (unsigned i = 0, j = 0, k = 0; i < sig.size(); ++i) { + if (j < rm.size() && rm[j] == i) { + project_var(i, sig[i], cfml); + ++j; + } + else { + vars.push_back(m.mk_var(k, sig[i])); + ++k; + } + } + + + check_equiv(fml, cfml); + } + + void check_equiv(expr* fml1, expr* fml2) { + TRACE("doc", tout << mk_pp(fml1, m) << "\n"; + tout << mk_pp(fml2, m) << "\n";); + smt_params fp; + smt::kernel solver(m, fp); + expr_ref tmp(m); + tmp = m.mk_not(m.mk_eq(fml1, fml2)); + solver.assert_expr(tmp); + lbool res = solver.check(); + SASSERT(res == l_false); + } + + void project_var(unsigned i, sort* s, expr_ref& fml) { + var_ref v(m); + v = m.mk_var(i, s); + unsigned num_bits = bv.get_bv_size(s); + unsigned p = 1 << num_bits; + expr_ref_vector disj(m); + expr_ref tmp(m); + for (unsigned i = 0; i < p; ++i) { + expr_safe_replace repl(m); + repl.insert(v, bv.mk_numeral(rational(i), s)); + tmp = fml; + repl(tmp); + disj.push_back(tmp); + } + fml = mk_or(m, disj.size(), disj.c_ptr()); + } + 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);