mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 20:58:54 +00:00
Code Activity

rm lu

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-03-04 12:34:15 -08:00
parent a38be43264
commit 527f0d1242
4 changed files with 5 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -166,7 +166,6 @@ class lar_solver : public column_namer {
void adjust_initial_state_for_lu();
void adjust_initial_state_for_tableau_rows();
void fill_last_row_of_A_d(static_matrix<double, double> & A, const lar_term* ls);
bool use_lu() const;
bool sizes_are_correct() const;
bool implied_bound_is_correctly_explained(implied_bound const & be, const vector<std::pair<mpq, unsigned>> & explanation) const;