Home
last modified time | relevance | path

Searched refs:mk_join (Results 1 – 25 of 100) sorted by relevance

1234

/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dold_interval.cpp257 …m_lower_dep = m_lower.is_infinite() ? nullptr : m_manager.mk_join(m_lower_dep, other.m_lower_dep… in operator +=()
258 …m_upper_dep = m_upper.is_infinite() ? nullptr : m_manager.mk_join(m_upper_dep, other.m_upper_dep… in operator +=()
277 return m_manager.mk_join(m_manager.mk_join(d1, d2), m_manager.mk_join(d3,d4)); in join()
304 m_lower_dep = m_manager.mk_join(m_lower_dep, m_upper_dep); in operator *=()
535 m_lower_dep = m_manager.mk_join(m_lower_dep, m_upper_dep); in inv()
558 m_upper_dep = m_manager.mk_join(m_lower_dep, m_upper_dep); in inv()
612 … m_upper_dep = m_upper.is_infinite() ? nullptr : m_manager.mk_join(m_lower_dep, m_upper_dep); in expt()
623 … m_upper_dep = m_upper.is_infinite() ? nullptr : m_manager.mk_join(m_lower_dep, m_upper_dep); in expt()
636 … m_upper_dep = m_upper.is_infinite() ? nullptr : m_manager.mk_join(m_lower_dep, m_upper_dep); in expt()
H A Dold_interval.h72 v_dependency * join(v_dependency * d1, v_dependency * d2) { return m_manager.mk_join(d1, d2); } in join()
73 … * d1, v_dependency * d2, v_dependency * d3) { return m_manager.mk_join(m_manager.mk_join(d1, d2),… in join()
H A Dtheory_seq.cpp150 d = m_dm.mk_join(d, value.d); in find_rec()
159 d = m_dm.mk_join(d, value.d); in find1()
173 d = m_dm.mk_join(d, value.d); in find()
1023 deps = mk_join(deps, lits); in reduce_length_eq()
1036 deps = mk_join(deps, lits); in reduce_length_eq()
1372 dep = m_dm.mk_join(dep, c1->m_dep); in explain_eq()
1376 dep = m_dm.mk_join(dep, c2->m_dep); in explain_eq()
2468 eqs = m_dm.mk_join(eqs, ed.d); in try_expand()
2574 eqs = m_dm.mk_join(eqs, deps); in expand1()
2894 deps = mk_join(deps, l); in mk_join()
[all …]
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dold_interval.cpp257 …m_lower_dep = m_lower.is_infinite() ? nullptr : m_manager.mk_join(m_lower_dep, other.m_lower_dep… in operator +=()
258 …m_upper_dep = m_upper.is_infinite() ? nullptr : m_manager.mk_join(m_upper_dep, other.m_upper_dep… in operator +=()
277 return m_manager.mk_join(m_manager.mk_join(d1, d2), m_manager.mk_join(d3,d4)); in join()
304 m_lower_dep = m_manager.mk_join(m_lower_dep, m_upper_dep); in operator *=()
535 m_lower_dep = m_manager.mk_join(m_lower_dep, m_upper_dep); in inv()
558 m_upper_dep = m_manager.mk_join(m_lower_dep, m_upper_dep); in inv()
612 … m_upper_dep = m_upper.is_infinite() ? nullptr : m_manager.mk_join(m_lower_dep, m_upper_dep); in expt()
623 … m_upper_dep = m_upper.is_infinite() ? nullptr : m_manager.mk_join(m_lower_dep, m_upper_dep); in expt()
636 … m_upper_dep = m_upper.is_infinite() ? nullptr : m_manager.mk_join(m_lower_dep, m_upper_dep); in expt()
H A Dold_interval.h72 v_dependency * join(v_dependency * d1, v_dependency * d2) { return m_manager.mk_join(d1, d2); } in join()
73 … * d1, v_dependency * d2, v_dependency * d3) { return m_manager.mk_join(m_manager.mk_join(d1, d2),… in join()
H A Dtheory_seq.cpp150 d = m_dm.mk_join(d, value.d); in find_rec()
159 d = m_dm.mk_join(d, value.d); in find1()
173 d = m_dm.mk_join(d, value.d); in find()
1054 deps = mk_join(deps, lits); in reduce_length_eq()
1067 deps = mk_join(deps, lits); in reduce_length_eq()
1432 dep = m_dm.mk_join(dep, c1->m_dep); in explain_eq()
1436 dep = m_dm.mk_join(dep, c2->m_dep); in explain_eq()
2408 eqs = m_dm.mk_join(eqs, ed.d); in try_expand()
2514 eqs = m_dm.mk_join(eqs, deps); in expand1()
2837 deps = mk_join(deps, l); in mk_join()
[all …]
/dports/math/z3/z3-z3-4.8.13/src/math/interval/
H A Ddep_intervals.h115 dep = m_dep_manager.mk_join(dep, a.m_lower_dep); in mk_dependency()
118 dep = m_dep_manager.mk_join(dep, b.m_lower_dep); in mk_dependency()
121 dep = m_dep_manager.mk_join(dep, a.m_upper_dep); in mk_dependency()
124 dep = m_dep_manager.mk_join(dep, b.m_upper_dep); in mk_dependency()
132 dep = m_dep_manager.mk_join(dep, a.m_lower_dep); in mk_dependency()
135 dep = m_dep_manager.mk_join(dep, a.m_upper_dep); in mk_dependency()
155 u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_manager.mk_join(a, b); } in mk_join() function
316 dep = m_dep_manager.mk_join(dep, i.m_lower_dep); in check_interval_for_conflict_on_zero_lower()
327 dep = m_dep_manager.mk_join(dep, i.m_upper_dep); in check_interval_for_conflict_on_zero_upper()
H A Ddep_intervals.cpp54 a.m_lower_dep = mk_join(a.m_lower_dep, a.m_upper_dep); in set_zero_interval_deps_for_mult()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/interval/
H A Ddep_intervals.h115 dep = m_dep_manager.mk_join(dep, a.m_lower_dep); in mk_dependency()
118 dep = m_dep_manager.mk_join(dep, b.m_lower_dep); in mk_dependency()
121 dep = m_dep_manager.mk_join(dep, a.m_upper_dep); in mk_dependency()
124 dep = m_dep_manager.mk_join(dep, b.m_upper_dep); in mk_dependency()
132 dep = m_dep_manager.mk_join(dep, a.m_lower_dep); in mk_dependency()
135 dep = m_dep_manager.mk_join(dep, a.m_upper_dep); in mk_dependency()
155 u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_manager.mk_join(a, b); } in mk_join() function
316 dep = m_dep_manager.mk_join(dep, i.m_lower_dep); in check_interval_for_conflict_on_zero_lower()
327 dep = m_dep_manager.mk_join(dep, i.m_upper_dep); in check_interval_for_conflict_on_zero_upper()
H A Ddep_intervals.cpp54 a.m_lower_dep = mk_join(a.m_lower_dep, a.m_upper_dep); in set_zero_interval_deps_for_mult()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/
H A Ddependency_converter.cpp54 return expr_dependency_ref(m.mk_join(d1, d2), m); in operator ()()
80 if (dc) result = m.mk_join(result, (*dc)()); in operator ()()
/dports/math/z3/z3-z3-4.8.13/src/tactic/
H A Ddependency_converter.cpp54 return expr_dependency_ref(m.mk_join(d1, d2), m); in operator ()()
80 if (dc) result = m.mk_join(result, (*dc)()); in operator ()()
/dports/math/z3/z3-z3-4.8.13/src/util/
H A Ddependency.h149 dependency * mk_join(dependency * d1, dependency * d2) { in mk_join() function
295 dependency * mk_join(dependency * d1, dependency * d2) { in mk_join() function
296 return m_dep_manager.mk_join(d1, d2); in mk_join()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/util/
H A Ddependency.h149 dependency * mk_join(dependency * d1, dependency * d2) { in mk_join() function
295 dependency * mk_join(dependency * d1, dependency * d2) { in mk_join() function
296 return m_dep_manager.mk_join(d1, d2); in mk_join()
/dports/math/z3/z3-z3-4.8.13/src/math/lp/
H A Dnla_intervals.h39 … u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_intervals.mk_join(a, b); } in mk_join() function
H A Dnla_common.cpp66 dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(lc)); in add_deps_of_fixed()
67 dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(uc)); in add_deps_of_fixed()
H A Dnla_intervals.cpp205 a.m_lower_dep = mk_join(a.m_lower_dep, a.m_upper_dep); in set_zero_interval_deps_for_mult()
219 r = m_dep_intervals.mk_join(r, m_dep_intervals.mk_leaf(p.ci())); in mk_dep()
288 i.get().m_lower_dep = mk_join(i.get().m_lower_dep, mk_leaf(p.ci())); in interval_from_term()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/lp/
H A Dnla_intervals.h39 … u_dependency* mk_join(u_dependency* a, u_dependency* b) { return m_dep_intervals.mk_join(a, b); } in mk_join() function
H A Dnla_common.cpp66 dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(lc)); in add_deps_of_fixed()
67 dep = dep_manager.mk_join(dep, dep_manager.mk_leaf(uc)); in add_deps_of_fixed()
H A Dnla_intervals.cpp205 a.m_lower_dep = mk_join(a.m_lower_dep, a.m_upper_dep); in set_zero_interval_deps_for_mult()
219 r = m_dep_intervals.mk_join(r, m_dep_intervals.mk_leaf(p.ci())); in mk_dep()
288 i.get().m_lower_dep = mk_join(i.get().m_lower_dep, mk_leaf(p.ci())); in interval_from_term()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/math/grobner/
H A Dpdd_solver.cpp237 dst = m_dep_manager.mk_join(dst.dep(), src.dep()); in try_simplify_using()
255 dst = m_dep_manager.mk_join(dst.dep(), src.dep()); in simplify_using()
271 add(r, m_dep_manager.mk_join(eq1.dep(), eq2.dep())); in superpose()
/dports/math/z3/z3-z3-4.8.13/src/math/grobner/
H A Dpdd_solver.cpp237 dst = m_dep_manager.mk_join(dst.dep(), src.dep()); in try_simplify_using()
255 dst = m_dep_manager.mk_join(dst.dep(), src.dep()); in simplify_using()
271 add(r, m_dep_manager.mk_join(eq1.dep(), eq2.dep())); in superpose()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/tactic/arith/
H A Dlia2pb_tactic.cpp254 dep = m.mk_join(m_bm.lower_dep(x), m_bm.upper_dep(x));
278 dep = m.mk_join(m_rw.get_used_dependencies(), g->dep(idx)); in proto_register_gelf()
/dports/math/z3/z3-z3-4.8.13/src/tactic/arith/
H A Dlia2pb_tactic.cpp254 dep = m.mk_join(m_bm.lower_dep(x), m_bm.upper_dep(x)); in operator ()()
278 dep = m.mk_join(m_rw.get_used_dependencies(), g->dep(idx)); in operator ()()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/ast/rewriter/
H A Dexpr_replacer.cpp69 m_used_dependencies = m.mk_join(m_used_dependencies, d); in get_subst()

1234