Branch data     Line data    Source code

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