From 3e49d9fcfe1fdec5ebc9d4582d7e0f1934023101 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 3 Apr 2025 09:47:02 -0700 Subject: [PATCH] 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 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..f085ac5d6 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 4bc9b2fb3..3b48a0405 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 000000000..2057b3823 --- /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 9d2fe675e..e2f780ee1 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 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'),