From ee86ea83e4a03b7c228268d12033e393c6a3a899 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 27 Jun 2023 09:05:00 -0700 Subject: [PATCH] just branch on = 0 Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 4 +++- src/math/lp/nla_core.h | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index ecda601b9..ee85bf7c7 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -25,6 +25,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : m_evars(), m_lar_solver(s), m_reslim(lim), + m_params(p), m_tangents(this), m_basics(this), m_order(this), @@ -36,7 +37,6 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) : m_horner(this), m_grobner(this), m_emons(m_evars), - m_params(p), m_use_nra_model(false), m_nra(s, m_nra_lim, *this) { @@ -1535,10 +1535,12 @@ void core::add_bounds() { //m_lar_solver.print_column_info(j, verbose_stream() << "check variable " << j << " ") << "\n"; if (var_is_free(j)) m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero())); +#if 0 else if (has_lower_bound(j) && can_add_bound(j, m_lower_bounds_added)) m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::LE, get_lower_bound(j))); else if (has_upper_bound(j) && can_add_bound(j, m_upper_bounds_added)) m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::GE, get_upper_bound(j))); +#endif else continue; ++lp_settings().stats().m_nla_bounds; diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h index a7fadf8e3..42176b73e 100644 --- a/src/math/lp/nla_core.h +++ b/src/math/lp/nla_core.h @@ -83,6 +83,7 @@ class core { lp::lar_solver& m_lar_solver; reslimit& m_reslim; + smt_params_helper m_params; std::function m_relevant; vector * m_lemma_vec; vector * m_literal_vec = nullptr; @@ -104,7 +105,6 @@ class core { mutable lp::u_set m_active_var_set; reslimit m_nra_lim; - smt_params_helper m_params; bool m_use_nra_model = false; nra::solver m_nra;