From d0d71a09075ec8aecdce0ebd52e8586f0a67106f Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@microsoft.com>
Date: Thu, 11 May 2017 17:49:27 -0700
Subject: [PATCH 1/2] allow more failures in d_solver
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
---
src/util/lp/bound_analyzer_on_row.h | 1 -
src/util/lp/lar_core_solver.h | 2 +-
src/util/lp/lp_core_solver_base.hpp | 12 +++++++++---
src/util/lp/lu.hpp | 4 ++--
4 files changed, 12 insertions(+), 7 deletions(-)
diff --git a/src/util/lp/bound_analyzer_on_row.h b/src/util/lp/bound_analyzer_on_row.h
index b6c3c4ef2..508692e5a 100644
--- a/src/util/lp/bound_analyzer_on_row.h
+++ b/src/util/lp/bound_analyzer_on_row.h
@@ -253,7 +253,6 @@ public :
if (str)
strict = true;
}
-
bound /= l_coeff;
if (is_pos(l_coeff)) {
limit_j(m_column_of_l, bound, true, false, strict);
diff --git a/src/util/lp/lar_core_solver.h b/src/util/lp/lar_core_solver.h
index 58151c8be..ba5bbaa62 100644
--- a/src/util/lp/lar_core_solver.h
+++ b/src/util/lp/lar_core_solver.h
@@ -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
- 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);
m_r_solver.find_feasible_solution();
m_d_basis = m_r_basis;
diff --git a/src/util/lp/lp_core_solver_base.hpp b/src/util/lp/lp_core_solver_base.hpp
index 6407aec07..7dae0535a 100644
--- a/src/util/lp/lp_core_solver_base.hpp
+++ b/src/util/lp/lp_core_solver_base.hpp
@@ -534,13 +534,19 @@ update_basis_and_x(int entering, int leaving, X const & tt) {
init_factorization(m_factorization, m_A, m_basis, m_settings);
if (!find_x_by_solving()) {
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);
m_iters_with_no_cost_growing++;
if (m_factorization->get_status() != LU_status::OK) {
std::stringstream s;
- s << "failing refactor on off_result for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations();
- throw_exception(s.str());
+ // s << "failing refactor on off_result for entering = " << entering << ", leaving = " << leaving << " total_iterations = " << total_iterations();
+ m_status = FLOATING_POINT_ERROR;
+ return false;
}
return false;
}
diff --git a/src/util/lp/lu.hpp b/src/util/lp/lu.hpp
index b13583d17..2d2c7c7c4 100644
--- a/src/util/lp/lu.hpp
+++ b/src/util/lp/lu.hpp
@@ -605,13 +605,13 @@ void lu<T, X>::process_column(int j) {
unsigned pi, pj;
bool success = m_U.get_pivot_for_column(pi, pj, m_settings.c_partial_pivoting, j);
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;
return;
}
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;
return;
}
From 46791047fae20076942b6e1db028ac75a072429f Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 12 May 2017 14:28:55 +0100
Subject: [PATCH 2/2] Fixed VS 2017 platform toolset version in .vcxproj
---
scripts/mk_util.py | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index da00f6209..00c391fa7 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2959,7 +2959,11 @@ def get_platform_toolset_str():
if len(tokens) < 2:
return default
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):
f.write(' <ItemGroup Label="ProjectConfigurations">\n')