mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 15:53:41 +00:00
Code Activity

some refactoring of lar_solver.h

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-05-09 12:14:17 -07:00 • committed by Lev Nachmanson
parent fef954c028
commit 52241b6474
2 changed files with 40 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

78
src/math/lp/lar_solver.cpp
View file

@ -139,7 +139,41 @@ namespace lp {
return solver.get_status() == lp_status::INFEASIBLE; return solver.get_status() == lp_status::INFEASIBLE;
} }
} }
}; void require_nbasis_sort() { m_mpq_lar_core_solver.m_r_solver.m_nbasis_sort_counter = 0; }
void register_in_fixed_var_table(unsigned j, unsigned& equal_to_j) {
SASSERT(lra.column_is_fixed(j));
equal_to_j = null_lpvar;
const impq& bound = lra.get_lower_bound(j);
if (!bound.y.is_zero())
return;
const mpq& key = bound.x;
unsigned k;
bool j_is_int = lra.column_is_int(j);
if (j_is_int) {
if (!m_fixed_var_table_int.find(key, k)) {
m_fixed_var_table_int.insert(key, j);
return;
}
}
else { // j is not integral column
if (!m_fixed_var_table_real.find(key, k)) {
m_fixed_var_table_real.insert(key, j);
return;
}
}
CTRACE("arith", !lra.column_is_fixed(k), lra.print_terms(tout););
// SASSERT(column_is_fixed(k));
if (j != k && lra.column_is_fixed(k)) {
SASSERT(lra.column_is_int(j) == lra.column_is_int(k));
equal_to_j = k;
TRACE("lar_solver", tout << "found equal column k = " << k <<
", external = " << equal_to_j << "\n";);
}
}
}; // imp
unsigned_vector& lar_solver::row_bounds_to_replay() { return m_imp->m_row_bounds_to_replay; } unsigned_vector& lar_solver::row_bounds_to_replay() { return m_imp->m_row_bounds_to_replay; }
trail_stack& lar_solver::trail() { return m_imp->m_trail; } trail_stack& lar_solver::trail() { return m_imp->m_trail; }
@ -211,8 +245,6 @@ namespace lp {
indexed_uint_set& lar_solver::basic_columns_with_changed_cost() { return m_imp->m_basic_columns_with_changed_cost; } indexed_uint_set& lar_solver::basic_columns_with_changed_cost() { return m_imp->m_basic_columns_with_changed_cost; }
void lar_solver::require_nbasis_sort() { m_imp->m_mpq_lar_core_solver.m_r_solver.m_nbasis_sort_counter = 0; }
mpq lar_solver::bound_span_x(lpvar j) const { mpq lar_solver::bound_span_x(lpvar j) const {
SASSERT(column_has_upper_bound(j) && column_has_lower_bound(j)); SASSERT(column_has_upper_bound(j) && column_has_lower_bound(j));
return get_upper_bound(j).x - get_lower_bound(j).x; return get_upper_bound(j).x - get_lower_bound(j).x;
@ -533,7 +565,7 @@ namespace lp {
m_imp->m_usage_in_terms.pop(k); m_imp->m_usage_in_terms.pop(k);
m_imp->m_dependencies.pop_scope(k); m_imp->m_dependencies.pop_scope(k);
// init the nbasis sorting // init the nbasis sorting
require_nbasis_sort(); m_imp->require_nbasis_sort();
set_status(lp_status::UNKNOWN); set_status(lp_status::UNKNOWN);
} }
@ -759,7 +791,7 @@ namespace lp {
TRACE("lar_solver", print_term(term, tout << "maximize: ") << "\n" TRACE("lar_solver", print_term(term, tout << "maximize: ") << "\n"
<< constraints() << ", strategy = " << (int)settings().simplex_strategy() << "\n";); << constraints() << ", strategy = " << (int)settings().simplex_strategy() << "\n";);
if (settings().simplex_strategy() != simplex_strategy_enum::tableau_costs) if (settings().simplex_strategy() != simplex_strategy_enum::tableau_costs)
require_nbasis_sort(); m_imp->require_nbasis_sort();
flet f(settings().simplex_strategy(), simplex_strategy_enum::tableau_costs); flet f(settings().simplex_strategy(), simplex_strategy_enum::tableau_costs);
prepare_costs_for_r_solver(term); prepare_costs_for_r_solver(term);
ret = maximize_term_on_tableau(term, term_max); ret = maximize_term_on_tableau(term, term_max);
@ -1962,7 +1994,7 @@ namespace lp {
else { else {
get_core_solver().m_r_heading.push_back(-static_cast<int>(get_core_solver().m_r_nbasis.size()) - 1); get_core_solver().m_r_heading.push_back(-static_cast<int>(get_core_solver().m_r_nbasis.size()) - 1);
get_core_solver().m_r_nbasis.push_back(j); get_core_solver().m_r_nbasis.push_back(j);
require_nbasis_sort(); m_imp->require_nbasis_sort();
} }
} }
@ -2099,38 +2131,6 @@ namespace lp {
remove_non_fixed_from_table(m_imp->m_fixed_var_table_real); remove_non_fixed_from_table(m_imp->m_fixed_var_table_real);
} }
void lar_solver::register_in_fixed_var_table(unsigned j, unsigned& equal_to_j) {
SASSERT(column_is_fixed(j));
equal_to_j = null_lpvar;
const impq& bound = get_lower_bound(j);
if (!bound.y.is_zero())
return;
const mpq& key = bound.x;
unsigned k;
bool j_is_int = column_is_int(j);
if (j_is_int) {
if (!m_imp->m_fixed_var_table_int.find(key, k)) {
m_imp->m_fixed_var_table_int.insert(key, j);
return;
}
}
else { // j is not integral column
if (!m_imp->m_fixed_var_table_real.find(key, k)) {
m_imp->m_fixed_var_table_real.insert(key, j);
return;
}
}
CTRACE("arith", !column_is_fixed(k), print_terms(tout););
// SASSERT(column_is_fixed(k));
if (j != k && column_is_fixed(k)) {
SASSERT(column_is_int(j) == column_is_int(k));
equal_to_j = k;
TRACE("lar_solver", tout << "found equal column k = " << k <<
", external = " << equal_to_j << "\n";);
}
}
void lar_solver::activate_check_on_equal(constraint_index ci, unsigned& equal_column) { void lar_solver::activate_check_on_equal(constraint_index ci, unsigned& equal_column) {
auto const& c = m_imp->m_constraints[ci]; auto const& c = m_imp->m_constraints[ci];
@ -2318,7 +2318,7 @@ namespace lp {
update_column_type_and_bound(j, right_side, constr_index); update_column_type_and_bound(j, right_side, constr_index);
equal_to_j = null_lpvar; equal_to_j = null_lpvar;
if (column_is_fixed(j)) { if (column_is_fixed(j)) {
register_in_fixed_var_table(j, equal_to_j); m_imp->register_in_fixed_var_table(j, equal_to_j);
} }
} }

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

@ -54,7 +54,6 @@ class lar_solver : public column_namer {
////////////////// methods //////////////////////////////// ////////////////// methods ////////////////////////////////
static bool valid_index(unsigned j) { return static_cast<int>(j) >= 0; }
bool row_has_a_big_num(unsigned i) const; bool row_has_a_big_num(unsigned i) const;
// init region // init region
void register_new_external_var(unsigned ext_v, bool is_int); void register_new_external_var(unsigned ext_v, bool is_int);
@ -95,16 +94,14 @@ class lar_solver : public column_namer {
public: public:
bool validate_blocker() const { return m_validate_blocker; } bool validate_blocker() const { return m_validate_blocker; }
bool & validate_blocker() { return m_validate_blocker; } bool & validate_blocker() { return m_validate_blocker; }
void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
private: private:
void require_nbasis_sort();
void update_column_type_and_bound_with_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_column_type_and_bound_with_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_column_type_and_bound_with_no_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_column_type_and_bound_with_no_ub(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_bound_with_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_bound_with_no_ub_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_bound_with_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep); void update_bound_with_no_ub_no_lb(lpvar j, lconstraint_kind kind, const mpq& right_side, u_dependency* dep);
void register_in_fixed_var_table(unsigned, unsigned&);
void remove_non_fixed_from_fixed_var_table(); void remove_non_fixed_from_fixed_var_table();
constraint_index add_var_bound_on_constraint_for_term(lpvar j, lconstraint_kind kind, const mpq& right_side); constraint_index add_var_bound_on_constraint_for_term(lpvar j, lconstraint_kind kind, const mpq& right_side);
void set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep); void set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep);