From fec5b2cece4aeaa875980ac3e85b68f8af2e6b0f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Aug 2026 20:09:12 -0700 Subject: [PATCH] Avoid eager Diophantine matrix elimination on pop Mark derived Diophantine state stale when scoped terms are removed and rebuild it from surviving tracked terms on the next check. This keeps scope restoration bounded and avoids rational coefficient blow-up during pop. Add scoped rebuild coverage. Fix #10417 Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: a8f87ede-b718-4fe9-9839-cc9eaaf9c3a7 --- src/math/lp/dioph_eq.cpp | 59 ++++++++++++++++++++++++++++------- src/math/lp/static_matrix.cpp | 1 + src/test/lp/lp.cpp | 35 ++++++++++++++------- src/test/main.cpp | 1 + 4 files changed, 73 insertions(+), 23 deletions(-) diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp index 68aafaab6c..3f5bd862c0 100644 --- a/src/math/lp/dioph_eq.cpp +++ b/src/math/lp/dioph_eq.cpp @@ -91,6 +91,11 @@ namespace lp { unsigned size() const { return static_cast(m_map.size()); } + void clear() { + m_map.clear(); + m_rev_map.clear(); + } + void erase_val(unsigned b) { VERIFY(contains(m_rev_map, b) && contains(m_map, m_rev_map[b])); auto it = m_rev_map.find(b); @@ -174,6 +179,10 @@ namespace lp { bool has_key(unsigned j) const { return m_bij.has_key(j); } bool has_second_key(unsigned j) const { return m_bij.has_val(j); } + void clear() { + m_bij.clear(); + m_data.clear(); + } // Get the data by 'a', look up b in m_bij, then read from m_data const T& get_by_key(unsigned a) const { unsigned b = m_bij[a]; // relies on operator[](unsigned) from bijection @@ -348,6 +357,7 @@ namespace lp { // 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; + bool m_rebuild_required = 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; @@ -558,21 +568,10 @@ namespace lp { } return; } - // deregister the term that has been activated - for (const auto& p : t->ext_coeffs()) { - TRACE(dio_reg, tout << "derigister p.var():" << p.var() << "->" << t->j() << std::endl;); - auto it = m_columns_to_terms.find(p.var()); - SASSERT(it != m_columns_to_terms.end()); - it->second.erase(t->j()); - if (it->second.size() == 0) { - m_columns_to_terms.erase(it); - } - } SASSERT(std::find(m_added_terms.begin(), m_added_terms.end(), t) == m_added_terms.end()); SASSERT(contains(m_active_terms, t)); m_active_terms.erase(t); - TRACE(dio, tout << "the deleted term column in m_l_matrix" << std::endl; for (auto p : m_l_matrix.column(t->j())) { tout << "p.coeff():" << p.coeff() << ", row " << p.var() << std::endl; } tout << "m_l_matrix has " << m_l_matrix.column_count() << " columns" << std::endl; tout << "and " << m_l_matrix.row_count() << " rows" << std::endl; print_lar_term_L(*t, tout); tout << "; t->j()=" << t->j() << std::endl;); - shrink_matrices(); + m_rebuild_required = true; } struct undo_add_term : public trail { @@ -1233,6 +1232,8 @@ namespace lp { } void init(std_vector & f_vector) { + if (m_rebuild_required) + rebuild(); m_infeas_explanation.clear(); lia.get_term().clear(); reset_conflict(); @@ -1250,6 +1251,40 @@ namespace lp { SASSERT(entries_are_ok()); } + void rebuild() { + std::unordered_set tracked_terms = m_active_terms; + tracked_terms.insert(m_added_terms.begin(), m_added_terms.end()); + + m_sum_of_fixed.clear(); + m_var_register.clear(); + m_e_matrix.clear(); + m_l_matrix.clear(); + m_infeas_explanation.clear(); + m_c = mpq(0); + m_lspace.clear(); + m_espace.clear(); + m_k2s.clear(); + m_fresh_k2xt_terms.clear(); + m_row2fresh_defs.clear(); + m_changed_rows.reset(); + m_changed_f_columns.reset(); + m_changed_terms.reset(); + m_terms_to_tighten.reset(); + m_columns_to_terms.clear(); + m_q.reset(); + reset_conflict(); + + m_added_terms.clear(); + m_active_terms.clear(); + for (const lar_term* t : lra.terms()) { + if (contains(tracked_terms, t)) { + m_added_terms.push_back(t); + mark_term_change(t->j()); + } + } + m_rebuild_required = false; + } + template mpq gcd_of_coeffs(const K& k, bool check_for_one) { if (check_for_one) diff --git a/src/math/lp/static_matrix.cpp b/src/math/lp/static_matrix.cpp index 4abf0d88a0..685fd62a60 100644 --- a/src/math/lp/static_matrix.cpp +++ b/src/math/lp/static_matrix.cpp @@ -38,6 +38,7 @@ namespace lp { template mpq static_matrix::get_max_abs_in_row(unsigned int) const; template mpq static_matrix::get_min_abs_in_column(unsigned int) const; template mpq static_matrix::get_min_abs_in_row(unsigned int) const; + template void static_matrix::clear(); template void static_matrix::init_row_columns(unsigned int, unsigned int); template static_matrix::ref& static_matrix::ref::operator=(mpq const&); template void static_matrix::set(unsigned int, unsigned int, mpq const&); diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index 374c2e2aea..61775211ba 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -1696,24 +1696,34 @@ void test_dio() { for (auto & p: term_ls) { p.first = -p.first; } - unsigned t1 = solver.add_term(term_ls, 11); - solver.add_var_bound(fx_7, LE, mpq(-7)); solver.add_var_bound(fx_7, GE, mpq(-7)); - solver.add_var_bound(fx_17, LE, mpq(-17)); - solver.add_var_bound(fx_17, GE, mpq(-17)); solver.add_var_bound(t0, LE, mpq(0)); solver.add_var_bound(t0, GE, mpq(0)); + solver.find_feasible_solution(); + ENSURE(solver.get_status() == lp_status::OPTIMAL); +#ifdef Z3DEBUG + i_solver.dio_test(); +#endif + + solver.push(); + unsigned t1 = solver.add_term(term_ls, 11); + solver.add_var_bound(fx_17, LE, mpq(-17)); + solver.add_var_bound(fx_17, GE, mpq(-17)); solver.add_var_bound(t1, LE, mpq(0)); solver.add_var_bound(t1, GE, mpq(0)); -// solver.find_feasible_solution(); - //ENSURE(solver.get_status() == lp_status::OPTIMAL); - enable_trace("dioph_eq"); - enable_trace("dioph_eq_fresh"); -#ifdef Z3DEBUG + solver.find_feasible_solution(); + ENSURE(solver.get_status() == lp_status::OPTIMAL); +#ifdef Z3DEBUG i_solver.dio_test(); -#endif - +#endif + + solver.pop(); + solver.find_feasible_solution(); + ENSURE(solver.get_status() == lp_status::OPTIMAL); +#ifdef Z3DEBUG + i_solver.dio_test(); +#endif } #ifdef Z3DEBUG void test_hnf() { @@ -2024,6 +2034,9 @@ void test_lp_local(int argn, char **argv) { void tst_lp(char **argv, int argc, int &i) { lp::test_lp_local(argc - 2, argv + 2); } +void tst_lp_dio() { + lp::test_dio(); +} // clang-format on bool coprime(int a, int b) { return gcd(rational(a), rational(b)).is_one(); diff --git a/src/test/main.cpp b/src/test/main.cpp index b8d18d3b40..60dca29157 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -134,6 +134,7 @@ X(ackermannize) \ X(monomial_bounds) \ X(nla_intervals) \ + X(lp_dio) \ X(horner) \ X(prime_generator) \ X(permutation) \