#ifndef __STL_LIST
#define __STL_LIST

#include "definitions.h"
#include "type_traits"
#include "vector"

#define LIST_MAX_SIZE 20

namespace std
{
template <class T>
class list
{
public:
  typedef T &reference;
  typedef const T &const_reference;
  typedef unsigned int size_type;
  typedef int difference_type;
  typedef T value_type;
  typedef T *pointer;
  typedef const T *const_pointer;

  typedef bool(pred_double)(T, T);
  typedef bool(pred)(T &);

  // Doubly-linked list with index-based links so the structure survives
  // struct-by-value copies (a self-referential pointer would dangle into
  // the source object after a copy). _sentinel_prev/_sentinel_next play
  // the role of the sentinel node's prev/next fields. SENTINEL marks
  // "off the end" — equivalent to a null next/prev or to end().
  static const size_type SENTINEL = LIST_MAX_SIZE;

  struct node
  {
    T data;
    size_type prev_idx;
    size_type next_idx;
  };

  node _pool[LIST_MAX_SIZE];
  size_type _sentinel_prev;
  size_type _sentinel_next;
  // Monotonic high-water mark for the pool. erase does not reclaim
  // slots; total alloc per list instance is bounded by LIST_MAX_SIZE.
  size_type _next_free;
  size_type _size;

  void _init()
  {
    _sentinel_prev = SENTINEL;
    _sentinel_next = SENTINEL;
    _next_free = 0;
    _size = 0;
  }

  size_type _alloc_idx(const value_type &x)
  {
    __ESBMC_assert(_next_free < LIST_MAX_SIZE, "list capacity exceeded");
    size_type idx = _next_free;
    ++_next_free;
    _pool[idx].data = x;
    return idx;
  }

  // Splice node 'n_idx' before 'pos_idx'. pos_idx == SENTINEL means
  // append at the tail.
  void _link_before(size_type n_idx, size_type pos_idx)
  {
    if (pos_idx == SENTINEL)
    {
      _pool[n_idx].prev_idx = _sentinel_prev;
      _pool[n_idx].next_idx = SENTINEL;
      if (_sentinel_prev != SENTINEL)
        _pool[_sentinel_prev].next_idx = n_idx;
      else
        _sentinel_next = n_idx;
      _sentinel_prev = n_idx;
    }
    else
    {
      size_type prev = _pool[pos_idx].prev_idx;
      _pool[n_idx].prev_idx = prev;
      _pool[n_idx].next_idx = pos_idx;
      if (prev != SENTINEL)
        _pool[prev].next_idx = n_idx;
      else
        _sentinel_next = n_idx;
      _pool[pos_idx].prev_idx = n_idx;
    }
  }

  void _unlink(size_type n_idx)
  {
    size_type p = _pool[n_idx].prev_idx;
    size_type nx = _pool[n_idx].next_idx;
    if (p != SENTINEL)
      _pool[p].next_idx = nx;
    else
      _sentinel_next = nx;
    if (nx != SENTINEL)
      _pool[nx].prev_idx = p;
    else
      _sentinel_prev = p;
  }

  size_type _next_idx(size_type idx) const
  {
    if (idx == SENTINEL)
      return SENTINEL;
    return _pool[idx].next_idx;
  }

  size_type _prev_idx(size_type idx) const
  {
    if (idx == SENTINEL)
      return _sentinel_prev;
    return _pool[idx].prev_idx;
  }

  class iterator
  {
  public:
    list<T> *owner;
    size_type idx;

    iterator() : owner(NULL), idx(SENTINEL)
    {
    }
    iterator(list<T> *o, size_type i) : owner(o), idx(i)
    {
    }
    iterator(const iterator &x) : owner(x.owner), idx(x.idx)
    {
    }
    iterator &operator=(const iterator &x)
    {
      owner = x.owner;
      idx = x.idx;
      return *this;
    }

    reference operator*()
    {
      return owner->_pool[idx].data;
    }
    pointer operator->()
    {
      return &owner->_pool[idx].data;
    }

    iterator &operator++()
    {
      idx = owner->_next_idx(idx);
      return *this;
    }
    iterator operator++(int)
    {
      iterator tmp(*this);
      idx = owner->_next_idx(idx);
      return tmp;
    }
    iterator &operator--()
    {
      idx = owner->_prev_idx(idx);
      return *this;
    }
    iterator operator--(int)
    {
      iterator tmp(*this);
      idx = owner->_prev_idx(idx);
      return tmp;
    }

    bool operator==(const iterator &x) const
    {
      return idx == x.idx && owner == x.owner;
    }
    bool operator!=(const iterator &x) const
    {
      return !(*this == x);
    }
  };

  class reverse_iterator
  {
  public:
    list<T> *owner;
    size_type idx;

