mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 17:30:23 +00:00
Code Activity

rm get_column_in_lu_mode

Browse source
This commit is contained in:
Lev Nachmanson 2023-03-04 11:56:23 -08:00
parent ea16f6608c
commit 97c1ba4641
1 changed files with 1 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/lar_solver.h
View file

@ -267,13 +267,7 @@ class lar_solver : public column_namer {
void shrink_explanation_to_minimum(vector<std::pair<mpq, constraint_index>> & explanation) const; void shrink_explanation_to_minimum(vector<std::pair<mpq, constraint_index>> & explanation) const;
inline bool column_value_is_integer(unsigned j) const { return get_column_value(j).is_int(); } inline bool column_value_is_integer(unsigned j) const { return get_column_value(j).is_int(); }
bool model_is_int_feasible() const; bool model_is_int_feasible() const;
inline
indexed_vector<mpq> & get_column_in_lu_mode(unsigned j) {
m_column_buffer.clear();
m_column_buffer.resize(A_r().row_count());
m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer);
return m_column_buffer;
}
bool bound_is_integer_for_integer_column(unsigned j, const mpq & right_side) const; bool bound_is_integer_for_integer_column(unsigned j, const mpq & right_side) const;
inline lar_core_solver & get_core_solver() { return m_mpq_lar_core_solver; } inline lar_core_solver & get_core_solver() { return m_mpq_lar_core_solver; }
void catch_up_in_updating_int_solver(); void catch_up_in_updating_int_solver();