mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

just branch on = 0

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-06-27 09:05:00 -07:00
parent 2ee91d866a
commit ee86ea83e4
2 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/nla_core.cpp
View file

@ -25,6 +25,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
m_evars(), m_evars(),
m_lar_solver(s), m_lar_solver(s),
m_reslim(lim), m_reslim(lim),
m_params(p),
m_tangents(this), m_tangents(this),
m_basics(this), m_basics(this),
m_order(this), m_order(this),
@ -36,7 +37,6 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
m_horner(this), m_horner(this),
m_grobner(this), m_grobner(this),
m_emons(m_evars), m_emons(m_evars),
m_params(p),
m_use_nra_model(false), m_use_nra_model(false),
m_nra(s, m_nra_lim, *this) 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"; //m_lar_solver.print_column_info(j, verbose_stream() << "check variable " << j << " ") << "\n";
if (var_is_free(j)) if (var_is_free(j))
m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero())); 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)) 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))); 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)) 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))); m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::GE, get_upper_bound(j)));
#endif
else else
continue; continue;
++lp_settings().stats().m_nla_bounds; ++lp_settings().stats().m_nla_bounds;

2
src/math/lp/nla_core.h
View file

@ -83,6 +83,7 @@ class core {
lp::lar_solver& m_lar_solver; lp::lar_solver& m_lar_solver;
reslimit& m_reslim; reslimit& m_reslim;
smt_params_helper m_params;
std::function<bool(lpvar)> m_relevant; std::function<bool(lpvar)> m_relevant;
vector<lemma> * m_lemma_vec; vector<lemma> * m_lemma_vec;
vector<ineq> * m_literal_vec = nullptr; vector<ineq> * m_literal_vec = nullptr;
@ -104,7 +105,6 @@ class core {
mutable lp::u_set m_active_var_set; mutable lp::u_set m_active_var_set;
reslimit m_nra_lim; reslimit m_nra_lim;
smt_params_helper m_params;
bool m_use_nra_model = false; bool m_use_nra_model = false;
nra::solver m_nra; nra::solver m_nra;