#ifndef STL_QUEUE
#define STL_QUEUE

#include <vector>
#include "deque"
#include "list"
#include "functional"

namespace std
{
#define QUEUE_CAPACITY 1000

template <
  class T,
  class Container = vector<T>,
  class Compare = less<typename Container::value_type>>
class priority_queue
{
  T buf[QUEUE_CAPACITY];
  size_t _size;
  T head;
  T tail;
  Compare comp; // Store the comparator

public:
  priority_queue() : _size(0), head(0), tail(0), comp(Compare())
  {
  }

  ~priority_queue()
  {
    _size = 0;
  }

  // Constructor that takes const reference (handles temporaries)
  priority_queue(const Compare &x) : _size(0), head(0), tail(0), comp(x)
  {
  }

  // Constructor that takes reference (for existing code)
  priority_queue(Compare &x) : _size(0), head(0), tail(0), comp(x)
  {
  }

  template <typename Iterator>
  priority_queue(
    Iterator begin,
    Iterator end,
    const Compare &compare = Compare())
    : _size(0), head(0), tail(0), comp(compare)
  {
    for (auto it = begin; it != end; ++it)
      this->push(*it);
  }

  void push(const T &x)
  {
    size_t i = 0;
    T tmp = x, y;
    // Use the comparator instead of hardcoded comparison
    while ((comp(x, this->buf[i])) && (i != this->_size))
    {
      i++;
    }
    if (i == 0)
      this->head = x;
    if (i == this->_size)
      this->tail = x;
    for (; i < this->_size; i++)
    {
      y = tmp;
      tmp = this->buf[i];
      this->buf[i] = y;
    }
    this->buf[i] = tmp;
    this->_size++;
  }
  bool empty() const
  {
    if (this->_size == 0)
      return true;
    return false;
  }
  size_t size() const
  {
    return this->_size;
  }
  T top() const
  {
    __ESBMC_assert(!(this->empty()), "the queue is empty");
    return this->head;
  }
  void pop()
  {
    __ESBMC_assert(!(this->empty()), "the queue is empty");
    int i;
    if (this->_size == 1)
    {
      this->head = this->tail = this->buf[0] = NULL;
      this->_size--;
      return;
    }
    for (i = 0; i < this->_size; i++)
    {
      this->buf[i] = this->buf[i + 1];
    }
    this->head = this->buf[0];
    this->_size--;
    this->tail = this->buf[this->_size - 1];
  }
};

template <class T, class Container = deque<T>>
class queue
{
  T buf[QUEUE_CAPACITY];
  size_t _size;
  size_t head;
  size_t tail;

public:
  queue() : _size(0), head(0), tail(0)
  {
  }

  ~queue()
  {
    _size = 0;
  }
  queue(std::deque<int> &x) : _size(x.size()), head(0), tail(0)
  {
  }
  queue(std::list<int> &x) : _size(x.size()), head(0), tail(0)
  {
  }

  void push(const T &t)
  {
    assert(0 <= _size);
    __ESBMC_assert(_size < QUEUE_CAPACITY, "queue overflow");
    buf[tail] = t;
    _size++;
    if (tail == QUEUE_CAPACITY)
      tail = 1;
    else
      tail++;
  }

  bool empty() const
  {
    if (head == tail)
      return true;
    else
      return false;
  }

  T &front()
  {
    assert(!empty());
    return buf[head];
  }

  int size() const
  {
    assert(0 <= _size && _size <= QUEUE_CAPACITY);
    return _size;
  }

  void pop()
  {
    __ESBMC_assert(size() > 0, "queue underflow");
    _size--;
    if (head == QUEUE_CAPACITY)
      head = 1;
    else
      head++;
  }

  T &back()
  {
    assert(!empty());
    return buf[tail - 1];
  }
};

} // namespace std

#endif