diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index d6ee28466..41b3d55dc 100644 --- a/src/math/lp/CMakeLists.txt +++ b/src/math/lp/CMakeLists.txt @@ -43,6 +43,8 @@ z3_add_component(lp polynomial nlsat smt_params + PYG_FILES + lp_params_helper.pyg ) include_directories(${src_SOURCE_DIR}) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 02cc62228..b8d942235 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -343,7 +343,10 @@ namespace lp { return out; } - bool m_has_non_integral_term = false; + // the maximal size of the term to try to tighten the bounds: + // if the size of the term is large than the chances are that the GCD of the coefficients is one + unsigned m_tighten_size_max = 10; + bool m_some_terms_are_ignored = false; std_vector m_sum_of_fixed; // we have to use m_var_register because of the fresh variables: otherwise they clash with the existing lar_solver column indices var_register m_var_register; @@ -360,8 +363,9 @@ namespace lp { // set S - iterate over bijection m_k2s mpq m_c; // the constant of the equation struct term_with_index { - // The invariant is that m_index[m_data[k].var()] = k, for each 0 <= k < m_data.size(), - // and m_index[j] = -1, or m_tmp[m_index[j]].var() = j, for every 0 <= j < m_index.size(). + // The invariant is + // 1) m_index[m_data[k].var()] = k, for each 0 <= k < m_data.size(), and + // 2) m_index[j] = -1, or m_data[m_index[j]].var() = j, for every 0 <= j < m_index.size(). // For example m_data = [(coeff, 5), (coeff, 3)] // then m_index = [-1,-1, -1, 1, -1, 0, -1, ....]. std_vector m_data; @@ -375,6 +379,8 @@ namespace lp { return r; } + auto size() const { return m_data.size(); } + bool has(unsigned k) const { return k < m_index.size() && m_index[k] >= 0; } @@ -498,9 +504,9 @@ namespace lp { std::unordered_map> m_row2fresh_defs; indexed_uint_set m_changed_rows; - // m_changed_columns are the columns that just became fixed, or those that just stopped being fixed. + // m_changed_f_columns are the columns that just became fixed, or those that just stopped being fixed. // If such a column appears in an entry it has to be recalculated. - indexed_uint_set m_changed_columns; + indexed_uint_set m_changed_f_columns; indexed_uint_set m_changed_terms; // represented by term columns indexed_uint_set m_terms_to_tighten; // represented by term columns // m_column_to_terms[j] is the set of all k such lra.get_term(k) depends on j @@ -596,34 +602,61 @@ namespace lp { }; struct protected_queue { - std::queue m_q; - indexed_uint_set m_in_q; + std::list m_q; + std::unordered_map::iterator> m_positions; + bool empty() const { return m_q.empty(); } unsigned size() const { - return (unsigned)m_q.size(); + return static_cast(m_q.size()); } void push(unsigned j) { - if (m_in_q.contains(j)) return; - m_in_q.insert(j); - m_q.push(j); + if (m_positions.find(j) != m_positions.end()) return; + m_q.push_back(j); + m_positions[j] = std::prev(m_q.end()); } unsigned pop_front() { unsigned j = m_q.front(); - m_q.pop(); - SASSERT(m_in_q.contains(j)); - m_in_q.remove(j); + m_q.pop_front(); + m_positions.erase(j); return j; } + void remove(unsigned j) { + auto it = m_positions.find(j); + if (it != m_positions.end()) { + m_q.erase(it->second); + m_positions.erase(it); + } + SASSERT(invariant()); + } + + bool contains(unsigned j) const { + return m_positions.find(j) != m_positions.end(); + } + void reset() { - while (!m_q.empty()) - m_q.pop(); - m_in_q.reset(); + m_q.clear(); + m_positions.clear(); + } + // Invariant method to ensure m_q and m_positions are aligned + bool invariant() const { + if (m_q.size() != m_positions.size()) + return false; + + for (auto it = m_q.begin(); it != m_q.end(); ++it) { + auto pos_it = m_positions.find(*it); + if (pos_it == m_positions.end()) + return false; + if (pos_it->second != it) + return false; + } + + return true; } }; @@ -743,28 +776,36 @@ namespace lp { void add_changed_column(unsigned j) { TRACE("dio", lra.print_column_info(j, tout);); - m_changed_columns.insert(j); + m_changed_f_columns.insert(j); } std_vector m_added_terms; std::unordered_set m_active_terms; std_vector m_branch_stats; std_vector m_branch_stack; std_vector m_explanation_of_branches; + // it is a non-const function : it can set m_some_terms_are_ignored to true + bool term_has_big_number(const lar_term& t) { + for (const auto& p : t) { + if (p.coeff().is_big() || (is_fixed(p.var()) && lra.get_lower_bound(p.var()).x.is_big())) { + m_some_terms_are_ignored = true; + return true; + } + } + return false; + } + + bool ignore_big_nums() const { return lra.settings().dio_ignore_big_nums(); } + + // we add all terms, even those with big numbers, but we might choose to non process the latter. void add_term_callback(const lar_term* t) { unsigned j = t->j(); TRACE("dio", tout << "term column t->j():" << j << std::endl; lra.print_term(*t, tout) << std::endl;); if (!lra.column_is_int(j)) { TRACE("dio", tout << "ignored a non-integral column" << std::endl;); - m_has_non_integral_term = true; + m_some_terms_are_ignored = true; return; } - CTRACE("dio", !lra.column_has_term(j), tout << "added term that is not associated with a column yet" << std::endl;); - - if (!lia.column_is_int(t->j())) { - TRACE("dio", tout << "not all vars are integrall\n";); - return; - } m_added_terms.push_back(t); mark_term_change(t->j()); auto undo = undo_add_term(*this, t); @@ -784,7 +825,7 @@ namespace lp { if (!lra.column_is_fixed(j)) return; TRACE("dio", tout << "j:" << j << "\n"; lra.print_column_info(j, tout);); - m_changed_columns.insert(j); + m_changed_f_columns.insert(j); lra.trail().push(undo_fixed_column(*this, j)); } @@ -812,7 +853,7 @@ namespace lp { } void register_columns_to_term(const lar_term& t) { - TRACE("dio_reg", tout << "register term:"; lra.print_term(t, tout); tout << ", t.j()=" << t.j() << std::endl;); + CTRACE("dio_reg", t.j() == 1337, tout << "register term:"; lra.print_term(t, tout); tout << ", t.j()=" << t.j() << std::endl;); for (const auto& p : t.ext_coeffs()) { auto it = m_columns_to_terms.find(p.var()); TRACE("dio_reg", tout << "register p.var():" << p.var() << "->" << t.j() << std::endl;); @@ -854,7 +895,7 @@ namespace lp { } subs_entry(entry_index); SASSERT(entry_invariant(entry_index)); - TRACE("dio", print_entry(entry_index, tout) << std::endl;); + TRACE("dio_entry", print_entry(entry_index, tout) << std::endl;); } void subs_entry(unsigned ei) { if (ei >= m_e_matrix.row_count()) return; @@ -965,7 +1006,7 @@ namespace lp { } void find_changed_terms_and_more_changed_rows() { - for (unsigned j : m_changed_columns) { + for (unsigned j : m_changed_f_columns) { const auto it = m_columns_to_terms.find(j); if (it != m_columns_to_terms.end()) for (unsigned k : it->second) { @@ -1013,15 +1054,28 @@ namespace lp { } } - void process_changed_columns(std_vector &f_vector) { + // this is a non-const function - it can set m_some_terms_are_ignored to true + bool is_big_term_or_no_term(unsigned j) { + return + j >= lra.column_count() + || + !lra.column_has_term(j) + || + (ignore_big_nums() && term_has_big_number(lra.get_term(j))); + } + +// Processes columns that have changed due to variables becoming fixed/unfixed or terms being updated. +// It identifies affected terms and rows, recalculates entries, removes irrelevant fresh definitions, +// and ensures substituted variables are properly eliminated from changed F entries, m_e_matrix. +// The function maintains internal consistency of data structures after these updates. + void process_m_changed_f_columns(std_vector &f_vector) { find_changed_terms_and_more_changed_rows(); for (unsigned j: m_changed_terms) { - m_terms_to_tighten.insert(j); - if (j < m_l_matrix.column_count()) { - for (const auto& cs : m_l_matrix.column(j)) { - m_changed_rows.insert(cs.var()); - } - } + if (!is_big_term_or_no_term(j)) + m_terms_to_tighten.insert(j); + if (j < m_l_matrix.column_count()) + for (const auto& cs : m_l_matrix.column(j)) + m_changed_rows.insert(cs.var()); } // find more entries to recalculate @@ -1031,39 +1085,34 @@ namespace lp { if (it == m_row2fresh_defs.end()) continue; for (unsigned xt : it->second) { SASSERT(var_is_fresh(xt)); - for (const auto& p : m_e_matrix.m_columns[xt]) { + for (const auto& p : m_e_matrix.m_columns[xt]) more_changed_rows.push_back(p.var()); - } } } - for (unsigned ei : more_changed_rows) { + for (unsigned ei : more_changed_rows) m_changed_rows.insert(ei); - } - + for (unsigned ei : m_changed_rows) { if (ei >= m_e_matrix.row_count()) continue; if (belongs_to_s(ei)) f_vector.push_back(ei); + recalculate_entry(ei); if (m_e_matrix.m_columns.back().size() == 0) { m_e_matrix.m_columns.pop_back(); m_var_register.shrink(m_e_matrix.column_count()); } - if (m_l_matrix.m_columns.back().size() == 0) { + if (m_l_matrix.m_columns.back().size() == 0) m_l_matrix.m_columns.pop_back(); - } } - remove_irrelevant_fresh_defs(); - eliminate_substituted_in_changed_rows(); - m_changed_columns.reset(); + m_changed_f_columns.reset(); m_changed_rows.reset(); m_changed_terms.reset(); - SASSERT(entries_are_ok()); } int get_sign_in_e_row(unsigned ei, unsigned j) const { @@ -1131,7 +1180,7 @@ namespace lp { m_lra_level = 0; reset_conflict(); - process_changed_columns(f_vector); + process_m_changed_f_columns(f_vector); for (const lar_term* t : m_added_terms) { m_active_terms.insert(t); f_vector.push_back(m_e_matrix.row_count()); // going to add a row in fill_entry @@ -1295,6 +1344,59 @@ namespace lp { bool is_substituted_by_fresh(unsigned k) const { return m_fresh_k2xt_terms.has_key(k); } + + // find a variable in q, not neccessarily at the beginning of the queue, that when substituted would create the minimal + // number of non-zeroes + unsigned find_var_to_substitute_on_espace(protected_queue& q) { + // go over all q elements j + // say j is substituted by entry ei = m_k2s[j] + // count the number of variables i in m_e_matrix[ei] that m_espace does not contain i, + // and choose ei where this number is minimal + + unsigned best_var = UINT_MAX; + size_t min_new_vars = std::numeric_limits::max(); + unsigned num_candidates = 0; + std::vector to_remove; + for (unsigned j : q.m_q) { + size_t new_vars = 0; + if (!m_espace.has(j)) { + to_remove.push_back(j); + continue; + } + if (m_k2s.has_key(j)) { + unsigned ei = m_k2s[j]; // entry index for substitution + for (const auto& p : m_e_matrix.m_rows[ei]) + if (p.var() != j && !m_espace.has(p.var())) + ++new_vars; + } + else if (m_fresh_k2xt_terms.has_key(j)) { + const lar_term& fresh_term = m_fresh_k2xt_terms.get_by_key(j).first; + for (const auto& p : fresh_term) + if (p.var() != j && !m_espace.has(p.var())) + ++new_vars; + } + if (new_vars < min_new_vars) { + min_new_vars = new_vars; + best_var = j; + num_candidates = 1; + } + else if (new_vars == min_new_vars) { + ++num_candidates; + if ((lra.settings().random_next() % num_candidates) == 0) + best_var = j; + } + } + + if (best_var != UINT_MAX) + q.remove(best_var); + + for (unsigned j: to_remove) + q.remove(j); + + + return best_var; + } + // The term giving the substitution is in form (+-)x_k + sum {a_i*x_i} + c = 0. // We substitute x_k in t by (+-)coeff*(sum {a_i*x_i} + c), where coeff is // the coefficient of x_k in t. @@ -1303,11 +1405,11 @@ namespace lp { auto r = tighten_on_espace(j); if (r == lia_move::conflict) return lia_move::conflict; - unsigned k = q.pop_front(); - if (!m_espace.has(k)) - return lia_move::undef; + unsigned k = find_var_to_substitute_on_espace(q); + if (k == UINT_MAX) + return lia_move::undef; + SASSERT(m_espace.has(k)); // we might substitute with a term from S or a fresh term - SASSERT(can_substitute(k)); lia_move ret; if (is_substituted_by_fresh(k)) @@ -1385,7 +1487,7 @@ namespace lp { lia_move subs_with_S_and_fresh(protected_queue& q, unsigned j) { lia_move r = lia_move::undef; - while (!q.empty() && r != lia_move::conflict) { + while (!q.empty() && r != lia_move::conflict && m_espace.size() <= m_tighten_size_max) { lia_move ret = subs_front_with_S_and_fresh(q, j); r = join(ret, r); } @@ -1436,8 +1538,13 @@ namespace lp { // print_bounds(tout); ); for (unsigned j : sorted_changed_terms) { - m_terms_to_tighten.remove(j); + if (is_big_term_or_no_term(j)) { + m_terms_to_tighten.remove(j); + continue; + } auto ret = tighten_bounds_for_term_column(j); + m_terms_to_tighten.remove(j); + r = join(ret, r); if (r == lia_move::conflict) break; @@ -1459,25 +1566,37 @@ namespace lp { // We will have lar_t, and let j is lar_t.j(), the term column. // In the m_espace we have lar_t. The result of open_ml((1*j)) is lar_t - (1, j). - // So we have "equality" m_espace = open(m_lspace) + (1*lar_t.j()) - void init_substitutions(const lar_term& lar_t, protected_queue& q) { + // So we have "equality" m_espace = open(m_lspace) + (1*lar_t.j()) + // return false iff seen a big number and dio_ignore_big_nums() is true + bool init_substitutions(const lar_term& lar_t, protected_queue& q) { m_espace.clear(); m_c = mpq(0); m_lspace.clear(); m_lspace.add(mpq(1), lar_t.j()); + bool ret = true; SASSERT(get_extended_term_value(lar_t).is_zero()); for (const auto& p : lar_t) { if (is_fixed(p.j())) { - m_c += p.coeff() * lia.lower_bound(p.j()).x; + const mpq& b = lia.lower_bound(p.j()).x; + if (ignore_big_nums() && b.is_big()) { + ret = false; + break; + } + m_c += p.coeff() * b; } else { unsigned lj = lar_solver_to_local(p.j()); + if (ignore_big_nums() && p.coeff().is_big()) { + ret = false; + break; + } m_espace.add(p.coeff(), lj);; if (can_substitute(lj)) q.push(lj); } } SASSERT(subs_invariant(lar_t.j())); + return ret; } unsigned lar_solver_to_local(unsigned j) const { @@ -1499,8 +1618,6 @@ namespace lp { lia_move tighten_on_espace(unsigned j) { mpq g = gcd_of_coeffs(m_espace.m_data, true); - TRACE("dio", tout << "after process_q_with_S\nt:"; print_term_o(create_term_from_espace(), tout) << std::endl; tout << "g:" << g << std::endl;); - if (g.is_one()) return lia_move::undef; if (g.is_zero()) { @@ -1517,7 +1634,7 @@ namespace lp { auto r = tighten_bounds_for_non_trivial_gcd(g, j, true); if (r == lia_move::undef) r = tighten_bounds_for_non_trivial_gcd(g, j, false); - if (r == lia_move::undef && m_changed_columns.contains(j)) + if (r == lia_move::undef && m_changed_f_columns.contains(j)) r = lia_move::continue_with_check; return r; } @@ -1533,12 +1650,13 @@ namespace lp { lia_move tighten_bounds_for_term_column(unsigned j) { // q is the queue of variables that can be substituted in term_to_tighten protected_queue q; - TRACE("dio", tout << "j:" << j << " , intitial term t: "; print_lar_term_L(lra.get_term(j), tout) << std::endl; + TRACE("dio", tout << "j:" << j << " , initial term t: "; print_lar_term_L(lra.get_term(j), tout) << std::endl; for( const auto& p : lra.get_term(j).ext_coeffs()) { lra.print_column_info(p.var(), tout); } ); - init_substitutions(lra.get_term(j), q); + if (!init_substitutions(lra.get_term(j), q)) + return lia_move::undef; TRACE("dio", tout << "t:"; tout << "m_espace:"; @@ -1687,30 +1805,23 @@ namespace lp { mpq rs; bool is_strict = false; u_dependency* b_dep = nullptr; - SASSERT(!g.is_zero()); + SASSERT(!g.is_zero() && !g.is_one()); if (lra.has_bound_of_type(j, b_dep, rs, is_strict, is_upper)) { - TRACE("dio", - tout << "current " << (is_upper? "upper":"lower") << " bound for x" << j << ":" - << rs << std::endl;); + TRACE("dio", tout << "x" << j << (is_upper? " <= ":" >= ") << rs << std::endl;); mpq rs_g = (rs - m_c) % g; - if (rs_g.is_neg()) { + if (rs_g.is_neg()) rs_g += g; - } - if (! (!rs_g.is_neg() && rs_g.is_int())) { - std::cout << "rs:" << rs << "\n"; - std::cout << "m_c:" << m_c << "\n"; - std::cout << "g:" << g << "\n"; - std::cout << "rs_g:" << rs_g << "\n"; - } - SASSERT(rs_g.is_int()); + + SASSERT(rs_g.is_int() && !rs_g.is_neg()); + TRACE("dio", tout << "(rs - m_c) % g:" << rs_g << std::endl;); if (!rs_g.is_zero()) { if (tighten_bound_kind(g, j, rs, rs_g, is_upper)) return lia_move::conflict; - } else { - TRACE("dio", tout << "no improvement in the bound\n";); } + else + TRACE("dio", tout << "rs_g is zero: no improvement in the bound\n";); } return lia_move::undef; } @@ -1773,10 +1884,7 @@ namespace lp { for (const auto& p: fixed_part_of_the_term) { SASSERT(is_fixed(p.var())); if (p.coeff().is_int() && (p.coeff() % g).is_zero()) { - // we can skip this dependency - // because the monomial p.coeff()*p.var() is 0 modulo g, and it does not matter that p.var() is fixed. - // We could have added p.coeff()*p.var() to g*t_, substructed the value of p.coeff()*p.var() from m_c and - // still get the same result. + // we can skip this dependency as explained above TRACE("dio", tout << "skipped dep:\n"; print_deps(tout, lra.get_bound_constraint_witnesses_for_column(p.var()));); continue; } @@ -1788,7 +1896,6 @@ namespace lp { if (lra.settings().get_cancel_flag()) return false; lra.update_column_type_and_bound(j, kind, bound, dep); - lp_status st = lra.find_feasible_solution(); if (is_sat(st) || st == lp::lp_status::CANCELLED) return false; @@ -1852,7 +1959,7 @@ namespace lp { return lia_move::undef; if (r == lia_move::conflict || r == lia_move::undef) break; - SASSERT(m_changed_columns.size() == 0); + SASSERT(m_changed_f_columns.size() == 0); } while (f_vector.size()); @@ -2180,11 +2287,12 @@ namespace lp { bool is_in_sync() const { for (unsigned j = 0; j < m_e_matrix.column_count(); j++) { unsigned external_j = m_var_register.local_to_external(j); - if (external_j == UINT_MAX) continue; - if (external_j >= lra.column_count() && m_e_matrix.m_columns[j].size()) { - // It is OK to have an empty column in m_e_matrix. + if (external_j == UINT_MAX) + continue; + if (external_j >= lra.column_count() && m_e_matrix.m_columns[j].size()) return false; - } + // It is OK to have an empty column in m_e_matrix. + } for (unsigned ei = 0; ei < m_e_matrix.row_count(); ei++) { @@ -2219,6 +2327,8 @@ namespace lp { ret = branching_on_undef(); m_max_of_branching_iterations = (unsigned)m_max_of_branching_iterations / 2; + if (ret == lia_move::undef) + lra.settings().dio_calls_period() *= 2; return ret; } @@ -2692,8 +2802,8 @@ namespace lp { // needed for the template bound_analyzer_on_row.h const lar_solver& lp() const { return lra; } lar_solver& lp() {return lra;} - bool has_non_integral_term() const { - return m_has_non_integral_term; + bool some_terms_are_ignored() const { + return m_some_terms_are_ignored; } }; // Constructor definition @@ -2712,8 +2822,8 @@ namespace lp { m_imp->explain(ex); } - bool dioph_eq::has_non_integral_term() const { - return m_imp->has_non_integral_term(); + bool dioph_eq::some_terms_are_ignored() const { + return m_imp->some_terms_are_ignored(); } diff --git a/src/math/lp/dioph_eq.h b/src/math/lp/dioph_eq.h index e266e7dd6..9adc04da7 100644 --- a/src/math/lp/dioph_eq.h +++ b/src/math/lp/dioph_eq.h @@ -30,6 +30,6 @@ namespace lp { ~dioph_eq(); lia_move check(); void explain(lp::explanation&); - bool has_non_integral_term() const; + bool some_terms_are_ignored() const; }; } diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 4bc9b2fb3..960287ab4 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -41,7 +41,6 @@ namespace lp { mpq m_k; // the right side of the cut hnf_cutter m_hnf_cutter; unsigned m_hnf_cut_period; - unsigned m_dioph_eq_period; dioph_eq m_dio; int_gcd_test m_gcd; @@ -51,7 +50,6 @@ namespace lp { imp(int_solver& lia): lia(lia), lra(lia.lra), lrac(lia.lrac), m_hnf_cutter(lia), m_dio(lia), m_gcd(lia) { m_hnf_cut_period = settings().hnf_cut_period(); - m_dioph_eq_period = settings().m_dioph_eq_period; } bool has_lower(unsigned j) const { @@ -187,20 +185,19 @@ namespace lp { } bool should_gomory_cut() { - bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() || - m_dio.has_non_integral_term(); - + bool dio_allows_gomory = !settings().dio() || settings().dio_enable_gomory_cuts() || + m_dio.some_terms_are_ignored(); return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0; } bool should_solve_dioph_eq() { - return lia.settings().dio_eqs() && m_number_of_calls % m_dioph_eq_period == 0; + return lia.settings().dio() && (m_number_of_calls % settings().dio_calls_period() == 0); } // HNF bool should_hnf_cut() { - return (!settings().dio_eqs() || settings().dio_enable_hnf_cuts()) + return (!settings().dio() || settings().dio_enable_hnf_cuts()) && settings().enable_hnf() && m_number_of_calls % settings().hnf_cut_period() == 0; } @@ -226,7 +223,7 @@ namespace lp { lia_move r = lia_move::undef; - if (m_gcd.should_apply()) + if (m_gcd.should_apply() || (settings().dio() && m_dio.some_terms_are_ignored())) r = m_gcd(); check_return_helper pc(lra); diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg new file mode 100644 index 000000000..3e393dc03 --- /dev/null +++ b/src/math/lp/lp_params_helper.pyg @@ -0,0 +1,13 @@ +def_module_params(module_name='lp', + class_name='lp_params_helper', + description='linear programming parameters', + export=True, + params=(('dio', BOOL, False, 'use Diophantine equalities'), + ('dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'), + ('dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'), + ('dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'), + ('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'), + ('dio_calls_period', UINT, 4, 'Period of calling the Diophantine handler in the final_check()'), + ('dio_run_gcd', BOOL, True, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'), + )) + diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 9d2fe675e..ea662f111 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -17,6 +17,7 @@ Revision History: --*/ +#include "math/lp/lp_params_helper.hpp" #include #include "util/vector.h" #include "smt/params/smt_params_helper.hpp" @@ -25,6 +26,7 @@ template bool lp::vectors_are_equal(vector const&, vector(p.arith_simplex_strategy()); m_nlsat_delay = p.arith_nl_delay(); - m_dio_eqs = p.arith_lp_dio_eqs(); - m_dio_enable_gomory_cuts = p.arith_lp_dio_cuts_enable_gomory(); - m_dio_enable_hnf_cuts = p.arith_lp_dio_cuts_enable_hnf(); - m_dio_branching_period = p.arith_lp_dio_branching_period(); + m_dio = lp_p.dio(); + m_dio_enable_gomory_cuts = lp_p.dio_cuts_enable_gomory(); + m_dio_enable_hnf_cuts = lp_p.dio_cuts_enable_hnf(); + m_dio_branching_period = lp_p.dio_branching_period(); m_dump_bound_lemmas = p.arith_dump_bound_lemmas(); + m_dio_ignore_big_nums = lp_p.dio_ignore_big_nums(); + m_dio_calls_period = lp_p.dio_calls_period(); + m_dio_run_gcd = lp_p.dio_run_gcd(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index ab90fee38..82af740d0 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -218,8 +218,12 @@ public: void updt_params(params_ref const& p); bool enable_hnf() const { return m_enable_hnf; } unsigned nlsat_delay() const { return m_nlsat_delay; } - bool int_run_gcd_test() const { return m_int_run_gcd_test; } - bool& int_run_gcd_test() { return m_int_run_gcd_test; } + bool int_run_gcd_test() const { + if (!m_dio) + return m_int_run_gcd_test; + return m_dio_run_gcd; + } + void set_run_gcd_test(bool v) { m_int_run_gcd_test = v; } unsigned reps_in_scaler = 20; int c_partial_pivoting = 10; // this is the constant c from page 410 unsigned depth_of_rook_search = 4; @@ -243,7 +247,6 @@ public: unsigned column_number_threshold_for_using_lu_in_lar_solver = 4000; unsigned m_int_gomory_cut_period = 4; unsigned m_int_find_cube_period = 4; - unsigned m_dioph_eq_period = 1; private: unsigned m_hnf_cut_period = 4; bool m_int_run_gcd_test = true; @@ -255,23 +258,30 @@ private: bool m_enable_hnf = true; bool m_print_external_var_name = false; bool m_propagate_eqs = false; - bool m_dio_eqs = false; + bool m_dio = false; bool m_dio_enable_gomory_cuts = false; bool m_dio_enable_hnf_cuts = true; unsigned m_dio_branching_period = 100; // do branching rarely unsigned m_dio_report_branch_with_term_tigthening_period = 10000000; // period of reporting the branch with term tigthening bool m_dump_bound_lemmas = false; + bool m_dio_ignore_big_nums = false; + unsigned m_dio_calls_period = 4; + bool m_dio_run_gcd = true; public: + unsigned dio_calls_period() const { return m_dio_calls_period; } + unsigned & dio_calls_period() { return m_dio_calls_period; } bool print_external_var_name() const { return m_print_external_var_name; } bool propagate_eqs() const { return m_propagate_eqs;} unsigned hnf_cut_period() const { return m_hnf_cut_period; } void set_hnf_cut_period(unsigned period) { m_hnf_cut_period = period; } unsigned random_next() { return m_rand(); } unsigned random_next(unsigned u ) { return m_rand(u); } - bool dio_eqs() { return m_dio_eqs; } - bool dio_enable_gomory_cuts() const { return m_dio_eqs && m_dio_enable_gomory_cuts; } - bool dio_enable_hnf_cuts() const { return m_dio_eqs && m_dio_enable_hnf_cuts; } + bool dio() { return m_dio; } + bool dio_enable_gomory_cuts() const { return m_dio && m_dio_enable_gomory_cuts; } + bool dio_run_gcd() const { return m_dio && m_dio_run_gcd; } + bool dio_enable_hnf_cuts() const { return m_dio && m_dio_enable_hnf_cuts; } unsigned dio_branching_period() const { return m_dio_branching_period; } + bool dio_ignore_big_nums() const { return m_dio_ignore_big_nums; } void set_random_seed(unsigned s) { m_rand.set_seed(s); } unsigned dio_report_branch_with_term_tigthening_period() const { return m_dio_report_branch_with_term_tigthening_period; } bool bound_progation() const { diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 813faba3d..cd280d158 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -35,7 +35,7 @@ namespace arith { lp().updt_params(ctx.s().params()); lp().settings().set_resource_limit(m_resource_limit); lp().settings().bound_propagation() = bound_prop_mode::BP_NONE != propagation_mode(); - lp().settings().int_run_gcd_test() = get_config().m_arith_gcd_test; + lp().settings().set_run_gcd_test(get_config().m_arith_gcd_test); lp().settings().set_random_seed(get_config().m_random_seed); m_lia = alloc(lp::int_solver, *m_solver.get()); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 15641315e..c1eb0148a 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -57,10 +57,6 @@ def_module_params(module_name='smt', ('bv.solver', UINT, 0, 'bit-vector solver engine: 0 - bit-blasting, 1 - polysat, 2 - intblast, requires sat.smt=true'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), - ('arith.lp.dio_eqs', BOOL, False, 'use Diophantine equalities'), - ('arith.lp.dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'), - ('arith.lp.dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'), - ('arith.lp.dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'), ('arith.nl', BOOL, True, '(incomplete) nonlinear arithmetic support based on Groebner basis and interval propagation, relevant only if smt.arith.solver=2'), ('arith.nl.nra', BOOL, True, 'call nra_solver when incremental linearization does not produce a lemma, this option is ignored when arith.nl=false, relevant only if smt.arith.solver=6'), ('arith.nl.branching', BOOL, True, 'branching on integer variables in non linear clusters'), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 72fac2371..657775a6a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -871,7 +871,7 @@ public: unsigned branch_cut_ratio = ctx().get_fparams().m_arith_branch_cut_ratio; lp().set_cut_strategy(branch_cut_ratio); - lp().settings().int_run_gcd_test() = ctx().get_fparams().m_arith_gcd_test; + lp().settings().set_run_gcd_test(ctx().get_fparams().m_arith_gcd_test); lp().settings().set_random_seed(ctx().get_fparams().m_random_seed); m_lia = alloc(lp::int_solver, *m_solver.get()); }