use std_vector more and getting NOT_IMPLEMENTING in C:\dev\z3\src\math\lp\dioph_eq.cpp

levnach · levnach · commit 008e9229a575 · 2025-02-11T12:23:00.000-10:00
Signed-off-by: Lev Nachmanson &lt;levnach@hotmail.com&gt;
diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
@@ -328,6 +328,7 @@ namespace lp {
        public:
         imp(int_solver& lia, lar_solver& lra) : lia(lia), lra(lra) {
             lra.register_add_term_delegate([this](const lar_term*t){add_term_delegate(t);});
+            lra.register_add_column_bound_delegate([this](unsigned j) {add_column_bound_delegate(j);});
         }
         term_o get_term_from_entry(unsigned i) const {
             term_o t;
@@ -395,15 +396,10 @@ namespace lp {
         }
 
         void init() {
-            m_e_matrix = static_matrix<mpq, mpq>();
             m_report_branch = false;
-            m_k2s.clear();
-            m_fresh_definitions.clear();
             m_conflict_index = -1;
             m_infeas_explanation.clear();
             lia.get_term().clear();
-            m_entries.clear();
-            m_var_register.clear();
             m_number_of_iterations = 0;
             m_branch_stack.clear();
             m_lra_level = 0;
@@ -1071,7 +1067,6 @@ namespace lp {
                     if (m_branch_stack.size() == 0) {
                            lra.stats().m_dio_branching_infeasibles++;
                            transfer_explanations_from_closed_branches();
-                           enable_trace("dioph_eq");
                            return lia_move::conflict;
                     }
                     TRACE("dio_br", tout << lp_status_to_string(lra.get_status()) << std::endl;
@@ -1393,7 +1388,7 @@ namespace lp {
                     m_e_matrix.add_new_element(fresh_row, i, q);
             }
 
-            m_k2s.resize(std::max(k + 1, xt + 1), -1);
+            m_k2s.resize(k + 1, -1);
             m_k2s[k] = fresh_row;
             m_fresh_definitions.resize(xt + 1, -1);
             m_fresh_definitions[xt] = fresh_row;
diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
@@ -668,7 +668,7 @@ namespace lp {
         return display_row(out, row);
     }
 
-    std::ostream & int_solver::display_row(std::ostream & out, vector<row_cell<rational>> const & row) const {
+    std::ostream & int_solver::display_row(std::ostream & out, std_vector<row_cell<rational>> const & row) const {
         return m_imp->display_row(out, row);
 }
     
diff --git a/src/math/lp/int_solver.h b/src/math/lp/int_solver.h
@@ -89,7 +89,7 @@ class int_solver {
 
     bool shift_var(unsigned j, unsigned range);
     std::ostream&  display_row_info(std::ostream & out, unsigned row_index) const;
-    std::ostream & display_row(std::ostream & out, vector<row_cell<rational>> const & row) const;
+    std::ostream & display_row(std::ostream & out, std_vector<row_cell<rational>> const & row) const;
     bool is_term(unsigned j) const;
     unsigned column_count() const;
     int select_int_infeasible_var();
diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h
@@ -34,7 +34,7 @@ class lar_core_solver  {
     stacked_vector<unsigned> m_r_pushed_basis;
     vector<unsigned>         m_r_basis;
     vector<unsigned>         m_r_nbasis;
-    vector<int>              m_r_heading;
+    std_vector<int>              m_r_heading;
     
 
     lp_primal_core_solver<mpq, numeric_pair<mpq>> m_r_solver; // solver in rational numbers
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
@@ -684,7 +684,7 @@ class lar_solver : public column_namer {
     bool ax_is_correct() const;
     bool get_equality_and_right_side_for_term_on_current_x(lpvar j, mpq& rs, u_dependency*& ci, bool& upper_bound) const;
     bool var_is_int(lpvar v) const;
-    inline const vector<int>& r_heading() const { return m_mpq_lar_core_solver.m_r_heading; }
+    inline const std_vector<int>& r_heading() const { return m_mpq_lar_core_solver.m_r_heading; }
     inline const vector<unsigned>& r_basis() const { return m_mpq_lar_core_solver.r_basis(); }
     inline const vector<unsigned>& r_nbasis() const { return m_mpq_lar_core_solver.r_nbasis(); }
     inline bool column_is_real(unsigned j) const { return !column_is_int(j); }
diff --git a/src/math/lp/lp_core_solver_base.cpp b/src/math/lp/lp_core_solver_base.cpp
@@ -30,7 +30,7 @@ template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init
 template void lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::init_basis_heading_and_non_basic_columns_vector();
 template lp::lp_core_solver_base<lp::mpq, lp::numeric_pair<lp::mpq> >::lp_core_solver_base(lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >&, 
     // vector<lp::numeric_pair<lp::mpq> >&, 
-    vector<unsigned int >&, vector<unsigned> &, vector<int> &, vector<lp::numeric_pair<lp::mpq> >&, vector<lp::mpq>&, lp::lp_settings&, const column_namer&, const vector<lp::column_type >&,
+    vector<unsigned int >&, vector<unsigned> &, std_vector<int> &, vector<lp::numeric_pair<lp::mpq> >&, vector<lp::mpq>&, lp::lp_settings&, const column_namer&, const vector<lp::column_type >&,
                                                                                                    const vector<lp::numeric_pair<lp::mpq> >&,
                                                                                                    const vector<lp::numeric_pair<lp::mpq> >&);
 
@@ -39,7 +39,8 @@ template lp::lp_core_solver_base<lp::mpq, lp::mpq>::lp_core_solver_base(
                                                                               lp::static_matrix<lp::mpq, lp::mpq>&,
                                                                               //vector<lp::mpq>&,
                                                                               vector<unsigned int >&,
-                                                                              vector<unsigned> &, vector<int> &,
+                                                                              vector<unsigned> &,
+                                                                              std_vector<int> &,
                                                                               vector<lp::mpq>&,
                                                                               vector<lp::mpq>&,
                                                                               lp::lp_settings&,
diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h
@@ -79,7 +79,7 @@ class lp_core_solver_base {
     // vector<X> const &           m_b; // the right side
     vector<unsigned> &    m_basis;
     vector<unsigned>&     m_nbasis;
-    vector<int>&          m_basis_heading;
+    std_vector<int>&      m_basis_heading;
     vector<X> &           m_x; // a feasible solution, the first time set in the constructor
     vector<T> &           m_costs;
     lp_settings &         m_settings;
@@ -124,7 +124,7 @@ class lp_core_solver_base {
                         //vector<X> & b, // the right side vector
                         vector<unsigned> & basis,
                         vector<unsigned> & nbasis,
-                        vector<int> & heading,
+                        std_vector<int> & heading,
                         vector<X> & x,
                         vector<T> & costs,
                         lp_settings & settings,
@@ -516,8 +516,8 @@ class lp_core_solver_base {
     }
 
     
-    template <typename K>
-    static void swap(vector<K> &v, unsigned i, unsigned j) noexcept {
+    template <typename T>
+    void swap(T &v, unsigned i, unsigned j) noexcept {
         auto t = v[i];
         v[i] = v[j];
         v[j] = t;
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
@@ -31,7 +31,7 @@ lp_core_solver_base(static_matrix<T, X> & A,
                     // vector<X> & b, // the right side vector
                     vector<unsigned> & basis,
                     vector<unsigned> & nbasis,
-                    vector<int> & heading,
+                    std_vector<int> & heading,
                     vector<X> & x,
                     vector<T> & costs,
                     lp_settings & settings,
diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
@@ -640,7 +640,7 @@ namespace lp {
         vector<X> &b,  // the right side vector
         vector<X> &x,  // the number of elements in x needs to be at least as large
                        // as the number of columns in A
-        vector<unsigned> &basis, vector<unsigned> &nbasis, vector<int> &heading,
+        vector<unsigned> &basis, vector<unsigned> &nbasis, std_vector<int> &heading,
         vector<T> &costs, const vector<column_type> &column_type_array,
         const vector<X> &lower_bound_values, const vector<X> &upper_bound_values,
         lp_settings &settings, const column_namer &column_names)
diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp
@@ -127,4 +127,4 @@ template <typename T> void common::create_sum_from_row(const T& row,
 
 
 }
-template void nla::common::create_sum_from_row<vector<lp::row_cell<rational>, true, unsigned int> >(vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, u_dependency*&);  
+template void nla::common::create_sum_from_row<std_vector<lp::row_cell<rational>> >(std_vector<lp::row_cell<rational>> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, u_dependency*&);  
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
@@ -558,7 +558,7 @@ namespace nla {
         add_eq(r, dep);
     }
 
-    void grobner::add_row(const vector<lp::row_cell<rational>> & row) {
+    void grobner::add_row(const std_vector<lp::row_cell<rational>> & row) {
         u_dependency *dep = nullptr;
         rational val;
         dd::pdd sum = m_pdd_manager.mk_val(rational(0));
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
@@ -60,7 +60,7 @@ namespace nla {
         void find_nl_cluster();
         void prepare_rows_and_active_vars();
         void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar>& q);           
-        void add_row(const vector<lp::row_cell<rational>>& row);
+        void add_row(const std_vector<lp::row_cell<rational>>& row);
         void add_fixed_monic(unsigned j);
         bool is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r);
         void add_eq(dd::pdd& p, u_dependency* dep);        
diff --git a/src/math/lp/static_matrix.cpp b/src/math/lp/static_matrix.cpp
@@ -54,7 +54,6 @@ template void static_matrix<mpq, numeric_pair<mpq> >::set(unsigned int, unsigned
 template bool lp::static_matrix<lp::mpq, lp::mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
 template bool lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
 template void lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::pivot_row_to_row_given_cell_with_sign(unsigned int, column_cell&, unsigned int, int);
-template void lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::remove_element(vector<lp::row_cell<lp::mpq>, true, unsigned int>&, lp::row_cell<lp::mpq>&);
 template void lp::static_matrix<mpq, mpq>::pivot_row_to_row_given_cell_with_sign(unsigned int, lp::row_cell<lp::empty_struct>&, unsigned int, int);
 template void lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::add_rows(mpq const&, unsigned int, unsigned int);
 template void lp::static_matrix<lp::mpq,lp::mpq>::add_rows(class rational const &,unsigned int,unsigned int);
diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h
@@ -41,10 +41,10 @@ std::ostream& operator<<(std::ostream& out, const row_cell<T>& rc) {
 }
 struct empty_struct {};
 typedef row_cell<empty_struct> column_cell;
-typedef vector<column_cell> column_strip;
+typedef std_vector<column_cell> column_strip;
 
 template <typename T>
-using row_strip = vector<row_cell<T>>; 
+using row_strip = std_vector<row_cell<T>>; 
 template <typename K> mpq get_denominators_lcm(const K & row) {
     SASSERT(row.size() > 0);
     mpq r = mpq(1);
@@ -79,8 +79,8 @@ class static_matrix
     
     vector<int> m_work_vector_of_row_offsets;
     indexed_vector<T> m_work_vector;
-    vector<row_strip<T>> m_rows;
-    vector<column_strip> m_columns;
+    std_vector<row_strip<T>> m_rows;
+    std_vector<column_strip> m_columns;
     // starting inner classes
     class ref {
         static_matrix & m_matrix;
@@ -153,7 +153,7 @@ class static_matrix
 
     void remove_last_column(unsigned j);
 
-    void remove_element(vector<row_cell<T>> & row, row_cell<T> & elem_to_remove);
+    void remove_element(std_vector<row_cell<T>> & row, row_cell<T> & elem_to_remove);
     
     void multiply_column(unsigned column, T const & alpha) {
         for (auto & t : m_columns[column]) {
@@ -245,7 +245,7 @@ class static_matrix
         m_stack.push(d);
     }
 
-    void pop_row_columns(const vector<row_cell<T>> & row) {
+    void pop_row_columns(const std_vector<row_cell<T>> & row) {
         for (auto & c : row) {
             unsigned j = c.var();
             auto & col = m_columns[j];
@@ -291,7 +291,7 @@ class static_matrix
         }
     }
     
-    T dot_product_with_column(const vector<T> & y, unsigned j) const {
+    T dot_product_with_column(const std_vector<T> & y, unsigned j) const {
         lp_assert(j < column_count());
         T ret = numeric_traits<T>::zero();
         for (auto & it : m_columns[j]) {
@@ -320,7 +320,7 @@ class static_matrix
         }
     
     }
-    void fill_last_row_with_pivoting_loop_block(unsigned j, const vector<int> & basis_heading) {
+    void fill_last_row_with_pivoting_loop_block(unsigned j, const std_vector<int> & basis_heading) {
         int row_index = basis_heading[j];
         if (row_index < 0)
             return;
@@ -352,7 +352,7 @@ class static_matrix
     template <typename term>
     void fill_last_row_with_pivoting(const term& row,
                                      unsigned bj, // the index of the basis column
-                                     const vector<int> & basis_heading) {
+                                     const std_vector<int> & basis_heading) {
         lp_assert(row_count() > 0);
         m_work_vector.resize(column_count());
         T a;
@@ -377,7 +377,7 @@ class static_matrix
         set(last_row, column_count() - 1, one_of_type<T>());
     }
 
-    void copy_column_to_vector (unsigned j, vector<T> & v) const {
+    void copy_column_to_vector (unsigned j, std_vector<T> & v) const {
         v.resize(row_count(), numeric_traits<T>::zero());
         for (auto & it : m_columns[j]) {
             const T& val = get_val(it);
@@ -387,7 +387,7 @@ class static_matrix
     }
     
     template <typename L>
-    L dot_product_with_row(unsigned row, const vector<L> & w) const {
+    L dot_product_with_row(unsigned row, const std_vector<L> & w) const {
         L ret = zero_of_type<L>();
         lp_assert(row < m_rows.size());
         for (auto & it : m_rows[row]) {
@@ -444,11 +444,12 @@ class static_matrix
         };
 
         const_iterator begin() const {
-            return const_iterator(m_A.m_columns[m_j].begin(), m_A);
+            return const_iterator(m_A.m_columns[m_j].data(), m_A);
         }
         
         const_iterator end() const {
-            return const_iterator(m_A.m_columns[m_j].end(), m_A);
+            const auto & column = m_A.m_columns[m_j];
+            return const_iterator(column.data() + column.size(), m_A);
         }
     };
 
diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h
@@ -421,7 +421,7 @@ template <typename T, typename X> bool static_matrix<T, X>::is_correct() const {
 }
 
 template <typename T, typename X>
-void static_matrix<T, X>::remove_element(vector<row_cell<T>> & row_vals, row_cell<T> & row_el_iv) {
+void static_matrix<T, X>::remove_element(std_vector<row_cell<T>> & row_vals, row_cell<T> & row_el_iv) {
     unsigned column_offset = row_el_iv.offset();
     auto & column_vals = m_columns[row_el_iv.var()];
     column_cell& cs = m_columns[row_el_iv.var()][column_offset];

Original file line number	Diff line number	Diff line change
`@@ -668,7 +668,7 @@ namespace lp {`
`668`	`668`	`return display_row(out, row);`
`669`	`669`	`}`
`670`	`670`
`671`		`- std::ostream & int_solver::display_row(std::ostream & out, vector<row_cell<rational>> const & row) const {`
	`671`	`+ std::ostream & int_solver::display_row(std::ostream & out, std_vector<row_cell<rational>> const & row) const {`
`672`	`672`	`return m_imp->display_row(out, row);`
`673`	`673`	`}`
`674`	`674`
Original file line number	Diff line number	Diff line change
`@@ -127,4 +127,4 @@ template <typename T> void common::create_sum_from_row(const T& row,`
`127`	`127`
`128`	`128`
`129`	`129`	`}`
`130`		`-template void nla::common::create_sum_from_row<vector<lp::row_cell<rational>, true, unsigned int> >(vector<lp::row_cell<rational>, true, unsigned int> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, u_dependency*&);`
	`130`	`+template void nla::common::create_sum_from_row<std_vector<lp::row_cell<rational>> >(std_vector<lp::row_cell<rational>> const&, nla::nex_creator&, nla::nex_creator::sum_factory&, u_dependency*&);`