    reverse_iterator() : owner(NULL), idx(SENTINEL)
    {
    }
    reverse_iterator(list<T> *o, size_type i) : owner(o), idx(i)
    {
    }
    reverse_iterator(const reverse_iterator &x) : owner(x.owner), idx(x.idx)
    {
    }
    reverse_iterator &operator=(const reverse_iterator &x)
    {
      owner = x.owner;
      idx = x.idx;
      return *this;
    }

    reference operator*()
    {
      return owner->_pool[idx].data;
    }
    pointer operator->()
    {
      return &owner->_pool[idx].data;
    }

    reverse_iterator &operator++()
    {
      idx = owner->_prev_idx(idx);
      return *this;
    }
    reverse_iterator operator++(int)
    {
      reverse_iterator tmp(*this);
      idx = owner->_prev_idx(idx);
      return tmp;
    }
    reverse_iterator &operator--()
    {
      // Reverse iteration: --rit moves forward in the underlying list.
      // From rend (idx == SENTINEL), --rit must land on the first forward
      // element so that *(--rend()) reads the front of the list per std::
      // reverse_iterator semantics. _next_idx(SENTINEL) returns SENTINEL
      // (the correct behaviour for forward ++end()), so handle the
      // boundary explicitly here.
      if (idx == SENTINEL)
        idx = owner->_sentinel_next;
      else
        idx = owner->_next_idx(idx);
      return *this;
    }
    reverse_iterator operator--(int)
    {
      reverse_iterator tmp(*this);
      if (idx == SENTINEL)
        idx = owner->_sentinel_next;
      else
        idx = owner->_next_idx(idx);
      return tmp;
    }

    bool operator==(const reverse_iterator &x) const
    {
      return idx == x.idx && owner == x.owner;
    }
    bool operator!=(const reverse_iterator &x) const
    {
      return !(*this == x);
    }
  };

  list()
  {
    _init();
  }

  list(size_type n, const value_type &value = value_type())
  {
    _init();
    for (size_type i = 0; i < n; i++)
      push_back(value);
  }

  list(value_type *t1, value_type *t2)
  {
    _init();
    for (value_type *p = t1; p != t2; ++p)
      push_back(*p);
  }

  list(iterator first, iterator last)
  {
    _init();
    for (iterator it = first; it != last; ++it)
      push_back(*it);
  }

  // Bulk pool copy bounded by x._next_free (the high-water mark — slots
  // at indices >= _next_free have never been allocated and are
  // unreachable through prev/next links). Copying by index instead of
  // walking the linked list via x._pool[i].next_idx lets ESBMC unroll
  // with a concrete index bound: under a low --unwind the loop
  // terminates naturally at x._next_free, instead of speculatively
  // unrolling to --unwind with a fresh LIST_MAX_SIZE-way case split per
  // step on the symbolic next_idx.
  list(const list<T> &x)
  {
    _sentinel_prev = x._sentinel_prev;
    _sentinel_next = x._sentinel_next;
    _next_free = x._next_free;
    _size = x._size;
    for (size_type i = 0; i < x._next_free; i++)
      _pool[i] = x._pool[i];
  }

  list<T> &operator=(const list<T> &x)
  {
    if (this != &x)
    {
      _sentinel_prev = x._sentinel_prev;
      _sentinel_next = x._sentinel_next;
      _next_free = x._next_free;
      _size = x._size;
      for (size_type i = 0; i < x._next_free; i++)
        _pool[i] = x._pool[i];
    }
    return *this;
  }

  ~list()
  {
  }

  typedef iterator const_iterator;
  typedef reverse_iterator const_reverse_iterator;

  iterator begin()
  {
    return iterator(this, _sentinel_next);
  }

  iterator end()
  {
    return iterator(this, SENTINEL);
  }

  // Const overloads. The node-based iterator stores a non-const owner
  // pointer so reading via _next_idx / _prev_idx can resolve the
  // sentinel boundary; cast away const on the receiver, the iterator
  // itself does not mutate the list.
  const_iterator begin() const
  {
    const_iterator it;
    it.owner = const_cast<list<T> *>(this);
    it.idx = _sentinel_next;
    return it;
  }
  const_iterator end() const
  {
    const_iterator it;
    it.owner = const_cast<list<T> *>(this);
    it.idx = SENTINEL;
    return it;
  }

  reverse_iterator rbegin()
  {
    return reverse_iterator(this, _sentinel_prev);
  }

  reverse_iterator rend()
  {
    return reverse_iterator(this, SENTINEL);
  }

  size_type size() const
  {
    return _size;
  }

  bool empty() const
  {
    return _size == 0;
  }

  size_type max_size() const
  {
    return LIST_MAX_SIZE;
  }

  reference front()
  {
    return _pool[_sentinel_next].data;
  }

