mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
commit
db679d702f
|
@ -50,7 +50,6 @@ public:
|
|||
// main function to check that the solution provided by lar_solver is valid for integral values,
|
||||
// or provide a way of how it can be adjusted.
|
||||
lia_move check(lar_term& t, mpq& k, explanation& ex, bool & upper);
|
||||
lia_move check_(lar_term& t, mpq& k, explanation& ex, bool & upper);
|
||||
bool move_non_basic_column_to_bounds(unsigned j);
|
||||
lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex);
|
||||
bool is_base(unsigned j) const;
|
||||
|
|
|
@ -542,8 +542,11 @@ lp_status lar_solver::maximize_term(unsigned ext_j,
|
|||
return lp_status::FEASIBLE; // it should not happen
|
||||
}
|
||||
m_int_solver->patch_nbasic_column(j, false);
|
||||
if (!column_value_is_integer(j))
|
||||
if (!column_value_is_integer(j)) {
|
||||
term_max = prev_value;
|
||||
m_mpq_lar_core_solver.m_r_x = backup;
|
||||
return lp_status::FEASIBLE;
|
||||
}
|
||||
change = true;
|
||||
}
|
||||
if (change) {
|
||||
|
|
|
@ -28,4 +28,25 @@ enum class lia_move {
|
|||
undef,
|
||||
unsat
|
||||
};
|
||||
inline std::string lia_move_to_string(lia_move m) {
|
||||
switch (m) {
|
||||
case lia_move::sat:
|
||||
return "sat";
|
||||
case lia_move::branch:
|
||||
return "branch";
|
||||
case lia_move::cut:
|
||||
return "cut";
|
||||
case lia_move::conflict:
|
||||
return "conflict";
|
||||
case lia_move::continue_with_check:
|
||||
return "continue_with_check";
|
||||
case lia_move::undef:
|
||||
return "undef";
|
||||
case lia_move::unsat:
|
||||
return "unsat";
|
||||
default:
|
||||
lp_assert(false);
|
||||
};
|
||||
return "strange";
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue