/* C++ */

/**********************************************************
*
*
*
* Purpose:
*
*            Operational model of STL vector
*
*    A vector is a kind of sequence container that supports
*    random-access iterators. A vector satisfies the
*    the requirements of a container and of a reversible
*    container.
*
* Authors:
*
*      Nicolas Blanc,
*      Alex Groce,
*      Daniel Kroening
*
**********************************************************/

#ifndef __STL_VECTOR
#define __STL_VECTOR

#include <assert.h>
#include <iterator>
#include <container>

namespace std {

  template<typename T>
  class vector: public container<T>
  {
  public:

  /************************************
  *
  *      Container requirements
  *
  ************************************/

  typedef T  value_type;
  typedef T& reference;
  typedef const T& const_reference;

  typedef unsigned size_type;

  typedef _iterator<T> iterator;
  typedef _const_iterator<T> const_iterator;
  typedef _reverse_iterator<T> reverse_iterator;
  typedef _const_reverse_iterator<T> const_reverse_iterator;

  vector():_size(0), _capacity(0)
  #ifdef VERS1
  , _version(0)
  #endif
  {
  }

  vector(unsigned n, const T& t):_size(0), _capacity(0)
  #ifdef VERS1
  , _version(0)
  #endif
  {
    resize(n,t);
  }

  vector(const vector& vec):_size(0),  _capacity(0)
  #ifdef VERS1
  , _version(0)
  #endif
  {
    resize(vec.size());
    for(int i=0;i<size();i++)
      data(i) = vec.data(i);
  }

  vector& operator=(const vector& cp)
  {
    resize(cp.size());
    for(int i=0;i<size();i++)
      data(i) = cp.data(i);
    return *this;
  }

  ~vector()
  {
    clear();
  }

  iterator begin()
  {
    __CPROVER_HIDE:
    return iterator(this,0);
  }

  iterator end()
  {
    __CPROVER_HIDE:
    return iterator(this, size());
  }

  const_iterator const_begin() const
  {
    __CPROVER_HIDE:
    return const_iterator(this, 0);
  }

  const_iterator const_end() const
  {
    __CPROVER_HIDE:
    return const_iterator(this, size());
  }

  reverse_iterator rend()
  {
    __CPROVER_HIDE:
    return reverse_iterator(this,0);
  }

  reverse_iterator rbegin()
  {
    __CPROVER_HIDE:
    return reverse_iterator(this, size());
  }

  const_reverse_iterator const_rend() const
  {
    __CPROVER_HIDE:
    return const_reverse_iterator(this, 0);
  }

  const_reverse_iterator const_rbegin() const
  {
    __CPROVER_HIDE:
    return const_reverse_iterator(this, size());
  }

  unsigned size() const
  {
    __CPROVER_HIDE:
    return _size;
  }

  bool empty() const
  {
    __CPROVER_HIDE:
    return size() == 0;
  }

  friend bool operator==(const vector& v1,
    const vector& v2)
  {
    if(v1.size() != v2.size())
      return false;
    for(int i=0; i < v1.size(); i++)
      if(v1.at(i) != v2.at(i)) return false;
        return true;
  }

  friend bool operator!=(const vector& v1,
    const vector& v2)
  {
    return !(v1 == v2);
  }

  /************************************
  *
  *      Sequence requirements
  *
  ************************************/

  iterator insert(const iterator& it, const reference t)
  {
    __CPROVER_HIDE:
    it.assert_valid();
    __CPROVER_assert(it.c == this, "insert() with iterator not pointing to container");

    resize(size()+1);

    #ifndef NO_DATA
    for(int i = size()-1 ; it.offset < i ; i--)
      data(i) = data(i)-1;
    data(it.offset) = t;
    #endif

    #ifdef VERS1
    _version++;
    #elif defined VERS1
    for(int i = it.offset; i <= size(); i++)
    _version[i]++;
    #else
    __CPROVER_assert(0, "VERS not defined");
    #endif

    return iterator(this, it.offset);
  }

  iterator erase(iterator& it)
  {
    __CPROVER_HIDE:
    it.assert_dereferenceable();
    __CPROVER_assert(it.c == this, "erase() with iterator not pointing to container");
    __CPROVER_assert(it.version == version(it.offset), "erase() with invalidated iterator");

    #ifndef NO_DATA
    for(int i = it.offset; i < size()-1; i++)
      data(i) = data(i+1);
    #endif

    resize(size()-1);

    #ifdef VERS1
    _version++;
    #elif defined VERS1
    for(int i = it.offset; i <= size(); i++)
    _version[i]++;
    #else
    __CPROVER_assert(0, "VERS not defined");
    #endif

    return iterator(this, it.offset);
  }

