#ifndef ESBMC_UNORDERED_SET_H
#define ESBMC_UNORDERED_SET_H

#include <utility>

namespace std {

#ifndef SIZE_MAX
#define SIZE_MAX ((size_t)-1)
#endif

// Simple hash function
template<typename T>
struct esbmc_hash {
    size_t operator()(const T& key) const {
        return static_cast<size_t>(key);
    }
};

// Simple equality comparison
template<typename T>
struct esbmc_equal_to {
    bool operator()(const T& lhs, const T& rhs) const {
        return lhs == rhs;
    }
};

// Forward declaration
template<typename Key, typename Hash = esbmc_hash<Key>, 
         typename KeyEqual = esbmc_equal_to<Key>>
class unordered_set;

// Simple array-based implementation - much simpler than hash table
template<typename Key, typename Hash, typename KeyEqual>
class esbmc_unordered_set_iterator {
public:
    typedef Key value_type;
    typedef const Key& reference;
    typedef const Key* pointer;
    typedef ptrdiff_t difference_type;

    // Grant friend access to unordered_set
    friend class unordered_set<Key, Hash, KeyEqual>;

private:
    const Key* data_;
    size_t pos_;
    size_t size_;

public:
    // Constructors
    esbmc_unordered_set_iterator() : data_(nullptr), pos_(0), size_(0) {}
    
    esbmc_unordered_set_iterator(const Key* data, size_t position, size_t size)
        : data_(data), pos_(position), size_(size) {}

    // Dereference operators
    reference operator*() const {
        return data_[pos_];
    }
    
    pointer operator->() const {
        return &data_[pos_];
    }

    // Increment operators
    esbmc_unordered_set_iterator& operator++() {
        if (pos_ < size_) {
            ++pos_;
        }
        return *this;
    }
    
    esbmc_unordered_set_iterator operator++(int) {
        esbmc_unordered_set_iterator temp = *this;
        ++(*this);
        return temp;
    }

    // Comparison operators
    bool operator==(const esbmc_unordered_set_iterator& other) const {
        return data_ == other.data_ && pos_ == other.pos_;
    }
    
    bool operator!=(const esbmc_unordered_set_iterator& other) const {
        return !(*this == other);
    }
};

// Simple unordered_set implementation using fixed-size array
template<typename Key, typename Hash, typename KeyEqual>
class unordered_set {
public:
    // Type definitions
    typedef Key key_type;
    typedef Key value_type;
    typedef Hash hasher;
    typedef KeyEqual key_equal;
    typedef value_type& reference;
    typedef const value_type& const_reference;
    typedef value_type* pointer;
    typedef const value_type* const_pointer;
    typedef size_t size_type;
    typedef ptrdiff_t difference_type;
    
    typedef esbmc_unordered_set_iterator<Key, Hash, KeyEqual> iterator;
    typedef esbmc_unordered_set_iterator<Key, Hash, KeyEqual> const_iterator;

private:
    // TODO: Implement a hash table if needed.
    // Simple fixed-size array storage
    static const size_t MAX_SIZE = 1024; // Small size for verification
    Key data_[MAX_SIZE];
    size_type size_;
    hasher hash_function_;
    key_equal equal_function_;

    // Find index of key, or MAX_SIZE if not found
    size_type find_index(const Key& key) const {
        for (size_type i = 0; i < size_; ++i) {
            if (equal_function_(data_[i], key)) {
                return i;
            }
        }
        return MAX_SIZE;
    }

public:
    // Constructors
    unordered_set() : size_(0) {}

    ~unordered_set() { size_ = 0; }

    explicit unordered_set(size_type /*bucket_count*/) : size_(0) {}
    
    // Iterator range constructor
    template<typename InputIterator>
    unordered_set(InputIterator first, InputIterator last) : size_(0) {
        insert(first, last);
    }
    
    // Copy constructor
    unordered_set(const unordered_set& other) 
        : size_(other.size_), hash_function_(other.hash_function_), 
          equal_function_(other.equal_function_) {
        for (size_type i = 0; i < size_; ++i) {
            data_[i] = other.data_[i];
        }
    }
    
    // Move constructor
    unordered_set(unordered_set&& other) noexcept
        : size_(other.size_), hash_function_(other.hash_function_), 
          equal_function_(other.equal_function_) {
        for (size_type i = 0; i < size_; ++i) {
            data_[i] = other.data_[i];
        }
        other.size_ = 0;
    }

    // Assignment operators
    unordered_set& operator=(const unordered_set& other) {
        if (this != &other) {
            size_ = other.size_;
            hash_function_ = other.hash_function_;
            equal_function_ = other.equal_function_;
            for (size_type i = 0; i < size_; ++i) {
                data_[i] = other.data_[i];
            }
        }
        return *this;
    }
    
    unordered_set& operator=(unordered_set&& other) noexcept {
        if (this != &other) {
            size_ = other.size_;
            hash_function_ = other.hash_function_;
            equal_function_ = other.equal_function_;
            for (size_type i = 0; i < size_; ++i) {
                data_[i] = other.data_[i];
            }
            other.size_ = 0;
        }
        return *this;
    }