  reference back()
  {
    return _pool[_sentinel_prev].data;
  }

  void resize(size_type sz, value_type c = value_type())
  {
    while (_size > sz)
      pop_back();
    while (_size < sz)
      push_back(c);
  }

  void push_back(const value_type &x)
  {
    size_type i = _alloc_idx(x);
    _link_before(i, SENTINEL);
    ++_size;
  }

  void push_front(const value_type &x)
  {
    size_type i = _alloc_idx(x);
    _link_before(i, _sentinel_next);
    ++_size;
  }

  void pop_back()
  {
    __ESBMC_assert(_size > 0, "pop_back on empty list");
    _unlink(_sentinel_prev);
    --_size;
  }

  void pop_front()
  {
    __ESBMC_assert(_size > 0, "pop_front on empty list");
    _unlink(_sentinel_next);
    --_size;
  }

  iterator insert(iterator position, const value_type &x)
  {
    size_type i = _alloc_idx(x);
    _link_before(i, position.idx);
    ++_size;
    return iterator(this, i);
  }

  void insert(iterator position, size_type n, const value_type &x)
  {
    for (size_type i = 0; i < n; i++)
      insert(position, x);
  }

  template <
    class InputIterator,
    typename =
      typename std::enable_if<!std::is_integral<InputIterator>::value>::type>
  void insert(iterator position, InputIterator first, InputIterator last)
  {
    for (InputIterator p = first; p != last; ++p)
      insert(position, *p);
  }

  void assign(iterator first, iterator last)
  {
    *this = list(first, last);
  }

  void assign(value_type *first, value_type *last)
  {
    *this = list(first, last);
  }

  void assign(size_type n, const value_type &u)
  {
    *this = list(n, u);
  }

  iterator erase(iterator position)
  {
    size_type nx = _pool[position.idx].next_idx;
    _unlink(position.idx);
    --_size;
    return iterator(this, nx);
  }

  iterator erase(iterator first, iterator &last)
  {
    while (first != last)
      first = erase(first);
    return last;
  }

  void swap(list<value_type> &x)
  {
    list<value_type> tmp(*this);
    *this = x;
    x = tmp;
  }

  void clear()
  {
    _init();
  }

  // Splice all of x's elements before position. After the call, x is
  // empty. Implemented as copy-and-erase rather than node transfer
  // because pool slots are owned per-instance.
  void splice(iterator position, list<value_type> &x)
  {
    iterator it = x.begin();
    while (it != x.end())
    {
      iterator next = it;
      ++next;
      insert(position, *it);
      x.erase(it);
      it = next;
    }
  }

  void splice(iterator position, list<value_type> &x, iterator i)
  {
    insert(position, *i);
    x.erase(i);
  }

  // Range splice. Moves [first, last) out of x and re-inserts it before
  // position. Self-splice-safe (x may alias *this): 'next' is captured
  // before insert/erase so the loop never reads through an erased node.
  // 'last' is taken by value, so even when x and *this overlap, its idx
  // is stable across the erases (we never erase the node at last).
  void splice(
    iterator position,
    list<value_type> &x,
    iterator first,
    iterator last)
  {
    iterator it = first;
    while (it != last)
    {
      iterator next = it;
      ++next;
      insert(position, *it);
      x.erase(it);
      it = next;
    }
  }

  void remove(const value_type &value)
  {
    iterator it = begin();
    while (it != end())
    {
      iterator next = it;
      ++next;
      if (*it == value)
        erase(it);
      it = next;
    }
  }

  template <class Predicate>
  void remove_if(Predicate pred)
  {
    iterator it = begin();
    while (it != end())
    {
      iterator next = it;
      ++next;
      if (pred(*it))
        erase(it);
      it = next;
    }
  }

  void unique()
  {
    if (_size < 2)
      return;
    iterator it = begin();
    ++it;
    while (it != end())
    {
      iterator next = it;
      ++next;
      iterator prev = it;
      --prev;
      if (*it == *prev)
        erase(it);
      it = next;
    }
  }

  void unique(pred_double *x)
  {
    if (_size < 2)
      return;
    iterator it = begin();
    ++it;
    while (it != end())
    {
      iterator next = it;
      ++next;
      iterator prev = it;
      --prev;
      if (x(*prev, *it))
        erase(it);
      it = next;
    }
  }

  template <class Predicate>
  void unique(Predicate pred)
  {
    if (_size < 2)
      return;
    iterator it = begin();
    ++it;
    while (it != end())
    {
      iterator next = it;
      ++next;
      iterator prev = it;
      --prev;
      if (pred(*prev, *it))
        erase(it);
      it = next;
    }
  }

