mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

make m_ibounds inside of lp_bound_propagator

Browse source 
a reference
This commit is contained in:
Lev Nachmanson 2023-09-20 17:13:25 -07:00
parent 20c02f4f45
commit 536930b4a1
4 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/lp_bound_propagator.h
View file

@ -20,7 +20,7 @@ class lp_bound_propagator {
u_map<unsigned> m_improved_upper_bounds;
T& m_imp;
std_vector<implied_bound> m_ibounds;
std_vector<implied_bound>& m_ibounds;
map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_val2fixed_row;
// works for rows of the form x + y + sum of fixed = 0
@ -109,7 +109,7 @@ private:
};
public:
lp_bound_propagator(T& imp) : m_imp(imp) {}
lp_bound_propagator(T& imp, std_vector<implied_bound> & ibounds) : m_imp(imp), m_ibounds(ibounds) {}
const std_vector<implied_bound>& ibounds() const { return m_ibounds; }

2
src/sat/smt/arith_solver.cpp
View file

@ -26,7 +26,7 @@ namespace arith {
m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
m_local_search(*this),
m_resource_limit(*this),
m_bp(*this),
m_bp(*this, m_implied_bounds),
a(m),
m_bound_terms(m),
m_bound_predicate(m)

1
src/sat/smt/arith_solver.h
View file

@ -243,6 +243,7 @@ namespace arith {
resource_limit m_resource_limit;
lp_bounds m_new_bounds;
symbol m_farkas;
std_vector<lp::implied_bound> m_implied_bounds;
lp::lp_bound_propagator<solver> m_bp;
mutable vector<std::pair<lp::tv, rational>> m_todo_terms;

3
src/smt/theory_lra.cpp
View file

@ -225,6 +225,7 @@ class theory_lra::imp {
lp_bounds m_new_bounds;
symbol m_farkas;
vector<parameter> m_bound_params;
std_vector<lp::implied_bound> m_implied_bounds;
lp::lp_bound_propagator<imp> m_bp;
context& ctx() const { return th.get_context(); }
@ -873,7 +874,7 @@ public:
m_solver(nullptr),
m_resource_limit(*this),
m_farkas("farkas"),
m_bp(*this),
m_bp(*this, m_implied_bounds),
m_bounded_range_idx(0),
m_bounded_range_lit(null_literal),
m_bound_terms(m),