mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

speed up in get_model and fix in git_model_do_not_care_...

Browse source 
Signed-off-by: Lev Nachmanson <levnach@microsoft.com>
This commit is contained in:
Lev Nachmanson 2017-07-10 22:14:56 -07:00
parent 2fe846d9fc
commit 69d6b022b8
2 changed files with 24 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/util/lp/int_solver.cpp
View file

@ -39,24 +39,26 @@ void int_solver::failed() {
} }
void int_solver::trace_inf_rows() const { void int_solver::trace_inf_rows() const {
unsigned num = m_lar_solver->A_r().column_count(); TRACE("arith_int_rows",
for (unsigned v = 0; v < num; v++) { unsigned num = m_lar_solver->A_r().column_count();
if (is_int(v) && !get_value(v).is_int()) { for (unsigned v = 0; v < num; v++) {
display_column(tout, v); if (is_int(v) && !get_value(v).is_int()) {
} display_column(tout, v);
} }
}
num = 0; num = 0;
for (unsigned i = 0; i < m_lar_solver->A_r().row_count(); i++) { for (unsigned i = 0; i < m_lar_solver->A_r().row_count(); i++) {
unsigned j = m_lar_solver->m_mpq_lar_core_solver.m_r_basis[i]; unsigned j = m_lar_solver->m_mpq_lar_core_solver.m_r_basis[i];
if (column_is_int_inf(j)) { if (column_is_int_inf(j)) {
num++; num++;
iterator_on_row<mpq> it(m_lar_solver->A_r().m_rows[i]); iterator_on_row<mpq> it(m_lar_solver->A_r().m_rows[i]);
m_lar_solver->print_linear_iterator(&it, tout); m_lar_solver->print_linear_iterator(&it, tout);
tout << "\n"; tout << "\n";
} }
} }
tout << "num of int infeasible: " << num << "\n"; tout << "num of int infeasible: " << num << "\n";
);
} }
int int_solver::find_inf_int_base_column() { int int_solver::find_inf_int_base_column() {

7
src/util/lp/lar_solver.cpp
View file

@ -368,7 +368,6 @@ void lar_solver::pop(unsigned k) {
unsigned m = A_r().row_count(); unsigned m = A_r().row_count();
clean_popped_elements(m, m_rows_with_changed_bounds); clean_popped_elements(m, m_rows_with_changed_bounds);
clean_inf_set_of_r_solver_after_pop(); clean_inf_set_of_r_solver_after_pop();
m_status = m_mpq_lar_core_solver.m_r_solver.current_x_is_feasible()? lp_status::OPTIMAL: lp_status::UNKNOWN;
lp_assert(m_settings.simplex_strategy() == simplex_strategy_enum::undecided || lp_assert(m_settings.simplex_strategy() == simplex_strategy_enum::undecided ||
(!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); (!use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
@ -389,6 +388,8 @@ void lar_solver::pop(unsigned k) {
m_settings.simplex_strategy() = m_simplex_strategy; m_settings.simplex_strategy() = m_simplex_strategy;
lp_assert(sizes_are_correct()); lp_assert(sizes_are_correct());
lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau()); lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
m_status = m_mpq_lar_core_solver.m_r_solver.current_x_is_feasible()? lp_status::OPTIMAL: lp_status::UNKNOWN;
} }
vector<constraint_index> lar_solver::get_all_constraint_indices() const { vector<constraint_index> lar_solver::get_all_constraint_indices() const {
@ -1139,9 +1140,11 @@ void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values)
} }
void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const { void lar_solver::get_model_do_not_care_about_diff_vars(std::unordered_map<var_index, mpq> & variable_values) const {
mpq delta = mpq(1);
delta = m_mpq_lar_core_solver.find_delta_for_strict_bounds(delta);
for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) { for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
const impq & rp = m_mpq_lar_core_solver.m_r_x[i]; const impq & rp = m_mpq_lar_core_solver.m_r_x[i];
variable_values[i] = rp.x + rp.y; variable_values[i] = rp.x + delta * rp.y;
} }
} }