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

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-07-07 09:29:49 -07:00
parent 8c7525c97f ff875c936f
commit f450bc4ae0
5 changed files with 9 additions and 81 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1380,72 +1380,6 @@ namespace lp {
return m_mpq_lar_core_solver.column_is_free(j);
}
// column is at lower or upper bound, lower and upper bound are different.
// the lower/upper bound is not strict.
// the LP obtained by making the bound strict is infeasible
// -> the column has to be fixed
bool lar_solver::is_fixed_at_bound(column_index const& j, vector<std::tuple<explanation, column_index, bool, mpq>>& bounds) {
if (column_is_fixed(j))
return false;
mpq val;
if (!has_value(j, val))
return false;
lp::lconstraint_kind k;
if (column_has_upper_bound(j) &&
get_upper_bound(j).x == val) {
push();
k = column_is_int(j) ? LE : LT;
auto ci = mk_var_bound(j, k, column_is_int(j) ? val - 1 : val);
update_column_type_and_bound(j, k, column_is_int(j) ? val - 1 : val, ci);
auto st = find_feasible_solution();
bool infeasible = st == lp_status::INFEASIBLE;
if (infeasible) {
explanation exp;
get_infeasibility_explanation(exp);
unsigned_vector cis;
exp.remove(ci);
verbose_stream() << "tight upper bound " << j << " " << val << "\n";
bounds.push_back({exp, j, true, val});
}
pop(1);
return infeasible;
}
if (column_has_lower_bound(j) &&
get_lower_bound(j).x == val) {
push();
k = column_is_int(j) ? GE : GT;
auto ci = mk_var_bound(j, k, column_is_int(j) ? val + 1 : val);
update_column_type_and_bound(j, k, column_is_int(j) ? val + 1 : val, ci);
auto st = find_feasible_solution();
bool infeasible = st == lp_status::INFEASIBLE;
if (infeasible) {
explanation exp;
get_infeasibility_explanation(exp);
exp.remove(ci);
verbose_stream() << "tight lower bound " << j << " " << val << "\n";
bounds.push_back({exp, j, false, val});
}
pop(1);
return infeasible;
}
return false;
}
bool lar_solver::has_fixed_at_bound(vector<std::tuple<explanation, column_index, bool, mpq>>& bounds) {
verbose_stream() << "has-fixed-at-bound\n";
for (unsigned j = 0; j < A_r().m_columns.size(); ++j) {
auto ci = column_index(j);
if (is_fixed_at_bound(ci, bounds))
verbose_stream() << "fixed " << j << "\n";
}
verbose_stream() << "num fixed " << bounds.size() << "\n";
if (!bounds.empty())
find_feasible_solution();
return !bounds.empty();
}
// below is the initialization functionality of lar_solver
bool lar_solver::strategy_is_undecided() const {

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

@ -364,9 +364,6 @@ class lar_solver : public column_namer {
}
}
bool is_fixed_at_bound(column_index const& j, vector<std::tuple<explanation, column_index, bool, mpq>>& bounds);
bool has_fixed_at_bound(vector<std::tuple<explanation, column_index, bool, mpq>>& bounds);
bool is_fixed(column_index const& j) const { return column_is_fixed(j); }
inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); }
bool external_is_used(unsigned) const;
@ -396,10 +393,6 @@ class lar_solver : public column_namer {
m_mpq_lar_core_solver.m_r_solver.inf_heap().clear();
}
inline void remove_column_from_inf_set(unsigned j) {
m_mpq_lar_core_solver.m_r_solver.remove_column_from_inf_heap(j);
}
void pivot(int entering, int leaving) {
m_mpq_lar_core_solver.pivot(entering, leaving);
}

6
src/math/lp/lp_core_solver_base.h
View file

@ -55,7 +55,7 @@ private:
lp_status m_status;
public:
bool current_x_is_feasible() const {
TRACE("feas",
TRACE("feas_bug",
if (!m_inf_heap.empty()) {
tout << "column " << *m_inf_heap.begin() << " is infeasible" << std::endl;
print_column_info(*m_inf_heap.begin(), tout);
@ -572,13 +572,13 @@ public:
void insert_column_into_inf_heap(unsigned j) {
if (!m_inf_heap.contains(j)) {
m_inf_heap.insert(j);
TRACE("lar_solver", tout << "j = " << j << "\n";);
TRACE("lar_solver_inf_heap", tout << "insert into heap j = " << j << "\n";);
}
lp_assert(!column_is_feasible(j));
}
void remove_column_from_inf_heap(unsigned j) {
if (m_inf_heap.contains(j)) {
TRACE("lar_solver", tout << "j = " << j << "\n";);
TRACE("lar_solver_inf_heap", tout << "insert into heap j = " << j << "\n";);
m_inf_heap.erase(j);
}
lp_assert(column_is_feasible(j));

6
src/math/lp/lp_primal_core_solver.h
View file

@ -341,6 +341,7 @@ namespace lp {
int find_smallest_inf_column() {
if (this->inf_heap().empty())
return -1;
return this->inf_heap().min_value();
}
@ -393,7 +394,10 @@ namespace lp {
const X &new_val_for_leaving = get_val_for_leaving(leaving);
X theta = (this->m_x[leaving] - new_val_for_leaving) / a_ent;
this->m_x[leaving] = new_val_for_leaving;
this->remove_column_from_inf_heap(leaving);
// this will remove the leaving from the heap
TRACE("lar_solver_inf_heap", tout << "leaving = " << leaving
<< " removed from inf_heap()\n";);
this->inf_heap().erase_min();
advance_on_entering_and_leaving_tableau_rows(entering, leaving, theta);
if (this->current_x_is_feasible())
this->set_status(lp_status::OPTIMAL);

5
src/smt/theory_lra.cpp
View file

@ -1659,10 +1659,7 @@ public:
unsigned old_idx = m_final_check_idx;
switch (is_sat) {
case l_true:
TRACE("arith", display(tout));
// if (lp().has_fixed_at_bound()) // explain and propagate.
TRACE("arith", display(tout));
#if 0
m_dist.reset();
m_dist.push(0, 1);