From 3b61f0b874d404d3579b86f0b2603c2ed1694732 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 17 Dec 2019 10:21:41 -1000 Subject: [PATCH] enable interval multiplication without dependencies Signed-off-by: Lev Nachmanson --- src/math/lp/nla_intervals.cpp | 15 ++++++++++----- src/math/lp/nla_intervals.h | 3 +++ 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 4a0f7c4f9..c5b38b90d 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -438,7 +438,8 @@ interv intervals::interval_of_mul(const nex_mul& e) { const nex* zero_interval_child = get_zero_interval_child(e); if (zero_interval_child) { interv a = interval_of_expr(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); ); return a; } @@ -450,10 +451,14 @@ interv intervals::interval_of_mul(const nex_mul& e) { interv b = interval_of_expr(ep.e(), ep.pow()); TRACE("nla_intervals_details", tout << "ep = " << ep << ", "; display(tout, b); ); interv c; - interval_deps_combine_rule comb_rule; - mul_two_intervals(a, b, c, comb_rule); - TRACE("nla_intervals_details", tout << "c before combine_deps() "; display(tout, c);); - combine_deps(a, b, comb_rule, c); + if (wd == with_deps) { + interval_deps_combine_rule comb_rule; + mul_two_intervals(a, b, c, comb_rule); + 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 << "c "; display(tout, c);); set(a, c); diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 3bef696d8..4ac0540e3 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -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) { m_imanager.mul(a, b, c); } + + void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const { SASSERT(&a != &i && &b != &i); m_config.add_deps(a, b, deps, i);