mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix init reorder warning

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-05-11 10:54:18 -07:00
parent 431feab1bf
commit cf8b35a6f3
9 changed files with 38 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/random_updater.h
View file

@ -16,7 +16,6 @@ namespace lean {
template <typename T> struct numeric_pair; // forward definition
class lar_core_solver; // forward definition
class random_updater {
unsigned range ;
struct interval {
bool upper_bound_is_set;
numeric_pair<mpq> upper_bound;
@ -61,6 +60,7 @@ class random_updater {
};
std::set<var_index> m_var_set;
lar_core_solver & m_core_solver;
unsigned range;
linear_combination_iterator<mpq>* m_column_j; // the actual column
interval find_shift_interval(unsigned j);
interval get_interval_of_non_basic_var(unsigned j);