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                 :            :  *
      10                 :            :  * This is an abstraction of a Map from unsigned integers to elements
      11                 :            :  * of type T.
      12                 :            :  *
      13                 :            :  * This is an abstraction of a Map from an unsigned integer to elements of
      14                 :            :  * type T.
      15                 :            :  * This class is designed to provide constant time insertion, deletion,
      16                 :            :  * element_of, and fast iteration. This is done by storing backing vectors of
      17                 :            :  * size greater than the maximum key.
      18                 :            :  * This datastructure is appropriate for heavy use datastructures where the
      19                 :            :  * Keys are a dense set of integers.
      20                 :            :  *
      21                 :            :  * T must support T(), and operator=().
      22                 :            :  *
      23                 :            :  * The derived utility classes DenseSet and DenseMultiset are also defined.
      24                 :            :  */
      25                 :            : 
      26                 :            : #include "cvc5_private.h"
      27                 :            : 
      28                 :            : #pragma once
      29                 :            : 
      30                 :            : #include <limits>
      31                 :            : #include <vector>
      32                 :            : 
      33                 :            : #include "base/check.h"
      34                 :            : #include "util/index.h"
      35                 :            : 
      36                 :            : namespace cvc5::internal {
      37                 :            : 
      38                 :            : template <class T>
      39                 :            : class DenseMap
      40                 :            : {
      41                 :            :  public:
      42                 :            :   typedef Index Key;
      43                 :            :   typedef std::vector<Key> KeyList;
      44                 :            :   typedef KeyList::const_iterator const_iterator;
      45                 :            : 
      46                 :            :  private:
      47                 :            :   // List of the keys in the dense map.
      48                 :            :   KeyList d_list;
      49                 :            : 
      50                 :            :   typedef Index Position;
      51                 :            :   typedef std::vector<Position> PositionMap;
      52                 :            :   static const Position POSITION_SENTINEL =
      53                 :            :       std::numeric_limits<Position>::max();
      54                 :            : 
      55                 :            :   // Each Key in the set is mapped to its position in d_list.
      56                 :            :   // Each Key not in the set is mapped to KEY_SENTINEL
      57                 :            :   PositionMap d_posVector;
      58                 :            : 
      59                 :            :   typedef std::vector<T> ImageMap;
      60                 :            :   // d_image : Key |-> T
      61                 :            :   ImageMap d_image;
      62                 :            : 
      63                 :            :  public:
      64                 :    1477299 :   DenseMap() : d_list(), d_posVector(), d_image() {}
      65                 :            : 
      66                 :            :   /** Returns the number of elements in the set. */
      67                 :   56000137 :   size_t size() const { return d_list.size(); }
      68                 :            : 
      69                 :            :   /** Returns true if the map is empty(). */
      70                 :  175514563 :   bool empty() const { return d_list.empty(); }
      71                 :            : 
      72                 :            :   /**
      73                 :            :    * Similar to a std::vector::clear().
      74                 :            :    *
      75                 :            :    * Invalidates iterators.
      76                 :            :    */
      77                 :            :   void clear()
      78                 :            :   {
      79                 :            :     d_list.clear();
      80                 :            :     d_posVector.clear();
      81                 :            :     d_image.clear();
      82                 :            :     Assert(empty());
      83                 :            :   }
      84                 :            : 
      85                 :            :   /**
      86                 :            :    * Similar to a clear(), but the datastructures are not reset in size.
      87                 :            :    * Invalidates iterators.
      88                 :            :    */
      89                 :    8150543 :   void purge()
      90                 :            :   {
      91         [ +  + ]:   22869914 :     while (!empty())
      92                 :            :     {
      93                 :   14719371 :       pop_back();
      94                 :            :     }
      95 [ -  + ][ -  + ]:    8150543 :     Assert(empty());
                 [ -  - ]
      96                 :    8150543 :   }
      97                 :            : 
      98                 :            :   /** Returns true if k is a key of this datastructure. */
      99                 : 1668158908 :   bool isKey(Key x) const
     100                 :            :   {
     101         [ +  + ]: 1668158908 :     if (x >= allocated())
     102                 :            :     {
     103                 :    3932955 :       return false;
     104                 :            :     }
     105                 :            :     else
     106                 :            :     {
     107 [ -  + ][ -  + ]: 1664225953 :       Assert(x < allocated());
                 [ -  - ]
     108                 : 1664225953 :       return d_posVector[x] != +POSITION_SENTINEL;
     109                 :            :     }
     110                 :            :   }
     111                 :            : 
     112                 :            :   /**
     113                 :            :    * Maps the key to value in the map.
     114                 :            :    * Invalidates iterators.
     115                 :            :    */
     116                 :   62726025 :   void set(Key key, const T& value)
     117                 :            :   {
     118         [ +  + ]:   62726025 :     if (key >= allocated())
     119                 :            :     {
     120                 :    1941899 :       increaseSize(key);
     121                 :            :     }
     122                 :            : 
     123         [ +  + ]:   62726025 :     if (!isKey(key))
     124                 :            :     {
     125                 :   52481889 :       d_posVector[key] = size();
     126                 :   52481889 :       d_list.push_back(key);
     127                 :            :     }
     128                 :   62726025 :     d_image[key] = value;
     129                 :   62726025 :   }
     130                 :            : 
     131                 :            :   /** Returns a mutable reference to the element mapped by key. */
     132                 :  288161666 :   T& get(Key key)
     133                 :            :   {
     134 [ -  + ][ -  + ]:  288161666 :     Assert(isKey(key));
                 [ -  - ]
     135                 :  288161666 :     return d_image[key];
     136                 :            :   }
     137                 :            : 
     138                 :            :   /** Returns a const reference to the element mapped by key.*/
     139                 :  951703727 :   const T& operator[](Key key) const
     140                 :            :   {
     141 [ -  + ][ -  + ]:  951703727 :     Assert(isKey(key));
                 [ -  - ]
     142                 :  951703727 :     return d_image[key];
     143                 :            :   }
     144                 :            : 
     145                 :            :   /** Returns an iterator over the keys of the map. */
     146                 :   10448704 :   const_iterator begin() const { return d_list.begin(); }
     147                 :   25945673 :   const_iterator end() const { return d_list.end(); }
     148                 :            : 
     149                 :            :   const KeyList& getKeys() const { return d_list; }
     150                 :            : 
     151                 :            :   /**
     152                 :            :    * Removes the mapping associated with key.
     153                 :            :    * This changes the order of the keys.
     154                 :            :    *
     155                 :            :    * Invalidates iterators.
     156                 :            :    */
     157                 :     951710 :   void remove(Key x)
     158                 :            :   {
     159 [ -  + ][ -  + ]:     951710 :     Assert(isKey(x));
                 [ -  - ]
     160                 :     951710 :     swapToBack(x);
     161 [ -  + ][ -  + ]:     951710 :     Assert(d_list.back() == x);
                 [ -  - ]
     162                 :     951710 :     pop_back();
     163                 :     951710 :   }
     164                 :            : 
     165                 :            :   /** Returns the key at the back of a non-empty list.*/
     166                 :   87348577 :   Key back() const { return d_list.back(); }
     167                 :            : 
     168                 :            :   /** Removes the element associated with the last Key from the map. */
     169                 :   51033974 :   void pop_back()
     170                 :            :   {
     171 [ -  + ][ -  + ]:   51033974 :     Assert(!empty());
                 [ -  - ]
     172                 :   51033974 :     Key atBack = back();
     173                 :   51033974 :     d_posVector[atBack] = +POSITION_SENTINEL;
     174                 :   51033974 :     d_image[atBack] = T();
     175                 :   51033974 :     d_list.pop_back();
     176                 :   51033974 :   }
     177                 :            : 
     178                 :            :   /** Adds at least a constant fraction of the elements in the current map to
     179                 :            :    * another map. */
     180                 :            :   void splitInto(DenseMap<T>& target)
     181                 :            :   {
     182                 :            :     uint32_t targetSize = size() / 2;
     183                 :            :     while (size() > targetSize)
     184                 :            :     {
     185                 :            :       Key key = back();
     186                 :            :       target.set(key, get(key));
     187                 :            :       pop_back();
     188                 :            :     }
     189                 :            :   }
     190                 :            : 
     191                 :            :   /** Adds the current target map to the current map.*/
     192                 :          0 :   void addAll(const DenseMap<T>& target)
     193                 :            :   {
     194         [ -  - ]:          0 :     for (const_iterator i = target.begin(), e = target.end(); i != e; ++i)
     195                 :            :     {
     196                 :          0 :       Key k = *i;
     197                 :          0 :       set(k, target[k]);
     198                 :            :     }
     199                 :          0 :   }
     200                 :            : 
     201                 :            :  private:
     202                 : 3397052785 :   size_t allocated() const
     203                 :            :   {
     204 [ -  + ][ -  + ]: 3397052785 :     Assert(d_posVector.size() == d_image.size());
                 [ -  - ]
     205                 : 3397052785 :     return d_posVector.size();
     206                 :            :   }
     207                 :            : 
     208                 :    1941899 :   void increaseSize(Key max)
     209                 :            :   {
     210 [ -  + ][ -  + ]:    1941899 :     Assert(max >= allocated());
                 [ -  - ]
     211                 :    1941899 :     d_posVector.resize(max + 1, +POSITION_SENTINEL);
     212                 :    1941899 :     d_image.resize(max + 1);
     213                 :    1941899 :   }
     214                 :            : 
     215                 :            :   /** Swaps a member x to the back of d_list. */
     216                 :     951710 :   void swapToBack(Key x)
     217                 :            :   {
     218 [ -  + ][ -  + ]:     951710 :     Assert(isKey(x));
                 [ -  - ]
     219                 :            : 
     220                 :     951710 :     Position currentPos = d_posVector[x];
     221                 :     951710 :     Key atBack = back();
     222                 :            : 
     223                 :     951710 :     d_list[currentPos] = atBack;
     224                 :     951710 :     d_posVector[atBack] = currentPos;
     225                 :            : 
     226                 :     951710 :     Position last = size() - 1;
     227                 :            : 
     228                 :     951710 :     d_list[last] = x;
     229                 :     951710 :     d_posVector[x] = last;
     230                 :     951710 :   }
     231                 :            : }; /* class DenseMap<T> */
     232                 :            : 
     233                 :            : /**
     234                 :            :  * This provides an abstraction for a set of unsigned integers with similar
     235                 :            :  * capabilities as DenseMap. This is implemented as a light wrapper for
     236                 :            :  * DenseMap<bool> with an interface designed for use as a set instead of a map.
     237                 :            :  */
     238                 :            : class DenseSet
     239                 :            : {
     240                 :            :  private:
     241                 :            :   typedef DenseMap<bool> BackingMap;
     242                 :            :   BackingMap d_map;
     243                 :            : 
     244                 :            :  public:
     245                 :            :   typedef BackingMap::const_iterator const_iterator;
     246                 :            :   typedef BackingMap::Key Element;
     247                 :            : 
     248                 :          0 :   size_t size() const { return d_map.size(); }
     249                 :   42800423 :   bool empty() const { return d_map.empty(); }
     250                 :            : 
     251                 :            :   /** See DenseMap's documentation. */
     252                 :    6008810 :   void purge() { d_map.purge(); }
     253                 :            :   void clear() { d_map.clear(); }
     254                 :            : 
     255                 :   14983192 :   bool isMember(Element x) const { return d_map.isKey(x); }
     256                 :            : 
     257                 :            :   /**
     258                 :            :    * Adds an element that is not a member of the set to the set.
     259                 :            :    */
     260                 :     245856 :   void add(Element x)
     261                 :            :   {
     262 [ -  + ][ -  + ]:     245856 :     Assert(!isMember(x));
                 [ -  - ]
     263                 :     245856 :     d_map.set(x, true);
     264                 :     245856 :   }
     265                 :            : 
     266                 :            :   /** Adds an element to the set even if it is already an element of the set. */
     267                 :   34656982 :   void softAdd(Element x) { d_map.set(x, true); }
     268                 :            : 
     269                 :            :   /** Removes an element from the set. */
     270                 :       3925 :   void remove(Element x) { d_map.remove(x); }
     271                 :            : 
     272                 :    2096647 :   const_iterator begin() const { return d_map.begin(); }
     273                 :    2096647 :   const_iterator end() const { return d_map.end(); }
     274                 :            : 
     275                 :   19352242 :   Element back() { return d_map.back(); }
     276                 :   19352242 :   void pop_back() { d_map.pop_back(); }
     277                 :            : }; /* class DenseSet */
     278                 :            : 
     279                 :            : /**
     280                 :            :  * This provides an abstraction for a multiset of unsigned integers with similar
     281                 :            :  * capabilities as DenseMap.
     282                 :            :  * This is implemented as a light wrapper for DenseMap<bool> with an
     283                 :            :  * interface designed for use as a set instead of a map.
     284                 :            :  */
     285                 :            : class DenseMultiset
     286                 :            : {
     287                 :            :  public:
     288                 :            :   typedef uint32_t CountType;
     289                 :            : 
     290                 :            :  private:
     291                 :            :   typedef DenseMap<CountType> BackingMap;
     292                 :            :   BackingMap d_map;
     293                 :            : 
     294                 :            :  public:
     295                 :            :   typedef BackingMap::const_iterator const_iterator;
     296                 :            :   typedef BackingMap::Key Element;
     297                 :            : 
     298                 :     101880 :   DenseMultiset() : d_map() {}
     299                 :            : 
     300                 :            :   size_t size() const { return d_map.size(); }
     301                 :            :   bool empty() const { return d_map.empty(); }
     302                 :            : 
     303                 :     176085 :   void purge() { d_map.purge(); }
     304                 :            :   void clear() { d_map.clear(); }
     305                 :            : 
     306                 :            :   bool isMember(Element x) const { return d_map.isKey(x); }
     307                 :            : 
     308                 :     361485 :   void add(Element x, CountType c = 1u)
     309                 :            :   {
     310 [ -  + ][ -  + ]:     361485 :     Assert(c > 0);
                 [ -  - ]
     311         [ +  + ]:     361485 :     if (d_map.isKey(x))
     312                 :            :     {
     313                 :       2661 :       d_map.set(x, d_map.get(x) + c);
     314                 :            :     }
     315                 :            :     else
     316                 :            :     {
     317                 :     358824 :       d_map.set(x, c);
     318                 :            :     }
     319                 :     361485 :   }
     320                 :            : 
     321                 :          0 :   void setCount(Element x, CountType c) { d_map.set(x, c); }
     322                 :            : 
     323                 :          0 :   void removeAll(Element x) { return d_map.remove(x); }
     324                 :            : 
     325                 :          0 :   void removeOne(Element x)
     326                 :            :   {
     327                 :          0 :     CountType c = count(x);
     328    [ -  - ][ - ]:          0 :     switch (c)
     329                 :            :     {
     330                 :          0 :       case 0: break;                        // do nothing
     331                 :          0 :       case 1: removeAll(x); break;          // remove
     332                 :          0 :       default: d_map.set(x, c - 1); break;  // decrease
     333                 :            :     }
     334                 :          0 :   }
     335                 :            : 
     336                 :          0 :   void removeOneOfEverything()
     337                 :            :   {
     338                 :          0 :     BackingMap::KeyList keys(d_map.begin(), d_map.end());
     339                 :          0 :     for (BackingMap::const_iterator i = keys.begin(), i_end = keys.end();
     340         [ -  - ]:          0 :          i != i_end;
     341                 :          0 :          ++i)
     342                 :            :     {
     343                 :          0 :       removeOne(*i);
     344                 :            :     }
     345                 :          0 :   }
     346                 :            : 
     347                 :     361667 :   CountType count(Element x) const
     348                 :            :   {
     349         [ +  + ]:     361667 :     if (d_map.isKey(x))
     350                 :            :     {
     351                 :       2843 :       return d_map[x];
     352                 :            :     }
     353                 :            :     else
     354                 :            :     {
     355                 :     358824 :       return 0;
     356                 :            :     }
     357                 :            :   }
     358                 :            : 
     359                 :          0 :   const_iterator begin() const { return d_map.begin(); }
     360                 :          0 :   const_iterator end() const { return d_map.end(); }
     361                 :            :   Element back() { return d_map.back(); }
     362                 :            :   void pop_back() { d_map.pop_back(); }
     363                 :            : }; /* class DenseMultiset */
     364                 :            : 
     365                 :            : }  // namespace cvc5::internal