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

more efficient column_is_fixed

Browse source
This commit is contained in:
Lev Nachmanson 2023-08-05 13:40:35 -10:00 • committed by Lev Nachmanson
parent 0fbf8f92f5
commit 858eebca82
3 changed files with 9 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -215,9 +215,7 @@ public:
} }
bool column_is_fixed(unsigned j) const { bool column_is_fixed(unsigned j) const {
return m_column_types()[j] == column_type::fixed || return m_column_types()[j] == column_type::fixed;
( m_column_types()[j] == column_type::boxed &&
m_r_solver.m_lower_bounds[j] == m_r_solver.m_upper_bounds[j]);
} }
bool column_is_free(unsigned j) const { bool column_is_free(unsigned j) const {

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

@ -489,6 +489,7 @@ class lar_solver : public column_namer {
void updt_params(params_ref const& p); void updt_params(params_ref const& p);
column_type get_column_type(unsigned j) const { return m_mpq_lar_core_solver.m_column_types()[j]; } column_type get_column_type(unsigned j) const { return m_mpq_lar_core_solver.m_column_types()[j]; }
const vector<column_type>& get_column_types() const { return m_mpq_lar_core_solver.m_column_types(); }
const impq& get_lower_bound(unsigned j) const { return m_mpq_lar_core_solver.m_r_lower_bounds()[j]; } const impq& get_lower_bound(unsigned j) const { return m_mpq_lar_core_solver.m_r_lower_bounds()[j]; }
const impq& get_upper_bound(unsigned j) const { return m_mpq_lar_core_solver.m_r_upper_bounds()[j]; } const impq& get_upper_bound(unsigned j) const { return m_mpq_lar_core_solver.m_r_upper_bounds()[j]; }
std::ostream& print_terms(std::ostream& out) const; std::ostream& print_terms(std::ostream& out) const;

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

@ -25,6 +25,8 @@ class lp_bound_propagator {
map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_row2index_pos; map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_row2index_pos;
// works for rows of the form x - y + sum of fixed = 0 // works for rows of the form x - y + sum of fixed = 0
map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_row2index_neg; map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_row2index_neg;
const vector<column_type>* m_column_types;
// returns true iff there is only one non-fixed column in the row // returns true iff there is only one non-fixed column in the row
bool only_one_nfixed(unsigned r, unsigned& x) { bool only_one_nfixed(unsigned r, unsigned& x) {
x = UINT_MAX; x = UINT_MAX;
@ -90,13 +92,14 @@ class lp_bound_propagator {
m_improved_upper_bounds.clear(); m_improved_upper_bounds.clear();
m_improved_lower_bounds.clear(); m_improved_lower_bounds.clear();
m_ibounds.reset(); m_ibounds.reset();
m_column_types = &lp().get_column_types();
} }
const lar_solver& lp() const { return m_imp.lp(); } const lar_solver& lp() const { return m_imp.lp(); }
lar_solver& lp() { return m_imp.lp(); } lar_solver& lp() { return m_imp.lp(); }
column_type get_column_type(unsigned j) const { column_type get_column_type(unsigned j) const {
return m_imp.lp().get_column_type(j); return (*m_column_types)[j];
} }
const impq& get_lower_bound(unsigned j) const { const impq& get_lower_bound(unsigned j) const {
@ -117,7 +120,7 @@ class lp_bound_propagator {
// require also the zero infinitesemal part // require also the zero infinitesemal part
bool column_is_fixed(lpvar j) const { bool column_is_fixed(lpvar j) const {
return lp().column_is_fixed(j) && get_lower_bound(j).y.is_zero(); return (*m_column_types)[j] == column_type::fixed && get_lower_bound(j).y.is_zero();
} }
void try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) { void try_add_bound(mpq const& v, unsigned j, bool is_low, bool coeff_before_j_is_pos, unsigned row_or_term_index, bool strict) {
@ -265,7 +268,7 @@ class lp_bound_propagator {
unsigned num_of_non_fixed_in_row(unsigned row_index) const { unsigned num_of_non_fixed_in_row(unsigned row_index) const {
unsigned n_of_nfixed = 0; unsigned n_of_nfixed = 0;
for (const auto& c : lp().get_row(row_index)) { for (const auto& c : lp().get_row(row_index)) {
if (lp().column_is_fixed(c.var())) if (column_is_fixed(c.var()))
continue; continue;
n_of_nfixed++; n_of_nfixed++;
if (n_of_nfixed > 1) if (n_of_nfixed > 1)
@ -370,7 +373,7 @@ class lp_bound_propagator {
unsigned i = c.var(); // the running index of the row unsigned i = c.var(); // the running index of the row
if (i == row_index) if (i == row_index)
continue; continue;
if (check_insert(m_visited_rows, i) == false) if (!check_insert(m_visited_rows, i))
continue; continue;
unsigned y_nb; unsigned y_nb;
nf = extract_non_fixed(i, x, y_nb, y_sign); nf = extract_non_fixed(i, x, y_nb, y_sign);