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

fix column patching

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-02-07 12:14:45 -08:00
parent 8c016abb12
commit f45e17c47e
5 changed files with 40 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -450,28 +450,24 @@ void int_solver::set_value_for_nbasic_column_ignore_old_values(unsigned j, const
auto & x = m_lar_solver->m_mpq_lar_core_solver.m_r_x[j];
auto delta = new_val - x;
x = new_val;
TRACE("int_solver", tout << "x[" << j << "] = " << x << "\n";);
m_lar_solver->change_basic_columns_dependend_on_a_given_nb_column(j, delta);
}
void int_solver::patch_nbasic_column(unsigned j, bool patch_only_int_vals) {
void int_solver::patch_nbasic_column(unsigned j) {
auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
impq & val = lcs.m_r_x[j];
bool val_is_int = val.is_int();
if (patch_only_int_vals && !val_is_int)
return;
bool inf_l, inf_u;
impq l, u;
mpq m;
if (!get_freedom_interval_for_column(j, val_is_int, inf_l, l, inf_u, u, m)) {
if (!get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m)) {
return;
}
bool m_is_one = m.is_one();
if (m.is_one() && val_is_int) {
return;
}
bool val_is_int = value_is_int(j);
// check whether value of j is already a multiple of m.
if (val_is_int && (val.x / m).is_int()) {
if (val_is_int && (m_is_one || (val.x / m).is_int())) {
return;
}
TRACE("patch_int",
@ -506,7 +502,7 @@ lia_move int_solver::patch_nbasic_columns() {
settings().stats().m_patches++;
lp_assert(is_feasible());
for (unsigned j : m_lar_solver->m_mpq_lar_core_solver.m_r_nbasis) {
patch_nbasic_column(j, settings().m_int_patch_only_integer_values);
patch_nbasic_column(j);
}
lp_assert(is_feasible());
if (!has_inf_int()) {
@ -734,11 +730,12 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) {
}
}
bool int_solver::get_freedom_interval_for_column(unsigned j, bool val_is_int, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
auto & lcs = m_lar_solver->m_mpq_lar_core_solver;
if (lcs.m_r_heading[j] >= 0) // the basic var
return false;
TRACE("random_update", display_column(tout, j) << ", is_int = " << column_is_int(j) << "\n";);
impq const & xj = get_value(j);
inf_l = true;
@ -753,7 +750,6 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool val_is_int, bo
set_upper(u, inf_u, upper_bound(j) - xj);
}
mpq a; // the coefficient in the column
unsigned row_index;
lp_assert(settings().use_tableau());
const auto & A = m_lar_solver->A_r();
@ -762,11 +758,11 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool val_is_int, bo
row_index = c.var();
const mpq & a = c.coeff();
unsigned i = lcs.m_r_basis[row_index];
if (column_is_int(i) && column_is_int(j) && !a.is_int())
TRACE("random_update", tout << "i = " << i << ", a = " << a << "\n";);
if (!a.is_int())
m = lcm(m, denominator(a));
}
if (val_is_int && m.is_one())
return false;
TRACE("random_update", tout << "m = " << m << "\n";);
for (const auto &c : A.column(j)) {
if (!inf_l && !inf_u && l >= u) break;
@ -845,8 +841,9 @@ const impq & int_solver::get_value(unsigned j) const {
return m_lar_solver->m_mpq_lar_core_solver.m_r_x[j];
}
void int_solver::display_column(std::ostream & out, unsigned j) const {
std::ostream& int_solver::display_column(std::ostream & out, unsigned j) const {
m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_info(j, out);
return out;
}
bool int_solver::column_is_int_inf(unsigned j) const {
@ -928,6 +925,8 @@ unsigned int_solver::random() {
return m_lar_solver->get_core_solver().settings().random_next();
}
// at this point the
bool int_solver::shift_var(unsigned j, unsigned range) {
if (is_fixed(j) || is_base(j))
return false;
@ -935,55 +934,49 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
bool inf_l, inf_u;
impq l, u;
mpq m;
get_freedom_interval_for_column(j, false, inf_l, l, inf_u, u, m);
get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m);
const impq & x = get_value(j);
// x, the value of j column, might be shifted on a multiple of m
if (inf_l && inf_u) {
impq new_val = impq(random() % (range + 1));
impq new_val = m * impq(random() % (range + 1)) + x;
set_value_for_nbasic_column_ignore_old_values(j, new_val);
return true;
}
if (column_is_int(j)) {
if (!inf_l) {
l = impq(ceil(l));
if (!m.is_one())
l = impq(m*ceil(l/m));
}
if (!inf_u) {
u = impq(floor(u));
if (!m.is_one())
u = impq(m*floor(u/m));
}
}
if (!inf_l && !inf_u && l >= u)
return false;
if (inf_u) {
SASSERT(!inf_l);
impq delta = impq(random() % (range + 1));
impq new_val = l + m*delta;
impq new_val = x + m * impq(random() % (range + 1));
set_value_for_nbasic_column_ignore_old_values(j, new_val);
return true;
}
if (inf_l) {
SASSERT(!inf_u);
impq delta = impq(random() % (range + 1));
impq new_val = u - m*delta;
set_value_for_nbasic_column_ignore_old_values(j, new_val);
return true;
}
if (!column_is_int(j)) {
SASSERT(!inf_l && !inf_u);
mpq delta = mpq(random() % (range + 1));
impq new_val = l + ((delta * (u - l)) / mpq(range));
set_value_for_nbasic_column_ignore_old_values(j, new_val);
return true;
}
else {
mpq r = (u.x - l.x) / m;
if (r < mpq(range))
range = static_cast<unsigned>(r.get_uint64());
impq new_val = l + m * (impq(random() % (range + 1)));
impq new_val = x - m * impq(random() % (range + 1));
set_value_for_nbasic_column_ignore_old_values(j, new_val);
return true;
}
SASSERT(!inf_l && !inf_u);
mpq r = floor((u.x - l.x) / m);
if (r < mpq(range)) range = static_cast<unsigned>(r.get_uint64());
// the interval contains at least range multiples of m.
// the number of multiples to the left of the value of j is floor((get_value(j) - l.x)/m)
// shift either left or right of the current value by available multiples.
impq shift = impq(random() % (range + 1)) - impq(floor(x.x - l.x) / m);
impq new_val = x + m * shift;
SASSERT(l <= new_val && new_val <= u);
set_value_for_nbasic_column_ignore_old_values(j, new_val); return true;
}
bool int_solver::non_basic_columns_are_at_bounds() const {

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

@ -88,7 +88,7 @@ private:
void fill_explanation_from_fixed_columns(const row_strip<mpq> & row);
void add_to_explanation_from_fixed_or_boxed_column(unsigned j);
lia_move patch_nbasic_columns();
bool get_freedom_interval_for_column(unsigned j, bool val_is_int, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m);
bool get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m);
private:
bool is_boxed(unsigned j) const;
bool is_fixed(unsigned j) const;
@ -121,7 +121,7 @@ private:
unsigned row_of_basic_column(unsigned j) const;
public:
void display_column(std::ostream & out, unsigned j) const;
std::ostream& display_column(std::ostream & out, unsigned j) const;
constraint_index column_upper_bound_constraint(unsigned j) const;
constraint_index column_lower_bound_constraint(unsigned j) const;
bool current_solution_is_inf_on_cut() const;
@ -152,6 +152,6 @@ public:
void try_add_term_to_A_for_hnf(unsigned term_index);
bool hnf_has_var_with_non_integral_value() const;
bool hnf_cutter_is_full() const;
void patch_nbasic_column(unsigned j, bool patch_only_int_vals);
void patch_nbasic_column(unsigned j);
};
}

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

@ -612,7 +612,7 @@ lp_status lar_solver::maximize_term(unsigned j_or_term,
return lp_status::FEASIBLE; // it should not happen
}
}
m_int_solver->patch_nbasic_column(j, false);
m_int_solver->patch_nbasic_column(j);
if (!column_value_is_integer(j)) {
term_max = prev_value;
m_mpq_lar_core_solver.m_r_x = backup;

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

@ -196,7 +196,6 @@ private:
public:
bool m_int_run_gcd_test;
bool m_int_pivot_fixed_vars_from_basis;
bool m_int_patch_only_integer_values;
unsigned limit_on_rows_for_hnf_cutter;
unsigned limit_on_columns_for_hnf_cutter;
bool m_enable_hnf;
@ -268,7 +267,6 @@ public:
m_hnf_cut_period(4),
m_int_run_gcd_test(true),
m_int_pivot_fixed_vars_from_basis(false),
m_int_patch_only_integer_values(true),
limit_on_rows_for_hnf_cutter(75),
limit_on_columns_for_hnf_cutter(150),
m_enable_hnf(true),

9
src/math/lp/random_updater_def.h
View file

@ -39,13 +39,6 @@ bool random_updater::shift_var(unsigned v) {
return m_lar_solver.get_int_solver()->shift_var(v, m_range);
}
bool random_updater::random_shift_var(unsigned j) {
if (m_lar_solver.A_r().m_columns.size() >= 50) {
return false;
}
return shift_var(j);
}
void random_updater::update() {
for (auto j : m_var_set) {
@ -53,7 +46,7 @@ void random_updater::update() {
break; // we are done
}
auto old_x = m_lar_solver.get_column_value(j);
if (random_shift_var(j)) {
if (shift_var(j)) {
remove_value(old_x);
add_value(m_lar_solver.get_column_value(j));
}