mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Handle correctly cancelled run (#5695)

Browse source 
* remove the bound on total iterations in simplex

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* remove unncesseray checks in  get_freedom_interval_for_column()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix the build of test-z3

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* Revert "remove unncesseray checks in  get_freedom_interval_for_column()"

This reverts commit 6770ed85e3.

* optimize get_freedom_interval_for_column() for feasible case

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* add function lar_solver::status_feasible

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* rename status_is_feasible() to is_feasible()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

* fix the linux build

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2021-12-05 16:38:37 -10:00 • committed by GitHub
parent 0242566792
commit 7758b519bc
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
13 changed files with 55 additions and 72 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/int_solver.cpp
View file

@ -324,6 +324,7 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) {
}
}
// this function assumes that all basic columns dependend on j are feasible
bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
if (lrac.m_r_heading[j] >= 0) // the basic var
return false;
@ -360,13 +361,12 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
const mpq & a = c.coeff();
unsigned i = lrac.m_r_basis[row_index];
impq const & xi = get_value(i);
lp_assert(lrac.m_r_solver.column_is_feasible(i));
if (column_is_int(i) && !a.is_int())
m = lcm(m, denominator(a));
if (!inf_l && !inf_u) {
if (l > u)
break;
if (l == u)
continue;
}

12
src/math/lp/lar_core_solver_def.h
View file

@ -179,11 +179,17 @@ void lar_core_solver::solve() {
}
lp_assert(!settings().use_tableau() || r_basis_is_OK());
}
if (m_r_solver.get_status() == lp_status::INFEASIBLE) {
switch (m_r_solver.get_status())
{
case lp_status::INFEASIBLE:
fill_not_improvable_zero_sum();
}
else if (m_r_solver.get_status() != lp_status::UNBOUNDED) {
break;
case lp_status::CANCELLED:
case lp_status::UNBOUNDED: // do nothing in these cases
break;
default: // adjust the status to optimal
m_r_solver.set_status(lp_status::OPTIMAL);
break;
}
lp_assert(r_basis_is_OK());
lp_assert(m_r_solver.non_basic_columns_are_set_correctly());

12
src/math/lp/lar_solver.cpp
View file

@ -798,6 +798,18 @@ namespace lp {
}
// this function just looks at the status
bool lar_solver::is_feasible() const {
switch (this->get_status()) {
case lp_status::OPTIMAL:
case lp_status::FEASIBLE:
case lp_status::UNBOUNDED:
return true;
default:
return false;
}
}
numeric_pair<mpq> lar_solver::get_basic_var_value_from_row(unsigned i) {
numeric_pair<mpq> r = zero_of_type<numeric_pair<mpq>>();

2
src/math/lp/lar_solver.h
View file

@ -296,6 +296,8 @@ class lar_solver : public column_namer {
mutable mpq m_delta;
public:
// this function just looks at the status
bool is_feasible() const;
const map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>>& fixed_var_table_int() const {
return m_fixed_var_table_int;
}

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

@ -100,10 +100,7 @@ template <typename T, typename X> bool lp_dual_core_solver<T, X>::done() {
if (this->get_status() == lp_status::OPTIMAL) {
return true;
}
if (this->total_iterations() > this->m_settings.max_total_number_of_iterations) { // debug !!!!
this->set_status(lp_status::ITERATIONS_EXHAUSTED);
return true;
}
return false; // todo, need to be more cases
}
@ -747,6 +744,6 @@ template <typename T, typename X> void lp_dual_core_solver<T, X>::solve() { // s
one_iteration();
} while (this->get_status() != lp_status::FLOATING_POINT_ERROR && this->get_status() != lp_status::DUAL_UNBOUNDED && this->get_status() != lp_status::OPTIMAL &&
this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
&& this->total_iterations() <= this->m_settings.max_total_number_of_iterations);
);
}
}

3
src/math/lp/lp_dual_simplex_def.h
View file

@ -31,9 +31,6 @@ template <typename T, typename X> void lp_dual_simplex<T, X>::decide_on_status_a
break;
case lp_status::DUAL_UNBOUNDED:
lp_unreachable();
case lp_status::ITERATIONS_EXHAUSTED:
this->m_status = lp_status::ITERATIONS_EXHAUSTED;
break;
case lp_status::TIME_EXHAUSTED:
this->m_status = lp_status::TIME_EXHAUSTED;
break;

