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                 :            :  * Context-dependent insert only hashmap built using trail of edits
      11                 :            :  *
      12                 :            :  * Context-dependent hashmap that only allows for one insertion per element.
      13                 :            :  * This can be viewed as a highly restricted version of CDHashMap.
      14                 :            :  * It is significantly lighter in memory usage than CDHashMap.
      15                 :            :  *
      16                 :            :  * See also:
      17                 :            :  *  CDTrailHashMap : A lightweight CD hash map with poor iteration
      18                 :            :  *    characteristics and some quirks in usage.
      19                 :            :  *  CDHashMap : A fully featured CD hash map. (The closest to <ext/hash_map>)
      20                 :            :  *
      21                 :            :  * Notes:
      22                 :            :  * - To iterate efficiently over the elements use the key_iterators.
      23                 :            :  * - operator[] is only supported as a const derefence (must succeed).
      24                 :            :  * - insert(k) must always work.
      25                 :            :  * - Use insert_safe if you want to check if the element has been inserted
      26                 :            :  *   and only insert if it has not yet been.
      27                 :            :  * - Does not accept TNodes as keys.
      28                 :            :  */
      29                 :            : 
      30                 :            : #include "cvc5parser_public.h"
      31                 :            : 
      32                 :            : #ifndef CVC5__CONTEXT__CDINSERT_HASHMAP_H
      33                 :            : #define CVC5__CONTEXT__CDINSERT_HASHMAP_H
      34                 :            : 
      35                 :            : #include <deque>
      36                 :            : #include <functional>
      37                 :            : #include <unordered_map>
      38                 :            : #include <utility>
      39                 :            : 
      40                 :            : #include "base/check.h"
      41                 :            : #include "base/output.h"
      42                 :            : #include "context/cdinsert_hashmap_forward.h"
      43                 :            : #include "context/context.h"
      44                 :            : 
      45                 :            : namespace cvc5 {
      46                 :            : 
      47                 :            : namespace internal {
      48                 :            : template <bool ref_count>
      49                 :            : class NodeTemplate;
      50                 :            : }
      51                 :            : 
      52                 :            : namespace context {
      53                 :            : 
      54                 :            : template <class Key, class Data, class HashFcn = std::hash<Key> >
      55                 :            : class InsertHashMap
      56                 :            : {
      57                 :            :  private:
      58                 :            :   using KeyVec = std::deque<Key>;
      59                 :            :   /** A list of the keys in the map maintained as a stack. */
      60                 :            :   KeyVec d_keys;
      61                 :            : 
      62                 :            :   using HashMap = std::unordered_map<const Key, const Data, HashFcn>;
      63                 :            :   /** The hash_map used for element lookup. */
      64                 :            :   HashMap d_hashMap;
      65                 :            : 
      66                 :            :  public:
      67                 :            :   /**
      68                 :            :    * An iterator over a list of keys.
      69                 :            :    * Use this to efficiently iterate over the elements.
      70                 :            :    * (See std::deque<>::iterator).
      71                 :            :    */
      72                 :            :   typedef typename KeyVec::const_iterator key_iterator;
      73                 :            : 
      74                 :            :   /**An iterator over the elements in the hash_map. */
      75                 :            :   typedef typename HashMap::const_iterator const_iterator;
      76                 :            : 
      77                 :            :   // The type of the <Key, Data> values in the hashmap.
      78                 :            :   using value_type = typename HashMap::value_type;
      79                 :            : 
      80                 :            :   /**
      81                 :            :    * Returns an iterator to the begining of the HashMap.
      82                 :            :    * Acts like a hash_map::const_iterator.
      83                 :            :    */
      84                 :     352829 :   const_iterator begin() const { return d_hashMap.begin(); }
      85                 :            :   /**
      86                 :            :    * Returns an iterator to the end of the HashMap.
      87                 :            :    * Acts like a hash_map::const_iterator.
      88                 :            :    */
      89                 : 1039513032 :   const_iterator end() const { return d_hashMap.end(); }
      90                 :            : 
      91                 :            :   /**
      92                 :            :    * Returns an iterator to the Key k of the map.
      93                 :            :    * See hash_map::find()
      94                 :            :    */
      95                 : 1039160051 :   const_iterator find(const Key& k) const { return d_hashMap.find(k); }
      96                 :            : 
      97                 :            :   /** Returns an iterator to the start of the set of keys. */
      98                 :        755 :   key_iterator key_begin() const { return d_keys.begin(); }
      99                 :            :   /** Returns an iterator to the end of the set of keys. */
     100                 :        755 :   key_iterator key_end() const { return d_keys.end(); }
     101                 :            : 
     102                 :            :   /** Returns true if the map is empty. */
     103                 :  113304564 :   bool empty() const { return d_keys.empty(); }
     104                 :            :   /** Returns the number of elements in the map. */
     105                 :  266242718 :   size_t size() const { return d_keys.size(); }
     106                 :            : 
     107                 :            :   /** Returns true if k is a mapped key. */
     108                 :  311783807 :   bool contains(const Key& k) const { return find(k) != end(); }
     109                 :            : 
     110                 :            :   /**
     111                 :            :    * Returns a reference the data mapped by k.
     112                 :            :    * This must succeed.
     113                 :            :    */
     114                 :  178641148 :   const Data& operator[](const Key& k) const
     115                 :            :   {
     116                 :  178641148 :     const_iterator ci = find(k);
     117 [ -  + ][ -  + ]:  178641148 :     Assert(ci != end());
                 [ -  - ]
     118                 :  178641148 :     return (*ci).second;
     119                 :            :   }
     120                 :            : 
     121                 :            :   /**
     122                 :            :    * Inserts an element into the map, and pushes its key to the front
     123                 :            :    * of the stack. The key inserted must be not be currently mapped.
     124                 :            :    */
     125                 :            :   void push_front(const Key& k, const Data& d)
     126                 :            :   {
     127                 :            :     Assert(!contains(k));
     128                 :            :     d_hashMap.insert(std::make_pair(k, d));
     129                 :            :     d_keys.push_front(k);
     130                 :            :   }
     131                 :            : 
     132                 :            :   /**
     133                 :            :    * Inserts an element into the map, and pushes its key onto the
     134                 :            :    * back on the stack.  The key inserted must be not be currently mapped.
     135                 :            :    */
     136                 :  131438748 :   void push_back(const Key& k, const Data& d)
     137                 :            :   {
     138 [ -  + ][ -  + ]:  131438748 :     Assert(!contains(k));
                 [ -  - ]
     139                 :  131438748 :     d_hashMap.insert(std::make_pair(k, d));
     140                 :  131438748 :     d_keys.push_back(k);
     141                 :  131438748 :   }
     142                 :            : 
     143                 :            :   /**
     144                 :            :    * Pops the key at the front of the list off and removes its key from the map.
     145                 :            :    */
     146                 :            :   void pop_front()
     147                 :            :   {
     148                 :            :     Assert(!empty());
     149                 :            :     const Key& front = d_keys.front();
     150                 :            :     d_hashMap.erase(front);
     151                 :            : 
     152                 :            :     Trace("TrailHashMap") << "TrailHashMap pop_front " << size() << std::endl;
     153                 :            :     d_keys.pop_front();
     154                 :            :   }
     155                 :            : 
     156                 :            :   /**
     157                 :            :    * Pops the key at the back of the stack off and removes its key from the map.
     158                 :            :    */
     159                 :  113304564 :   void pop_back()
     160                 :            :   {
     161 [ -  + ][ -  + ]:  113304564 :     Assert(!empty());
                 [ -  - ]
     162                 :  113304564 :     const Key& back = d_keys.back();
     163                 :  113304564 :     d_hashMap.erase(back);
     164                 :            : 
     165         [ +  - ]:  113304564 :     Trace("TrailHashMap") << "TrailHashMap pop_back " << size() << std::endl;
     166                 :  113304564 :     d_keys.pop_back();
     167                 :  113304564 :   }
     168                 :            : 
     169                 :            :   /**
     170                 :            :    * Pops the back of the stack until the size is below s.
     171                 :            :    */
     172                 :    7409696 :   void pop_to_size(size_t s)
     173                 :            :   {
     174         [ +  + ]:  120714260 :     while (size() > s)
     175                 :            :     {
     176                 :  113304564 :       pop_back();
     177                 :            :     }
     178                 :    7409696 :   }
     179                 :            : }; /* class TrailHashMap<> */
     180                 :            : 
     181                 :            : template <class Key, class Data, class HashFcn>
     182                 :            : class CDInsertHashMap : public ContextObj
     183                 :            : {
     184                 :            :  private:
     185                 :            :   typedef InsertHashMap<Key, Data, HashFcn> IHM;
     186                 :            : 
     187                 :            :   /** An InsertHashMap that backs all of the data. */
     188                 :            :   IHM* d_insertMap;
     189                 :            : 
     190                 :            :   /** For restores, we need to keep track of the previous size. */
     191                 :            :   size_t d_size;
     192                 :            : 
     193                 :            :   /**
     194                 :            :    * Private copy constructor used only by save().  d_insertMap is
     195                 :            :    * not copied: only the base class information and
     196                 :            :    * d_size are needed in restore.
     197                 :            :    */
     198                 :    7411426 :   CDInsertHashMap(const CDInsertHashMap& l)
     199                 :    7411426 :       : ContextObj(l), d_insertMap(nullptr), d_size(l.d_size)
     200                 :            :   {
     201         [ +  - ]:    7411426 :     Trace("CDInsertHashMap") << "copy ctor: " << this << " from " << &l
     202                 :          0 :                              << " size " << d_size << std::endl;
     203                 :    7411426 :   }
     204                 :            :   CDInsertHashMap& operator=(const CDInsertHashMap&) = delete;
     205                 :            : 
     206                 :            :   /**
     207                 :            :    * Implementation of mandatory ContextObj method save: simply copies
     208                 :            :    * the current size information to a copy using the copy constructor (the
     209                 :            :    * pointer and the allocated size are *not* copied as they are not
     210                 :            :    * restored on a pop).  The saved information is allocated using the
     211                 :            :    * ContextMemoryManager.
     212                 :            :    */
     213                 :    7411426 :   ContextObj* save(ContextMemoryManager* pCMM) override
     214                 :            :   {
     215                 :    7411426 :     ContextObj* data = new (pCMM) CDInsertHashMap<Key, Data, HashFcn>(*this);
     216                 :    7411426 :     return data;
     217                 :            :   }
     218                 :            : 
     219                 :            :  protected:
     220                 :            :   /**
     221                 :            :    * Implementation of mandatory ContextObj method restore:
     222                 :            :    * restore to the previous size taking into account the number
     223                 :            :    * of new pushFront calls have happened since saving.
     224                 :            :    * The d_insertMap is untouched.
     225                 :            :    */
     226                 :    7409696 :   void restore(ContextObj* data) override
     227                 :            :   {
     228                 :    7409696 :     size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size;
     229                 :            : 
     230                 :            :     // The size to restore to.
     231                 :    7409696 :     size_t restoreSize = oldSize;
     232                 :    7409696 :     d_insertMap->pop_to_size(restoreSize);
     233                 :    7409696 :     d_size = restoreSize;
     234 [ -  + ][ -  + ]:    7409696 :     Assert(d_insertMap->size() == d_size);
                 [ -  - ]
     235                 :    7409696 :   }
     236                 :            : 
     237                 :            :  public:
     238                 :            :   /**
     239                 :            :    * Main constructor: d_insertMap starts as an empty map, with the size is 0
     240                 :            :    */
     241                 :    6680014 :   CDInsertHashMap(Context* context)
     242                 :    6680014 :       : ContextObj(context), d_insertMap(new IHM()), d_size(0)
     243                 :            :   {
     244 [ -  + ][ -  + ]:    6680014 :     Assert(d_insertMap->size() == d_size);
                 [ -  - ]
     245                 :    6680014 :   }
     246                 :            : 
     247                 :            :   /**
     248                 :            :    * Destructor: delete the d_insertMap
     249                 :            :    */
     250                 :    6638275 :   ~CDInsertHashMap()
     251                 :            :   {
     252                 :    6638275 :     this->destroy();
     253         [ +  - ]:    6638275 :     delete d_insertMap;
     254                 :   13276550 :   }
     255                 :            : 
     256                 :            :   /** An iterator over the elements in the hash_map. */
     257                 :            :   typedef typename IHM::const_iterator const_iterator;
     258                 :            : 
     259                 :            :   /**
     260                 :            :    * An iterator over a list of keys.
     261                 :            :    * Use this to efficiently iterate over the elements.
     262                 :            :    * (See std::deque<>::iterator).
     263                 :            :    */
     264                 :            :   typedef typename IHM::key_iterator key_iterator;
     265                 :            : 
     266                 :            :   // The type of the <key, data> values in the hashmap.
     267                 :            :   using value_type = typename IHM::value_type;
     268                 :            : 
     269                 :            :   /** Returns true if the map is empty in the current context. */
     270                 :          0 :   bool empty() const { return d_size == 0; }
     271                 :            : 
     272                 :            :   /** Returns true the size of the map in the current context. */
     273                 :   26067121 :   size_t size() const { return d_size; }
     274                 :            : 
     275                 :            :   /**
     276                 :            :    * Inserts an element into the map.
     277                 :            :    * The key inserted must be not be currently mapped.
     278                 :            :    * This is implemented using d_insertMap.push_back().
     279                 :            :    */
     280                 :  131438748 :   void insert(const Key& k, const Data& d)
     281                 :            :   {
     282                 :  131438748 :     makeCurrent();
     283                 :  131438748 :     ++d_size;
     284                 :  131438748 :     d_insertMap->push_back(k, d);
     285 [ -  + ][ -  + ]:  131438748 :     Assert(d_insertMap->size() == d_size);
                 [ -  - ]
     286                 :  131438748 :   }
     287                 :            : 
     288                 :            :   /**
     289                 :            :    * Checks if the key k is mapped already.
     290                 :            :    * If it is, this returns false.
     291                 :            :    * Otherwise it is inserted and this returns true.
     292                 :            :    */
     293                 :   68198274 :   bool insert_safe(const Key& k, const Data& d)
     294                 :            :   {
     295         [ +  + ]:   68198274 :     if (contains(k))
     296                 :            :     {
     297                 :     554251 :       return false;
     298                 :            :     }
     299                 :            :     else
     300                 :            :     {
     301                 :   67644023 :       insert(k, d);
     302                 :   67644023 :       return true;
     303                 :            :     }
     304                 :            :   }
     305                 :            : 
     306                 :            :   /** Returns true if k is a mapped key in the context. */
     307                 :  180345059 :   bool contains(const Key& k) const { return d_insertMap->contains(k); }
     308                 :            : 
     309                 :            :   /**
     310                 :            :    * Returns a reference the data mapped by k.
     311                 :            :    * k must be in the map in this context.
     312                 :            :    */
     313                 :  178641148 :   const Data& operator[](const Key& k) const { return (*d_insertMap)[k]; }
     314                 :            : 
     315                 :            :   /**
     316                 :            :    * Returns a const_iterator to the value_type if k is a mapped key in
     317                 :            :    * the context.
     318                 :            :    */
     319                 :  548735096 :   const_iterator find(const Key& k) const { return d_insertMap->find(k); }
     320                 :            : 
     321                 :            :   /**
     322                 :            :    * Returns an iterator to the begining of the map.
     323                 :            :    * Acts like a hash_map::const_iterator.
     324                 :            :    */
     325                 :     352829 :   const_iterator begin() const { return d_insertMap->begin(); }
     326                 :            : 
     327                 :            :   /**
     328                 :            :    * Returns an iterator to the end of the map.
     329                 :            :    * Acts like a hash_map::const_iterator.
     330                 :            :    */
     331                 :  549088077 :   const_iterator end() const { return d_insertMap->end(); }
     332                 :            : 
     333                 :            :   /** Returns an iterator to the start of the set of keys. */
     334                 :        755 :   key_iterator key_begin() const { return d_insertMap->key_begin(); }
     335                 :            :   /** Returns an iterator to the end of the set of keys. */
     336                 :        755 :   key_iterator key_end() const { return d_insertMap->key_end(); }
     337                 :            : }; /* class CDInsertHashMap<> */
     338                 :            : 
     339                 :            : template <class Data, class HashFcn>
     340                 :            : class CDInsertHashMap<internal::NodeTemplate<false>, Data, HashFcn>
     341                 :            :     : public ContextObj
     342                 :            : {
     343                 :            :   /* CDInsertHashMap is challenging to get working with TNode.
     344                 :            :    * Consider using CDHashMap<TNode,...> instead.
     345                 :            :    *
     346                 :            :    * Explanation:
     347                 :            :    * CDInsertHashMap uses keys for deallocation.
     348                 :            :    * If the key is a TNode and the backing (the hard node reference)
     349                 :            :    * for the key in another data structure removes the key at the same context
     350                 :            :    * the ref count could drop to 0.  The key would then not be eligible to be
     351                 :            :    * hashed. Getting the order right with a guarantee is too hard.
     352                 :            :    */
     353                 :            : 
     354                 :            :   static_assert(sizeof(Data) == 0,
     355                 :            :                 "Cannot create a CDInsertHashMap with TNode keys");
     356                 :            : };
     357                 :            : 
     358                 :            : }  // namespace context
     359                 :            : }  // namespace cvc5
     360                 :            : 
     361                 :            : #endif