mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

fix the build

Browse source
This commit is contained in:
Lev Nachmanson 2023-07-10 12:19:32 -07:00
parent 1840fd17da
commit 9ae6c88e3f
1 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -695,6 +695,7 @@ namespace lp {
} }
} }
void lar_solver::detect_rows_with_changed_bounds_for_column(unsigned j) {
if (m_mpq_lar_core_solver.m_r_heading[j] >= 0) if (m_mpq_lar_core_solver.m_r_heading[j] >= 0)
insert_row_with_changed_bounds(m_mpq_lar_core_solver.m_r_heading[j]); insert_row_with_changed_bounds(m_mpq_lar_core_solver.m_r_heading[j]);
else else
@ -1751,7 +1752,8 @@ namespace lp {
} }
// clang-format off // clang-format off
void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j, void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j,
const mpq& right_side, lconstraint_kind kind,
const mpq& right_side,
constraint_index constr_index, constraint_index constr_index,
unsigned& equal_to_j) { unsigned& equal_to_j) {
update_column_type_and_bound(j, kind, right_side, constr_index); update_column_type_and_bound(j, kind, right_side, constr_index);
@ -1895,7 +1897,8 @@ namespace lp {
} }
// clang-format off // clang-format off
void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) { void lar_solver::update_bound_with_no_ub_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound); lp_assert(column_has_lower_bound(j) && !column_has_upper_bound(j));
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::lower_bound);
mpq y_of_bound(0); mpq y_of_bound(0);
switch (kind) { switch (kind) {
@ -1943,7 +1946,8 @@ namespace lp {
} }
// clang-format off // clang-format off
void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) { void lar_solver::update_bound_with_ub_no_lb(var_index j, lconstraint_kind kind, const mpq& right_side, constraint_index ci) {
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound); lp_assert(!column_has_lower_bound(j) && column_has_upper_bound(j));
lp_assert(m_mpq_lar_core_solver.m_column_types[j] == column_type::upper_bound);
mpq y_of_bound(0); mpq y_of_bound(0);
switch (kind) { switch (kind) {
case LT: case LT:
@ -2029,7 +2033,8 @@ namespace lp {
} }
// clang-format off // clang-format off
bool lar_solver::column_corresponds_to_term(unsigned j) const { bool lar_solver::column_corresponds_to_term(unsigned j) const {
} return tv::is_term(m_var_register.local_to_external(j));
}
var_index lar_solver::to_column(unsigned ext_j) const { var_index lar_solver::to_column(unsigned ext_j) const {
return m_var_register.external_to_local(ext_j); return m_var_register.external_to_local(ext_j);