From ccc9a77a1ff8c59ab529a23d90519ebbc8e43810 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 30 Jul 2019 10:48:24 -0700 Subject: [PATCH] Nikolaj's changes related to dependencies on infinite interval bounds Signed-off-by: Lev Nachmanson --- src/math/interval/interval.h | 5 +++++ src/math/lp/nla_intervals.cpp | 25 ------------------------- src/math/lp/nla_intervals.h | 14 +++++--------- 3 files changed, 10 insertions(+), 34 deletions(-) diff --git a/src/math/interval/interval.h b/src/math/interval/interval.h index a4d6def83..0b11569a4 100644 --- a/src/math/interval/interval.h +++ b/src/math/interval/interval.h @@ -43,6 +43,11 @@ public: unsigned m_upper_open:1; unsigned m_lower_inf:1; unsigned m_upper_inf:1; + interval(): + m_lower_open(false), + m_upper_open(false), + m_lower_inf(true), + m_upper_inf(true) {} }; // Should be NOOPs for precise numeral types. diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index e9d13bbbf..9a59c016b 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -4,31 +4,6 @@ #include "util/mpq.h" namespace nla { -void intervals::test_inf() { - interval a; // [1, inf) - m_config.set_lower(a, rational(1)); - m_config.set_lower_is_open(a, false); - m_config.set_upper_is_inf(a, true); - a.m_lower_dep = mk_dep(1); - - interval b; // [-1,-1] - m_config.set_lower(b, rational(-1)); - m_config.set_lower_is_open(b, false); - m_config.set_upper(b, rational(-1)); - m_config.set_upper_is_open(b, false); - - b.m_lower_dep = mk_dep(2); - b.m_upper_dep = mk_dep(4); - - interval_deps_combine_rule comb_rule; - interval c; - mul(a, b, c, comb_rule); - TRACE("nla_horner_test", tout << "c before combine_deps() "; display(tout, c);); - combine_deps(a, b, comb_rule, c); - SASSERT(lower_is_inf(c)); - SASSERT(!dep_in_upper1(comb_rule.m_lower_combine)); - -} void intervals::set_var_interval_with_deps(lpvar v, interval& b) { lp::constraint_index ci; rational val; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 0563a29b1..4761b92d5 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -73,11 +73,10 @@ class intervals : common { ci_dependency * m_upper_dep; // justification for the upper bound }; - void add_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const { - i.m_lower_dep = mk_dependency(a, b, deps.m_lower_combine); - i.m_upper_dep = mk_dependency(a, b, deps.m_upper_combine); + i.m_lower_dep = lower_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_lower_combine); + i.m_upper_dep = upper_is_inf(i) ? nullptr : mk_dependency(a, b, deps.m_upper_combine); } @@ -159,10 +158,7 @@ public: m_dep_manager(m_val_manager, m_alloc), m_config(m_num_manager, m_dep_manager), m_imanager(lim, im_config(m_num_manager, m_dep_manager)) - { - test_inf(); - } - void test_inf(); + {} interval mul(const svector&) const; void get_explanation_of_upper_bound_for_monomial(lpvar j, svector& expl) const; void get_explanation_of_lower_bound_for_monomial(lpvar j, svector& expl) const; @@ -180,8 +176,8 @@ public: void add(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.add(a, b, c, deps); } void set(interval& a, const interval& b) { m_imanager.set(a, b); - a.m_lower_dep = lower_is_inf(a)? nullptr : b.m_lower_dep; - a.m_upper_dep = upper_is_inf(a)?nullptr : b.m_upper_dep; + a.m_lower_dep = b.m_lower_dep; + a.m_upper_dep = b.m_upper_dep; } void mul(const interval& a, const interval& b, interval& c, interval_deps_combine_rule& deps) { m_imanager.mul(a, b, c, deps); } void combine_deps(interval const& a, interval const& b, interval_deps_combine_rule const& deps, interval& i) const {