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

do not random_update int vars

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-02-03 12:48:07 -08:00
parent 47cdb5f46e
commit a05dec99cf
7 changed files with 30 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -338,7 +338,7 @@ public:
for (const auto & cc : m_r_solver.m_A.m_columns[j]){
unsigned i = cc.var();
unsigned jb = m_r_solver.m_basis[i];
m_r_solver.update_x_with_delta_and_track_feasibility(jb, - delta * m_r_solver.m_A.get_val(cc));
m_r_solver.add_delta_to_x_and_track_feasibility(jb, - delta * m_r_solver.m_A.get_val(cc));
}
CASSERT("A_off", m_r_solver.A_mult_x_is_off() == false);
}

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

@ -784,7 +784,7 @@ void lar_solver::change_basic_columns_dependend_on_a_given_nb_column(unsigned j,
if (tableau_with_costs()) {
m_basic_columns_with_changed_cost.insert(bj);
}
m_mpq_lar_core_solver.m_r_solver.update_x_with_delta_and_track_feasibility(bj, - A_r().get_val(c) * delta);
m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, - A_r().get_val(c) * delta);
TRACE("change_x_del",
tout << "changed basis column " << bj << ", it is " <<
( m_mpq_lar_core_solver.m_r_solver.column_is_feasible(bj)? "feas":"inf") << std::endl;);
@ -796,7 +796,7 @@ void lar_solver::change_basic_columns_dependend_on_a_given_nb_column(unsigned j,
m_mpq_lar_core_solver.m_r_solver.solve_Bd(j, m_column_buffer);
for (unsigned i : m_column_buffer.m_index) {
unsigned bj = m_mpq_lar_core_solver.m_r_basis[i];
m_mpq_lar_core_solver.m_r_solver.update_x_with_delta_and_track_feasibility(bj, -m_column_buffer[i] * delta);
m_mpq_lar_core_solver.m_r_solver.add_delta_to_x_and_track_feasibility(bj, -m_column_buffer[i] * delta);
}
}
}
@ -1439,11 +1439,15 @@ void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * v
for (unsigned i = 0; i < sz; i++) {
var_index var = vars[i];
if (var >= m_terms_start_index) { // handle the term
lpvar j = adjust_term_index(var);
if (column_is_int(j))
continue;
for (auto it : *m_terms[var - m_terms_start_index]) {
column_list.push_back(it.var());
}
} else {
column_list.push_back(var);
if (!column_is_int(var))
column_list.push_back(var);
}
}
}
@ -1728,6 +1732,7 @@ void lar_solver::add_new_var_to_core_fields_for_doubles(bool register_in_basis)
void lar_solver::add_new_var_to_core_fields_for_mpq(bool register_in_basis) {
unsigned j = A_r().column_count();
TRACE("add_var", tout << "j = " << j << std::endl;);
A_r().add_column();
lp_assert(m_mpq_lar_core_solver.m_r_x.size() == j);
// lp_assert(m_mpq_lar_core_solver.m_r_lower_bounds.size() == j && m_mpq_lar_core_solver.m_r_upper_bounds.size() == j); // restore later
@ -1841,7 +1846,7 @@ void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned
else {
fill_last_row_of_A_r(A_r(), term);
}
m_mpq_lar_core_solver.m_r_solver.update_x_and_call_tracker(j, get_basic_var_value_from_row(A_r().row_count() - 1));
m_mpq_lar_core_solver.m_r_solver.update_x(j, get_basic_var_value_from_row(A_r().row_count() - 1));
if (use_lu())
fill_last_row_of_A_d(A_d(), term);
}
@ -2313,7 +2318,7 @@ void lar_solver::fix_terms_with_rounded_columns() {
if (need_to_fix) {
lpvar j = external_to_local(ti);
impq v = t.apply(m_mpq_lar_core_solver.m_r_x);
m_mpq_lar_core_solver.m_r_solver.update_x_and_call_tracker(j, v);
m_mpq_lar_core_solver.m_r_solver.update_x(j, v);
}
}
SASSERT(ax_is_correct());

6
src/math/lp/lp_core_solver_base.cpp
View file

