From 2a00f2b38cb09a49e5a2cffe8a1297eac174410e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Sep 2014 05:19:52 -0700 Subject: [PATCH] adding unit tests for doc Signed-off-by: Nikolaj Bjorner --- src/muz/ddnf/doc.cpp | 64 ++++++++++++++++++------- src/muz/ddnf/doc.h | 16 ++++--- src/test/doc.cpp | 93 ++++++++++++++++++++++++++++++++++++ src/test/main.cpp | 1 + src/test/sorting_network.cpp | 3 +- 5 files changed, 153 insertions(+), 24 deletions(-) create mode 100644 src/test/doc.cpp diff --git a/src/muz/ddnf/doc.cpp b/src/muz/ddnf/doc.cpp index 27192ed26..b9aca8bc7 100644 --- a/src/muz/ddnf/doc.cpp +++ b/src/muz/ddnf/doc.cpp @@ -22,49 +22,81 @@ Revision History: #include "doc.h" void doc_manager::reset() { + // m.reset(); - not until docs are in small object allocator. } doc* doc_manager::allocate() { - return 0; + return alloc(doc, m.allocate()); } doc* doc_manager::allocate1() { - return 0; + return alloc(doc, m.allocate1()); } doc* doc_manager::allocate0() { - return 0; + return alloc(doc, m.allocate0()); } doc* doc_manager::allocateX() { - return 0; + return alloc(doc, m.allocateX()); } doc* doc_manager::allocate(doc const& src) { - return 0; + doc* r = alloc(doc, m.allocate(src.pos())); + for (unsigned i = 0; i < src.neg().size(); ++i) { + r->neg().push_back(m.allocate(src.neg()[i])); + } + return r; } doc* doc_manager::allocate(uint64 n) { - return 0; + return alloc(doc, m.allocate(n)); } doc* doc_manager::allocate(rational const& r) { - return 0; + return alloc(doc, m.allocate(r)); } doc* doc_manager::allocate(uint64 n, unsigned hi, unsigned lo) { - return 0; + return alloc(doc, m.allocate(n, hi, lo)); } -doc* doc_manager::allocate(doc, unsigned const* permutation) { - return 0; +doc* doc_manager::allocate(doc const& src, unsigned const* permutation) { + doc* r = alloc(doc, m.allocate(src.pos(), permutation)); + for (unsigned i = 0; i < src.neg().size(); ++i) { + r->neg().push_back(m.allocate(src.neg()[i], permutation)); + } + return r; } void doc_manager::deallocate(doc* src) { + dealloc(src); } -void doc_manager::copy(doc& dst, doc const& src) const { +void doc_manager::copy(doc& dst, doc const& src) { + m.copy(dst.pos(), src.pos()); + unsigned n = std::min(src.neg().size(), dst.neg().size()); + 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); + } + for (unsigned i = n; i < src.neg().size(); ++i) { + dst.neg().push_back(m.allocate(src.neg()[i])); + } } -doc& doc_manager::fill0(doc& src) const { +doc& doc_manager::fill0(doc& src) { + src.neg().reset(m); + m.fill0(src.pos()); return src; } -doc& doc_manager::fill1(doc& src) const { +doc& doc_manager::fill1(doc& src) { + src.neg().reset(m); + m.fill1(src.pos()); return src; } -doc& doc_manager::fillX(doc& src) const { +doc& doc_manager::fillX(doc& src) { + src.neg().reset(m); + m.fillX(src.pos()); return src; } -bool doc_manager::set_and(doc& dst, doc const& src) const { - return false; +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 < src.neg().size(); ++i) { + dst.neg().insert(m, m.allocate(src.neg()[i])); + } + return (src.neg().is_empty() || fold_neg(dst)); } bool doc_manager::fold_neg(doc& dst) { start_over: diff --git a/src/muz/ddnf/doc.h b/src/muz/ddnf/doc.h index 78cd5c94b..3b24b52d1 100644 --- a/src/muz/ddnf/doc.h +++ b/src/muz/ddnf/doc.h @@ -44,15 +44,15 @@ public: doc* allocate(uint64 n); doc* allocate(rational const& r); doc* allocate(uint64 n, unsigned hi, unsigned lo); - doc* allocate(doc, unsigned const* permutation); + doc* allocate(doc const& src, unsigned const* permutation); void deallocate(doc* src); - void copy(doc& dst, doc const& src) const; - doc& reset(doc& src) const { return fill0(src); } - doc& fill0(doc& src) const; - doc& fill1(doc& src) const; - doc& fillX(doc& src) const; + void copy(doc& dst, doc const& src); + doc& reset(doc& src) { return fill0(src); } + doc& fill0(doc& src); + doc& fill1(doc& src); + doc& fillX(doc& src); bool is_full(doc const& src) const; - bool set_and(doc& dst, doc const& src) const; + bool set_and(doc& dst, doc const& src); bool fold_neg(doc& dst); bool intersect(doc const& A, doc const& B, doc& result) const; void complement(doc const& src, ptr_vector& result); @@ -328,6 +328,7 @@ public: } }; + doc(tbv* t): m_pos(t) {} tbv& pos() { return *m_pos; } utbv& neg() { return m_neg; } tbv const& pos() const { return *m_pos; } @@ -349,6 +350,7 @@ public: doc_ref& operator=(doc* d2) { if (d) dm.deallocate(d); d = d2; + return *this; } doc& operator*() { return *d; } doc* operator->() { return d; } diff --git a/src/test/doc.cpp b/src/test/doc.cpp new file mode 100644 index 000000000..27508bac4 --- /dev/null +++ b/src/test/doc.cpp @@ -0,0 +1,93 @@ +#include "doc.h" + +static void tst_doc1(unsigned n) { + doc_manager m(n); + + m.allocate(); + m.reset(); + + doc_ref d(m, m.allocate()); + doc_ref d1(m, m.allocate1()); + doc_ref d0(m, m.allocate0()); + doc_ref dX(m, m.allocateX()); + doc_ref dXc(m, m.allocate(*dX)); + doc_ref d10(m, m.allocate(10)); + doc_ref d20(m, m.allocate(rational(20))); + unsigned hi = 3, lo = 1; + SASSERT(hi <= n); + doc_ref d111X(m, m.allocate(0xFF, hi, lo)); + m.copy(*d, *d10); + SASSERT(m.equals(*d, *d10)); + m.reset(*d); + SASSERT(!m.equals(*d, *d10)); + m.fill0(*d10); + SASSERT(m.equals(*d, *d10)); + m.fill1(*d); + d10 = m.allocate(10); + SASSERT(!m.equals(*d, *d10)); + SASSERT(m.equals(*d, *d1)); + m.fillX(*d); + SASSERT(m.equals(*d, *dX)); + SASSERT(m.is_full(*dX)); + SASSERT(!m.is_full(*d1)); + + VERIFY(m.set_and(*dX,*dX)); + SASSERT(m.equals(*dXc,*dX)); + VERIFY(m.set_and(*dX,*d1)); + SASSERT(!m.equals(*dXc,*dX)); + SASSERT(m.equals(*dX,*d1)); + VERIFY(m.fold_neg(*dX)); + ptr_vector result; + // VERIFY(!m.intersect(*d1,*d0, result)); + m.subtract(*d1,*d0, result); + SASSERT(result.empty()); + SASSERT(m.contains(*dX,*d1)); + SASSERT(m.contains(*dX,*d0)); + SASSERT(!m.contains(*d0,*d1)); + SASSERT(!m.contains(*d1,*d0)); + + + d1->neg().push_back(m.tbvm().allocate0()); + m.display(std::cout, *d1) << " -> "; + VERIFY(m.fold_neg(*d1)); + m.display(std::cout, *d1) << "\n"; + + + svector to_delete(n); + to_delete[1] = true; + to_delete[3] = true; + doc_manager m1(n-2); + doc_ref d1_1(m1, m1.project(n, to_delete.c_ptr(), *d0)); + doc_ref d1_2(m1, m1.allocate1()); + m.display(std::cout, *d1) << " -> "; + m1.display(std::cout, *d1_1) << "\n"; + SASSERT(m1.equals(*d1_1,*d1_2)); + +} + + +// generate "all" clauses over num_vars +// create XXXX \ clauses +// project 0, 1, 2, 3 variables +// check that result is the same as QE over those clauses. + +class test_doc_project { + random_gen m_ran; + + void test_clauses(unsigned num_vars, unsigned num_clauses) { + // + } + +public: + void operator()(unsigned num_vars, unsigned min_clauses, unsigned max_clauses) { + for (unsigned i = min_clauses; i < max_clauses; ++i) { + test_clauses(num_vars, i); + } + } +}; + +void tst_doc() { + tst_doc1(5); + tst_doc1(10); + tst_doc1(70); +} diff --git a/src/test/main.cpp b/src/test/main.cpp index 5d30bb0af..f613402b8 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -142,6 +142,7 @@ int main(int argc, char ** argv) { TST(bit_vector); TST(fixed_bit_vector); TST(tbv); + TST(doc); TST(string_buffer); TST(map); TST(diff_logic); diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp index d54c575ca..dd46b61df 100644 --- a/src/test/sorting_network.cpp +++ b/src/test/sorting_network.cpp @@ -7,6 +7,7 @@ #include "smt_kernel.h" #include "model_smt2_pp.h" #include "smt_params.h" +#include "ast_util.h" @@ -171,7 +172,7 @@ struct ast_ext2 { return trail(m.mk_fresh_const("x", m.mk_bool_sort())); } void mk_clause(unsigned n, literal const* lits) { - m_clauses.push_back(m.mk_or_reduced(n, lits)); + m_clauses.push_back(mk_or(m, n, lits)); } };