From f85a5135c0b04a4bd7c224cd65eec55ce47554a4 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 3 Apr 2025 09:47:02 -0700 Subject: [PATCH 01/15] reuse dio branch Signed-off-by: Lev Nachmanson --- src/math/lp/CMakeLists.txt | 2 + src/math/lp/dioph_eq.cpp | 124 +++++++++++++++++++++++---- src/math/lp/int_solver.cpp | 2 +- src/math/lp/lp_params_helper.pyg | 10 +++ src/math/lp/lp_settings.cpp | 11 +-- src/smt/params/smt_params_helper.pyg | 4 - 6 files changed, 124 insertions(+), 29 deletions(-) create mode 100644 src/math/lp/lp_params_helper.pyg diff --git a/src/math/lp/CMakeLists.txt b/src/math/lp/CMakeLists.txt index d6ee28466e6..41b3d55dcf7 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 02cc62228d9..f085ac5d6df 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -596,34 +596,63 @@ 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); + } + if (!invariant()) { + throw std::runtime_error("Invariant violation in protected_queue"); + } + } + + 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; } }; @@ -750,6 +779,12 @@ namespace lp { std_vector m_branch_stats; std_vector m_branch_stack; std_vector m_explanation_of_branches; + bool term_has_big_number(const lar_term* t) const { + for (const auto& p : *t) + if (p.coeff().is_big()) + return true; + return false; + } 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;); @@ -761,8 +796,9 @@ namespace lp { 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";); + if (term_has_big_number(t)) { + TRACE("dio", tout << "term_has_big_number\n";); + m_has_non_integral_term = true; return; } m_added_terms.push_back(t); @@ -779,10 +815,12 @@ namespace lp { void update_column_bound_callback(unsigned j) { if (!lra.column_is_int(j)) return; - if (lra.column_has_term(j)) + if (lra.column_has_term(j) && !term_has_big_number(&lra.get_term(j))) m_terms_to_tighten.insert(j); // the boundary of the term has changed: we can be successful to tighten this term if (!lra.column_is_fixed(j)) return; + if (lra.get_lower_bound(j).x.is_big()) + return; TRACE("dio", tout << "j:" << j << "\n"; lra.print_column_info(j, tout);); m_changed_columns.insert(j); lra.trail().push(undo_fixed_column(*this, j)); @@ -1016,6 +1054,7 @@ namespace lp { void process_changed_columns(std_vector &f_vector) { find_changed_terms_and_more_changed_rows(); for (unsigned j: m_changed_terms) { + SASSERT(!term_has_big_number(&lra.get_term(j))); m_terms_to_tighten.insert(j); if (j < m_l_matrix.column_count()) { for (const auto& cs : m_l_matrix.column(j)) { @@ -1295,6 +1334,52 @@ 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; + + for (unsigned j : q.m_q) { + size_t new_vars = 0; + if (!m_espace.has(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); + + 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 +1388,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)) @@ -2203,6 +2288,7 @@ namespace lp { public: lia_move check() { lra.stats().m_dio_calls++; + std::cout << "check" << std::endl; TRACE("dio", tout << lra.stats().m_dio_calls << std::endl;); std_vector f_vector; lia_move ret; diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 11648f7bda5..87426fbf1d0 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -189,7 +189,7 @@ namespace lp { bool should_gomory_cut() { bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() || m_dio.has_non_integral_term(); - + std::cout << "should_gomory_cut:" << dio_allows_gomory << std::endl; return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0; } diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg new file mode 100644 index 00000000000..2057b382303 --- /dev/null +++ b/src/math/lp/lp_params_helper.pyg @@ -0,0 +1,10 @@ +def_module_params(module_name='lp', + class_name='lp_params_helper', + description='linear programming parameters', + export=True, + params=(('dio_eqs', 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'), + )) + \ No newline at end of file diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 9d2fe675e09..e2f780ee10d 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_dump_bound_lemmas = p.arith_dump_bound_lemmas(); + m_dio_eqs = lp_p.dio_eqs(); + 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(); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 15641315ee4..c1eb0148a74 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'), From d0a7aa3d43f973cc5b4e8c68d10d1fdf94951565 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 4 Apr 2025 08:51:35 -0700 Subject: [PATCH 02/15] throttle dio for big numbers Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 63 +++++++++++++++++++++----------- src/math/lp/dioph_eq.h | 2 +- src/math/lp/int_solver.cpp | 3 +- src/math/lp/lp_params_helper.pyg | 1 + src/math/lp/lp_settings.cpp | 1 + src/math/lp/lp_settings.h | 3 ++ 6 files changed, 48 insertions(+), 25 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index f085ac5d6df..61c671602ea 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -343,7 +343,7 @@ namespace lp { return out; } - bool m_has_non_integral_term = false; + 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; @@ -779,26 +779,29 @@ namespace lp { std_vector m_branch_stats; std_vector m_branch_stack; std_vector m_explanation_of_branches; - bool term_has_big_number(const lar_term* t) const { - for (const auto& p : *t) + bool term_has_big_number(const lar_term& t) const { + for (const auto& p : t) if (p.coeff().is_big()) return true; return false; } + + bool ignore_big_nums() const { return lra.settings().dio_ignore_big_nums(); } + 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 (term_has_big_number(t)) { + if (ignore_big_nums() && term_has_big_number(*t)) { TRACE("dio", tout << "term_has_big_number\n";); - m_has_non_integral_term = true; + m_some_terms_are_ignored = true; return; } m_added_terms.push_back(t); @@ -815,11 +818,12 @@ namespace lp { void update_column_bound_callback(unsigned j) { if (!lra.column_is_int(j)) return; - if (lra.column_has_term(j) && !term_has_big_number(&lra.get_term(j))) + if (lra.column_has_term(j) && + ignore_big_nums() && !term_has_big_number(lra.get_term(j))) m_terms_to_tighten.insert(j); // the boundary of the term has changed: we can be successful to tighten this term if (!lra.column_is_fixed(j)) return; - if (lra.get_lower_bound(j).x.is_big()) + if (ignore_big_nums() && lra.get_lower_bound(j).x.is_big()) return; TRACE("dio", tout << "j:" << j << "\n"; lra.print_column_info(j, tout);); m_changed_columns.insert(j); @@ -1054,7 +1058,9 @@ namespace lp { void process_changed_columns(std_vector &f_vector) { find_changed_terms_and_more_changed_rows(); for (unsigned j: m_changed_terms) { - SASSERT(!term_has_big_number(&lra.get_term(j))); + if (j >= lra.column_count()) + continue; + SASSERT(!ignore_big_nums() || !term_has_big_number(lra.get_term(j))); m_terms_to_tighten.insert(j); if (j < m_l_matrix.column_count()) { for (const auto& cs : m_l_matrix.column(j)) { @@ -1346,10 +1352,13 @@ namespace lp { 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)) continue; + 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]) @@ -1377,6 +1386,10 @@ namespace lp { if (best_var != UINT_MAX) q.remove(best_var); + for (unsigned j: to_remove) + q.remove(j); + + return best_var; } @@ -1544,8 +1557,9 @@ 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(); @@ -1553,16 +1567,21 @@ namespace lp { 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()) + return false; + m_c += p.coeff() * b; } else { unsigned lj = lar_solver_to_local(p.j()); + SASSERT(!p.coeff().is_big()); m_espace.add(p.coeff(), lj);; if (can_substitute(lj)) q.push(lj); } } SASSERT(subs_invariant(lar_t.j())); + return true; } unsigned lar_solver_to_local(unsigned j) const { @@ -1584,8 +1603,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()) { @@ -1623,7 +1640,8 @@ namespace lp { 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:"; @@ -2218,6 +2236,8 @@ namespace lp { for (unsigned k = 0; k < lra.terms().size(); k++) { const lar_term* t = lra.terms()[k]; if (!lia.column_is_int(t->j())) continue; + if (ignore_big_nums() && term_has_big_number(*t)) + continue; SASSERT(t->j() != UINT_MAX); for (const auto& p : (*t).ext_coeffs()) { unsigned j = p.var(); @@ -2288,7 +2308,6 @@ namespace lp { public: lia_move check() { lra.stats().m_dio_calls++; - std::cout << "check" << std::endl; TRACE("dio", tout << lra.stats().m_dio_calls << std::endl;); std_vector f_vector; lia_move ret; @@ -2778,8 +2797,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 @@ -2798,8 +2817,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 e266e7dd68e..9adc04da734 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 87426fbf1d0..167b23cbe95 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -188,8 +188,7 @@ namespace lp { bool should_gomory_cut() { bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() || - m_dio.has_non_integral_term(); - std::cout << "should_gomory_cut:" << dio_allows_gomory << std::endl; + m_dio.some_terms_are_ignored(); return dio_allows_gomory && m_number_of_calls % settings().m_int_gomory_cut_period == 0; } diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index 2057b382303..a2ef9328ed2 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -6,5 +6,6 @@ def_module_params(module_name='lp', ('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'), )) \ No newline at end of file diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index e2f780ee10d..2e3c464de0a 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -38,4 +38,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) { 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(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 8efff27bd6c..9c0db4f769e 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -261,6 +261,8 @@ struct lp_settings { 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; + public: bool print_external_var_name() const { return m_print_external_var_name; } bool propagate_eqs() const { return m_propagate_eqs;} @@ -272,6 +274,7 @@ struct lp_settings { 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; } 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 { From 9cf5665cd6df9a298e0cf4e68774c4a167fe03a5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 4 Apr 2025 13:34:16 -0700 Subject: [PATCH 03/15] throttle dio Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 61c671602ea..16d6a152e9a 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -343,6 +343,9 @@ namespace lp { return out; } + // 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 @@ -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; } @@ -626,9 +632,7 @@ namespace lp { m_q.erase(it->second); m_positions.erase(it); } - if (!invariant()) { - throw std::runtime_error("Invariant violation in protected_queue"); - } + SASSERT(invariant()); } bool contains(unsigned j) const { @@ -780,9 +784,12 @@ namespace lp { std_vector m_branch_stack; std_vector m_explanation_of_branches; bool term_has_big_number(const lar_term& t) const { - for (const auto& p : t) + for (const auto& p : t) { if (p.coeff().is_big()) return true; + if (is_fixed(p.var()) && lra.get_lower_bound(p.var()).x.is_big()) + return true; + } return false; } @@ -896,7 +903,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; @@ -1483,7 +1490,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); } @@ -1535,6 +1542,8 @@ namespace lp { ); for (unsigned j : sorted_changed_terms) { m_terms_to_tighten.remove(j); + if (ignore_big_nums() && term_has_big_number(lra.get_term(j))) + continue; auto ret = tighten_bounds_for_term_column(j); r = join(ret, r); if (r == lia_move::conflict) From d4ba75eb7965f81013c49e1716a17eacb01bbf3d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 4 Apr 2025 19:56:13 -0700 Subject: [PATCH 04/15] add parameter m_dio_calls_period Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 2 ++ src/math/lp/int_solver.cpp | 4 +--- src/math/lp/lp_params_helper.pyg | 1 + src/math/lp/lp_settings.cpp | 1 + src/math/lp/lp_settings.h | 4 +++- 5 files changed, 8 insertions(+), 4 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 16d6a152e9a..2864650d37f 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -2333,6 +2333,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; } diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index 167b23cbe95..e12767252e1 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 { @@ -193,7 +191,7 @@ namespace lp { } bool should_solve_dioph_eq() { - return lia.settings().dio_eqs() && m_number_of_calls % m_dioph_eq_period == 0; + return lia.settings().dio_eqs() && (m_number_of_calls % settings().dio_calls_period() == 0); } // HNF diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index a2ef9328ed2..b32b5c207f7 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -7,5 +7,6 @@ def_module_params(module_name='lp', ('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, 1, 'Period of calling the Diophantine handler in the final_check()'), )) \ No newline at end of file diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 2e3c464de0a..4df31abfc9d 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -39,4 +39,5 @@ void lp::lp_settings::updt_params(params_ref const& _p) { 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(); } diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 9c0db4f769e..9df44a22acf 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -243,7 +243,6 @@ struct lp_settings { 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; @@ -262,8 +261,11 @@ struct lp_settings { 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 = 1; 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; } From baadb9bb07cd574867443a8a41163b97ceb9aeee Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sat, 5 Apr 2025 10:25:39 -0700 Subject: [PATCH 05/15] Update lp_settings.cpp white space change --- src/math/lp/lp_settings.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/math/lp/lp_settings.cpp b/src/math/lp/lp_settings.cpp index 4df31abfc9d..42df2272445 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -37,7 +37,8 @@ void lp::lp_settings::updt_params(params_ref const& _p) { m_dio_eqs = lp_p.dio_eqs(); 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_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(); } From cc5c98f5b0f0edbb6c46bef6a2b7773badd1db79 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sat, 5 Apr 2025 10:26:35 -0700 Subject: [PATCH 06/15] Update lp_settings.h - m_dio_calls_period = 4 --- src/math/lp/lp_settings.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 9df44a22acf..73f39798ba1 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -261,7 +261,7 @@ struct lp_settings { 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 = 1; + unsigned m_dio_calls_period = 4; public: unsigned dio_calls_period() const { return m_dio_calls_period; } From 3fd7ee93be17b62c8c16a010b898c54e22308d6c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson <5377127+levnach@users.noreply.github.com> Date: Sat, 5 Apr 2025 10:27:49 -0700 Subject: [PATCH 07/15] dio_calls_period=4 --- src/math/lp/lp_params_helper.pyg | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index b32b5c207f7..75bd7c33372 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -7,6 +7,6 @@ def_module_params(module_name='lp', ('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, 1, 'Period of calling the Diophantine handler in the final_check()'), + ('dio_calls_period', UINT, 4, 'Period of calling the Diophantine handler in the final_check()'), )) - \ No newline at end of file + From df10608db8904f0058a3b63bd99184f4a47c653e Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 7 Apr 2025 11:49:39 -0700 Subject: [PATCH 08/15] reject more terms with big numbers Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 2864650d37f..4ae49787b10 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1065,9 +1065,11 @@ namespace lp { void process_changed_columns(std_vector &f_vector) { find_changed_terms_and_more_changed_rows(); for (unsigned j: m_changed_terms) { - if (j >= lra.column_count()) + if (j >= lra.column_count() || + !lra.column_has_term(j) || + (ignore_big_nums() && term_has_big_number(lra.get_term(j))) + ) continue; - SASSERT(!ignore_big_nums() || !term_has_big_number(lra.get_term(j))); m_terms_to_tighten.insert(j); if (j < m_l_matrix.column_count()) { for (const auto& cs : m_l_matrix.column(j)) { From 0011deea5c1736413d66d7a5def6ca9918388574 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 8 Apr 2025 06:18:57 -0700 Subject: [PATCH 09/15] typo Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 4ae49787b10..9270b4d62bd 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1646,7 +1646,7 @@ 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); } From dd1b2a294faa8e986eda494cb629584d2ee747f5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 8 Apr 2025 07:07:00 -0700 Subject: [PATCH 10/15] change the name of m_changed_columns to m_changed_f_columns Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 44 ++++++++++++++++------------------------ 1 file changed, 17 insertions(+), 27 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 9270b4d62bd..6ba0d8cc7ec 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -504,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 @@ -776,7 +776,7 @@ 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; @@ -833,7 +833,7 @@ namespace lp { if (ignore_big_nums() && lra.get_lower_bound(j).x.is_big()) 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)); } @@ -1014,7 +1014,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) { @@ -1114,7 +1114,7 @@ namespace lp { 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()); @@ -1630,7 +1630,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; } @@ -1801,30 +1801,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; } @@ -1887,10 +1880,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; } @@ -1966,7 +1956,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()); From 019da2308ec538a86e75456854dc08de7e44dc1c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 8 Apr 2025 10:47:51 -0700 Subject: [PATCH 11/15] always remove the tightened term Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 6ba0d8cc7ec..1458a70548e 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -1543,10 +1543,13 @@ namespace lp { // print_bounds(tout); ); for (unsigned j : sorted_changed_terms) { - m_terms_to_tighten.remove(j); - if (ignore_big_nums() && term_has_big_number(lra.get_term(j))) + if (ignore_big_nums() && term_has_big_number(lra.get_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; @@ -1892,7 +1895,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; From 7ee34151501242638597e0af7e4c3e1cd5934046 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 8 Apr 2025 16:10:17 -0700 Subject: [PATCH 12/15] make gcd call in dio optional Signed-off-by: Lev Nachmanson --- src/math/lp/int_solver.cpp | 6 +++--- src/math/lp/lp_params_helper.pyg | 3 ++- src/math/lp/lp_settings.cpp | 3 ++- src/math/lp/lp_settings.h | 19 ++++++++++++------- src/sat/smt/arith_solver.cpp | 2 +- src/smt/theory_lra.cpp | 2 +- 6 files changed, 21 insertions(+), 14 deletions(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index e12767252e1..fe081fa6e49 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -185,19 +185,19 @@ namespace lp { } bool should_gomory_cut() { - bool dio_allows_gomory = !settings().dio_eqs() || settings().dio_enable_gomory_cuts() || + 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 % settings().dio_calls_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; } diff --git a/src/math/lp/lp_params_helper.pyg b/src/math/lp/lp_params_helper.pyg index 75bd7c33372..3e393dc037f 100644 --- a/src/math/lp/lp_params_helper.pyg +++ b/src/math/lp/lp_params_helper.pyg @@ -2,11 +2,12 @@ def_module_params(module_name='lp', class_name='lp_params_helper', description='linear programming parameters', export=True, - params=(('dio_eqs', BOOL, False, 'use Diophantine equalities'), + 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 42df2272445..ea662f1116b 100644 --- a/src/math/lp/lp_settings.cpp +++ b/src/math/lp/lp_settings.cpp @@ -34,11 +34,12 @@ void lp::lp_settings::updt_params(params_ref const& _p) { report_frequency = p.arith_rep_freq(); m_simplex_strategy = static_cast(p.arith_simplex_strategy()); m_nlsat_delay = p.arith_nl_delay(); - m_dio_eqs = lp_p.dio_eqs(); + 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 73f39798ba1..92d7102b3fb 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -218,8 +218,12 @@ struct lp_settings { 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; @@ -254,7 +258,7 @@ struct lp_settings { 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 @@ -262,7 +266,7 @@ struct lp_settings { 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; } @@ -272,9 +276,10 @@ struct lp_settings { 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); } diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 813faba3d24..cd280d158e3 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/theory_lra.cpp b/src/smt/theory_lra.cpp index 72fac237149..657775a6ae9 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -871,7 +871,7 @@ class theory_lra::imp { 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()); } From 7e88064da96d8fb914a7be50776e5e9ed363bad2 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 9 Apr 2025 10:23:55 -0700 Subject: [PATCH 13/15] allow gcd when dio ignores some terms Signed-off-by: Lev Nachmanson --- src/math/lp/int_solver.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index fe081fa6e49..e3574d5defb 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -223,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); From 97bb449a24299f76effdebdd9e3a0d741a509107 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 9 Apr 2025 15:56:44 -0700 Subject: [PATCH 14/15] fix a bug in tracking the changes in dio Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 102 +++++++++++++++++++-------------------- 1 file changed, 51 insertions(+), 51 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 1458a70548e..d110ff508ff 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -783,18 +783,20 @@ namespace lp { std_vector m_branch_stats; std_vector m_branch_stack; std_vector m_explanation_of_branches; - bool term_has_big_number(const lar_term& t) const { + // 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()) - return true; - if (is_fixed(p.var()) && lra.get_lower_bound(p.var()).x.is_big()) + if (abs(p.coeff()) > mpq(5) || 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;); @@ -803,14 +805,7 @@ namespace lp { 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 (ignore_big_nums() && term_has_big_number(*t)) { - TRACE("dio", tout << "term_has_big_number\n";); - m_some_terms_are_ignored = true; - return; - } m_added_terms.push_back(t); mark_term_change(t->j()); auto undo = undo_add_term(*this, t); @@ -825,13 +820,10 @@ namespace lp { void update_column_bound_callback(unsigned j) { if (!lra.column_is_int(j)) return; - if (lra.column_has_term(j) && - ignore_big_nums() && !term_has_big_number(lra.get_term(j))) + if (lra.column_has_term(j)) m_terms_to_tighten.insert(j); // the boundary of the term has changed: we can be successful to tighten this term if (!lra.column_is_fixed(j)) return; - if (ignore_big_nums() && lra.get_lower_bound(j).x.is_big()) - return; TRACE("dio", tout << "j:" << j << "\n"; lra.print_column_info(j, tout);); m_changed_f_columns.insert(j); lra.trail().push(undo_fixed_column(*this, j)); @@ -861,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;); @@ -1062,20 +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) { - if (j >= lra.column_count() || - !lra.column_has_term(j) || - (ignore_big_nums() && term_has_big_number(lra.get_term(j))) - ) - continue; - 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 @@ -1085,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_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 { @@ -1185,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 @@ -1543,7 +1538,7 @@ namespace lp { // print_bounds(tout); ); for (unsigned j : sorted_changed_terms) { - if (ignore_big_nums() && term_has_big_number(lra.get_term(j))) { + if (is_big_term_or_no_term(j)) { m_terms_to_tighten.remove(j); continue; } @@ -1578,24 +1573,30 @@ namespace lp { 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())) { const mpq& b = lia.lower_bound(p.j()).x; - if (ignore_big_nums() && b.is_big()) - return false; + if (ignore_big_nums() && b.is_big()) { + ret = false; + break; + } m_c += p.coeff() * b; } else { unsigned lj = lar_solver_to_local(p.j()); - SASSERT(!p.coeff().is_big()); + 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 true; + return ret; } unsigned lar_solver_to_local(unsigned j) const { @@ -2239,8 +2240,6 @@ namespace lp { for (unsigned k = 0; k < lra.terms().size(); k++) { const lar_term* t = lra.terms()[k]; if (!lia.column_is_int(t->j())) continue; - if (ignore_big_nums() && term_has_big_number(*t)) - continue; SASSERT(t->j() != UINT_MAX); for (const auto& p : (*t).ext_coeffs()) { unsigned j = p.var(); @@ -2288,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++) { From 36a0006f595c746a98c133ba38671ab5659dacf6 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 9 Apr 2025 19:24:59 -0700 Subject: [PATCH 15/15] remove testing code in is_big_term_on_no_term Signed-off-by: Lev Nachmanson --- src/math/lp/dioph_eq.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index d110ff508ff..b8d94223575 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -786,7 +786,7 @@ namespace lp { // 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 (abs(p.coeff()) > mpq(5) || p.coeff().is_big() || (is_fixed(p.var()) && lra.get_lower_bound(p.var()).x.is_big())) { + 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; }