Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  * Utility functions for dealing with maps and related classes in a mostly
      10                 :            :  * uniform fashion.
      11                 :            :  *
      12                 :            :  * These are stylistically encouraged (but not required) in new code.
      13                 :            :  * Supports:
      14                 :            :  * - std::map
      15                 :            :  * - std::unordered_map
      16                 :            :  * - context::CDHashmap
      17                 :            :  * - context::CDInsertHashmap
      18                 :            :  * The ContainsKey function is also compatible with std::[unordered_]set.
      19                 :            :  *
      20                 :            :  * Currently implemented classes of functions:
      21                 :            :  * - ContainsKey
      22                 :            :  *   Returns true if a map contains a key. (Also Supports std::set and
      23                 :            :  *   std::unordered_set.)
      24                 :            :  * - FindOr*
      25                 :            :  *   Finds an data element mapped to by the map. Variants include FindOrNull
      26                 :            :  *   and FindOrDie.
      27                 :            :  *
      28                 :            :  * Potential future classes of functions:
      29                 :            :  * - InsertOrUpdate
      30                 :            :  * - InsertIfNotPresent
      31                 :            :  */
      32                 :            : 
      33                 :            : #include "cvc5_private.h"
      34                 :            : 
      35                 :            : #ifndef CVC5__BASE__MAP_UTIL_H
      36                 :            : #define CVC5__BASE__MAP_UTIL_H
      37                 :            : 
      38                 :            : #include "base/check.h"
      39                 :            : 
      40                 :            : namespace cvc5::internal {
      41                 :            : 
      42                 :            : // Returns true if the `map` contains the `key`.
      43                 :            : //
      44                 :            : // Supports sets as well.
      45                 :            : template <class M, class Key>
      46                 :     616619 : bool ContainsKey(const M& map, const Key& key)
      47                 :            : {
      48                 :     616619 :   return map.find(key) != map.end();
      49                 :            : }
      50                 :            : 
      51                 :            : template <typename M>
      52                 :            : using MapKeyTypeT = typename M::value_type::first_type;
      53                 :            : template <typename M>
      54                 :            : using MapMappedTypeT = typename M::value_type::second_type;
      55                 :            : 
      56                 :            : // Returns a pointer to the const value mapped by `key` if it exists, or nullptr
      57                 :            : // otherwise.
      58                 :            : template <class M>
      59                 :          8 : const MapMappedTypeT<M>* FindOrNull(const M& map, const MapKeyTypeT<M>& key)
      60                 :            : {
      61                 :          8 :   auto it = map.find(key);
      62         [ +  + ]:          8 :   if (it == map.end())
      63                 :            :   {
      64                 :          4 :     return nullptr;
      65                 :            :   }
      66                 :          4 :   return &((*it).second);
      67                 :            : }
      68                 :            : 
      69                 :            : // Returns a pointer to the non-const value mapped by `key` if it exists, or
      70                 :            : // nullptr otherwise.
      71                 :            : template <class M>
      72                 :       2113 : MapMappedTypeT<M>* FindOrNull(M& map, const MapKeyTypeT<M>& key)
      73                 :            : {
      74                 :       2113 :   auto it = map.find(key);
      75         [ +  + ]:       2113 :   if (it == map.end())
      76                 :            :   {
      77                 :       1883 :     return nullptr;
      78                 :            :   }
      79                 :        230 :   return &((*it).second);
      80                 :            : }
      81                 :            : 
      82                 :            : // Returns a const reference to the value mapped by `key` if it exists. Dies
      83                 :            : // if the element is not there.
      84                 :            : template <class M>
      85                 :          8 : const MapMappedTypeT<M>& FindOrDie(const M& map, const MapKeyTypeT<M>& key)
      86                 :            : {
      87                 :          8 :   auto it = map.find(key);
      88 [ -  + ][ -  + ]:          8 :   AlwaysAssert(it != map.end()) << "The map does not contain the key.";
                 [ -  - ]
      89                 :          8 :   return (*it).second;
      90                 :            : }
      91                 :            : 
      92                 :            : }  // namespace cvc5::internal
      93                 :            : 
      94                 :            : #endif /* CVC5__BASE__MAP_UTIL_H */