  void merge(list<value_type> &x)
  {
    iterator i = begin();
    iterator j = x.begin();
    while (j != x.end())
    {
      if (i == end() || *j < *i)
      {
        iterator next = j;
        ++next;
        insert(i, *j);
        x.erase(j);
        j = next;
      }
      else
      {
        ++i;
      }
    }
  }

  void merge(list<value_type> &x, pred_double *pred)
  {
    iterator i = begin();
    iterator j = x.begin();
    while (j != x.end())
    {
      if (i == end() || pred(*j, *i))
      {
        iterator next = j;
        ++next;
        insert(i, *j);
        x.erase(j);
        j = next;
      }
      else
      {
        ++i;
      }
    }
  }

  // Insertion sort. Walks rightward from the second element; for each
  // element, scans the prefix [begin, it) for the first node whose
  // value is not less than *it, then unlinks *it and re-links it before
  // that scan position. Stable for equal keys.
  //
  // Both loops are bounded by SENTINEL (== LIST_MAX_SIZE) step counters
  // so ESBMC's symbolic unrolling stays inside the pool size, instead of
  // speculatively unrolling to --unwind through pool[i].next_idx chains.
  void sort()
  {
    if (_size < 2)
      return;
    iterator it = begin();
    ++it;
    size_type outer = 0;
    while (outer < SENTINEL && it != end())
    {
      iterator next_it = it;
      ++next_it;
      iterator scan = begin();
      size_type inner = 0;
      while (inner < SENTINEL && scan != it && !(*it < *scan))
      {
        ++scan;
        ++inner;
      }
      if (scan != it)
      {
        size_type n = it.idx;
        _unlink(n);
        _link_before(n, scan.idx);
      }
      it = next_it;
      ++outer;
    }
  }

  template <class Compare>
  void sort(Compare comp)
  {
    if (_size < 2)
      return;
    iterator it = begin();
    ++it;
    size_type outer = 0;
    while (outer < SENTINEL && it != end())
    {
      iterator next_it = it;
      ++next_it;
      iterator scan = begin();
      size_type inner = 0;
      while (inner < SENTINEL && scan != it && !comp(*it, *scan))
      {
        ++scan;
        ++inner;
      }
      if (scan != it)
      {
        size_type n = it.idx;
        _unlink(n);
        _link_before(n, scan.idx);
      }
      it = next_it;
      ++outer;
    }
  }

  void reverse()
  {
    // Swap prev/next of every node, then swap sentinel ends.
    for (size_type i = _sentinel_next; i != SENTINEL;)
    {
      size_type nx = _pool[i].next_idx;
      size_type p = _pool[i].prev_idx;
      _pool[i].prev_idx = nx;
      _pool[i].next_idx = p;
      i = nx;
    }
    size_type tmp = _sentinel_prev;
    _sentinel_prev = _sentinel_next;
    _sentinel_next = tmp;
  }
};

void advance(list<unsigned int>::iterator &it, int n)
{
  if (n > 0)
    for (int i = 0; i < n; i++)
      ++it;
  else
    for (int i = 0; i < -n; i++)
      --it;
}

void advance(list<int>::iterator &it, int n)
{
  if (n > 0)
    for (int i = 0; i < n; i++)
      ++it;
  else
    for (int i = 0; i < -n; i++)
      --it;
}

bool operator==(const list<int> &x, const list<int> &y)
{
  if (x._size != y._size)
    return false;
  list<int>::size_type ix = x._sentinel_next;
  list<int>::size_type iy = y._sentinel_next;
  // Static step bound so ESBMC stops unrolling at LIST_MAX_SIZE
  // (== SENTINEL) instead of speculatively unrolling to --unwind.
  for (list<int>::size_type step = 0; step < list<int>::SENTINEL; step++)
  {
    if (ix == list<int>::SENTINEL)
      return iy == list<int>::SENTINEL;
    if (x._pool[ix].data != y._pool[iy].data)
      return false;
    ix = x._pool[ix].next_idx;
    iy = y._pool[iy].next_idx;
  }
  return true;
}

bool operator!=(const list<int> &x, const list<int> &y)
{
  return !(x == y);
}

bool operator==(const list<double> &x, const list<double> &y)
{
  if (x._size != y._size)
    return false;
  list<double>::size_type ix = x._sentinel_next;
  list<double>::size_type iy = y._sentinel_next;
  for (list<double>::size_type step = 0; step < list<double>::SENTINEL; step++)
  {
    if (ix == list<double>::SENTINEL)
      return iy == list<double>::SENTINEL;
    if (x._pool[ix].data != y._pool[iy].data)
      return false;
    ix = x._pool[ix].next_idx;
    iy = y._pool[iy].next_idx;
  }
  return true;
}

bool operator!=(const list<double> &x, const list<double> &y)
{
  return !(x == y);
}

} // namespace std

#endif
