mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Merge pull request #927 from mtrberzi/zstring-patch
Add boolean operators and stream<< to zstring
This commit is contained in:
commit
91eddecd6e
|
@ -284,8 +284,54 @@ zstring zstring::operator+(zstring const& other) const {
|
|||
return result;
|
||||
}
|
||||
|
||||
std::ostream& zstring::operator<<(std::ostream& out) const {
|
||||
return out << encode();
|
||||
bool zstring::operator==(const zstring& other) const {
|
||||
// two strings are equal iff they have the same length and characters
|
||||
if (length() != other.length()) {
|
||||
return false;
|
||||
}
|
||||
for (unsigned i = 0; i < length(); ++i) {
|
||||
unsigned Xi = m_buffer[i];
|
||||
unsigned Yi = other[i];
|
||||
if (Xi != Yi) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
bool zstring::operator!=(const zstring& other) const {
|
||||
return !(*this == other);
|
||||
}
|
||||
|
||||
std::ostream& operator<<(std::ostream &os, const zstring &str) {
|
||||
return os << str.encode();
|
||||
}
|
||||
|
||||
bool operator<(const zstring& lhs, const zstring& rhs) {
|
||||
// This has the same semantics as strcmp()
|
||||
unsigned len = lhs.length();
|
||||
if (rhs.length() < len) {
|
||||
len = rhs.length();
|
||||
}
|
||||
for (unsigned i = 0; i < len; ++i) {
|
||||
unsigned Li = lhs[i];
|
||||
unsigned Ri = rhs[i];
|
||||
if (Li < Ri) {
|
||||
return true;
|
||||
} else if (Li > Ri) {
|
||||
return false;
|
||||
} else {
|
||||
continue;
|
||||
}
|
||||
}
|
||||
// at this point, all compared characters are equal,
|
||||
// so decide based on the relative lengths
|
||||
if (lhs.length() < rhs.length()) {
|
||||
return true;
|
||||
} else {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -114,7 +114,11 @@ public:
|
|||
int indexof(zstring const& other, int offset) const;
|
||||
zstring extract(int lo, int hi) const;
|
||||
zstring operator+(zstring const& other) const;
|
||||
std::ostream& operator<<(std::ostream& out) const;
|
||||
bool operator==(const zstring& other) const;
|
||||
bool operator!=(const zstring& other) const;
|
||||
|
||||
friend std::ostream& operator<<(std::ostream &os, const zstring &str);
|
||||
friend bool operator<(const zstring& lhs, const zstring& rhs);
|
||||
};
|
||||
|
||||
class seq_decl_plugin : public decl_plugin {
|
||||
|
|
Loading…
Reference in a new issue