mirror of
https://github.com/Z3Prover/z3
synced 2025-07-25 13:47:01 +00:00
remove dead code
This commit is contained in:
parent
1c907e8d09
commit
4e327babda
3 changed files with 1 additions and 73 deletions
|
@ -1380,72 +1380,6 @@ namespace lp {
|
||||||
return m_mpq_lar_core_solver.column_is_free(j);
|
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
|
// below is the initialization functionality of lar_solver
|
||||||
|
|
||||||
bool lar_solver::strategy_is_undecided() const {
|
bool lar_solver::strategy_is_undecided() const {
|
||||||
|
|
|
@ -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); }
|
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)); }
|
inline column_index to_column_index(unsigned v) const { return column_index(external_to_column_index(v)); }
|
||||||
bool external_is_used(unsigned) const;
|
bool external_is_used(unsigned) const;
|
||||||
|
|
|
@ -1659,10 +1659,7 @@ public:
|
||||||
unsigned old_idx = m_final_check_idx;
|
unsigned old_idx = m_final_check_idx;
|
||||||
switch (is_sat) {
|
switch (is_sat) {
|
||||||
case l_true:
|
case l_true:
|
||||||
TRACE("arith", display(tout));
|
TRACE("arith", display(tout));
|
||||||
|
|
||||||
// if (lp().has_fixed_at_bound()) // explain and propagate.
|
|
||||||
|
|
||||||
#if 0
|
#if 0
|
||||||
m_dist.reset();
|
m_dist.reset();
|
||||||
m_dist.push(0, 1);
|
m_dist.push(0, 1);
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue