mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

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

Browse source
This commit is contained in:
Lev Nachmanson 2023-07-10 12:06:06 -07:00
commit 1840fd17da
52 changed files with 1909 additions and 1827 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1857,7 +1857,8 @@ namespace lp {
m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
set_upper_bound_witness(j, ci);
insert_to_columns_with_changed_bounds(j);
} break;
break;
}
case GT:
y_of_bound = 1;
case GE: {
@ -1872,8 +1873,8 @@ namespace lp {
set_lower_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = (low == m_mpq_lar_core_solver.m_r_upper_bounds[j] ? column_type::fixed : column_type::boxed);
insert_to_columns_with_changed_bounds(j);
} break;
break;
}
case EQ: {
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v > m_mpq_lar_core_solver.m_r_upper_bounds[j] || v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
@ -1909,8 +1910,8 @@ namespace lp {
set_upper_bound_witness(j, ci);
m_mpq_lar_core_solver.m_column_types[j] = (up == m_mpq_lar_core_solver.m_r_lower_bounds[j] ? column_type::fixed : column_type::boxed);
insert_to_columns_with_changed_bounds(j);
} break;
break;
}
case GT:
y_of_bound = 1;
case GE: {
@ -1921,8 +1922,8 @@ namespace lp {
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;
set_lower_bound_witness(j, ci);
insert_to_columns_with_changed_bounds(j);
} break;
break;
}
case EQ: {
auto v = numeric_pair<mpq>(right_side, zero_of_type<mpq>());
if (v < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {

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

@ -308,8 +308,9 @@ public:
case column_type::boxed:
if (x < m_lower_bounds[j]) {
delta = m_lower_bounds[j] - x;
ret = true;;
} else if (x > m_upper_bounds[j]) {
ret = true;
}
else if (x > m_upper_bounds[j]) {
delta = m_upper_bounds[j] - x;
ret = true;
}

3496
src/math/simplex/model_based_opt.cpp
View file

File diff suppressed because it is too large Load diff