From c03fac8390d83345df58d4da43828447c485f194 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 24 Apr 2021 14:50:59 -0700
Subject: [PATCH] Investigating std::vector and #5178

---
 src/math/polynomial/linear_eq_solver.h |  2 +-
 src/math/polynomial/polynomial.h       |  2 +-
 src/math/simplex/model_based_opt.h     |  3 ++-
 src/util/vector.h                      | 20 +++++++++++++++-----
 4 files changed, 19 insertions(+), 8 deletions(-)

diff --git a/src/math/polynomial/linear_eq_solver.h b/src/math/polynomial/linear_eq_solver.h
index 8499d3a5a..4196e5434 100644
--- a/src/math/polynomial/linear_eq_solver.h
+++ b/src/math/polynomial/linear_eq_solver.h
@@ -34,7 +34,7 @@ public:
     
     void flush() {
         SASSERT(b.size() == A.size());
-        unsigned sz = A.size();
+        auto sz = A.size();
         for (unsigned i = 0; i < sz; i++) {
             svector<numeral> & as = A[i];
             m.del(b[i]);
diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h
index 20c9b6b40..013464c31 100644
--- a/src/math/polynomial/polynomial.h
+++ b/src/math/polynomial/polynomial.h
@@ -133,7 +133,7 @@ namespace polynomial {
             /**
                \brief Number of distinct factors (not counting multiplicities).
             */
-            unsigned distinct_factors() const { return m_factors.size(); }
+            size_t distinct_factors() const { return m_factors.size(); }
             
             /**
                \brief Number of distinct factors (counting multiplicities).
diff --git a/src/math/simplex/model_based_opt.h b/src/math/simplex/model_based_opt.h
index 6ea38e0bb..047f03cc4 100644
--- a/src/math/simplex/model_based_opt.h
+++ b/src/math/simplex/model_based_opt.h
@@ -39,8 +39,9 @@ namespace opt {
     class model_based_opt {
     public:
         struct var {
-            unsigned m_id;
+            unsigned m_id { 0 };
             rational m_coeff;
+            var() {}
             var(unsigned id, rational const& c): m_id(id), m_coeff(c) {}
             struct compare {
                 bool operator()(var x, var y) {
diff --git a/src/util/vector.h b/src/util/vector.h
index c6981d362..a3787d300 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -53,6 +53,15 @@ Revision History:
 // };
 //
 
+// Note:
+// polynomial.h contains declaration
+// typedef svector<numeral>                        numeral_vector;
+// it is crucial that it uses svector and not vector. The destructors on elements of the numeral vector are handled outside.
+// Numeral gets instantiated by mpz and mpz does not support copy constructors.
+// porting svector to vector is therefore blocked on the semantics of svector being 
+// copy-constructor free.
+// 
+
 #include <vector>
 
 template<typename T, bool CallDestructors=true, typename SZ = unsigned>
@@ -63,13 +72,14 @@ public:
 
     vector() {}
     vector(SZ s) {
-        // resize(s, T());
+        // TODO resize(s, T());
     }
     vector(SZ s, T const& e) {
-        // resize(s, e);
+        // TODO resize(s, e);
     }
 
     vector(SZ s, T const* e) {
+        // TODO
     }
 
     void reset() { clear(); }
@@ -100,11 +110,11 @@ public:
     }
     
     void erase(iterator pos) {
-
+        // TODO
     }
 
     void erase(T const& e) {
-
+        // TODO
     }
     void fill(T const & elem) {
         for (auto& e : *this)
@@ -133,7 +143,7 @@ public:
     }
 
     void append(unsigned n,  T const* elems) {
-        
+        // TODO
     }
 
     bool contains(T const & elem) const {