mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

simplify the jump on entering

Browse source
This commit is contained in:
Lev Nachmanson 2023-11-02 11:09:01 -07:00
parent bdf1fcf5c1
commit 08d3a82ce0
3 changed files with 10 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -231,7 +231,7 @@ namespace lp {
return rc.var();
}
bool try_jump_to_another_bound_on_entering(unsigned entering, const X &theta, X &t, bool &unlimited);
bool try_jump_to_another_bound_on_entering(unsigned entering, X &t);
bool try_jump_to_another_bound_on_entering_unlimited(unsigned entering, X &t);

47
src/math/lp/lp_primal_core_solver_def.h
View file

@ -98,48 +98,17 @@ bool lp_primal_core_solver<T, X>::column_is_benefitial_for_entering_basis(unsign
}
return false;
}
template <typename T, typename X> bool lp_primal_core_solver<T, X>::try_jump_to_another_bound_on_entering(unsigned entering,
const X & theta,
X & t,
bool & unlimited) {
switch(this->m_column_types[entering]){
case column_type::boxed:
if (m_sign_of_entering_delta > 0) {
t = this->m_upper_bounds[entering] - this->m_x[entering];
if (unlimited || t <= theta){
lp_assert(t >= zero_of_type<X>());
return true;
}
} else { // m_sign_of_entering_delta == -1
t = this->m_x[entering] - this->m_lower_bounds[entering];
if (unlimited || t <= theta) {
lp_assert(t >= zero_of_type<X>());
return true;
}
}
// we assume that the columns are at their bounds
template <typename T, typename X> bool lp_primal_core_solver<T, X>::try_jump_to_another_bound_on_entering(unsigned entering, X & theta) {
if (this->m_column_types[entering] != column_type::boxed)
return false;
case column_type::upper_bound:
if (m_sign_of_entering_delta > 0) {
t = this->m_upper_bounds[entering] - this->m_x[entering];
if (unlimited || t <= theta){
lp_assert(t >= zero_of_type<X>());
return true;
}
}
return false;
case column_type::lower_bound:
if (m_sign_of_entering_delta < 0) {
t = this->m_x[entering] - this->m_lower_bounds[entering];
if (unlimited || t <= theta) {
lp_assert(t >= zero_of_type<X>());
return true;
}
}
return false;
default:return false;
X t = this->m_upper_bounds[entering] - this->m_lower_bounds[entering];
if (t <= theta) {
theta = t;
return true;
}
return false;
}
template <typename T, typename X> bool lp_primal_core_solver<T, X>::

5
src/math/lp/lp_primal_core_solver_tableau_def.h
View file

@ -246,10 +246,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
}
}
ratio = t;
unlimited = false;
if (try_jump_to_another_bound_on_entering(entering, t, ratio, unlimited)) {
t = ratio;
if (try_jump_to_another_bound_on_entering(entering, t)) {
return entering;
}
if (m_leaving_candidates.size() == 1)