mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
debugging cuts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
b7ec4489a6
commit
1e6d2fbbdc
|
@ -388,16 +388,12 @@ int gomory::find_basic_var() {
|
|||
int result = -1;
|
||||
unsigned n = 0;
|
||||
unsigned min_row_size = UINT_MAX;
|
||||
#if 0
|
||||
bool boxed = false;
|
||||
mpq min_range;
|
||||
#endif
|
||||
|
||||
|
||||
// Prefer smaller row size
|
||||
// Prefer boxed to non-boxed
|
||||
// Prefer smaller ranges
|
||||
|
||||
|
||||
for (unsigned j : lra.r_basis()) {
|
||||
if (!lia.column_is_int_inf(j))
|
||||
continue;
|
||||
|
@ -405,28 +401,7 @@ int gomory::find_basic_var() {
|
|||
if (!is_gomory_cut_target(row))
|
||||
continue;
|
||||
|
||||
#if 0
|
||||
if (is_boxed(j) && (min_row_size == UINT_MAX || 4*row.size() < 5*min_row_size)) {
|
||||
lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
|
||||
auto new_range = lclia.m_r_upper_bounds()[j].x - lclia.m_r_lower_bounds()[j].x;
|
||||
if (!boxed) {
|
||||
result = j;
|
||||
n = 1;
|
||||
min_row_size = row.size();
|
||||
boxed = true;
|
||||
min_range = new_range;
|
||||
continue;
|
||||
}
|
||||
if (min_range > 2*new_range || ((5*min_range > 4*new_range && (random() % (++n)) == 0))) {
|
||||
result = j;
|
||||
n = 1;
|
||||
min_row_size = row.size();
|
||||
min_range = std::min(min_range, new_range);
|
||||
continue;
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
IF_VERBOSE(20, lia.display_row_info(verbose_stream(), lia.row_of_basic_column(j)));
|
||||
if (min_row_size == UINT_MAX ||
|
||||
2*row.size() < min_row_size ||
|
||||
(4*row.size() < 5*min_row_size && lia.random() % (++n) == 0)) {
|
||||
|
|
|
@ -486,6 +486,19 @@ std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_inde
|
|||
auto & rslv = lrac.m_r_solver;
|
||||
bool first = true;
|
||||
for (const auto &c: rslv.m_A.m_rows[row_index]) {
|
||||
if (is_fixed(c.var())) {
|
||||
if (!get_value(c.var()).is_zero()) {
|
||||
impq val = get_value(c.var())*c.coeff();
|
||||
if (!first && val.is_pos())
|
||||
out << "+";
|
||||
if (val.y.is_zero())
|
||||
out << val.x << " ";
|
||||
else
|
||||
out << val << " ";
|
||||
}
|
||||
first = false;
|
||||
continue;
|
||||
}
|
||||
if (c.coeff().is_one()) {
|
||||
if (!first)
|
||||
out << "+";
|
||||
|
@ -508,6 +521,8 @@ std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_inde
|
|||
}
|
||||
out << "\n";
|
||||
for (const auto& c: rslv.m_A.m_rows[row_index]) {
|
||||
if (is_fixed(c.var()))
|
||||
continue;
|
||||
rslv.print_column_info(c.var(), out);
|
||||
if (is_base(c.var())) out << "j" << c.var() << " base\n";
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue