add == for const_ref and ref to disambiguate equality.

Z3Prover · Oct 2, 2024 · 93ff89b · 93ff89b
1 parent c7af973
commit 93ff89b
Showing 1 changed file with 16 additions and 4 deletions.
diff --git a/src/math/lp/stacked_vector.h b/src/math/lp/stacked_vector.h
@@ -51,13 +51,21 @@ template < typename B> class stacked_vector {
         operator const B&() const {
             return m_vec.m_vector[m_i];
         }
-        
+
         bool operator==(B const& other) const {
             return m_vec.m_vector[m_i] == other;
         }
         bool operator!=(B const& other) const {
             return m_vec.m_vector[m_i] != other;
         }
+        bool operator==(ref const& other) const {
+            return m_vec.m_vector[m_i] == other.m_vec.m_vector[other.m_i];
+        }
+        bool operator!=(ref  const& other) const {
+            return m_vec.m_vector[m_i] != other.m_vec.m_vectpr[other.m_i];
+        }
+
+
         B& operator+=(B const &delta) {
             // not tracking the change here!
             return m_vec.m_vector[m_i] += delta;
@@ -74,12 +82,16 @@ template < typename B> class stacked_vector {
     public:
         ref_const(const stacked_vector<B> &m, unsigned key) :m_vec(m), m_i(key) {
             lp_assert(key < m.size());
-        }
-
+        } 
         operator const B&() const {
             return m_vec.m_vector[m_i];
         }
-
+        bool operator==(ref_const const& other) const {
+            return m_vec.m_vector[m_i] == other.m_vec.m_vector[other.m_i];
+        }
+        bool operator!=(ref_const const& other) const {
+            return m_vec.m_vector[m_i] != other.m_vec.m_vectpr[other.m_i];
+        }
     };
 
 private: