mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

calculate power of intervals with depenencies

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-10-15 10:24:50 -07:00
parent dd4dc1ad14
commit 4daa841116
2 changed files with 26 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/horner.cpp
View file

@ -148,8 +148,10 @@ interv horner::power_with_deps(const interv& a, unsigned n) {
interv b;
interval_deps_combine_rule combine_rule;
m_intervals.power(a, n, b, combine_rule);
m_intervals.combine_deps(a, combine_rule, b);
TRACE("nla_horner_details", tout << "power of "; m_intervals.display(tout, a) << " = ";
m_intervals.display(tout, b) << "\n";);
m_intervals.display(tout, b) << "\n"; );
return b;
}

23
src/math/lp/nla_intervals.h
View file

@ -60,6 +60,12 @@ class intervals : common {
i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_combine);
}
void add_deps(interval const& a,
interval_deps_combine_rule const& deps, interval& i) const {
i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, deps.m_lower_combine);
i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, deps.m_upper_combine);
}
// Should be NOOPs for precise mpq types.
// For imprecise types (e.g., floats) it should set the rounding mode.
@ -114,6 +120,18 @@ class intervals : common {
}
return dep;
}
ci_dependency* mk_dependency(interval const& a, deps_combine_rule bd) const {
ci_dependency* dep = nullptr;
if (dep_in_lower1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_lower_dep);
}
if (dep_in_upper1(bd)) {
dep = m_dep_manager.mk_join(dep, a.m_upper_dep);
}
return dep;
}
};
region m_alloc;
@ -197,6 +215,11 @@ public:
m_config.add_deps(a, b, deps, i);
}
void combine_deps(interval const& a, interval_deps_combine_rule const& deps, interval& i) const {
SASSERT(&a != &i);
m_config.add_deps(a, deps, i);
}
void power(interval const & a, unsigned n, interval & b, interval_deps_combine_rule & b_deps) {
m_imanager.power(a, n, b, b_deps);
}