Optimization in z3 does not terminate.

[tquatmann]

z3 does not terminate on the following (rather simple) input:

(declare-const x Real)
(declare-const y Real)
(assert (<= x 1))
(assert (<= y 1))
(assert (<= (+ x y) 1))
(maximize x)
(check-sat)
(get-objectives)

I found out that it worked on v4.7.1 but not on v4.8.1.

[NikolajBjorner]

The main piece the diverges is in theory_lra's interaction with lar_solver. Starting at: https://github.com/Z3Prover/z3/blob/master/src/smt/theory_lra.cpp#L3332 it calls the lar_solver, obtains an optimum. It then re-initializes the model from lar_solver, assuming it provides the value at optimum. However, this isn't the case. The model that is extracted is the current feasible.

[levnach]

This is correct. What I am seeing is that there is a call with the stack shown below that changes the column values inside lar_solver. Maybe a cleaner option is to keep the "best couple" (value, model) in the caller above lar_solver - now the interface is broken. lar_solver might return optimum status, while term_max will be smaller than in the one of the previous call.

z3.exe!lp::lar_solver::update_x_and_inf_costs_for_column_with_changed_bounds(unsigned int j) Line 729 C++ z3.exe!lp::lar_solver::update_x_and_inf_costs_for_columns_with_changed_bounds_tableau() Line 770 C++ z3.exe!lp::lar_solver::solve_with_core_solver() Line 793 C++ z3.exe!lp::lar_solver::solve() Line 287 C++ z3.exe!lp::lar_solver::find_feasible_solution() Line 278 C++ z3.exe!smt::theory_lra::imp::make_feasible() Line 2995 C++ z3.exe!smt::theory_lra::imp::propagate() Line 2078 C++ z3.exe!smt::theory_lra::propagate() Line 3652 C++ z3.exe!smt::context::propagate_theories() Line 1674 C++ z3.exe!smt::context::propagate() Line 1760 C++ z3.exe!smt::context::bounded_search() Line 3682 C++ z3.exe!smt::context::search() Line 3565 C++ z3.exe!smt::context::check(unsigned int num_assumptions, expr const assumptions, bool reset_cancel) Line 3447 C++ z3.exe!smt::kernel::imp::check(unsigned int num_assumptions, expr const assumptions) Line 116 C++ z3.exe!smt::kernel::check(unsigned int num_assumptions, expr const assumptions) Line 312 C++ z3.exe!opt::opt_solver::check_sat_core2(unsigned int num_assumptions, expr const assumptions) Line 184 C++ z3.exe!solver_na2as::check_sat_core(unsigned int num_assumptions, expr const assumptions) Line 67 C++ z3.exe!solver::check_sat(unsigned int num_assumptions, expr const assumptions) Line 329 C++ z3.exe!opt::optsmt::geometric_lex(unsigned int obj_index, bool is_maximize) Line 193 C++ z3.exe!opt::optsmt::lex(unsigned int obj_index, bool is_maximize) Line 505 C++ z3.exe!opt::context::execute_min_max(unsigned int index, bool committed, bool scoped, bool is_max) Line 407 C++ z3.exe!opt::context::execute(const opt::context::objective & obj, bool committed, bool scoped) Line 433 C++ z3.exe!opt::context::optimize(const ref_vector<expr,ast_manager> & _asms) Line 330 C++ z3.exe!cmd_context::check_sat(unsigned int num_assumptions, expr const assumptions) Line 1537 C++ z3.exe!smt2::parser::parse_check_sat() Line 2622 C++ z3.exe!smt2::parser::parse_cmd() Line 2958 C++ z3.exe!smt2::parser::operator()() Line 3133 C++ z3.exe!parse_smt2_commands(cmd_context & ctx, std::basic_istream<char,std::char_traits > & is, bool interactive, const params_ref & ps, const char filename) Line 3181 C++ z3.exe!read_smtlib2_commands(const char file_name) Line 94 C++ z3.exe!main(int argc, char argv) Line 356 C++

[levnach]

I would like to add that the call above happens in between the calls to lar_solver::maximize_term(...).

[NikolajBjorner]

Instrumenting tracing indicates that v4 is (0,1) = epsilon and v5 is (1,-1) = 1 - epsilon. But the bound v4 + v5 <= 1 is non-strict so v5 can be improved to 1.

I added

std::ostream& lar_solver::print_values(std::ostream& out) const {
   for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
       const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[i];
       out << this->get_column_name(i) << " -> " << rp << "\n";
   }
   return out;

}

and called it from get_model.

[levnach]

As I see it from inside lar_solver the term to optimize is v5. If I increase v5 to 1 then v4 has to become at most 0, because of the v5 + v4 <= 1. However it is impossible because of the constraint that was not there at the first two calls and appeared in the third call, it is v4 > 0.

[NikolajBjorner]

lar_solver seems to expect "ext_j", the caller uses the internal variable:

        vi = m_theory_var2var_index[v];
        st = m_solver->maximize_term(vi, term_max);

So it should be changed to

        st = m_solver->maximize_term(v, term_max);

?

[levnach]

Yes, the fix is correct. And this sample works now. The concern expressed above, with the comment containing a stack, remains.