From 85db8163fa6a9e9c99c15899a306d59e20be9b6c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 19 Sep 2023 13:57:28 -0700
Subject: [PATCH] move allocator to memory_manager and std_vector to vector

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/lp_bound_propagator.h | 23 ++++++-----------------
 src/math/lp/nla_monotone_lemmas.h |  2 +-
 src/util/memory_manager.h         | 13 +++++++++++++
 src/util/vector.h                 |  3 +++
 4 files changed, 23 insertions(+), 18 deletions(-)

diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 6a01d4ace..d035d9bcb 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -9,29 +9,18 @@
 #include "math/lp/lp_settings.h"
 #include "util/uint_set.h"
 #include "math/lp/implied_bound.h"
-#include <vector>
+#include "util/vector.h"
 namespace lp {
-template <typename T>
-struct my_allocator {
-    using value_type = T;
-
-    T* allocate(std::size_t n) {
-        return static_cast<T*>(memory::allocate(n * sizeof(T)));
-    }
-
-    void deallocate(T* p, std::size_t n) {
-        memory::deallocate(p);
-    }
-};    
+    
 template <typename T>
 class lp_bound_propagator {
-	uint_set m_visited_rows;
+    uint_set m_visited_rows;
     // these maps map a column index to the corresponding index in ibounds
     u_map<unsigned> m_improved_lower_bounds;
     u_map<unsigned> m_improved_upper_bounds;
 
     T& m_imp;
-    std::vector<implied_bound, my_allocator<implied_bound>> m_ibounds;
+    std_vector<implied_bound> m_ibounds;
 
     map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_val2fixed_row;
     // works for rows of the form x + y + sum of fixed = 0
@@ -119,10 +108,10 @@ private:
         ~reset_cheap_eq() { p.reset_cheap_eq_eh(); }
     };
 
-   public:
+public:
     lp_bound_propagator(T& imp) : m_imp(imp) {}
 
-    const std::vector<implied_bound, my_allocator<implied_bound>>& ibounds() const { return m_ibounds; }
+    const std_vector<implied_bound>& ibounds() const { return m_ibounds; }
 
     void init() {
         m_improved_upper_bounds.reset();
diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h
index d13f588e8..2cb646777 100644
--- a/src/math/lp/nla_monotone_lemmas.h
+++ b/src/math/lp/nla_monotone_lemmas.h
@@ -16,7 +16,7 @@ private:
     void monotonicity_lemma(monic const& m);
     void monotonicity_lemma_gt(const monic& m);    
     void monotonicity_lemma_lt(const monic& m);
-    std::vector<rational> get_sorted_key(const monic& rm) const;
+    // std_vector<rational> get_sorted_key(const monic& rm) const;
     vector<std::pair<rational, lpvar>> get_sorted_key_with_rvars(const monic& a) const;
 };
 }
diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h
index 7dab520df..053816449 100644
--- a/src/util/memory_manager.h
+++ b/src/util/memory_manager.h
@@ -128,6 +128,19 @@ void dealloc_svect(T * ptr) {
     memory::deallocate(ptr);
 }
 
+template <typename T>
+struct std_allocator {
+    using value_type = T;
+
+    T* allocate(std::size_t n) {
+        return static_cast<T*>(memory::allocate(n * sizeof(T)));
+    }
+
+    void deallocate(T* p, std::size_t n) {
+        memory::deallocate(p);
+    }
+};
+
 struct mem_stat {
 };
 
diff --git a/src/util/vector.h b/src/util/vector.h
index 1cb25a8c4..9ca9a1103 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -33,6 +33,7 @@ Revision History:
 #include "util/memory_manager.h"
 #include "util/hash.h"
 #include "util/z3_exception.h"
+#include <vector>
 
 // disable warning for constant 'if' expressions.
 // these are used heavily in templates.
@@ -40,6 +41,8 @@ Revision History:
 #pragma warning(disable:4127)
 #endif
 
+template <typename T>
+class std_vector : public std::vector<T, std_allocator<T>> {};
 
 #if 0