  void clear()
  {
    __CPROVER_HIDE:
    resize(0);
  }


  /************************************
  *
  *  Optional sequence requirements
  *
  ************************************/

  void push_back(const T &x)
  {
    __CPROVER_HIDE:
    resize(size()+1, x);
  }

  void pop_back()
  {
    __CPROVER_HIDE:
    __CPROVER_assert(size()!=0, "pop_back() on empty vector");
    resize(size()-1);
  }

  T &operator [] (unsigned i)
  {
    __CPROVER_HIDE:
    __CPROVER_assert(i<size(), "vector-index upper bound");
    return _data[i];
  }

  const T &operator [] (unsigned i) const
  {
    __CPROVER_HIDE:
    __CPROVER_assert(i<size(), "vector-index upper bound");
    return _data[i];
  }

  T& at(int i) {
    __CPROVER_HIDE:
    return (*this)[i];
  }

  const T& at(int i) const {
    __CPROVER_HIDE:
    return (*this)[i];
  }

  const T & const_front() const
  {
    __CPROVER_HIDE:
    __CPROVER_assert(size() !=0, "front() on empty vector");
    return data(0);
  }

  const T & const_back() const
  {
    __CPROVER_HIDE:
    __CPROVER_assert(size() !=0, "back() on empty vector");
    return data(size()-1);
  }

  T & front()
  {
    __CPROVER_HIDE:
    __CPROVER_assert(size() !=0, "front() on empty vector");
    return _data[0];
  }

  T & back()
  {
    __CPROVER_HIDE:
    __CPROVER_assert(size() !=0, "back() on empty vector");
    return _data[size() - 1];
  }


  /************************************
  *
  *      Misc of Vector
  *
  ************************************/

  void reserve(unsigned s)
  {
    __CPROVER_HIDE:
    if(s> capacity())
    {
    _capacity=s;
    #ifdef VERS1
    _version++;
    #elif defined VERS2
    for(int i=0; i<=size(); i++) _version[i]++;
    #else
    __CPROVER_assert(0, "VERS not defined");
    #endif
    }
  }

  void resize(unsigned s)
  {
    __CPROVER_HIDE:
    unsigned old_size = size();
    reserve(s);

    _size=s;

    if(old_size < size())
    {
      #ifdef VERS1
      _version++;
      #elif defined VERS2
      for(i=old_size; i<=size(); i++) _version[i]++;
      #else
      __CPROVER_assert(0, "VERS not defined");
      #endif
    }
  }

  void resize(unsigned s, const T &x)
  {
    __CPROVER_HIDE:
    reserve(s);
    unsigned old_size = size();
    _size=s;

    if(old_size < size())
    {
      #ifdef VERS1
      _version++;
      #elif defined VERS2
      for(int i= old_size; i <= size(); i++)
        _version[i]++;
      #else
      __CPROVER_assert(0, "VERS not defined");
      #endif

      #ifndef NO_DATA
      for(unsigned i= old_size; i < size(); i++) data(i) = x;
      #endif
    }
  }

  unsigned capacity() const
  {
    __CPROVER_HIDE:
    return _capacity;
  }

  /************************************
  *
  *  Misc for modelisation only
  *
  ************************************/

  T& data(unsigned i) const
  {
    __CPROVER_HIDE:
    __CPROVER_assert(i< size(), "data(): vector-index upper bound");
    return _data[i];
  }

  const T& const_data(unsigned i) const
  {
    __CPROVER_HIDE:
    __CPROVER_assert(i< size(), "const_data(): vector-index upper bound");
    return _data[i];
  }

  unsigned version(unsigned i) const
  {
    __CPROVER_HIDE:
    __CPROVER_assert(i<= size(), "version(): vector-index upper bound");

    #ifdef VERS1
    return _version;
    #elif defined VERS2
    return _version[i];
    #else
    __CPROVER_assert(0, "VERS not defined");
    #endif
  }

  protected:
  unsigned _capacity;
  unsigned _size;

  #ifdef VERS1
  unsigned _version;
  #elif defined VERS2
  unsigned _version[__CPROVER::constant_infinity_uint];
  #endif

  T _data[__CPROVER::constant_infinity_uint];
  };

}
#endif

