mirror of
https://github.com/Z3Prover/z3
synced 2026-08-08 06:52:26 +00:00
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
This commit is contained in:
Nikolaj Bjorner
parent
9167020d83
commit
fec5b2cece
4 changed files with 73 additions and 23 deletions
|
|
@ -91,6 +91,11 @@ namespace lp {
|
|||
|
||||
unsigned size() const { return static_cast<unsigned>(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<mpq> 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<unsigned> & 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<const lar_term*> 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 <typename K>
|
||||
mpq gcd_of_coeffs(const K& k, bool check_for_one) {
|
||||
if (check_for_one)
|
||||
|
|
|
|||
|
|
@ -38,6 +38,7 @@ namespace lp {
|
|||
template mpq static_matrix<mpq, mpq>::get_max_abs_in_row(unsigned int) const;
|
||||
template mpq static_matrix<mpq, mpq>::get_min_abs_in_column(unsigned int) const;
|
||||
template mpq static_matrix<mpq, mpq>::get_min_abs_in_row(unsigned int) const;
|
||||
template void static_matrix<mpq, mpq>::clear();
|
||||
template void static_matrix<mpq, mpq>::init_row_columns(unsigned int, unsigned int);
|
||||
template static_matrix<mpq, mpq>::ref& static_matrix<mpq, mpq>::ref::operator=(mpq const&);
|
||||
template void static_matrix<mpq, mpq>::set(unsigned int, unsigned int, mpq const&);
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
|
|
|
|||
|
|
@ -134,6 +134,7 @@
|
|||
X(ackermannize) \
|
||||
X(monomial_bounds) \
|
||||
X(nla_intervals) \
|
||||
X(lp_dio) \
|
||||
X(horner) \
|
||||
X(prime_generator) \
|
||||
X(permutation) \
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue