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

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-05-12 07:59:30 -07:00
parent 64f3b3e316 45fc5d9fbd
commit 07474e4887
5 changed files with 17 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
scripts/mk_util.py
View file

@ -2959,7 +2959,11 @@ def get_platform_toolset_str():
if len(tokens) < 2: if len(tokens) < 2:
return default return default
else: else:
return 'v' + tokens[0] + tokens[1] if tokens[0] == "15":
# Visual Studio 2017 reports 15.* but the PlatformToolsetVersion is 141
return "v141"
else:
return 'v' + tokens[0] + tokens[1]
def mk_vs_proj_property_groups(f, name, target_ext, type): def mk_vs_proj_property_groups(f, name, target_ext, type):
f.write(' <ItemGroup Label="ProjectConfigurations">\n') f.write(' <ItemGroup Label="ProjectConfigurations">\n')

1
src/util/lp/bound_analyzer_on_row.h
View file

@ -253,7 +253,6 @@ public :
if (str) if (str)
strict = true; strict = true;
} }
bound /= l_coeff; bound /= l_coeff;
if (is_pos(l_coeff)) { if (is_pos(l_coeff)) {
limit_j(m_column_of_l, bound, true, false, strict); limit_j(m_column_of_l, bound, true, false, strict);

2
src/util/lp/lar_core_solver.h
View file

@ -599,7 +599,7 @@ public:
} }
if (no_r_lu()) { // it is the case where m_d_solver gives a degenerated basis, we need to roll back if (no_r_lu()) { // it is the case where m_d_solver gives a degenerated basis, we need to roll back
std::cout << "no_r_lu" << std::endl; // std::cout << "no_r_lu" << std::endl;
catch_up_in_lu_in_reverse(changes_of_basis, m_r_solver); catch_up_in_lu_in_reverse(changes_of_basis, m_r_solver);
m_r_solver.find_feasible_solution(); m_r_solver.find_feasible_solution();
m_d_basis = m_r_basis; m_d_basis = m_r_basis;

12
src/util/lp/lp_core_solver_base.hpp
View file

@ -533,13 +533,19 @@ update_basis_and_x(int entering, int leaving, X const & tt) {
init_factorization(m_factorization, m_A, m_basis, m_settings); init_factorization(m_factorization, m_A, m_basis, m_settings);
if (!find_x_by_solving()) { if (!find_x_by_solving()) {
restore_x(entering, tt); restore_x(entering, tt);
lean_assert(!A_mult_x_is_off()); if(A_mult_x_is_off()) {
m_status = FLOATING_POINT_ERROR;
m_iters_with_no_cost_growing++;
return false;
}
init_factorization(m_factorization, m_A, m_basis, m_settings); init_factorization(m_factorization, m_A, m_basis, m_settings);
m_iters_with_no_cost_growing++; m_iters_with_no_cost_growing++;
if (m_factorization->get_status() != LU_status::OK) { if (m_factorization->get_status() != LU_status::OK) {
std::stringstream s; std::stringstream s;
s << "failing refactor on off_result for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations(); // s << "failing refactor on off_result for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations();
throw_exception(s.str()); m_status = FLOATING_POINT_ERROR;
return false;
} }
return false; return false;
} }

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

@ -605,13 +605,13 @@ void lu<T, X>::process_column(int j) {
unsigned pi, pj; unsigned pi, pj;
bool success = m_U.get_pivot_for_column(pi, pj, m_settings.c_partial_pivoting, j); bool success = m_U.get_pivot_for_column(pi, pj, m_settings.c_partial_pivoting, j);
if (!success) { if (!success) {
LP_OUT(m_settings, "get_pivot returned false: cannot find the pivot for column " << j << std::endl); // LP_OUT(m_settings, "get_pivot returned false: cannot find the pivot for column " << j << std::endl);
m_failure = true; m_failure = true;
return; return;
} }
if (static_cast<int>(pi) == -1) { if (static_cast<int>(pi) == -1) {
LP_OUT(m_settings, "cannot find the pivot for column " << j << std::endl); // LP_OUT(m_settings, "cannot find the pivot for column " << j << std::endl);
m_failure = true; m_failure = true;
return; return;
} }