    // Iterators
    iterator begin() {
        return iterator(data_, 0, size_);
    }
    
    const_iterator begin() const {
        return const_iterator(data_, 0, size_);
    }
    
    iterator end() {
        return iterator(data_, size_, size_);
    }
    
    const_iterator end() const {
        return const_iterator(data_, size_, size_);
    }
    
    const_iterator cbegin() const {
        return begin();
    }
    
    const_iterator cend() const {
        return end();
    }

    // Capacity
    bool empty() const noexcept {
        return size_ == 0;
    }
    
    size_type size() const noexcept {
        return size_;
    }
    
    size_type max_size() const noexcept {
        return MAX_SIZE;
    }

    // Modifiers
    
    // Insert single element
    std::pair<iterator, bool> insert(const Key& key) {
        size_type idx = find_index(key);
        if (idx != MAX_SIZE) {
            // Already exists
            return std::make_pair(iterator(data_, idx, size_), false);
        }
        
        if (size_ >= MAX_SIZE) {
            // Array full
            return std::make_pair(end(), false);
        }
        
        // Insert new element
        data_[size_] = key;
        iterator result(data_, size_, size_ + 1);
        ++size_;
        return std::make_pair(result, true);
    }
    
    // Insert with move semantics
    std::pair<iterator, bool> insert(Key&& key) {
        return insert(key);
    }
    
    // Insert range
    template<typename InputIterator>
    void insert(InputIterator first, InputIterator last) {
        for (InputIterator it = first; it != last; ++it) {
            insert(*it);
        }
    }
    
    // Emplace
    template<typename... Args>
    std::pair<iterator, bool> emplace(Args&&... args) {
        Key key(args...);
        return insert(key);
    }
    
    // Erase by key
    size_type erase(const Key& key) {
        size_type idx = find_index(key);
        if (idx == MAX_SIZE) {
            return 0; // Not found
        }
        
        // Shift elements down
        for (size_type i = idx; i < size_ - 1; ++i) {
            data_[i] = data_[i + 1];
        }
        --size_;
        return 1;
    }
    
    // Erase by iterator
    iterator erase(const_iterator position) {
        if (position == end()) {
            return end();
        }
        
        // Calculate index from iterator position
        size_type idx = position.pos_;
        if (idx >= size_) {
            return end();
        }
        
        // Shift elements down
        for (size_type i = idx; i < size_ - 1; ++i) {
            data_[i] = data_[i + 1];
        }
        --size_;
        
        // Return iterator to next element (or end if we removed the last)
        return iterator(data_, idx, size_);
    }
    
    // Erase range
    iterator erase(const_iterator first, const_iterator last) {
        if (first == last) {
            return iterator(data_, first.pos_, size_);
        }
        
        // Simple implementation: erase elements one by one
        iterator current(data_, first.pos_, size_);
        while (current != end() && current.pos_ < last.pos_) {
            current = erase(current);
        }
        return current;
    }
    
    // Clear all elements
    void clear() noexcept {
        size_ = 0;
    }

    // Lookup operations
    
    // Find element
    iterator find(const Key& key) {
        size_type idx = find_index(key);
        if (idx != MAX_SIZE) {
            return iterator(data_, idx, size_);
        }
        return end();
    }
    
    const_iterator find(const Key& key) const {
        size_type idx = find_index(key);
        if (idx != MAX_SIZE) {
            return const_iterator(data_, idx, size_);
        }
        return end();
    }
    
    // Count occurrences (0 or 1 for set)
    size_type count(const Key& key) const {
        return find_index(key) != MAX_SIZE ? 1 : 0;
    }
    
    // Check if key exists (C++20)
    bool contains(const Key& key) const {
        return find_index(key) != MAX_SIZE;
    }

    // Bucket interface
    size_type bucket_count() const noexcept {
        return 1;
    }
    
    size_type bucket_size(size_type /*bucket_index*/) const {
        return size_;
    }
    
    size_type bucket(const Key& /*key*/) const {
        return 0;
    }

    // Hash policy
    double load_factor() const noexcept {
        return static_cast<double>(size_) / MAX_SIZE;
    }
    
    double max_load_factor() const noexcept {
        return 1.0;
    }
    
    void reserve(size_type /*count*/) {
        // No-op for fixed-size array
    }

    // Observers
    hasher hash_function() const {
        return hash_function_;
    }
    
    key_equal key_eq() const {
        return equal_function_;
    }

    // Comparison operators
    bool operator==(const unordered_set& other) const {
        if (size_ != other.size_) {
            return false;
        }
        
        // Check that all elements in this set exist in other
        for (size_type i = 0; i < size_; ++i) {
            if (!other.contains(data_[i])) {
                return false;
            }
        }
        return true;
    }
    
    bool operator!=(const unordered_set& other) const {
        return !(*this == other);
    }
};

} // namespace std

#endif // ESBMC_UNORDERED_SET_H