From f29b45561115d843bfaf702466906dcfbe0602ca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 8 Feb 2020 10:34:14 -0800 Subject: [PATCH] fix #2949 fix #2955 experiment with cut selection Signed-off-by: Nikolaj Bjorner --- src/math/lp/int_solver.cpp | 55 +++++++++++++++++++++++++++++++++-- src/math/lp/int_solver.h | 1 + src/math/lp/lar_constraints.h | 9 +++--- src/smt/smt_context.cpp | 16 +++++----- src/smt/smt_context.h | 2 +- src/smt/theory_lra.cpp | 29 ++---------------- src/util/mpz.cpp | 3 ++ 7 files changed, 74 insertions(+), 41 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index f341c5c01..0436c2ebf 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -37,6 +37,55 @@ bool int_solver::has_inf_int() const { return m_lar_solver->has_inf_int(); } +int int_solver::find_gomory_cut_column() { + int result = -1; + unsigned n = 0; + bool boxed = false; + unsigned min_row_size = UINT_MAX; + mpq min_range; + + // Prefer smaller row size +#if 0 + // Prefer boxed to non-boxed + // Prefer smaller ranges +#endif + + for (unsigned j : m_lar_solver->r_basis()) { + if (!column_is_int_inf(j)) + continue; + const row_strip& row = m_lar_solver->get_row(row_of_basic_column(j)); + if (!is_gomory_cut_target(row)) + continue; +#if 1 + if (is_boxed(j) && (min_row_size == UINT_MAX || 4*row.size() < 5*min_row_size)) { + lar_core_solver & lcs = m_lar_solver->m_mpq_lar_core_solver; + auto new_range = lcs.m_r_upper_bounds()[j].x - lcs.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 (min_row_size == UINT_MAX || (4*row.size() < 5*min_row_size && random() % (++n) == 0)) { + result = j; + n = 1; + min_row_size = std::min(min_row_size, row.size()); + } + } + return result; +} + int int_solver::find_inf_int_base_column() { unsigned inf_int_count = 0; int j = find_inf_int_boxed_base_column_with_smallest_range(inf_int_count); @@ -304,7 +353,8 @@ lia_move int_solver::gomory_cut() { lp_assert(st == lp_status::FEASIBLE || st == lp_status::OPTIMAL); } - int j = find_inf_int_base_column(); +// int j = find_inf_int_base_column(); + int j = find_gomory_cut_column(); if (j == -1) { j = find_inf_int_nbasis_column(); return j == -1? lia_move::sat : create_branch_on_column(j); @@ -1019,7 +1069,8 @@ lia_move int_solver::create_branch_on_column(int j) { if (is_free(j)) { m_upper = random() % 2; m_k = mpq(0); - } else { + } + else { m_upper = left_branch_is_more_narrow_than_right(j); m_k = m_upper? floor(get_value(j)) : ceil(get_value(j)); } diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h index 955371e1a..eb923fd9d 100644 --- a/src/math/lp/int_solver.h +++ b/src/math/lp/int_solver.h @@ -107,6 +107,7 @@ private: lia_move branch_or_sat(); int find_any_inf_int_column_basis_first(); int find_inf_int_base_column(); + int find_gomory_cut_column(); int find_inf_int_boxed_base_column_with_smallest_range(unsigned&); int get_kth_inf_int(unsigned) const; lp_settings& settings(); diff --git a/src/math/lp/lar_constraints.h b/src/math/lp/lar_constraints.h index 158c5a780..0260ab8cc 100644 --- a/src/math/lp/lar_constraints.h +++ b/src/math/lp/lar_constraints.h @@ -158,10 +158,6 @@ public: } void pop(unsigned k) { - m_constraint_count.pop(k); - for (unsigned i = m_constraints.size(); i-- > m_constraint_count; ) - m_constraints[i]->~lar_base_constraint(); - m_constraints.shrink(m_constraint_count); #if 1 m_active_lim.pop(k); for (unsigned i = m_active.size(); i-- > m_active_lim; ) { @@ -169,6 +165,11 @@ public: } m_active.shrink(m_active_lim); #endif + m_constraint_count.pop(k); + for (unsigned i = m_constraints.size(); i-- > m_constraint_count; ) + m_constraints[i]->~lar_base_constraint(); + m_constraints.shrink(m_constraint_count); + m_region.pop_scope(k); } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 88a34ed2d..f41cf8c31 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1861,13 +1861,15 @@ namespace smt { break; } } - if (m_lit_occs[l.index()] == 0) { - is_pos = false; - break; - } - if (m_lit_occs[(~l).index()] == 0) { - is_pos = true; - break; + if (track_occs()) { + if (m_lit_occs[l.index()] == 0) { + is_pos = false; + break; + } + if (m_lit_occs[(~l).index()] == 0) { + is_pos = true; + break; + } } is_pos = m_phase_default; break; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 41bd2c3a7..25af3317b 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -839,7 +839,7 @@ namespace smt { void mk_ite_cnstr(app * n); - bool track_occs() const { return m_fparams.m_phase_selection == PS_THEORY; } + bool track_occs() const { return m_fparams.m_phase_selection == PS_OCCURRENCE; } void dec_ref(literal l); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b4a63a0f9..02d64c3b3 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1864,28 +1864,6 @@ public: return atom; } - // bool make_sure_all_vars_have_bounds() { - // if (!has_int()) { - // return true; - // } - - // unsigned nv = std::min(th.get_num_vars(), m_theory_var2var_index.size()); - // bool all_bounded = true; - // for (unsigned v = 0; v < nv; ++v) { - // lpvar vi = m_theory_var2var_index[v]; - // if (vi == UINT_MAX) - // continue; - // if (!lp().is_term(vi) && !var_has_bound(vi, true) && !var_has_bound(vi, false)) { - // lp::lar_term term; - // term.add_coeff_var(rational::one(), vi); - // app_ref b = mk_bound(term, rational::zero(), true); - // TRACE("arith", tout << "added bound " << b << "\n";); - // IF_VERBOSE(2, verbose_stream() << "bound: " << b << "\n"); - // all_bounded = false; - // } - // } - // return all_bounded; - // } /** * n = (div p q) @@ -1919,7 +1897,6 @@ public: if (m_idiv_terms.empty()) { return true; } - // init_variable_values(); bool all_divs_valid = true; for (expr* n : m_idiv_terms) { expr* p = nullptr, *q = nullptr; @@ -1927,10 +1904,9 @@ public: theory_var v = mk_var(n); theory_var v1 = mk_var(p); lp::impq r1 = get_ivalue(v1); - SASSERT(r1.y.is_zero()); rational r2; - if (!r1.x.is_int() || r1.x.is_neg()) { + if (!r1.x.is_int() || r1.x.is_neg() || !r1.y.is_zero()) { // TBD // r1 = 223/4, r2 = 2, r = 219/8 // take ceil(r1), floor(r1), ceil(r2), floor(r2), for floor(r2) > 0 @@ -1946,8 +1922,7 @@ public: continue; } lp::impq val_v = get_ivalue(v); - SASSERT(val_v.y.is_zero()); - if (val_v.x == div(r1.x, r2)) continue; + if (val_v.y.is_zero() && val_v.x == div(r1.x, r2)) continue; TRACE("arith", tout << get_value(v) << " != " << r1 << " div " << r2 << "\n";); rational div_r = div(r1.x, r2); diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 6a7c531cc..424abc5b8 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -1680,6 +1680,9 @@ double mpz_manager::get_double(mpz const & a) const { else d *= static_cast(UINT_MAX); // 32-bit version } + if (!(r >= 0.0)) { + r = static_cast(UINT64_MAX); // some large number + } return a.m_val < 0 ? -r : r; #else return mpz_get_d(*a.m_ptr);