mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

add this qualifier for build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-11 16:58:29 -07:00
parent 7b35eacf63
commit a9e2a1204e
2 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/util/lp/lp_primal_core_solver.hpp
View file

@ -199,7 +199,7 @@ int lp_primal_core_solver<T, X>::choose_entering_column_presize(unsigned number_
entering_iter = non_basis_iter; entering_iter = non_basis_iter;
if (number_of_benefitial_columns_to_go_over) if (number_of_benefitial_columns_to_go_over)
number_of_benefitial_columns_to_go_over--; number_of_benefitial_columns_to_go_over--;
} else if (t == j_nz && m_settings.random_next() % 2 == 0) { } else if (t == j_nz && this->m_settings.random_next() % 2 == 0) {
entering_iter = non_basis_iter; entering_iter = non_basis_iter;
} }
}// while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb); }// while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb);
@ -268,7 +268,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::advance_on_so
if (slope_at_entering * m_sign_of_entering_delta > - m_epsilon_of_reduced_cost) { // the slope started to increase infeasibility if (slope_at_entering * m_sign_of_entering_delta > - m_epsilon_of_reduced_cost) { // the slope started to increase infeasibility
break; break;
} else { } else {
if ((numeric_traits<T>::precise() == false) || ( numeric_traits<T>::is_zero(slope_at_entering) && m_settings.random_next() % 2 == 0)) { if ((numeric_traits<T>::precise() == false) || ( numeric_traits<T>::is_zero(slope_at_entering) && this->m_settings.random_next() % 2 == 0)) {
// it is not cost benefitial to advance the delta more, so just break to increas the randomness // it is not cost benefitial to advance the delta more, so just break to increas the randomness
break; break;
} }
@ -307,7 +307,7 @@ find_leaving_on_harris_theta(X const & harris_theta, X & t) {
// we also know that harris_theta is limited, so we will find a leaving // we also know that harris_theta is limited, so we will find a leaving
zero_harris_eps(); zero_harris_eps();
unsigned steps = this->m_ed.m_index.size(); unsigned steps = this->m_ed.m_index.size();
unsigned k = m_settings.random_next() % steps; unsigned k = this->m_settings.random_next() % steps;
unsigned initial_k = k; unsigned initial_k = k;
do { do {
unsigned i = this->m_ed.m_index[k]; unsigned i = this->m_ed.m_index[k];
@ -398,7 +398,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
return find_leaving_and_t_with_breakpoints(entering, t); return find_leaving_and_t_with_breakpoints(entering, t);
bool unlimited = true; bool unlimited = true;
unsigned steps = this->m_ed.m_index.size(); unsigned steps = this->m_ed.m_index.size();
unsigned k = m_settings.random_next() % steps; unsigned k = this->m_settings.random_next() % steps;
unsigned initial_k = k; unsigned initial_k = k;
unsigned row_min_nz = this->m_n() + 1; unsigned row_min_nz = this->m_n() + 1;
m_leaving_candidates.clear(); m_leaving_candidates.clear();
@ -454,7 +454,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
t = ratio; t = ratio;
return entering; return entering;
} }
k = m_settings.random_next() % m_leaving_candidates.size(); k = this->m_settings.random_next() % m_leaving_candidates.size();
return m_leaving_candidates[k]; return m_leaving_candidates[k];
} }
@ -833,7 +833,7 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::get_num
if (ret == 0) { if (ret == 0) {
return 0; return 0;
} }
return std::max(static_cast<unsigned>(m_settings.random_next() % ret), 1u); return std::max(static_cast<unsigned>(this->m_settings.random_next() % ret), 1u);
} }
template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column_norms(std::ostream & out) { template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column_norms(std::ostream & out) {
@ -961,7 +961,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::init_column_
for (unsigned j = 0; j < this->m_n(); j++) { for (unsigned j = 0; j < this->m_n(); j++) {
this->m_column_norms[j] = T(static_cast<int>(this->m_A.m_columns[j].size() + 1)) this->m_column_norms[j] = T(static_cast<int>(this->m_A.m_columns[j].size() + 1))
+ T(static_cast<int>(m_settings.random_next() % 10000)) / T(100000); + T(static_cast<int>(this->m_settings.random_next() % 10000)) / T(100000);
} }
} }

4
src/util/lp/lp_primal_core_solver_tableau.hpp
View file

@ -62,7 +62,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::choose_enteri
if (number_of_benefitial_columns_to_go_over) if (number_of_benefitial_columns_to_go_over)
number_of_benefitial_columns_to_go_over--; number_of_benefitial_columns_to_go_over--;
} }
else if (t == j_nz && m_settings.random_next() % 2 == 0) { else if (t == j_nz && this->m_settings.random_next() % 2 == 0) {
entering_iter = non_basis_iter; entering_iter = non_basis_iter;
} }
}// while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb); }// while (number_of_benefitial_columns_to_go_over && initial_offset_in_non_basis != offset_in_nb);
@ -293,7 +293,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
} }
if (m_leaving_candidates.size() == 1) if (m_leaving_candidates.size() == 1)
return m_leaving_candidates[0]; return m_leaving_candidates[0];
k = m_settings.random_next() % m_leaving_candidates.size(); k = this->m_settings.random_next() % m_leaving_candidates.size();
return m_leaving_candidates[k]; return m_leaving_candidates[k];
} }
template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run_tableau() { template <typename T, typename X> void lp_primal_core_solver<T, X>::init_run_tableau() {