Line data    Source code

       1             : // Author(s): David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
       2             : //
       3             : // Copyright: see the accompanying file COPYING or copy at
       4             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       5             : //
       6             : // Distributed under the Boost Software License, Version 1.0.
       7             : // (See accompanying file LICENSE_1_0.txt or copy at
       8             : // http://www.boost.org/LICENSE_1_0.txt)
       9             : 
      10             : /// \file lts/detail/fixed_vector.h
      11             : ///
      12             : /// \brief a vector class that cannot be moved while it is not empty
      13             : ///
      14             : /// \details The stuttering equivalence algorithm by Groote / Jansen / Keiren /
      15             : /// Wijs is implemented using a large number of iterators that should not be
      16             : /// invalidated.  The `fixed_vector` class provides a data structure based on
      17             : /// std::vector that guarantees that its iterators remain valid.  All methods
      18             : /// that could reallocate the storage (and therefore invalidate the iterators)
      19             : /// are disabled, except clear(), which can be called just before destructing
      20             : /// the fixed_vector.
      21             : ///
      22             : /// \author David N. Jansen, Radboud Universiteit, Nijmegen, The Netherlands
      23             : 
      24             : #ifndef FIXED_VECTOR_H
      25             : #define FIXED_VECTOR_H
      26             : 
      27             : #include <vector>
      28             : #include <cassert>
      29             : 
      30             : namespace mcrl2
      31             : {
      32             : namespace lts
      33             : {
      34             : namespace detail
      35             : {
      36             : namespace bisim_gjkw
      37             : {
      38             : 
      39             : template <class T>
      40             : class fixed_vector : private std::vector<T>
      41             : {
      42             : public:
      43             :     // only reveal as much of the interface of std::vector<T> as is needed:
      44             :     using typename std::vector<T>::iterator;
      45             :     using typename std::vector<T>::const_iterator;
      46             :     using typename std::vector<T>::size_type;
      47             :     using std::vector<T>::begin;
      48             :     using std::vector<T>::cbegin;
      49             :     using std::vector<T>::cend;
      50             :     using std::vector<T>::end;
      51             :     using std::vector<T>::front;
      52             :     using std::vector<T>::back;
      53             :     using std::vector<T>::size;
      54             :     using std::vector<T>::clear;
      55             : 
      56        2487 :     explicit fixed_vector(size_type n)  :std::vector<T>(n)  {  }
      57             :     explicit fixed_vector(size_type n, T init)  :std::vector<T>(n, init)  {  }
      58             : 
      59             : #ifdef NDEBUG
      60             :     using std::vector<T>::operator[];
      61             : #else
      62             :     using std::vector<T>::empty;
      63             :     using std::vector<T>::data;
      64             : 
      65             :     // operator[] calls std::vector<T>::at because the latter checks bounds.
      66       46271 :     T& operator[](size_type n)  {  return std::vector<T>::at(n);  }
      67      139309 :     const T& operator[](size_type n) const  {  return std::vector<T>::at(n);  }
      68             : #endif
      69             : };
      70             : 
      71             : } // end namespace bisim_gjkw
      72             : } // end namespace detail
      73             : } // end namespace lts
      74             : } // end namespace mcrl2
      75             : 
      76             : #endif // #ifndef FIXED_VECTOR_H