Lines Matching refs:neg
52 for (unsigned i = 0; i < src.neg().size(); ++i) { in allocate()
53 r->neg().push_back(m.allocate(src.neg()[i])); in allocate()
76 for (unsigned i = 0; i < src.neg().size(); ++i) { in allocate()
77 r->neg().push_back(m.allocate(src.neg()[i], permutation)); in allocate()
84 src->neg().reset(m); in deallocate()
90 dst.neg().reset(m); in copy()
91 for (unsigned i = 0; i < src.neg().size(); ++i) { in copy()
92 dst.neg().push_back(m.allocate(src.neg()[i])); in copy()
96 src.neg().reset(m); in fill0()
101 src.neg().reset(m); in fill1()
106 src.neg().reset(m); in fillX()
113 + d.neg().get_size_estimate_bytes(m) in get_size_estimate_bytes()
120 dst.neg().intersect(m, dst.pos()); in set_and()
122 for (unsigned i = 0; i < src.neg().size(); ++i) { in set_and()
123 t = m.allocate(src.neg()[i]); in set_and()
125 dst.neg().insert(m, t.detach()); in set_and()
133 dst.neg().intersect(m, src); in set_and()
139 for (unsigned i = 0; i < d.neg().size(); ++i) { in well_formed()
140 if (!m.is_well_formed(d.neg()[i])) return false; in well_formed()
141 if (!m.contains(d.pos(), d.neg()[i])) return false; in well_formed()
148 for (unsigned i = 0; i < dst.neg().size(); ++i) { in fold_neg()
149 if (m.contains(dst.neg()[i], dst.pos())) in fold_neg()
153 unsigned count = diff_by_012(dst.pos(), dst.neg()[i], index); in fold_neg()
159 dst.neg().erase(tbvm(), i); in fold_neg()
163 m.set(dst.pos(), index, neg(dst.neg()[i][index])); in fold_neg()
164 dst.neg().intersect(tbvm(), dst.pos()); in fold_neg()
173 unsigned doc_manager::diff_by_012(tbv const& pos, tbv const& neg, unsigned& index) { in diff_by_012() argument
178 tbit b2 = neg[i]; in diff_by_012()
196 for (unsigned i = 0; i < d.neg().size(); ++i) { in set()
197 tbit b = d.neg()[i][idx]; in set()
199 d.neg().erase(tbvm(), i); in set()
203 m.set(d.neg()[i], idx, value); in set()
267 if (!d.neg().is_empty()) { in merge()
270 for (unsigned i = 0; all_x && i < d.neg().size(); ++i) { in merge()
271 all_x = (BIT_x == d.neg()[i][idx]); in merge()
283 d.neg().insert(tbvm(), t); in merge()
287 d.neg().insert(tbvm(), t); in merge()
319 if (src.neg().is_empty()) { in project()
328 for (unsigned i = 0; i < src.neg().size(); ++i) { in project()
329 todo.push_back(tbvm().allocate(src.neg()[i])); in project()
337 r->neg().push_back(t.detach()); in project()
358 utbv pos, neg; in project() local
363 case BIT_0: neg.push_back(&tx); break; in project()
374 for (unsigned i = 0; i < neg.size(); ++i) { in project()
375 tbvm().display(tout, neg[i]) << " "; in project()
379 SASSERT(pos.size() > 0 && neg.size() > 0); in project()
382 for (unsigned k = 0; k < neg.size(); ++k) { in project()
385 if (tbvm().set_and(*t1, neg[k])) { in project()
392 neg.reset(m); in project()
401 r->neg().reset(dstt); in project()
402 r->neg().push_back(t.detach()); in project()
405 if (r->neg().size() > 0 && dstt.equals(r->neg()[0], *t)) { in project()
408 r->neg().push_back(t.detach()); in project()
427 utbv& neg = d->neg(); in join() local
467 neg.push_back(t.detach()); in join()
471 neg.push_back(t.detach()); in join()
477 for (unsigned i = 0; i < d1.neg().size(); ++i) { in join()
479 m.set(*t, d1.neg()[i], mid - 1, 0); in join()
481 neg.push_back(t.detach()); in join()
484 for (unsigned i = 0; i < d2.neg().size(); ++i) { in join()
486 m.set(*t, d2.neg()[i], hi - 1, mid); in join()
488 neg.push_back(t.detach()); in join()
498 tbv const& pos, tbv_vector const& neg, bit_vector const& to_delete, unsigned& idx) { in pick_resolvent() argument
499 if (neg.empty()) return project_done; in pick_resolvent()
500 for (unsigned j = 0; j < neg.size(); ++j) { in pick_resolvent()
501 if (m.equals(pos, *neg[j])) return project_is_empty; in pick_resolvent()
511 tbit b1 = (*neg[0])[i]; in pick_resolvent()
515 for (unsigned j = 1; j < neg.size(); ++j) { in pick_resolvent()
516 tbit b2 = (*neg[j])[i]; in pick_resolvent()
565 r->neg().push_back(m.allocate(src.pos())); in complement()
567 for (unsigned i = 0; i < src.neg().size(); ++i) { in complement()
568 result.push_back(allocate(src.neg()[i])); in complement()
580 r->neg().insert(m, t.detach()); in subtract()
585 for (unsigned i = 0; i < B.neg().size(); ++i) { in subtract()
587 if (set_and(*r, B.neg()[i])) { in subtract()
594 if (a.neg().size() != b.neg().size()) return false; in equals()
595 for (unsigned i = 0; i < a.neg().size(); ++i) { in equals()
596 if (!m.equals(a.neg()[i], b.neg()[i])) return false; in equals()
601 return src.neg().is_empty() && m.equals(src.pos(), *m_full); in is_full()
604 if (src.neg().size() == 0) return false; in is_empty_complete()
620 for (unsigned i = 0; i < src.neg().size(); ++i) { in hash()
621 r = 2*r + m.hash(src.neg()[i]); in hash()
633 for (unsigned i = 0; i < a.neg().size(); ++i) { in contains()
635 for (unsigned j = 0; !found && j < b.neg().size(); ++j) { in contains()
636 found = m.contains(b.neg()[j],a.neg()[i]); in contains()
648 for (unsigned i = 0; i < a.neg().size(); ++i) { in contains()
650 for (unsigned j = 0; !found && j < b.neg().size(); ++j) { in contains()
651 found = m.contains(b.neg()[j], colsb, a.neg()[i], colsa); in contains()
665 if (b.neg().is_empty()) return out; in display()
667 b.neg().display(m, out, hi, lo); in display()
702 for (unsigned i = 0; i < src.neg().size(); ++i) { in to_formula()
703 conj.push_back(m.mk_not(tbvm().to_formula(m, src.neg()[i]))); in to_formula()