mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

use more descriptive functions than casting comparisons

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-03-19 21:03:36 -10:00 committed by Lev Nachmanson
parent 7fb40e86eb
commit 29c5c20267
2 changed files with 9 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/math/lp/dioph_eq.cpp
View file

@ -1801,12 +1801,12 @@ namespace lp {
lp_status st = lra.find_feasible_solution(); lp_status st = lra.find_feasible_solution();
if (st == lp_status::CANCELLED) if (st == lp_status::CANCELLED)
return false; return false;
if ((int)st >= (int)lp::lp_status::FEASIBLE) if (lp::is_sat(st))
return false; return false;
lra.get_infeasibility_explanation(m_infeas_explanation); lra.get_infeasibility_explanation(m_infeas_explanation);
return true; return true;
} }
// returns true only on a conflict // returns true only on a conflict
bool tighten_bound_kind(const mpq& g, unsigned j, const mpq& ub, bool upper) { bool tighten_bound_kind(const mpq& g, unsigned j, const mpq& ub, bool upper) {
@ -1840,10 +1840,8 @@ namespace lp {
lra.update_column_type_and_bound(j, kind, bound, dep); lra.update_column_type_and_bound(j, kind, bound, dep);
lp_status st = lra.find_feasible_solution(); lp_status st = lra.find_feasible_solution();
if ((int)st >= (int)lp::lp_status::FEASIBLE) { if (is_sat(st) || st == lp::lp_status::CANCELLED)
return false; return false;
}
if (st == lp_status::CANCELLED) return false;
lra.get_infeasibility_explanation(m_infeas_explanation); lra.get_infeasibility_explanation(m_infeas_explanation);
return true; return true;
} }
@ -2069,7 +2067,7 @@ namespace lp {
TRACE("dio_br", tout << "st:" << lp_status_to_string(st) << std::endl;); TRACE("dio_br", tout << "st:" << lp_status_to_string(st) << std::endl;);
if (st == lp_status::CANCELLED) if (st == lp_status::CANCELLED)
return lia_move::undef; return lia_move::undef;
else if ((int)st >= (int)(lp_status::FEASIBLE)) { else if (lp::is_sat(st)) {
// have a feasible solution // have a feasible solution
unsigned n_of_ii = get_number_of_int_inf(); unsigned n_of_ii = get_number_of_int_inf();
TRACE("dio_br", tout << "n_of_ii:" << n_of_ii << "\n";); TRACE("dio_br", tout << "n_of_ii:" << n_of_ii << "\n";);

7
src/math/lp/lp_settings.h
View file

@ -74,11 +74,14 @@ enum class lp_status {
OPTIMAL OPTIMAL
}; };
inline bool is_sat(lp_status st) {
return st == lp_status::FEASIBLE || st == lp_status::OPTIMAL;
}
// when the ratio of the vector length to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only // when the ratio of the vector length to domain size to is greater than the return value we switch to solve_By_for_T_indexed_only
template <typename X> template <typename X>
unsigned ratio_of_index_size_to_all_size() { unsigned ratio_of_index_size_to_all_size() {
return 10; return 10;
} }
const char* lp_status_to_string(lp_status status); const char* lp_status_to_string(lp_status status);