mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-17 03:16:17 +00:00
Code Activity

get_rid or inf eps

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-01-14 18:56:15 -08:00
parent 0e86c567cc
commit 30d35488d8
1 changed files with 9 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/lp/lar_solver.cpp
View file

@ -1329,6 +1329,15 @@ void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<var_in
} }
void lar_solver::get_rid_of_inf_eps() { void lar_solver::get_rid_of_inf_eps() {
bool y_is_zero = true;
for (unsigned j = 0; j < number_of_vars(); j++) {
if (!m_mpq_lar_core_solver.m_r_x[j].y.is_zero()) {
y_is_zero = false;
break;
}
}
if (y_is_zero)
return;
mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1)); mpq delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(mpq(1));
for (unsigned j = 0; j < number_of_vars(); j++) { for (unsigned j = 0; j < number_of_vars(); j++) {
auto & r = m_mpq_lar_core_solver.m_r_x[j]; auto & r = m_mpq_lar_core_solver.m_r_x[j];