mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 12:48:53 +00:00
Code Activity

enable interval multiplication without dependencies

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-17 10:21:41 -10:00
parent 0535e24dd1
commit 3b61f0b874
2 changed files with 13 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/lp/nla_intervals.cpp
View file

@ -438,7 +438,8 @@ interv intervals::interval_of_mul(const nex_mul& e) {
const nex* zero_interval_child = get_zero_interval_child(e); const nex* zero_interval_child = get_zero_interval_child(e);
if (zero_interval_child) { if (zero_interval_child) {
interv a = interval_of_expr<wd>(zero_interval_child, 1); interv a = interval_of_expr<wd>(zero_interval_child, 1);
set_zero_interval_deps_for_mult(a); if(wd == with_deps)
set_zero_interval_deps_for_mult(a);
TRACE("nla_intervals_details", tout << "zero_interval_child = " << *zero_interval_child << std::endl << "a = "; display(tout, a); ); TRACE("nla_intervals_details", tout << "zero_interval_child = " << *zero_interval_child << std::endl << "a = "; display(tout, a); );
return a; return a;
} }
@ -450,10 +451,14 @@ interv intervals::interval_of_mul(const nex_mul& e) {
interv b = interval_of_expr<wd>(ep.e(), ep.pow()); interv b = interval_of_expr<wd>(ep.e(), ep.pow());
TRACE("nla_intervals_details", tout << "ep = " << ep << ", "; display(tout, b); ); TRACE("nla_intervals_details", tout << "ep = " << ep << ", "; display(tout, b); );
interv c; interv c;
interval_deps_combine_rule comb_rule; if (wd == with_deps) {
mul_two_intervals(a, b, c, comb_rule); interval_deps_combine_rule comb_rule;
TRACE("nla_intervals_details", tout << "c before combine_deps() "; display(tout, c);); mul_two_intervals(a, b, c, comb_rule);
combine_deps(a, b, comb_rule, c); TRACE("nla_intervals_details", tout << "c before combine_deps() "; display(tout, c););
combine_deps(a, b, comb_rule, c);
} else {
mul_two_intervals(a, b, c);
}
TRACE("nla_intervals_details", tout << "a "; display(tout, a);); TRACE("nla_intervals_details", tout << "a "; display(tout, a););
TRACE("nla_intervals_details", tout << "c "; display(tout, c);); TRACE("nla_intervals_details", tout << "c "; display(tout, c););
set<wd>(a, c); set<wd>(a, c);

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

@ -217,6 +217,9 @@ public:
void mul_two_intervals(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); } void mul_two_intervals(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); }
void mul_two_intervals(const interval& a, const interval& b, interval& c) { m_imanager.mul(a, b, c); }
void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const { void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {
SASSERT(&a != &i && &b != &i); SASSERT(&a != &i && &b != &i);
m_config.add_deps(a, b, deps, i); m_config.add_deps(a, b, deps, i);