Searched refs:dep_in_lower1 (Results 1 – 6 of 6) sorted by relevance
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/math/interval/ |
| H A D | interval.h | 88 inline bool dep_in_lower1(deps_combine_rule d) { return (d & DEP_IN_LOWER1) != 0; } in dep_in_lower1() function
95 SASSERT(dep_in_lower1(d) == dep_in_lower2(r)); in dep1_to_dep2()
97 SASSERT(!dep_in_lower1(r) && !dep_in_upper1(r)); in dep1_to_dep2()
|
| H A D | dep_intervals.h | 114 if (dep_in_lower1(bd)) { in mk_dependency()
131 if (dep_in_lower1(bd)) { in mk_dependency()
|
| /dports/math/z3/z3-z3-4.8.13/src/math/interval/ |
| H A D | interval.h | 88 inline bool dep_in_lower1(deps_combine_rule d) { return (d & DEP_IN_LOWER1) != 0; } in dep_in_lower1() function
95 SASSERT(dep_in_lower1(d) == dep_in_lower2(r)); in dep1_to_dep2()
97 SASSERT(!dep_in_lower1(r) && !dep_in_upper1(r)); in dep1_to_dep2()
|
| H A D | dep_intervals.h | 114 if (dep_in_lower1(bd)) { in mk_dependency()
131 if (dep_in_lower1(bd)) { in mk_dependency()
|
| /dports/math/z3/z3-z3-4.8.13/src/test/ |
| H A D | interval.cpp | 218 …assert_hyp(out, nm, "a", a, dep_in_lower1(deps.m_lower_combine), dep_in_upper1(deps.m_lower_combin… in display_lemmas()
226 …assert_hyp(out, nm, "a", a, dep_in_lower1(deps.m_upper_combine), dep_in_upper1(deps.m_upper_combin… in display_lemmas()
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/test/ |
| H A D | interval.cpp | 218 …assert_hyp(out, nm, "a", a, dep_in_lower1(deps.m_lower_combine), dep_in_upper1(deps.m_lower_combin… in display_lemmas()
226 …assert_hyp(out, nm, "a", a, dep_in_lower1(deps.m_upper_combine), dep_in_upper1(deps.m_upper_combin… in display_lemmas()
|