12 #ifndef CPROVER_UTIL_DENSE_INTEGER_MAP_H 
   13 #define CPROVER_UTIL_DENSE_INTEGER_MAP_H 
   16 #include <unordered_set> 
   29     return std::forward<T>(t);
 
   52 template <
class K, 
class V, 
class KeyToDenseInteger = 
identity_functort>
 
   91     auto key_integer = KeyToDenseInteger{}(key);
 
   92     INVARIANT(((int64_t)key_integer) >= 
offset, 
"index should be in range");
 
   93     auto ret = (std::size_t)key_integer - (std::size_t)
offset;
 
  117   template <
class UnderlyingIterator, 
class UnderlyingValue>
 
  119     : 
public std::iterator<std::forward_iterator_tag, UnderlyingValue>
 
  122     typedef std::iterator<std::forward_iterator_tag, UnderlyingValue>
 
  139       typename backing_storet::const_iterator,
 
  140       const typename backing_storet::value_type>() 
const 
  175     UnderlyingIterator 
advance(UnderlyingIterator it)
 
  183       auto iterator_pos = (std::size_t)std::distance(
 
  185         (
typename backing_storet::const_iterator)it);
 
  204     typename backing_storet::iterator,
 
  205     typename backing_storet::value_type>
 
  210   typedef iterator_templatet<
 
  211     typename backing_storet::const_iterator,
 
  212     const typename backing_storet::value_type>
 
  226   template <
typename Iter>
 
  231       "setup_for_keys must only be called on a newly-constructed container");
 
  233     int64_t highest_key = std::numeric_limits<int64_t>::min();
 
  234     int64_t lowest_key = std::numeric_limits<int64_t>::max();
 
  235     std::unordered_set<int64_t> seen_keys;
 
  236     for(Iter it = first; it != last; ++it)
 
  238       int64_t integer_key = (int64_t)KeyToDenseInteger{}(*it);
 
  239       highest_key = std::max(integer_key, highest_key);
 
  240       lowest_key = std::min(integer_key, lowest_key);
 
  242         seen_keys.insert(integer_key).second,
 
  243         "keys for use in dense_integer_mapt must be unique");
 
  246     if(highest_key < lowest_key)
 
  252       std::size_t map_size = (std::size_t)((highest_key - lowest_key) + 1);
 
  255         "dense_integer_mapt size should fit in std::size_t");
 
  257         map_size <= std::numeric_limits<std::size_t>::max(),
 
  258         "dense_integer_mapt size should fit in std::size_t");
 
  260       map.resize(map_size);
 
  261       for(Iter it = first; it != last; ++it)
 
  269   const V &
at(
const K &key)
 const 
  273     return map.at(index).second;
 
  279     return map.at(index).second;
 
  286     return map.at(index).second;
 
  289   std::pair<iterator, bool> 
insert(
const std::pair<const K, V> &pair)
 
  293       static_cast<typename backing_storet::iterator::difference_type
>(index);
 
  294     iterator it{std::next(
map.begin(), signed_index), *
this};
 
  301       map.at(index).second = pair.second;
 
  306   std::size_t 
count(
const K &key)
 const 
  352 #endif // CPROVER_UTIL_DENSE_INTEGER_MAP_H