@ -56,7 +56,7 @@ template void lp::lp_core_solver_base<double, double>::solve_Bd(unsigned int);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq>>::solve_Bd(unsigned int, indexed_vector<lp::mpq>&);
template void lp::lp_core_solver_base<double, double>::solve_yB(vector<double >&);
template bool lp::lp_core_solver_base<double, double>::update_basis_and_x(int, int, double const&);
template void lp::lp_core_solver_base<double, double>::update_x(unsigned int, const double&);
template void lp::lp_core_solver_base<double, double>::add_delta_to_entering(unsigned int, const double&);
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::A_mult_x_is_off() const;
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::A_mult_x_is_off_on_index(const vector<unsigned> &) const;
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::basis_heading_is_correct() const ;
@ -73,7 +73,7 @@ template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_Ax_eq_b();
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_Bd(unsigned int);
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::solve_yB(vector<lp::mpq>&);
template bool lp::lp_core_solver_base<lp::mpq, lp::mpq>::update_basis_and_x(int, int, lp::mpq const&);
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::update_x(unsigned int, const lp::mpq&);
template void lp::lp_core_solver_base<lp::mpq, lp::mpq>::add_delta_to_entering(unsigned int, const lp::mpq&);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calculate_pivot_row_of_B_1(unsigned int);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init();
@ -87,7 +87,7 @@ template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::snap
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::solve_Ax_eq_b();
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::solve_Bd(unsigned int);
template bool lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::update_basis_and_x(int, int, lp::numeric_pair<lp::mpq> const&);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::update_x(unsigned int, const lp::numeric_pair<lp::mpq>&);
template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::add_delta_to_entering(unsigned int, const lp::numeric_pair<lp::mpq>&);
template lp::lp_core_solver_base<lp::mpq, lp::mpq>::lp_core_solver_base(
lp::static_matrix<lp::mpq, lp::mpq>&,
vector<lp::mpq>&,

16
src/math/lp/lp_core_solver_base.h
View file

@ -180,7 +180,7 @@ public:
void calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row);
void update_x(unsigned entering, const X & delta);
void add_delta_to_entering(unsigned entering, const X & delta);
const T & get_var_value(unsigned j) const {
return m_x[j];
@ -429,7 +429,7 @@ public:
break;
}
if (ret)
add_delta_to_x_and_do_not_track_feasibility(j, delta);
add_delta_to_x(j, delta);
return ret;
@ -685,21 +685,25 @@ public:
}
void update_x_with_feasibility_tracking(unsigned j, const X & v) {
TRACE("lar_solver", tout << "j = " << j << ", v = " << v << "\n";);
m_x[j] = v;
track_column_feasibility(j);
}
void update_x_with_delta_and_track_feasibility(unsigned j, const X & del) {
void add_delta_to_x_and_track_feasibility(unsigned j, const X & del) {
TRACE("lar_solver", tout << "del = " << del << ", was x[" << j << "] = " << m_x[j] << "\n";);
m_x[j] += del;
TRACE("lar_solver", tout << "became x[" << j << "] = " << m_x[j] << "\n";);
track_column_feasibility(j);
}
void update_x_and_call_tracker(unsigned j, const X & v) {
TRACE("lar_solver", tout << "j = " << j << "\n";);
void update_x(unsigned j, const X & v) {
TRACE("lar_solver", tout << "j = " << j << ", v = " << v << "\n";);
m_x[j] = v;
}
void add_delta_to_x_and_do_not_track_feasibility(unsigned j, const X & delta) {
void add_delta_to_x(unsigned j, const X & delta) {
TRACE("lar_solver", tout << "j = " << j << ", delta = " << delta << "\n";);
m_x[j] += delta;
}

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

@ -321,7 +321,7 @@ calculate_pivot_row_when_pivot_row_of_B1_is_ready(unsigned pivot_row) {
}
template <typename T, typename X> void lp_core_solver_base<T, X>::
update_x(unsigned entering, const X& delta) {
add_delta_to_entering(unsigned entering, const X& delta) {
m_x[entering] += delta;
if (!use_tableau())
for (unsigned i : m_ed.m_index) {
@ -526,7 +526,7 @@ template <typename T, typename X> bool lp_core_solver_base<T, X>::
update_basis_and_x(int entering, int leaving, X const & tt) {
if (!is_zero(tt)) {
update_x(entering, tt);
add_delta_to_entering(entering, tt);
if ((!numeric_traits<T>::precise()) && A_mult_x_is_off_on_index(m_ed.m_index) && !find_x_by_solving()) {
init_factorization(m_factorization, m_A, m_basis, m_settings);
if (!find_x_by_solving()) {

2
src/math/lp/lp_primal_core_solver_def.h
View file

@ -675,7 +675,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::calc_work
template <typename T, typename X>
void lp_primal_core_solver<T, X>::advance_on_entering_equal_leaving(int entering, X & t) {
CASSERT("A_off", !this->A_mult_x_is_off() );
this->update_x(entering, t * m_sign_of_entering_delta);
this->add_delta_to_entering(entering, t * m_sign_of_entering_delta);
if (this->A_mult_x_is_off_on_index(this->m_ed.m_index) && !this->find_x_by_solving()) {
this->init_lu();
if (!this->find_x_by_solving()) {

6
src/math/lp/lp_primal_core_solver_tableau_def.h
View file

@ -358,11 +358,11 @@ update_basis_and_x_tableau(int entering, int leaving, X const & tt) {
}
template <typename T, typename X> void lp_primal_core_solver<T, X>::
update_x_tableau(unsigned entering, const X& delta) {
this->add_delta_to_x_and_do_not_track_feasibility(entering, delta);
this->add_delta_to_x(entering, delta);
if (!this->m_using_infeas_costs) {
for (const auto & c : this->m_A.m_columns[entering]) {
unsigned i = c.var();
this->update_x_with_delta_and_track_feasibility(this->m_basis[i], - delta * this->m_A.get_val(c));
this->add_delta_to_x_and_track_feasibility(this->m_basis[i], - delta * this->m_A.get_val(c));
}
} else { // m_using_infeas_costs == true
lp_assert(this->column_is_feasible(entering));
@ -371,7 +371,7 @@ update_x_tableau(unsigned entering, const X& delta) {
for (const auto & c : this->m_A.m_columns[entering]) {
unsigned i = c.var();
unsigned j = this->m_basis[i];
this->add_delta_to_x_and_do_not_track_feasibility(j, -delta * this->m_A.get_val(c));
this->add_delta_to_x(j, -delta * this->m_A.get_val(c));
update_inf_cost_for_column_tableau(j);
if (is_zero(this->m_costs[j]))
this->remove_column_from_inf_set(j);