Move char_range and char_set from seq_nielsen to zstring

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/util/zstring.cpp

@@ -286,3 +286,146 @@ bool operator<(const zstring& lhs, const zstring& rhs) {
     // so decide based on the relative lengths
     return lhs.length() < rhs.length();
 }
+
+// -----------------------------------------------
+// char_set
+// -----------------------------------------------
+
+unsigned char_set::char_count() const {
+    unsigned count = 0;
+    for (auto const& r : m_ranges)
+        count += r.length();
+    return count;
+}
+
+bool char_set::contains(unsigned c) const {
+    // binary search over sorted non-overlapping ranges
+    int lo = 0, hi = static_cast<int>(m_ranges.size()) - 1;
+    while (lo <= hi) {
+        int mid = lo + (hi - lo) / 2;
+        if (c < m_ranges[mid].m_lo)
+            hi = mid - 1;
+        else if (c >= m_ranges[mid].m_hi)
+            lo = mid + 1;
+        else
+            return true;
+    }
+    return false;
+}
+
+void char_set::add(unsigned c) {
+    if (m_ranges.empty()) {
+        m_ranges.push_back(char_range(c));
+        return;
+    }
+    // binary search for insertion point
+    int lo = 0, hi = static_cast<int>(m_ranges.size()) - 1;
+    while (lo <= hi) {
+        int mid = lo + (hi - lo) / 2;
+        if (c < m_ranges[mid].m_lo)
+            hi = mid - 1;
+        else if (c >= m_ranges[mid].m_hi)
+            lo = mid + 1;
+        else
+            return; // already contained
+    }
+    // lo is the insertion point
+    unsigned idx = static_cast<unsigned>(lo);
+    bool merge_left  = idx > 0 && m_ranges[idx - 1].m_hi == c;
+    bool merge_right = idx < m_ranges.size() && m_ranges[idx].m_lo == c + 1;
+    if (merge_left && merge_right) {
+        m_ranges[idx - 1].m_hi = m_ranges[idx].m_hi;
+        m_ranges.erase(m_ranges.begin() + idx);
+    } else if (merge_left) {
+        m_ranges[idx - 1].m_hi = c + 1;
+    } else if (merge_right) {
+        m_ranges[idx].m_lo = c;
+    } else {
+        // positional insert: shift elements right and place new element
+        m_ranges.push_back(char_range());
+        for (unsigned k = m_ranges.size() - 1; k > idx; --k)
+            m_ranges[k] = m_ranges[k - 1];
+        m_ranges[idx] = char_range(c);
+    }
+}
+
+void char_set::add(char_set const& other) {
+    for (auto const& r : other.m_ranges) {
+        for (unsigned c = r.m_lo; c < r.m_hi; ++c)
+            add(c);
+    }
+}
+
+char_set char_set::intersect_with(char_set const& other) const {
+    char_set result;
+    unsigned i = 0, j = 0;
+    while (i < m_ranges.size() && j < other.m_ranges.size()) {
+        unsigned lo = std::max(m_ranges[i].m_lo, other.m_ranges[j].m_lo);
+        unsigned hi = std::min(m_ranges[i].m_hi, other.m_ranges[j].m_hi);
+        if (lo < hi)
+            result.m_ranges.push_back(char_range(lo, hi));
+        if (m_ranges[i].m_hi < other.m_ranges[j].m_hi)
+            ++i;
+        else
+            ++j;
+    }
+    return result;
+}
+
+char_set char_set::complement(unsigned max_char) const {
+    char_set result;
+    if (m_ranges.empty()) {
+        result.m_ranges.push_back(char_range(0, max_char + 1));
+        return result;
+    }
+    unsigned from = 0;
+    for (auto const& r : m_ranges) {
+        if (from < r.m_lo)
+            result.m_ranges.push_back(char_range(from, r.m_lo));
+        from = r.m_hi;
+    }
+    if (from <= max_char)
+        result.m_ranges.push_back(char_range(from, max_char + 1));
+    return result;
+}
+
+bool char_set::is_disjoint(char_set const& other) const {
+    unsigned i = 0, j = 0;
+    while (i < m_ranges.size() && j < other.m_ranges.size()) {
+        if (m_ranges[i].m_hi <= other.m_ranges[j].m_lo)
+            ++i;
+        else if (other.m_ranges[j].m_hi <= m_ranges[i].m_lo)
+            ++j;
+        else
+            return false;
+    }
+    return true;
+}
+
+std::ostream& char_set::display(std::ostream& out) const {
+    if (m_ranges.empty()) {
+        out << "{}";
+        return out;
+    }
+    out << "{ ";
+    bool first = true;
+    for (auto const& r : m_ranges) {
+        if (!first) out << ", ";
+        first = false;
+        if (r.is_unit()) {
+            unsigned c = r.m_lo;
+            if (c >= 'a' && c <= 'z')
+                out << (char)c;
+            else if (c >= 'A' && c <= 'Z')
+                out << (char)c;
+            else if (c >= '0' && c <= '9')
+                out << (char)c;
+            else
+                out << "#[" << c << "]";
+        } else {
+            out << "[" << r.m_lo << "-" << (r.m_hi - 1) << "]";
+        }
+    }
+    out << " }";
+    return out;
+}