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

rm_lp

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-03-04 14:58:49 -08:00
parent 1e8bf7669c
commit 1bbb35972b
19 changed files with 65 additions and 641 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lu.h
View file

@ -171,8 +171,6 @@ public:
void print_matrix_compact(std::ostream & f);
void print(indexed_vector<T> & w, const vector<unsigned>& basis);
void solve_Bd(unsigned a_column, vector<T> & d, indexed_vector<T> & w);
void solve_Bd(unsigned a_column, indexed_vector<T> & d, indexed_vector<T> & w);
void solve_Bd_faster(unsigned a_column, indexed_vector<T> & d); // d is the right side on the input and the solution at the exit
void solve_yB(vector<T>& y);