mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add == for const_ref and ref to disambiguate equality.

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-10-02 08:00:23 -07:00
parent c7af97364a
commit 93ff89bf98
1 changed files with 16 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/math/lp/stacked_vector.h
View file

@ -51,13 +51,21 @@ public:
operator const B&() const { operator const B&() const {
return m_vec.m_vector[m_i]; return m_vec.m_vector[m_i];
} }
bool operator==(B const& other) const { bool operator==(B const& other) const {
return m_vec.m_vector[m_i] == other; return m_vec.m_vector[m_i] == other;
} }
bool operator!=(B const& other) const { bool operator!=(B const& other) const {
return m_vec.m_vector[m_i] != other; 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) { B& operator+=(B const &delta) {
// not tracking the change here! // not tracking the change here!
return m_vec.m_vector[m_i] += delta; return m_vec.m_vector[m_i] += delta;
@ -74,12 +82,16 @@ public:
public: public:
ref_const(const stacked_vector<B> &m, unsigned key) :m_vec(m), m_i(key) { ref_const(const stacked_vector<B> &m, unsigned key) :m_vec(m), m_i(key) {
lp_assert(key < m.size()); lp_assert(key < m.size());
} }
operator const B&() const { operator const B&() const {
return m_vec.m_vector[m_i]; 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: private: