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) \