mirror of
https://github.com/Z3Prover/z3
synced 2025-06-28 17:08:45 +00:00
remove dead code
This commit is contained in:
Nikolaj Bjorner
parent
dd0b0b47b8
commit
125787c458
4 changed files with 1 additions and 175 deletions
|
|
@ -176,174 +176,7 @@ namespace lp {
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
|
||||||
lia_move int_solver::patcher::patch_nbasic_columns() {
|
|
||||||
remove_fixed_vars_from_base();
|
|
||||||
lia.settings().stats().m_patches++;
|
|
||||||
lp_assert(lia.is_feasible());
|
|
||||||
m_patch_success = 0;
|
|
||||||
m_patch_fail = 0;
|
|
||||||
m_num_ones = 0;
|
|
||||||
m_num_divides = 0;
|
|
||||||
//unsigned non_int_before = count_non_int();
|
|
||||||
|
|
||||||
unsigned num = lra.A_r().column_count();
|
|
||||||
for (unsigned v = 0; v < num; v++) {
|
|
||||||
if (lia.is_base(v))
|
|
||||||
continue;
|
|
||||||
patch_nbasic_column(v);
|
|
||||||
}
|
|
||||||
unsigned num_fixed = 0;
|
|
||||||
for (unsigned v = 0; v < num; v++)
|
|
||||||
if (lia.is_fixed(v))
|
|
||||||
++num_fixed;
|
|
||||||
|
|
||||||
lp_assert(lia.is_feasible());
|
|
||||||
//verbose_stream() << "patch " << m_patch_success << " fails " << m_patch_fail << " ones " << m_num_ones << " divides " << m_num_divides << " num fixed " << num_fixed << "\n";
|
|
||||||
//lra.display(verbose_stream());
|
|
||||||
//exit(0);
|
|
||||||
//unsigned non_int_after = count_non_int();
|
|
||||||
|
|
||||||
// verbose_stream() << non_int_before << " -> " << non_int_after << "\n";
|
|
||||||
if (!lia.has_inf_int()) {
|
|
||||||
lia.settings().stats().m_patches_success++;
|
|
||||||
return lia_move::sat;
|
|
||||||
}
|
|
||||||
return lia_move::undef;
|
|
||||||
}
|
|
||||||
|
|
||||||
void int_solver::patcher::patch_nbasic_column(unsigned j) {
|
|
||||||
impq & val = lrac.m_r_x[j];
|
|
||||||
bool inf_l, inf_u;
|
|
||||||
impq l, u;
|
|
||||||
mpq m;
|
|
||||||
bool has_free = lia.get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m);
|
|
||||||
if (!has_free)
|
|
||||||
return;
|
|
||||||
bool m_is_one = m.is_one();
|
|
||||||
bool val_is_int = lia.value_is_int(j);
|
|
||||||
|
|
||||||
#if 0
|
|
||||||
const auto & A = lra.A_r();
|
|
||||||
#endif
|
|
||||||
// check whether value of j is already a multiple of m.
|
|
||||||
if (val_is_int && (m_is_one || (val.x / m).is_int())) {
|
|
||||||
if (m_is_one)
|
|
||||||
++m_num_ones;
|
|
||||||
else
|
|
||||||
++m_num_divides;
|
|
||||||
#if 0
|
|
||||||
for (auto c : A.column(j)) {
|
|
||||||
unsigned row_index = c.var();
|
|
||||||
unsigned i = lrac.m_r_basis[row_index];
|
|
||||||
if (!lia.get_value(i).is_int() ||
|
|
||||||
(lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) ||
|
|
||||||
(lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) {
|
|
||||||
verbose_stream() << "skip " << j << " " << m << ": ";
|
|
||||||
lia.display_row(verbose_stream(), A.m_rows[row_index]);
|
|
||||||
verbose_stream() << "\n";
|
|
||||||
}
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
|
|
||||||
#if 0
|
|
||||||
if (!m_is_one) {
|
|
||||||
// lia.display_column(verbose_stream(), j);
|
|
||||||
for (auto c : A.column(j)) {
|
|
||||||
continue;
|
|
||||||
unsigned row_index = c.var();
|
|
||||||
lia.display_row(verbose_stream(), A.m_rows[row_index]);
|
|
||||||
verbose_stream() << "\n";
|
|
||||||
}
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
|
|
||||||
TRACE("patch_int",
|
|
||||||
tout << "TARGET j" << j << " -> [";
|
|
||||||
if (inf_l) tout << "-oo"; else tout << l;
|
|
||||||
tout << ", ";
|
|
||||||
if (inf_u) tout << "oo"; else tout << u;
|
|
||||||
tout << "]";
|
|
||||||
tout << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";);
|
|
||||||
|
|
||||||
#if 0
|
|
||||||
verbose_stream() << "path " << m << " ";
|
|
||||||
if (!inf_l) verbose_stream() << "infl " << l.x << " ";
|
|
||||||
if (!inf_u) verbose_stream() << "infu " << u.x << " ";
|
|
||||||
verbose_stream() << "\n";
|
|
||||||
if (m.is_big() || (!inf_l && l.x.is_big()) || (!inf_u && u.x.is_big())) {
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
|
|
||||||
#if 0
|
|
||||||
verbose_stream() << "TARGET v" << j << " -> [";
|
|
||||||
if (inf_l) verbose_stream() << "-oo"; else verbose_stream() << ceil(l.x) << " " << l << "\n";
|
|
||||||
verbose_stream() << ", ";
|
|
||||||
if (inf_u) verbose_stream() << "oo"; else verbose_stream() << floor(u.x) << " " << u << "\n";
|
|
||||||
verbose_stream() << "]";
|
|
||||||
verbose_stream() << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";
|
|
||||||
#endif
|
|
||||||
|
|
||||||
#if 0
|
|
||||||
if (!inf_l)
|
|
||||||
l = impq(ceil(l));
|
|
||||||
if (!inf_u)
|
|
||||||
u = impq(floor(u));
|
|
||||||
#endif
|
|
||||||
|
|
||||||
if (!inf_l) {
|
|
||||||
l = impq(m_is_one ? ceil(l) : m * ceil(l / m));
|
|
||||||
if (inf_u || l <= u) {
|
|
||||||
TRACE("patch_int", tout << "patching with l: " << l << '\n';);
|
|
||||||
lra.set_value_for_nbasic_column(j, l);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
//verbose_stream() << "fail: " << j << " " << m << "\n";
|
|
||||||
++m_patch_fail;
|
|
||||||
TRACE("patch_int", tout << "not patching " << l << "\n";);
|
|
||||||
#if 0
|
|
||||||
verbose_stream() << "not patched\n";
|
|
||||||
for (auto c : A.column(j)) {
|
|
||||||
unsigned row_index = c.var();
|
|
||||||
unsigned i = lrac.m_r_basis[row_index];
|
|
||||||
if (!lia.get_value(i).is_int() ||
|
|
||||||
(lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) ||
|
|
||||||
(lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) {
|
|
||||||
lia.display_row(verbose_stream(), A.m_rows[row_index]);
|
|
||||||
verbose_stream() << "\n";
|
|
||||||
}
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else if (!inf_u) {
|
|
||||||
u = impq(m_is_one ? floor(u) : m * floor(u / m));
|
|
||||||
lra.set_value_for_nbasic_column(j, u);
|
|
||||||
TRACE("patch_int", tout << "patching with u: " << u << '\n';);
|
|
||||||
}
|
|
||||||
else {
|
|
||||||
lra.set_value_for_nbasic_column(j, impq(0));
|
|
||||||
TRACE("patch_int", tout << "patching with 0\n";);
|
|
||||||
}
|
|
||||||
++m_patch_success;
|
|
||||||
#if 0
|
|
||||||
verbose_stream() << "patched " << j << "\n";
|
|
||||||
for (auto c : A.column(j)) {
|
|
||||||
unsigned row_index = c.var();
|
|
||||||
unsigned i = lrac.m_r_basis[row_index];
|
|
||||||
if (!lia.get_value(i).is_int() ||
|
|
||||||
(lia.has_lower(i) && lia.get_value(i) < lra.get_lower_bound(i)) ||
|
|
||||||
(lia.has_upper(i) && lia.get_value(i) > lra.get_upper_bound(i))) {
|
|
||||||
lia.display_row(verbose_stream(), A.m_rows[row_index]);
|
|
||||||
verbose_stream() << "\n";
|
|
||||||
}
|
|
||||||
}
|
|
||||||
#endif
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
int_solver::int_solver(lar_solver& lar_slv) :
|
int_solver::int_solver(lar_solver& lar_slv) :
|
||||||
lra(lar_slv),
|
lra(lar_slv),
|
||||||
|
|
|
||||||
|
|
@ -52,15 +52,13 @@ class int_solver {
|
||||||
patcher(int_solver& lia);
|
patcher(int_solver& lia);
|
||||||
bool should_apply() const { return true; }
|
bool should_apply() const { return true; }
|
||||||
lia_move operator()() { return patch_basic_columns(); }
|
lia_move operator()() { return patch_basic_columns(); }
|
||||||
void patch_nbasic_column(unsigned j);
|
|
||||||
bool patch_basic_column_on_row_cell(unsigned v, row_cell<mpq> const& c);
|
bool patch_basic_column_on_row_cell(unsigned v, row_cell<mpq> const& c);
|
||||||
void patch_basic_column(unsigned j);
|
void patch_basic_column(unsigned j);
|
||||||
bool try_patch_column(unsigned v, unsigned j, mpq const& delta);
|
bool try_patch_column(unsigned v, unsigned j, mpq const& delta);
|
||||||
unsigned count_non_int();
|
unsigned count_non_int();
|
||||||
private:
|
private:
|
||||||
void remove_fixed_vars_from_base();
|
|
||||||
lia_move patch_nbasic_columns();
|
|
||||||
lia_move patch_basic_columns();
|
lia_move patch_basic_columns();
|
||||||
|
void remove_fixed_vars_from_base();
|
||||||
};
|
};
|
||||||
|
|
||||||
lar_solver& lra;
|
lar_solver& lra;
|
||||||
|
|
@ -134,7 +132,6 @@ public:
|
||||||
bool all_columns_are_bounded() const;
|
bool all_columns_are_bounded() const;
|
||||||
void find_feasible_solution();
|
void find_feasible_solution();
|
||||||
lia_move hnf_cut();
|
lia_move hnf_cut();
|
||||||
void patch_nbasic_column(unsigned j) { m_patcher.patch_nbasic_column(j); }
|
|
||||||
|
|
||||||
int select_int_infeasible_var();
|
int select_int_infeasible_var();
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -534,7 +534,6 @@ namespace lp {
|
||||||
return lp_status::FEASIBLE; // it should not happen
|
return lp_status::FEASIBLE; // it should not happen
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
m_int_solver->patch_nbasic_column(j);
|
|
||||||
if (!column_value_is_integer(j)) {
|
if (!column_value_is_integer(j)) {
|
||||||
term_max = prev_value;
|
term_max = prev_value;
|
||||||
m_mpq_lar_core_solver.m_r_x = backup;
|
m_mpq_lar_core_solver.m_r_x = backup;
|
||||||
|
|
|
||||||
|
|
@ -1639,9 +1639,6 @@ public:
|
||||||
return FC_GIVEUP;
|
return FC_GIVEUP;
|
||||||
}
|
}
|
||||||
|
|
||||||
unsigned m_final_check_idx = 0;
|
|
||||||
distribution m_dist { 0 };
|
|
||||||
|
|
||||||
final_check_status final_check_eh() {
|
final_check_status final_check_eh() {
|
||||||
if (propagate_core())
|
if (propagate_core())
|
||||||
return FC_CONTINUE;
|
return FC_CONTINUE;
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue