mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

add logging to lar-solver to capture state for unbounded optimization

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-03 20:33:12 -08:00
parent 19e7b75536
commit 0c0e79a937
4 changed files with 19 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/util/lp/lar_core_solver_def.h
View file

@ -265,12 +265,14 @@ unsigned lar_core_solver::get_number_of_non_ints() const {
}
void lar_core_solver::solve() {
TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
lp_assert(m_r_solver.non_basic_columns_are_set_correctly());
lp_assert(m_r_solver.inf_set_is_correct());
TRACE("find_feas_stats", tout << "infeasibles = " << m_r_solver.m_inf_set.size() << ", int_infs = " << get_number_of_non_ints() << std::endl;);
if (m_r_solver.current_x_is_feasible() && m_r_solver.m_look_for_feasible_solution_only) {
m_r_solver.set_status(lp_status::OPTIMAL);
return;
m_r_solver.set_status(lp_status::OPTIMAL);
TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
return;
}
++settings().st().m_need_to_solve_inf;
CASSERT("A_off", !m_r_solver.A_mult_x_is_off());
@ -310,6 +312,8 @@ void lar_core_solver::solve() {
lp_assert(r_basis_is_OK());
lp_assert(m_r_solver.non_basic_columns_are_set_correctly());
lp_assert(m_r_solver.inf_set_is_correct());
TRACE("lar_solver", tout << m_r_solver.get_status() << "\n";);
}

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

@ -403,12 +403,15 @@ bool lar_solver::maximize_term_on_tableau(const lar_term & term,
m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::FEASIBLE);
m_mpq_lar_core_solver.solve();
if (m_mpq_lar_core_solver.m_r_solver.get_status() == lp_status::UNBOUNDED)
lp_status st = m_mpq_lar_core_solver.m_r_solver.get_status();
TRACE("lar_solver", tout << st << "\n";);
if (st == lp_status::UNBOUNDED) {
return false;
term_max = term.apply(m_mpq_lar_core_solver.m_r_x);
return true;
}
else {
term_max = term.apply(m_mpq_lar_core_solver.m_r_x);
return true;
}
}
bool lar_solver::costs_are_zeros_for_r_solver() const {
@ -452,7 +455,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) {
void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
TRACE("lar_solver", print_term(term, tout << "prepare: "););
TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";);
auto & rslv = m_mpq_lar_core_solver.m_r_solver;
rslv.m_using_infeas_costs = false;
lp_assert(costs_are_zeros_for_r_solver());

2
src/util/lp/lp_core_solver_base.h
View file

@ -136,8 +136,6 @@ public:
}
const vector<unsigned> & non_basis() const { return m_nbasis; }
void set_status(lp_status status) {
m_status = status;

6
src/util/lp/lp_primal_core_solver_def.h
View file

@ -775,6 +775,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
X t;
int leaving = find_leaving_and_t_precise(entering, t);
if (leaving == -1) {
TRACE("lar_solver", tout << "non-leaving\n";);
this->set_status(lp_status::UNBOUNDED);
return;
}
@ -828,6 +829,7 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::advance_on_e
} else {
this->set_status(lp_status::TENTATIVE_UNBOUNDED);
}
TRACE("lar_solver", tout << this->get_status() << "\n";);
return;
}
advance_on_entering_and_leaving(entering, leaving, t);
@ -857,11 +859,11 @@ template <typename T, typename X> void lp_primal_core_solver<T, X>::print_column
out << this->m_column_norms[j] << " ";
}
out << std::endl;
out << std::endl;
}
}
// returns the number of iterations
template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve() {
TRACE("lar_solver", pretty_print(tout););
if (numeric_traits<T>::precise() && this->m_settings.use_tableau())
return solve_with_tableau();