From 93ff89bf9807ca305b49faae77f379f0bfab36ac Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 2 Oct 2024 08:00:23 -0700
Subject: [PATCH] add == for const_ref and ref to disambiguate equality.

---
 src/math/lp/stacked_vector.h | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

diff --git a/src/math/lp/stacked_vector.h b/src/math/lp/stacked_vector.h
index 69ff99263..88e79749b 100644
--- a/src/math/lp/stacked_vector.h
+++ b/src/math/lp/stacked_vector.h
@@ -51,13 +51,21 @@ public:
         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 @@ public:
     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: