/dports/math/z3/z3-z3-4.8.13/src/muz/rel/ |
H A D | doc.h | 92 …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 D | udoc_relation.h | 69 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 D | udoc_relation.cpp | 731 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 D | doc.cpp | 214 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 D | doc.h | 92 …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 D | udoc_relation.h | 69 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 D | udoc_relation.cpp | 732 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 D | doc.cpp | 214 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 D | doc.cpp | 304 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 D | doc.cpp | 304 bit_vector discard_cols; 305 discard_cols.resize(N, false); 325 if (dm.merge(*d, lo, 1, equalities, discard_cols)) {
|