From f22252112e68f5af12d461e3f3d939734c650b6f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 6 Jun 2019 10:17:42 -0700 Subject: [PATCH] remove lar_solver from nla_intervals fields Signed-off-by: Lev Nachmanson --- src/math/lp/nla_intervals.cpp | 188 +++++++++++++++++----------------- src/math/lp/nla_intervals.h | 8 +- src/math/lp/nla_solver.cpp | 2 +- 3 files changed, 99 insertions(+), 99 deletions(-) diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 8d325a14b..721b10c9e 100755 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -1,109 +1,110 @@ - - #include "math/lp/nla_core.h" #include "math/interval/interval_def.h" #include "math/lp/nla_intervals.h" namespace nla { - bool intervals::check() { - // m_region.reset(); - // for (auto const& m : m_core->emons()) { - // if (!check(m)) { - // return false; - // } - // } - // for (auto const& t : m_solver.terms()) { - // if (!check(*t)) { - // return false; - // } - // } +bool intervals::check() { + // m_region.reset(); + // for (auto const& m : m_core->emons()) { + // if (!check(m)) { + // return false; + // } + // } + // for (auto const& t : ls().terms()) { + // if (!check(*t)) { + // return false; + // } + // } + return true; +} + +bool intervals::check(monomial const& m) { + interval a, b, c, d; + m_imanager.set(a, rational(1).to_mpq()); + set_interval(m.var(), d); + if (m_imanager.lower_is_inf(d) && m_imanager.upper_is_inf(d)) { return true; } - - bool intervals::check(monomial const& m) { - interval a, b, c, d; - m_imanager.set(a, rational(1).to_mpq()); - set_interval(m.var(), d); - if (m_imanager.lower_is_inf(d) && m_imanager.upper_is_inf(d)) { + for (lpvar v : m.vars()) { + // TBD allow for division to get range of a + // m = a*b*c, where m and b*c are bounded, then interval for a is m/b*c + if (m_imanager.lower_is_inf(a) && m_imanager.upper_is_inf(a)) { return true; } - for (lpvar v : m.vars()) { - // TBD allow for division to get range of a - // m = a*b*c, where m and b*c are bounded, then interval for a is m/b*c - if (m_imanager.lower_is_inf(a) && m_imanager.upper_is_inf(a)) { - return true; - } - // TBD: deal with powers v^n interval instead of multiplying v*v .. * v - set_interval(v, b); - interval_deps deps; - m_imanager.mul(a, b, c, deps); - m_imanager.set(a, c); - m_config.set_deps(a, b, deps, a); - } - if (m_imanager.before(a, d)) { - svector cs; - m_dep_manager.linearize(a.m_upper_dep, cs); - m_dep_manager.linearize(d.m_lower_dep, cs); - for (auto ci : cs) { - //expl.push_justification(ci); - } - // TBD conflict - return false; - } - if (m_imanager.before(d, a)) { - svector cs; - m_dep_manager.linearize(a.m_lower_dep, cs); - m_dep_manager.linearize(d.m_upper_dep, cs); - for (auto ci : cs) { - //expl.push_justification(ci); - } - // TBD conflict - return false; - } - // could also perform bounds propagation: - // a has tighter lower/upper bound than m.var(), - // -> transfer bound to m.var() - // all but one variable has bound - // -> transfer bound to that variable using division - return true; + // TBD: deal with powers v^n interval instead of multiplying v*v .. * v + set_interval(v, b); + interval_deps deps; + m_imanager.mul(a, b, c, deps); + m_imanager.set(a, c); + m_config.set_deps(a, b, deps, a); } + if (m_imanager.before(a, d)) { + svector cs; + m_dep_manager.linearize(a.m_upper_dep, cs); + m_dep_manager.linearize(d.m_lower_dep, cs); + for (auto ci : cs) { + (void)ci; + SASSERT(false); + //expl.push_justification(ci); + } + // TBD conflict + return false; + } + if (m_imanager.before(d, a)) { + svector cs; + m_dep_manager.linearize(a.m_lower_dep, cs); + m_dep_manager.linearize(d.m_upper_dep, cs); + for (auto ci : cs) { + (void)ci; + SASSERT(false); //expl.push_justification(ci); + } + // TBD conflict + return false; + } + // could also perform bounds propagation: + // a has tighter lower/upper bound than m.var(), + // -> transfer bound to m.var() + // all but one variable has bound + // -> transfer bound to that variable using division + return true; +} - void intervals::set_interval(lpvar v, interval& b) { - lp::constraint_index ci; - rational val; - bool is_strict; - if (m_solver.has_lower_bound(v, ci, val, is_strict)) { - m_config.set_lower(b, val); - m_config.set_lower_is_open(b, is_strict); - m_config.set_lower_is_inf(b, false); - b.m_lower_dep = mk_dep(ci); - } - else { - m_config.set_lower_is_open(b, true); - m_config.set_lower_is_inf(b, true); - b.m_lower_dep = nullptr; - } - if (m_solver.has_upper_bound(v, ci, val, is_strict)) { - m_config.set_upper(b, val); - m_config.set_upper_is_open(b, is_strict); - m_config.set_upper_is_inf(b, false); - b.m_upper_dep = mk_dep(ci); - } - else { - m_config.set_upper_is_open(b, true); - m_config.set_upper_is_inf(b, true); - b.m_upper_dep = nullptr; - } +void intervals::set_interval(lpvar v, interval& b) { + lp::constraint_index ci; + rational val; + bool is_strict; + if (ls().has_lower_bound(v, ci, val, is_strict)) { + m_config.set_lower(b, val); + m_config.set_lower_is_open(b, is_strict); + m_config.set_lower_is_inf(b, false); + b.m_lower_dep = mk_dep(ci); } + else { + m_config.set_lower_is_open(b, true); + m_config.set_lower_is_inf(b, true); + b.m_lower_dep = nullptr; + } + if (ls().has_upper_bound(v, ci, val, is_strict)) { + m_config.set_upper(b, val); + m_config.set_upper_is_open(b, is_strict); + m_config.set_upper_is_inf(b, false); + b.m_upper_dep = mk_dep(ci); + } + else { + m_config.set_upper_is_open(b, true); + m_config.set_upper_is_inf(b, true); + b.m_upper_dep = nullptr; + } +} - intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) { - return m_dep_manager.mk_leaf(ci); - } +intervals::ci_dependency *intervals::mk_dep(lp::constraint_index ci) { + return m_dep_manager.mk_leaf(ci); +} - bool intervals::check(lp::lar_term const& t) { - // convert term into factors for improved precision - return true; - } +bool intervals::check(lp::lar_term const& t) { + // convert term into factors for improved precision + return true; +} lp::impq intervals::get_upper_bound_of_monomial(lpvar j) const { SASSERT(false); @@ -117,7 +118,7 @@ lp::impq intervals::get_lower_bound_of_monomial(lpvar j) const { bool intervals::product_has_upper_bound(int sign, const svector&) const { interval a; - throw; + SASSERT(false); } bool intervals::monomial_has_lower_bound(lpvar j) const { @@ -129,5 +130,6 @@ bool intervals::monomial_has_upper_bound(lpvar j) const { const monomial& m = m_core->emons()[j]; return product_has_upper_bound(-1, m.vars()); } +lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; } } template class interval_manager; diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index b86140754..c23621955 100755 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -142,7 +142,6 @@ namespace nla { im_config m_config; interval_manager m_imanager; region m_region; - lp::lar_solver& m_solver; typedef interval_manager::interval interval; @@ -153,15 +152,14 @@ namespace nla { ci_dependency* mk_dep(lp::constraint_index ci); bool check(lp::lar_term const& t); - + lp::lar_solver& ls(); public: - intervals(core* c, reslimit& lim, lp::lar_solver& s) : + intervals(core* c, reslimit& lim) : m_core(c), m_alloc("intervals"), 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)), - m_solver(s) + m_imanager(lim, im_config(m_num_manager, m_dep_manager)) {} bool check(); bool monomial_has_lower_bound(lpvar j) const; diff --git a/src/math/lp/nla_solver.cpp b/src/math/lp/nla_solver.cpp index 60becfa3f..3f58ead75 100644 --- a/src/math/lp/nla_solver.cpp +++ b/src/math/lp/nla_solver.cpp @@ -55,7 +55,7 @@ void solver::pop(unsigned n) { } -solver::solver(lp::lar_solver& s): m_core(alloc(core, s)), m_intervals(m_core, m_res_limit, s) { +solver::solver(lp::lar_solver& s): m_core(alloc(core, s)), m_intervals(m_core, m_res_limit) { } solver::~solver() {