8
src/math/lp/lp_primal_core_solver_def.h
View file

@ -956,8 +956,6 @@ template <typename T, typename X> unsigned lp_primal_core_solver<T, X>::solve()
&&
this->iters_with_no_cost_growing() <= this->m_settings.max_number_of_iterations_with_no_improvements
&&
this->total_iterations() <= this->m_settings.max_total_number_of_iterations
&&
!(this->current_x_is_feasible() && this->m_look_for_feasible_solution_only));
lp_assert(this->get_status() == lp_status::FLOATING_POINT_ERROR
@ -1097,10 +1095,8 @@ template <typename T, typename X> bool lp_primal_core_solver<T, X>::done() {
return true;
}
if (this->m_iters_with_no_cost_growing >= this->m_settings.max_number_of_iterations_with_no_improvements) {
this->get_status() = lp_status::ITERATIONS_EXHAUSTED; return true;
}
if (this->total_iterations() >= this->m_settings.max_total_number_of_iterations) {
this->get_status() = lp_status::ITERATIONS_EXHAUSTED; return true;
this->set_status(lp_status::CANCELLED);
return true;
}
return false;
}

4
src/math/lp/lp_primal_core_solver_tableau_def.h
View file

@ -182,9 +182,7 @@ unsigned lp_primal_core_solver<T, X>::solve_with_tableau() {
if (this->m_settings.get_cancel_flag()
||
this->iters_with_no_cost_growing() > this->m_settings.max_number_of_iterations_with_no_improvements
||
this->total_iterations() > this->m_settings.max_total_number_of_iterations
) {
) {
this->set_status(lp_status::CANCELLED);
break; // from the loop
}

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

@ -71,7 +71,6 @@ enum class lp_status {
FEASIBLE,
FLOATING_POINT_ERROR,
TIME_EXHAUSTED,
ITERATIONS_EXHAUSTED,
EMPTY,
UNSTABLE,
CANCELLED
@ -210,7 +209,6 @@ public:
double harris_feasibility_tolerance { 1e-7 }; // page 179 of Istvan Maros
double ignore_epsilon_of_harris { 10e-5 };
unsigned max_number_of_iterations_with_no_improvements { 2000000 };
unsigned max_total_number_of_iterations { 20000000 };
double time_limit; // the maximum time limit of the total run time in seconds
// dual section
double dual_feasibility_tolerance { 1e-7 }; // page 71 of the PhD thesis of Achim Koberstein

2
src/math/lp/lp_settings_def.h
View file

@ -45,7 +45,6 @@ const char* lp_status_to_string(lp_status status) {
case lp_status::FEASIBLE: return "FEASIBLE";
case lp_status::FLOATING_POINT_ERROR: return "FLOATING_POINT_ERROR";
case lp_status::TIME_EXHAUSTED: return "TIME_EXHAUSTED";
case lp_status::ITERATIONS_EXHAUSTED: return "ITERATIONS_EXHAUSTED";
case lp_status::EMPTY: return "EMPTY";
case lp_status::UNSTABLE: return "UNSTABLE";
default:
@ -62,7 +61,6 @@ lp_status lp_status_from_string(std::string status) {
if (status == "FEASIBLE") return lp_status::FEASIBLE;
if (status == "FLOATING_POINT_ERROR") return lp_status::FLOATING_POINT_ERROR;
if (status == "TIME_EXHAUSTED") return lp_status::TIME_EXHAUSTED;
if (status == "ITERATIONS_EXHAUSTED") return lp_status::ITERATIONS_EXHAUSTED;
if (status == "EMPTY") return lp_status::EMPTY;
lp_unreachable();
return lp_status::UNKNOWN; // it is unreachable

8
src/math/lp/lp_solver.h
View file

@ -158,13 +158,7 @@ public:
m_settings.time_limit = time_limit_in_seconds;
}
void set_max_iterations_per_stage(unsigned max_iterations) {
m_settings.max_total_number_of_iterations = max_iterations;
}
unsigned get_max_iterations_per_stage() const {
return m_settings.max_total_number_of_iterations;
}
protected:
bool problem_is_empty();