mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

consolidate some bounds references

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-23 15:45:44 -07:00
parent f6fbeda9d7
commit fae60946bf
2 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -9,7 +9,6 @@ Author:
#include "util/vector.h"
#include <string>
#include <utility>
#include "math/lp/lp_core_solver_base.h"
#include <algorithm>
#include "math/lp/indexed_vector.h"
#include "math/lp/lp_primal_core_solver.h"

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

@ -32,7 +32,6 @@
#include "math/lp/lar_constraints.h"
#include "math/lp/lar_core_solver.h"
#include "math/lp/lp_bound_propagator.h"
#include "math/lp/lp_primal_core_solver.h"
#include "math/lp/lp_types.h"
#include "math/lp/nra_solver.h"
#include "math/lp/numeric_pair.h"
@ -524,7 +523,7 @@ public:
}
inline mpq bound_span_x(lpvar j) const {
return m_mpq_lar_core_solver.m_r_solver.m_upper_bounds[j].x - m_mpq_lar_core_solver.m_r_solver.m_lower_bounds[j].x;
return get_upper_bound(j).x - get_lower_bound(j).x;
}
bool has_lower_bound(lpvar var, u_dependency*& ci, mpq& value, bool& is_strict) const;