mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 11:58:31 +00:00
Code Activity

delete remove_fixed_vars_from_base() from

Browse source 
int_solver
This commit is contained in:
Lev Nachmanson 2023-08-05 09:31:55 -10:00 • committed by Lev Nachmanson
parent c3a373e225
commit 0fbf8f92f5
3 changed files with 4 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -18,22 +18,6 @@ namespace lp {
lrac(lia.lrac) lrac(lia.lrac)
{} {}
void int_solver::patcher::remove_fixed_vars_from_base() {
unsigned num = lra.A_r().column_count();
for (unsigned v = 0; v < num; v++) {
if (!lia.is_base(v) || !lia.is_fixed(v))
continue;
auto const & r = lra.basic2row(v);
for (auto const& c : r) {
if (c.var() != v && !lia.is_fixed(c.var())) {
lra.pivot(c.var(), v);
break;
}
}
}
}
unsigned int_solver::patcher::count_non_int() { unsigned int_solver::patcher::count_non_int() {
unsigned non_int = 0; unsigned non_int = 0;
for (auto j : lra.r_basis()) for (auto j : lra.r_basis())
@ -43,22 +27,12 @@ namespace lp {
} }
lia_move int_solver::patcher::patch_basic_columns() { lia_move int_solver::patcher::patch_basic_columns() {
remove_fixed_vars_from_base();
lia.settings().stats().m_patches++; lia.settings().stats().m_patches++;
lra.remove_fixed_vars_from_base();
lp_assert(lia.is_feasible()); lp_assert(lia.is_feasible());
// unsigned non_int_before, non_int_after;
// non_int_before = count_non_int();
// unsigned num = lra.A_r().column_count();
for (unsigned j : lra.r_basis()) for (unsigned j : lra.r_basis())
if (!lra.get_value(j).is_int()) if (!lra.get_value(j).is_int())
patch_basic_column(j); patch_basic_column(j);
// non_int_after = count_non_int();
// verbose_stream() << non_int_before << " -> " << non_int_after << "\n";
if (!lia.has_inf_int()) { if (!lia.has_inf_int()) {
lia.settings().stats().m_patches_success++; lia.settings().stats().m_patches_success++;
return lia_move::sat; return lia_move::sat;
@ -177,7 +151,6 @@ namespace lp {
} }
int_solver::int_solver(lar_solver& lar_slv) : int_solver::int_solver(lar_solver& lar_slv) :
lra(lar_slv), lra(lar_slv),
lrac(lra.m_mpq_lar_core_solver), lrac(lra.m_mpq_lar_core_solver),

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

@ -52,13 +52,12 @@ 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(); }
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:
bool patch_basic_column_on_row_cell(unsigned v, row_cell<mpq> const& c);
lia_move patch_basic_columns(); lia_move patch_basic_columns();
void remove_fixed_vars_from_base();
}; };
lar_solver& lra; lar_solver& lra;

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

@ -333,8 +333,9 @@ class lar_solver : public column_namer {
void add_column_rows_to_touched_rows(lpvar j); void add_column_rows_to_touched_rows(lpvar j);
template <typename T> template <typename T>
void propagate_bounds_for_touched_rows(lp_bound_propagator<T>& bp) { void propagate_bounds_for_touched_rows(lp_bound_propagator<T>& bp) {
remove_fixed_vars_from_base();
if (settings().propagate_eqs()) { if (settings().propagate_eqs()) {
if (settings().random_next() % 10 == 0)
remove_fixed_vars_from_base();
bp.clear_for_eq(); bp.clear_for_eq();
for (unsigned i : m_touched_rows) { for (unsigned i : m_touched_rows) {
unsigned offset_eqs = stats().m_offset_eqs; unsigned offset_eqs = stats().m_offset_eqs;