Home
last modified time | relevance | path

Searched refs:discard_cols (Results 1 – 10 of 10) sorted by relevance

/dports/math/z3/z3-z3-4.8.13/src/muz/rel/
H A Ddoc.h92 …c& d, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols);
100 bool merge(doc& d, unsigned idx, subset_ints const& equalities, bit_vector const& discard_cols);
284 …& m, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols) { in merge() argument
288 if (!m.merge(*m_elems[i], lo, length, equalities, discard_cols)) { in merge()
299 void merge(M& m, unsigned lo1, unsigned lo2, unsigned length, bit_vector const& discard_cols) { in merge() argument
302 for (unsigned i = 0; i < discard_cols.size(); ++i) { in merge()
308 merge(m, lo1, length, equalities, discard_cols); in merge()
312 bit_vector const& discard_cols) { in merge() argument
314 merge(m, roots[i], 1, equalities, discard_cols); in merge()
H A Dudoc_relation.h69 void compile_guard(expr* g, udoc& result, bit_vector const& discard_cols) const;
74 …_guard(expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const;
76 bool apply_bv_eq(expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const;
H A Dudoc_relation.cpp731 for (unsigned i = 0, e = discard_cols.size(); i < e; ++i) { in compile_guard()
734 apply_guard(g, result, equalities, discard_cols); in compile_guard()
774 if (!apply_bv_eq(e, e3, discard_cols, result)) return false; in apply_bv_eq()
792 result.merge(dm, idx1, idx2, length, discard_cols); in apply_bv_eq()
837 empty.resize(discard_cols.size(), false); in apply_guard()
853 apply_guard(arg, sub, equalities, discard_cols); in apply_guard()
878 apply_guard(e1, diff1, equalities, discard_cols); in apply_guard()
879 apply_guard(f2, diff1, equalities, discard_cols); in apply_guard()
882 apply_guard(f1, diff2, equalities, discard_cols); in apply_guard()
883 apply_guard(e2, diff2, equalities, discard_cols); in apply_guard()
[all …]
H A Ddoc.cpp214 subset_ints const& equalities, bit_vector const& discard_cols) { in merge() argument
217 if (!merge(d, idx, equalities, discard_cols)) return false; in merge()
222 bit_vector const& discard_cols) { in merge() argument
240 if (!discard_cols.get(idx)) { in merge()
279 if ((!discard_cols.get(idx) || !all_x) && idx != root1) { in merge()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/muz/rel/
H A Ddoc.h92 …c& d, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols);
100 bool merge(doc& d, unsigned idx, subset_ints const& equalities, bit_vector const& discard_cols); in get_size_estimate_rows()
284 …& m, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols) {
288 if (!m.merge(*m_elems[i], lo, length, equalities, discard_cols)) {
299 void merge(M& m, unsigned lo1, unsigned lo2, unsigned length, bit_vector const& discard_cols) {
302 for (unsigned i = 0; i < discard_cols.size(); ++i) {
308 merge(m, lo1, length, equalities, discard_cols);
312 bit_vector const& discard_cols) {
314 merge(m, roots[i], 1, equalities, discard_cols);
H A Dudoc_relation.h69 void compile_guard(expr* g, udoc& result, bit_vector const& discard_cols) const;
74 …_guard(expr* g, udoc& result, subset_ints const& equalities, bit_vector const& discard_cols) const;
76 bool apply_bv_eq(expr* e1, expr* e2, bit_vector const& discard_cols, udoc& result) const;
H A Dudoc_relation.cpp732 for (unsigned i = 0, e = discard_cols.size(); i < e; ++i) { in compile_guard()
735 apply_guard(g, result, equalities, discard_cols); in compile_guard()
775 if (!apply_bv_eq(e, e3, discard_cols, result)) return false; in apply_bv_eq()
793 result.merge(dm, idx1, idx2, length, discard_cols); in apply_bv_eq()
838 empty.resize(discard_cols.size(), false); in apply_guard()
854 apply_guard(arg, sub, equalities, discard_cols); in apply_guard()
879 apply_guard(e1, diff1, equalities, discard_cols); in apply_guard()
880 apply_guard(f2, diff1, equalities, discard_cols); in apply_guard()
883 apply_guard(f1, diff2, equalities, discard_cols); in apply_guard()
884 apply_guard(e2, diff2, equalities, discard_cols); in apply_guard()
[all …]
H A Ddoc.cpp214 subset_ints const& equalities, bit_vector const& discard_cols) { in merge() argument
217 if (!merge(d, idx, equalities, discard_cols)) return false; in merge()
222 bit_vector const& discard_cols) { in merge() argument
240 if (!discard_cols.get(idx)) { in merge()
279 if ((!discard_cols.get(idx) || !all_x) && idx != root1) { in merge()
/dports/math/z3/z3-z3-4.8.13/src/test/
H A Ddoc.cpp304 bit_vector discard_cols; in test_merge() local
305 discard_cols.resize(N, false); in test_merge()
325 if (dm.merge(*d, lo, 1, equalities, discard_cols)) { in test_merge()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/test/
H A Ddoc.cpp304 bit_vector discard_cols;
305 discard_cols.resize(N, false);
325 if (dm.merge(*d, lo, 1, equalities, discard_cols)) {