diff --git a/src/muz/ddnf/doc.cpp b/src/muz/ddnf/doc.cpp index 2d8df7758..ec66d5c34 100644 --- a/src/muz/ddnf/doc.cpp +++ b/src/muz/ddnf/doc.cpp @@ -34,35 +34,38 @@ void doc_manager::reset() { // m.reset(); - not until docs are in small object allocator. } doc* doc_manager::allocate() { - return alloc(doc, m.allocate()); + return allocate(m.allocate()); } doc* doc_manager::allocate1() { - return alloc(doc, m.allocate1()); + return allocate(m.allocate1()); } doc* doc_manager::allocate0() { - return alloc(doc, m.allocate0()); + return allocate(m.allocate0()); } doc* doc_manager::allocateX() { - return alloc(doc, m.allocateX()); + return allocate(m.allocateX()); } doc* doc_manager::allocate(doc const& src) { - doc* r = alloc(doc, m.allocate(src.pos())); + doc* r = allocate(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(tbv const& src) { + return allocate(m.allocate(src)); +} doc* doc_manager::allocate(uint64 n) { - return alloc(doc, m.allocate(n)); + return allocate(m.allocate(n)); } doc* doc_manager::allocate(rational const& r) { - return alloc(doc, m.allocate(r)); + return allocate(m.allocate(r)); } doc* doc_manager::allocate(uint64 n, unsigned hi, unsigned lo) { - return alloc(doc, m.allocate(n, hi, lo)); + return allocate(m.allocate(n, hi, lo)); } doc* doc_manager::allocate(doc const& src, unsigned const* permutation) { - doc* r = alloc(doc, m.allocate(src.pos(), permutation)); + doc* r = allocate(m.allocate(src.pos(), permutation)); for (unsigned i = 0; i < src.neg().size(); ++i) { r->neg().push_back(m.allocate(src.neg()[i], permutation)); } @@ -252,143 +255,141 @@ bool doc_manager::merge(doc& d, unsigned idx, subset_ints& equalities, bit_vecto return true; } -doc* doc_manager::project(unsigned n, bool const* to_delete, doc const& src) { - tbv* p = tbvm().project(n, to_delete, src.pos()); +// +// 1. If n = 0,1: can project directly. +// 2. If tbv_i uses X in all positions with vars or constant where tbv is constant: can project directly. +// 3. Perform resolution on remaining tbv_i +// +// tbv & ~tbv1 & ~tbv2 & .. & ~tbv_n +// Semantics of ~tbv1 is that it is a clause of literals. +// indices where BIT_1 is set are negative. +// indices where BIT_0 is set are positive. +// + +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())); + if (src.neg().is_empty()) { - // build doc from p. - return 0; + return r; } - NOT_IMPLEMENTED_YET(); + if (src.neg().size() == 1) { + r->neg().push_back(dstt.project(n, to_delete, src.neg()[0])); + return r; + } + + // + // All negations can be projected if they are sign compatible. + // + tbv_ref bits(tbvm(), tbvm().allocateX()); + for (unsigned i = 0; i < src.neg().size(); ++i) { + tbvm().set_and(*bits, src.neg()[i]); + } + bool can_project_all = true; + for (unsigned i = 0; can_project_all && i < n; ++i) { + can_project_all = !to_delete[i] || (*bits)[i] != BIT_z; + } + if (can_project_all) { + for (unsigned i = 0; i < src.neg().size(); ++i) { + r->neg().push_back(dstt.project(n, to_delete, src.neg()[i])); + } + return r; + } + + // + // A negation can be projected directly if it does not constrain + // deleted variables. + // ptr_vector todo; -#if 0 - // tbv & ~tbv1 & ~tbv2 & .. - // Semantics of ~tbv1 is that it is a clause of literals. - // indices where BIT_1 is set are negative. - // indices where BIT_0 is set are positive. - // The first loop is supposed to project tbv_i directly - // when some safety condition is met. - // The second loop handles the remaining tbv_i that - // don't meet the safety condition. - for (unsigned i = 0; i < src.neg().size(); ++i) { - if (can_project_neg(n, to_delete, src.neg()[i])) { - + for (unsigned i = 0; i < src.neg().size(); ++i) { + if (can_project_neg(src.pos(), n, to_delete, src.neg()[i])) { + r->neg().push_back(dstt.project(n, to_delete, src.neg()[i])); + } + else { + todo.push_back(tbvm().allocate(src.neg()[i])); } } -#endif -#if 0 - // REVIEW: what is the spec for this code? - ternary_diff_bitvector TBV(*this); - if (!TBV.fold_neg()) - return false; - - std::set todo; - cpy_bits_t cpy_bits; - ternary_bitvector newneg; - for (union_ternary_bitvector::iterator I = TBV.m_neg.begin(), - E = TBV.m_neg.end(); I != E; ++I) { - // check if subtract TBV should be skiped - for (unsigned i = 0; i < delcols.size()-1; ++i) { - unsigned idx = delcols[i]; - if (I->get(idx) != TBV.m_pos.get(idx)) { // xx \ 1x - if (analyze_copy_bit(TBV.m_pos, *I, delcols, cpy_bits)) - todo.insert(&*I); - goto skip_row; - } - } - - newneg.reset(); - I->project(delcols, new_size, newneg); - result.m_neg.add_fact(newneg); - skip_row: ; + if (todo.empty()) { + return r; } - - if (!todo.empty()) { - for (std::set::iterator I = todo.begin(), - E = todo.end(); I != E; ++I) { - for (unsigned i = 0; i < delcols.size()-1; ++i) { - unsigned idx = delcols[i]; - if ((*I)->get(idx) != TBV.m_pos.get(idx)) { - cpy_bits_t::iterator II = cpy_bits.find(idx); - if (II == cpy_bits.end()) - goto skip_bv; - - unsigned idx_keep = II->second.first; - unsigned cpy_val = II->second.second; - - if (!((*I)->get(idx) & cpy_val) || (*I)->get(idx_keep) != BIT_x) - goto skip_bv; - - (*I)->set(idx_keep, (*I)->get(idx)); + ptr_vector pos, neg, new_todo; + tbv_ref t1(tbvm()), t2(tbvm()); + for (unsigned i = 0; i < n; ++i) { + if (to_delete[i] && (*bits)[i] == BIT_z) { + new_todo.reset(); + for (unsigned j = 0; j < todo.size(); ++j) { + tbv& t = *todo[j]; + switch(t[i]) { + case BIT_x: new_todo.push_back(&t); break; + case BIT_0: pos.push_back(&t); break; + case BIT_1: neg.push_back(&t); break; + default: UNREACHABLE(); break; } } - - newneg.reset(); - (*I)->project(delcols, new_size, newneg); - result.m_neg.add_fact(newneg); - skip_bv: ; + if (pos.empty() || neg.empty()) { + continue; + } + for (unsigned j = 0; j < pos.size(); ++j) { + t1 = tbvm().allocate(*pos[j]); + (*t1).set(i, BIT_x); + for (unsigned k = 0; k < neg.size(); ++k) { + if (tbvm().set_and(*t1, *neg[k])) { + new_todo.push_back(t1.detach()); + t1 = tbvm().allocate(*pos[j]); + (*t1).set(i, BIT_x); + } + } + } + for (unsigned i = 0; i < pos.size(); ++i) { + tbvm().deallocate(pos[i]); + } + for (unsigned i = 0; i < neg.size(); ++i) { + tbvm().deallocate(neg[i]); + } + std::swap(todo, new_todo); } } - - return !result.is_empty(); - - - // idx_del -> - // val -> BIT_* - typedef std::map > cpy_bits_t; - - static bool analyze_copy_bit(const ternary_bitvector& pos, const ternary_bitvector& neg, - const unsigned_vector& delcols, cpy_bits_t& cpy_bits) { - unsigned *del = delcols.c_ptr(); - bool got_del_col = false, got_keep_col = false; - unsigned del_col = 0, keep_col = 0; - - for (unsigned i = 0; i < pos.size(); ++i) { - if (pos.get(i) != neg.get(i)) { - if (*del == i) { - if (got_del_col) - return true; - del_col = i; - got_del_col = true; - } else { - if (got_keep_col) - return true; - keep_col = i; - got_keep_col = true; - } - } - - if (i == *del) - ++del; - } - - if (!got_del_col || !got_keep_col) - return true; - if (neg.get(keep_col) == neg.get(del_col)) - return false; - - - unsigned char val = neg.get(del_col); - cpy_bits_t::iterator I = cpy_bits.find(del_col); - if (I == cpy_bits.end()) - cpy_bits[del_col] = std::make_pair(keep_col, val); - else { - // FIXME: eq classes with size > 1 not supported for now - SASSERT(I->second.first == keep_col); - I->second.second |= val; - } - - return false; + for (unsigned i = 0; i < todo.size(); ++i) { + r->neg().push_back(dstt.project(n, to_delete, *todo[i])); + tbvm().deallocate(todo[i]); } - -#endif - return 0; + return r; } +bool doc_manager::can_project_neg(tbv const& pos, unsigned n, bool const* to_delete, tbv const& neg) { + for (unsigned i = 0; i < n; ++i) { + if (to_delete[i] && BIT_x != neg[i] && BIT_x == pos[i]) return false; + } + return true; +} + + void doc_manager::complement(doc const& src, ptr_vector& result) { - NOT_IMPLEMENTED_YET(); + result.reset(); + if (is_full(src)) { + return; + } + doc* r = allocateX(); + r->neg().push_back(m.allocate(src.pos())); + result.push_back(r); + for (unsigned i = 0; i < src.neg().size(); ++i) { + result.push_back(allocate(src.neg()[i])); + } } void doc_manager::subtract(doc const& A, doc const& B, ptr_vector& result) { - NOT_IMPLEMENTED_YET(); + doc_ref r(*this), r2(*this); + r = allocate(A); + if (r->neg().insert(m, m.allocate(B.pos()))) { + result.push_back(r.detach()); + r = allocate(A); + } + for (unsigned i = 0; i < B.neg().size(); ++i) { + r2 = allocate(B.neg()[i]); + if (set_and(*r, *r2)) { + result.push_back(r.detach()); + r = allocate(A); + } + } } bool doc_manager::equals(doc const& a, doc const& b) const { if (!m.equals(a.pos(), b.pos())) return false; diff --git a/src/muz/ddnf/doc.h b/src/muz/ddnf/doc.h index 7ee9a2db8..107720a23 100644 --- a/src/muz/ddnf/doc.h +++ b/src/muz/ddnf/doc.h @@ -44,6 +44,8 @@ public: doc* allocate0(); doc* allocateX(); doc* allocate(doc const& src); + doc* allocate(tbv const& src); + doc* allocate(tbv * src); doc* allocate(uint64 n); doc* allocate(rational const& r); doc* allocate(uint64 n, unsigned hi, unsigned lo); @@ -65,13 +67,14 @@ public: bool contains(doc const& a, doc const& b) const; std::ostream& display(std::ostream& out, doc const& b) const; unsigned num_tbits() const { return m.num_tbits(); } - doc* project(unsigned n, bool const* to_delete, doc const& src); + doc* project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src); bool well_formed(doc const& d) const; bool merge(doc& d, unsigned lo, unsigned length, subset_ints& equalities, bit_vector const& discard_cols); void set(doc& d, unsigned idx, tbit value); private: unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index); bool merge(doc& d, unsigned idx, subset_ints& equalities, bit_vector const& discard_cols); + bool can_project_neg(tbv const& pos, unsigned n, bool const* to_delete, tbv const& neg); }; @@ -293,6 +296,7 @@ public: } doc& operator*() { return *d; } doc* operator->() { return d; } + doc* detach() { doc* r = d; d = 0; return r; } }; #endif /* _DOC_H_ */