From a50cbef877c0f6e79012d87c4a994173f5b746d4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Sep 2014 19:01:15 -0700 Subject: [PATCH] testing doc Signed-off-by: Nikolaj Bjorner --- src/muz/rel/dl_instruction.cpp | 21 ++++++ src/muz/rel/dl_instruction.h | 2 + src/muz/rel/doc.cpp | 23 ++++--- src/muz/rel/doc.h | 48 +++++++++----- src/muz/rel/tbv.cpp | 3 +- src/muz/rel/udoc_relation.cpp | 75 +++++++++++++++++++-- src/test/tbv.cpp | 15 +++++ src/test/udoc_relation.cpp | 115 +++++++++++++++++++++++++++------ src/util/fixed_bit_vector.cpp | 3 +- src/util/fixed_bit_vector.h | 81 +++++++++++------------ 10 files changed, 291 insertions(+), 95 deletions(-) diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index a702c27ce..1dfdf96b9 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -154,6 +154,10 @@ namespace datalog { display_body_impl(ctx, out, indentation); } + void instruction::log_verbose(execution_context& ctx) { + IF_VERBOSE(2, display(ctx.get_rel_context(), verbose_stream());); + } + class instr_io : public instruction { bool m_store; func_decl_ref m_pred; @@ -162,6 +166,7 @@ namespace datalog { instr_io(bool store, func_decl_ref pred, reg_idx reg) : m_store(store), m_pred(pred), m_reg(reg) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); if (m_store) { if (ctx.reg(m_reg)) { ctx.get_rel_context().store_relation(m_pred, ctx.release_reg(m_reg)); @@ -237,6 +242,7 @@ namespace datalog { instr_clone_move(bool clone, reg_idx src, reg_idx tgt) : m_clone(clone), m_src(src), m_tgt(tgt) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); ctx.make_empty(m_tgt); if (m_clone) { ctx.set_reg(m_tgt, ctx.reg(m_src) ? ctx.reg(m_src)->clone() : 0); @@ -296,6 +302,7 @@ namespace datalog { dealloc(m_body); } virtual bool perform(execution_context & ctx) { + log_verbose(ctx); TRACE("dl", tout << "loop entered\n";); unsigned count = 0; while (!control_is_empty(ctx)) { @@ -339,6 +346,7 @@ namespace datalog { : m_rel1(rel1), m_rel2(rel2), m_cols1(col_cnt, cols1), m_cols2(col_cnt, cols2), m_res(result) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); ctx.make_empty(m_res); if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) { return true; @@ -400,6 +408,7 @@ namespace datalog { instr_filter_equal(ast_manager & m, reg_idx reg, const relation_element & value, unsigned col) : m_reg(reg), m_value(value, m), m_col(col) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); if (!ctx.reg(m_reg)) { return true; } @@ -447,6 +456,7 @@ namespace datalog { instr_filter_identical(reg_idx reg, unsigned col_cnt, const unsigned * identical_cols) : m_reg(reg), m_cols(col_cnt, identical_cols) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); if (!ctx.reg(m_reg)) { return true; } @@ -493,6 +503,7 @@ namespace datalog { if (!ctx.reg(m_reg)) { return true; } + log_verbose(ctx); relation_mutator_fn * fn; relation_base & r = *ctx.reg(m_reg); @@ -543,6 +554,7 @@ namespace datalog { m_res(result) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); if (!ctx.reg(m_src)) { ctx.make_empty(m_res); return true; @@ -601,6 +613,7 @@ namespace datalog { instr_union(reg_idx src, reg_idx tgt, reg_idx delta, bool widen) : m_src(src), m_tgt(tgt), m_delta(delta), m_widen(widen) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); TRACE("dl", tout << "union " << m_src << " into " << m_tgt << " " << ctx.reg(m_src) << " " << ctx.reg(m_tgt) << "\n";); if (!ctx.reg(m_src)) { @@ -713,6 +726,7 @@ namespace datalog { reg_idx tgt) : m_projection(projection), m_src(src), m_cols(col_cnt, cols), m_tgt(tgt) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); ctx.make_empty(m_tgt); if (!ctx.reg(m_src)) { return true; @@ -778,6 +792,7 @@ namespace datalog { m_cols2(joined_col_cnt, cols2), m_removed_cols(removed_col_cnt, removed_cols), m_res(result) { } virtual bool perform(execution_context & ctx) { + log_verbose(ctx); ctx.make_empty(m_res); if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) { return true; @@ -839,6 +854,7 @@ namespace datalog { } virtual bool perform(execution_context & ctx) { + log_verbose(ctx); if (!ctx.reg(m_src)) { ctx.make_empty(m_result); return true; @@ -893,6 +909,7 @@ namespace datalog { const unsigned * cols2) : m_tgt(tgt), m_neg_rel(neg_rel), m_cols1(col_cnt, cols1), m_cols2(col_cnt, cols2) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); if (!ctx.reg(m_tgt) || !ctx.reg(m_neg_rel)) { return true; } @@ -948,6 +965,7 @@ namespace datalog { m_fact.push_back(val); } virtual bool perform(execution_context & ctx) { + log_verbose(ctx); ctx.make_empty(m_tgt); relation_base * rel = ctx.get_rel_context().get_rmanager().mk_empty_relation(m_sig, m_pred); rel->add_fact(m_fact); @@ -980,6 +998,7 @@ namespace datalog { public: instr_mk_total(const relation_signature & sig, func_decl* p, reg_idx tgt) : m_sig(sig), m_pred(p), m_tgt(tgt) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); ctx.make_empty(m_tgt); ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred)); return true; @@ -1006,6 +1025,7 @@ namespace datalog { instr_mark_saturated(ast_manager & m, func_decl * pred) : m_pred(pred, m) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); ctx.get_rel_context().get_rmanager().mark_saturated(m_pred); return true; } @@ -1027,6 +1047,7 @@ namespace datalog { instr_assert_signature(const relation_signature & s, reg_idx tgt) : m_sig(s), m_tgt(tgt) {} virtual bool perform(execution_context & ctx) { + log_verbose(ctx); if (ctx.reg(m_tgt)) { SASSERT(ctx.reg(m_tgt)->get_signature()==m_sig); } diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h index fa705a172..b816f9e55 100644 --- a/src/muz/rel/dl_instruction.h +++ b/src/muz/rel/dl_instruction.h @@ -222,6 +222,8 @@ namespace datalog { Each line must be prepended by \c indentation and ended by a newline character. */ virtual void display_body_impl(rel_context const & ctx, std::ostream & out, std::string indentation) const {} + void log_verbose(execution_context& ctx); + public: typedef execution_context::reg_type reg_type; typedef execution_context::reg_idx reg_idx; diff --git a/src/muz/rel/doc.cpp b/src/muz/rel/doc.cpp index 1db1ac2b7..6ddc5b6b4 100644 --- a/src/muz/rel/doc.cpp +++ b/src/muz/rel/doc.cpp @@ -50,6 +50,7 @@ doc* doc_manager::allocate(doc const& src) { return r; } doc* doc_manager::allocate(tbv* t) { + SASSERT(t); void* mm = m_alloc.allocate(sizeof(doc)); return new (mm) doc(t); } @@ -85,9 +86,7 @@ void doc_manager::copy(doc& dst, doc const& src) { for (unsigned i = 0; i < n; ++i) { m.copy(dst.neg()[i], src.neg()[i]); } - for (unsigned i = n; i < dst.neg().size(); ++i) { - dst.neg().erase(m, dst.neg().size()-1); - } + dst.neg().reset(m); for (unsigned i = n; i < src.neg().size(); ++i) { dst.neg().push_back(m.allocate(src.neg()[i])); } @@ -110,12 +109,7 @@ doc& doc_manager::fillX(doc& src) { bool doc_manager::set_and(doc& dst, doc const& src) { // (A \ B) & (C \ D) = (A & C) \ (B u D) if (!m.set_and(dst.pos(), src.pos())) return false; - for (unsigned i = 0; i < dst.neg().size(); ++i) { - if (!m.set_and(dst.neg()[i], dst.pos())) { - dst.neg().erase(m, i); - --i; - } - } + dst.neg().intersect(m, src.pos()); tbv_ref t(m); for (unsigned i = 0; i < src.neg().size(); ++i) { t = m.allocate(src.neg()[i]); @@ -279,6 +273,7 @@ bool doc_manager::intersect(doc const& A, doc const& B, doc& result) { doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src) { tbv_manager& dstt = dstm.m; doc* r = dstm.allocate(dstt.project(n, to_delete, src.pos())); + SASSERT(r); if (src.neg().is_empty()) { return r; @@ -405,13 +400,21 @@ void doc_manager::complement(doc const& src, ptr_vector& result) { result.push_back(allocate(src.neg()[i])); } } +// (A \ {A1}) \ (B \ {B1}) +// (A & !A1 & & !B) | (A & B1 & !A1) +// A \ {A1 u B} u (A & B1) \ {A1} void doc_manager::subtract(doc const& A, doc const& B, ptr_vector& result) { doc_ref r(*this), r2(*this); + tbv_ref t(m); r = allocate(A); - if (r->neg().insert(m, m.allocate(B.pos()))) { + t = m.allocate(B.pos()); + if (m.set_and(*t, A.pos()) && r->neg().insert(m, t.detach())) { result.push_back(r.detach()); r = allocate(A); } + else { + result.push_back(allocate(A)); + } for (unsigned i = 0; i < B.neg().size(); ++i) { r2 = allocate(B.neg()[i]); if (set_and(*r, *r2)) { diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h index e56196026..b29ecb7c6 100644 --- a/src/muz/rel/doc.h +++ b/src/muz/rel/doc.h @@ -111,12 +111,16 @@ public: } void push_back(T* t) { + SASSERT(t); m_elems.push_back(t); } void erase(M& m, unsigned idx) { - T* t = m_elems[idx]; - m_elems.erase(t); - m.deallocate(t); + m.deallocate(m_elems[idx]); + unsigned sz = m_elems.size(); + for (unsigned i = idx+1; i < sz; ++i) { + m_elems[i-1] = m_elems[i]; + } + m_elems.resize(sz-1); } void reset(M& m) { for (unsigned i = 0; i < m_elems.size(); ++i) { @@ -125,21 +129,20 @@ public: m_elems.reset(); } bool insert(M& m, T* t) { + SASSERT(t); unsigned sz = size(), j = 0; bool found = false; for (unsigned i = 0; i < sz; ++i, ++j) { + if (m.contains(*m_elems[i], *t)) { + found = true; + } if (!found && m.contains(*t, *m_elems[i])) { m.deallocate(m_elems[i]); --j; } - else { - if (m.contains(*m_elems[i], *t)) { - found = true; - } - if (i != j) { - m_elems[j] = m_elems[i]; - } - } + else if (i != j) { + m_elems[j] = m_elems[i]; + } } if (j != sz) m_elems.resize(j); if (found) { @@ -150,7 +153,7 @@ public: } return !found; } - void intersect(M& m, T& t) { + void intersect(M& m, T const& t) { unsigned sz = size(); unsigned j = 0; for (unsigned i = 0; i < sz; ++i, ++j) { @@ -159,7 +162,7 @@ public: --j; } else if (i != j) { - m_elems[i] = m_elems[j]; + m_elems[j] = m_elems[i]; } } if (j != sz) m_elems.resize(j); @@ -233,13 +236,26 @@ public: std::swap(*this, result); } - void merge(M& m, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols) { + bool well_formed(M& m) const { for (unsigned i = 0; i < size(); ++i) { + if (!m.well_formed(*m_elems[i])) return false; + } + return true; + } + + void merge(M& m, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols) { + unsigned j = 0; + unsigned sz = size(); + for (unsigned i = 0; i < sz; ++i, ++j) { if (!m.merge(*m_elems[i], lo, length, equalities, discard_cols)) { - erase(m, i); - --i; + --j; + m.deallocate(m_elems[i]); + } + else if (i != j) { + m_elems[j] = m_elems[i]; } } + if (j != sz) m_elems.resize(j); } void merge(M& m, unsigned lo1, unsigned lo2, unsigned length, bit_vector const& discard_cols) { diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 23745f333..458aea9d0 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -92,7 +92,8 @@ tbv* tbv_manager::allocate(uint64 val, unsigned hi, unsigned lo) { } tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) { tbv* r = allocate(); - for (unsigned i = 0; i < num_tbits(); ++i) { + unsigned sz = num_tbits(); + for (unsigned i = 0; i < sz; ++i) { r->set(permutation[i], bv[i]); } return r; diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp index 874885e5f..17b2ded0c 100644 --- a/src/muz/rel/udoc_relation.cpp +++ b/src/muz/rel/udoc_relation.cpp @@ -373,6 +373,7 @@ namespace datalog { } } TRACE("doc", result->display(tout << "result:\n");); + SASSERT(r.well_formed(result->get_dm())); return result; } }; @@ -412,6 +413,7 @@ namespace datalog { ud2.push_back(d2.detach()); } TRACE("doc", tout << "final size: " << r->get_size_estimate_rows() << '\n';); + SASSERT(ud2.well_formed(dm2)); return r; } }; @@ -431,20 +433,60 @@ namespace datalog { rename_fn(udoc_relation const& t, unsigned cycle_len, const unsigned * cycle) : convenient_relation_rename_fn(t.get_signature(), cycle_len, cycle) { udoc_plugin& p = t.get_plugin(); + ast_manager& m = p.get_ast_manager(); + relation_signature const& sig1 = t.get_signature(); + relation_signature const& sig2 = get_result_signature(); + unsigned_vector permutation0, column_info; for (unsigned i = 0; i < t.get_num_bits(); ++i) { m_permutation.push_back(i); } - unsigned len = t.column_num_bits(cycle[0]); + for (unsigned i = 0; i < sig1.size(); ++i) { + permutation0.push_back(i); + } for (unsigned i = 0; i < cycle_len; ++i) { unsigned j = (i + 1)%cycle_len; unsigned col1 = cycle[i]; unsigned col2 = cycle[j]; - unsigned lo1 = t.column_idx(col1); - unsigned lo2 = t.column_idx(col2); + permutation0[col2] = col1; + } + unsigned column = 0; + for (unsigned i = 0; i < sig2.size(); ++i) { + column_info.push_back(column); + column += p.num_sort_bits(sig2[i]); + } + column_info.push_back(column); + SASSERT(column == t.get_num_bits()); + + TRACE("doc", + sig1.output(m, tout << "sig1: "); tout << "\n"; + sig2.output(m, tout << "sig2: "); tout << "\n"; + tout << "permute: "; + for (unsigned i = 0; i < permutation0.size(); ++i) { + tout << permutation0[i] << " "; + } + tout << "\n"; + tout << "cycle: "; + for (unsigned i = 0; i < cycle_len; ++i) { + tout << cycle[i] << " "; + } + tout << "\n"; + ); + + + // 0 -> 2 + // [3:2:1] -> [1:2:3] + // [3,4,5,1,2,0] + + for (unsigned i = 0; i < sig1.size(); ++i) { + unsigned len = t.column_num_bits(i); + unsigned lo1 = t.column_idx(i); + unsigned col2 = permutation0[i]; + unsigned lo2 = column_info[col2]; + SASSERT(lo2 + len <= t.get_num_bits()); + SASSERT(lo1 + len <= t.get_num_bits()); for (unsigned k = 0; k < len; ++k) { m_permutation[k + lo1] = k + lo2; } - SASSERT(t.column_num_bits(col1) == t.column_num_bits(col2)); } } @@ -457,10 +499,12 @@ namespace datalog { udoc const& src = r.get_udoc(); udoc& dst = result->get_udoc(); doc_manager& dm = r.get_dm(); + SASSERT(&result->get_dm() == &dm); for (unsigned i = 0; i < src.size(); ++i) { dst.push_back(dm.allocate(src[i], m_permutation.c_ptr())); } TRACE("doc", result->display(tout << "result:\n");); + SASSERT(dst.well_formed(dm)); return result; } }; @@ -488,6 +532,8 @@ 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); + SASSERT(r.get_udoc().well_formed(dm)); + SASSERT(!d1 || d1->well_formed(dm)); TRACE("doc", _r.display(tout << "dst':\n"); ); } }; @@ -547,6 +593,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); + SASSERT(d.well_formed(dm)); TRACE("doc", tout << "final size: " << r.get_size_estimate_rows() << '\n';); } }; @@ -575,6 +622,7 @@ namespace datalog { virtual void operator()(relation_base & tb) { udoc_relation & t = get(tb); t.get_udoc().intersect(dm, *m_filter); + SASSERT(t.get_udoc().well_formed(t.get_dm())); } }; relation_mutator_fn * udoc_plugin::mk_filter_equal_fn( @@ -826,11 +874,15 @@ namespace datalog { virtual void operator()(relation_base & tb) { udoc_relation & t = get(tb); udoc& u = t.get_udoc(); + SASSERT(u.well_formed(dm)); u.intersect(dm, m_udoc); + SASSERT(u.well_formed(dm)); if (m_condition && !u.is_empty()) { t.apply_guard(m_condition, u, m_equalities, m_empty_bv); + SASSERT(u.well_formed(dm)); } u.simplify(dm); + SASSERT(u.well_formed(dm)); TRACE("doc", tout << "final size: " << t.get_size_estimate_rows() << '\n';); } }; @@ -896,7 +948,12 @@ namespace datalog { } renamed_neg.push_back(newD.detach()); } - dst.subtract(t.get_dm(), renamed_neg); + TRACE("doc", dst.display(dm, tout) << "\n"; + renamed_neg.display(dm, tout) << "\n"; + ); + dst.subtract(dm, renamed_neg); + TRACE("doc", dst.display(dm, tout) << "\n";); + SASSERT(dst.well_formed(dm)); renamed_neg.reset(t.get_dm()); } void copy_column( @@ -971,17 +1028,23 @@ namespace datalog { udoc const& u1 = t.get_udoc(); doc_manager& dm = t.get_dm(); udoc u2; + SASSERT(u1.well_formed(dm)); u2.copy(dm, u1); + SASSERT(u2.well_formed(dm)); u2.intersect(dm, m_udoc); - u2.merge(dm, m_roots, m_equalities, m_col_list); + SASSERT(u2.well_formed(dm)); + u2.merge(dm, m_roots, m_equalities, m_col_list); + SASSERT(u2.well_formed(dm)); if (m_condition && !u2.is_empty()) { t.apply_guard(m_condition, u2, m_equalities, m_col_list); + SASSERT(u2.well_formed(dm)); } udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature())); doc_manager& dm2 = r->get_dm(); for (unsigned i = 0; i < u2.size(); ++i) { doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), u2[i]); r->get_udoc().insert(dm2, d); + SASSERT(r->get_udoc().well_formed(dm2)); } u2.reset(dm); return r; diff --git a/src/test/tbv.cpp b/src/test/tbv.cpp index d56fcd84a..7fab0b56c 100644 --- a/src/test/tbv.cpp +++ b/src/test/tbv.cpp @@ -40,7 +40,22 @@ static void tst1(unsigned num_bits) { m.deallocate(bN); } +static void tst0() { + tbv_manager m(0); + + tbv_ref t1(m), t2(m), t3(m); + t1 = m.allocate1(); + t2 = m.allocate0(); + t3 = m.allocateX(); + m.display(std::cout, *t1) << "\n"; + m.display(std::cout, *t2) << "\n"; + m.display(std::cout, *t3) << "\n"; + SASSERT(m.equals(*t1, *t2)); + SASSERT(m.equals(*t1, *t3)); +} + void tst_tbv() { + tst0(); tst1(31); tst1(11); tst1(15); diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp index 13623aeeb..197186bbf 100644 --- a/src/test/udoc_relation.cpp +++ b/src/test/udoc_relation.cpp @@ -88,8 +88,10 @@ public: udoc_relation* t1, *t2, *t3; expr_ref fml(m); + test_rename(); test_filter_neg(); + // empty { std::cout << "empty\n"; @@ -168,26 +170,6 @@ public: t1->deallocate(); } - // rename - { - t1 = mk_empty(sig); - unsigned_vector cycle; - cycle.push_back(0); - cycle.push_back(2); - datalog::relation_transformer_fn* rename = p.mk_rename_fn(*t1, cycle.size(), cycle.c_ptr()); - - t1->add_fact(fact1); - t1->add_fact(fact2); - t1->add_fact(fact3); - t = (*rename)(*t1); - t1->display(std::cout); std::cout << "\n"; - t->display(std::cout); std::cout << "\n"; - t->deallocate(); - - dealloc(rename); - t1->deallocate(); - } - // union { t1 = mk_empty(sig); @@ -342,6 +324,98 @@ public: } + void test_rename() { + udoc_relation* t1; + // rename + datalog::relation_signature sig; + sig.push_back(bv.mk_sort(12)); + sig.push_back(bv.mk_sort(6)); + sig.push_back(bv.mk_sort(2)); + datalog::relation_fact fact1(m); + fact1.push_back(bv.mk_numeral(rational(1), 12)); + fact1.push_back(bv.mk_numeral(rational(6), 6)); + fact1.push_back(bv.mk_numeral(rational(3), 2)); + t1 = mk_empty(sig); + t1->add_fact(fact1); + unsigned_vector cycle; + cycle.push_back(0); + cycle.push_back(2); + check_permutation(t1, cycle); + + sig.reset(); + sig.push_back(bv.mk_sort(2)); + sig.push_back(bv.mk_sort(6)); + sig.push_back(bv.mk_sort(12)); + fact1.reset(); + fact1.push_back(bv.mk_numeral(rational(3), 2)); + fact1.push_back(bv.mk_numeral(rational(6), 6)); + fact1.push_back(bv.mk_numeral(rational(1), 12)); + t1 = mk_empty(sig); + t1->add_fact(fact1); + cycle.reset(); + cycle.push_back(0); + cycle.push_back(2); + check_permutation(t1, cycle); + + t1 = mk_empty(sig); + t1->add_fact(fact1); + cycle.reset(); + cycle.push_back(0); + cycle.push_back(1); + cycle.push_back(2); + check_permutation(t1, cycle); + } + + void check_permutation(relation_base* t1, unsigned_vector const& cycle) { + scoped_ptr rename; + rename = p.mk_rename_fn(*t1, cycle.size(), cycle.c_ptr()); + relation_base* t = (*rename)(*t1); + verify_permutation(*t1,*t, cycle); + t1->display(std::cout); std::cout << "\n"; + t->display(std::cout); std::cout << "\n"; + t->deallocate(); + t1->deallocate(); + } + + void verify_permutation(relation_base const& src, relation_base const& dst, + unsigned_vector const& cycle) { + unsigned_vector perm; + relation_signature const& sig1 = src.get_signature(); + relation_signature const& sig2 = dst.get_signature(); + for (unsigned i = 0; i < sig1.size(); ++i) { + perm.push_back(i); + } + for (unsigned i = 0; i < cycle.size(); ++i) { + unsigned j = (i + 1)%cycle.size(); + unsigned col1 = cycle[i]; + unsigned col2 = cycle[j]; + perm[col2] = col1; + } + for (unsigned i = 0; i < perm.size(); ++i) { + SASSERT(sig2[perm[i]] == sig1[i]); + } + expr_ref_vector sub(m); + for (unsigned i = 0; i < perm.size(); ++i) { + sub.push_back(m.mk_var(perm[i], sig1[i])); + } + var_subst subst(m, false); + expr_ref fml1(m), fml2(m); + src.to_formula(fml1); + dst.to_formula(fml2); + subst(fml1, sub.size(), sub.c_ptr(), fml1); + expr_ref_vector vars(m); + for (unsigned i = 0; i < sig2.size(); ++i) { + std::stringstream strm; + strm << "x" << i; + vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig2[i])); + } + + subst(fml1, vars.size(), vars.c_ptr(), fml1); + subst(fml2, vars.size(), vars.c_ptr(), fml2); + + check_equiv(fml1, fml2); + } + /* The filter_by_negation postcondition: filter_by_negation(tgt, neg, columns in tgt: c1,...,cN, @@ -499,7 +573,6 @@ public: } } - check_equiv(fml, cfml); } diff --git a/src/util/fixed_bit_vector.cpp b/src/util/fixed_bit_vector.cpp index f2af843c7..3711ef5eb 100644 --- a/src/util/fixed_bit_vector.cpp +++ b/src/util/fixed_bit_vector.cpp @@ -37,6 +37,7 @@ fixed_bit_vector_manager::fixed_bit_vector_manager(unsigned num_bits): fixed_bit_vector* fixed_bit_vector_manager::allocate() { + if (m_num_bytes == 0) return &m_0; return static_cast(m_alloc.allocate(m_num_bytes)); } @@ -59,7 +60,7 @@ fixed_bit_vector* fixed_bit_vector_manager::allocate(fixed_bit_vector const& bv) } void fixed_bit_vector_manager::deallocate(fixed_bit_vector* bv) { - m_alloc.deallocate(m_num_bytes, bv); + if (m_num_bytes > 0) m_alloc.deallocate(m_num_bytes, bv); } diff --git a/src/util/fixed_bit_vector.h b/src/util/fixed_bit_vector.h index 1ac3363d4..11cb91fef 100644 --- a/src/util/fixed_bit_vector.h +++ b/src/util/fixed_bit_vector.h @@ -25,46 +25,6 @@ Revision History: #include"debug.h" #include"small_object_allocator.h" -class fixed_bit_vector; -class fixed_bit_vector_manager { - friend class fixed_bit_vector; - small_object_allocator m_alloc; - unsigned m_num_bits; - unsigned m_num_bytes; - unsigned m_num_words; - unsigned m_mask; - - static unsigned num_words(unsigned num_bits) { - return (num_bits + 31) / 32; - } - -public: - fixed_bit_vector_manager(unsigned num_bits); - - void reset() { m_alloc.reset(); } - fixed_bit_vector* allocate(); - fixed_bit_vector* allocate1(); - fixed_bit_vector* allocate0(); - fixed_bit_vector* allocate(fixed_bit_vector const& bv); - void deallocate(fixed_bit_vector* bv); - - void copy(fixed_bit_vector& dst, fixed_bit_vector const& src) const; - unsigned num_words() const { return m_num_words; } - unsigned num_bytes() const { return m_num_bytes; } - unsigned num_bits() const { return m_num_bits; } - fixed_bit_vector& reset(fixed_bit_vector& bv) const { return fill0(bv); } - fixed_bit_vector& fill0(fixed_bit_vector& bv) const; - fixed_bit_vector& fill1(fixed_bit_vector& bv) const; - fixed_bit_vector& set_and(fixed_bit_vector& dst, fixed_bit_vector const& src) const; - fixed_bit_vector& set_or(fixed_bit_vector& dst, fixed_bit_vector const& src) const; - fixed_bit_vector& set_neg(fixed_bit_vector& dst) const; - unsigned last_word(fixed_bit_vector const& bv) const; - bool equals(fixed_bit_vector const& a, fixed_bit_vector const& b) const; - unsigned hash(fixed_bit_vector const& src) const; - bool contains(fixed_bit_vector const& a, fixed_bit_vector const& b) const; - std::ostream& display(std::ostream& out, fixed_bit_vector const& b) const; -}; - class fixed_bit_vector { friend class fixed_bit_vector_manager; friend class tbv_manager; @@ -114,6 +74,47 @@ public: }; +class fixed_bit_vector_manager { + friend class fixed_bit_vector; + small_object_allocator m_alloc; + unsigned m_num_bits; + unsigned m_num_bytes; + unsigned m_num_words; + unsigned m_mask; + fixed_bit_vector m_0; + + static unsigned num_words(unsigned num_bits) { + return (num_bits + 31) / 32; + } + +public: + fixed_bit_vector_manager(unsigned num_bits); + + void reset() { m_alloc.reset(); } + fixed_bit_vector* allocate(); + fixed_bit_vector* allocate1(); + fixed_bit_vector* allocate0(); + fixed_bit_vector* allocate(fixed_bit_vector const& bv); + void deallocate(fixed_bit_vector* bv); + + void copy(fixed_bit_vector& dst, fixed_bit_vector const& src) const; + unsigned num_words() const { return m_num_words; } + unsigned num_bytes() const { return m_num_bytes; } + unsigned num_bits() const { return m_num_bits; } + fixed_bit_vector& reset(fixed_bit_vector& bv) const { return fill0(bv); } + fixed_bit_vector& fill0(fixed_bit_vector& bv) const; + fixed_bit_vector& fill1(fixed_bit_vector& bv) const; + fixed_bit_vector& set_and(fixed_bit_vector& dst, fixed_bit_vector const& src) const; + fixed_bit_vector& set_or(fixed_bit_vector& dst, fixed_bit_vector const& src) const; + fixed_bit_vector& set_neg(fixed_bit_vector& dst) const; + unsigned last_word(fixed_bit_vector const& bv) const; + bool equals(fixed_bit_vector const& a, fixed_bit_vector const& b) const; + unsigned hash(fixed_bit_vector const& src) const; + bool contains(fixed_bit_vector const& a, fixed_bit_vector const& b) const; + std::ostream& display(std::ostream& out, fixed_bit_vector const& b) const; +}; + + #endif /* _FIXED_BIT_VECTOR_H_ */