diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp index 832f4f12c..f9920e766 100644 --- a/src/math/lp/nla_grobner.cpp +++ b/src/math/lp/nla_grobner.cpp @@ -289,13 +289,10 @@ namespace nla { auto coeff = m.coeff * denom; if (m.vars.empty()) k -= coeff; - else if (m.vars.size() == 1) { + else if (m.vars.size() == 1) lo_t.add_monomial(coeff, m.vars[0]); - } - else if (c().find_canonical_monic_of_vars(m.vars, j)) { - //verbose_stream() << "canonical monic\n"; + else if (c().find_canonical_monic_of_vars(m.vars, j)) lo_t.add_monomial(coeff, j); - } else return false; } diff --git a/src/math/lp/nla_intervals.cpp b/src/math/lp/nla_intervals.cpp index 298d57c41..f2352b128 100644 --- a/src/math/lp/nla_intervals.cpp +++ b/src/math/lp/nla_intervals.cpp @@ -276,14 +276,6 @@ void intervals::set_var_interval1(lpvar v, interval& b) { } } -template -bool intervals::set_var_interval2(lpvar v, scoped_dep_interval& b) { - if (ls().column_corresponds_to_term(v)) { - auto const& lt = ls().column_index_to_term(v); - return interval_from_lar_term(lt, b); - } - return false; -} template void intervals::set_var_interval(lpvar v, interval& b) { @@ -505,7 +497,6 @@ lp::lar_solver& intervals::ls() { return m_core->m_lar_solver; } const lp::lar_solver& intervals::ls() const { return m_core->m_lar_solver; } - } // end of nla namespace diff --git a/src/math/lp/nla_intervals.h b/src/math/lp/nla_intervals.h index 7455f676d..4db9aad7b 100644 --- a/src/math/lp/nla_intervals.h +++ b/src/math/lp/nla_intervals.h @@ -56,7 +56,13 @@ public: void set_var_interval1(lpvar v, interval& b); template - bool set_var_interval2(lpvar v, scoped_dep_interval& b); + bool set_var_interval2(lpvar v, scoped_dep_interval& b) { + if (ls().column_corresponds_to_term(v)) { + auto const& lt = ls().column_index_to_term(v); + return interval_from_lar_term(lt, b); + } + return false; + } template bool interval_from_term(const nex& e, scoped_dep_interval& i);