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                 :            : private:
      57                 :            :   using KeyVec = std::deque<Key>;
      58                 :            :   /** A list of the keys in the map maintained as a stack. */
      59                 :            :   KeyVec d_keys;
      60                 :            : 
      61                 :            :   using HashMap = std::unordered_map<const Key, const Data, HashFcn>;
      62                 :            :   /** The hash_map used for element lookup. */
      63                 :            :   HashMap d_hashMap;
      64                 :            : 
      65                 :            : public:
      66                 :            :   /**
      67                 :            :    * An iterator over a list of keys.
      68                 :            :    * Use this to efficiently iterate over the elements.
      69                 :            :    * (See std::deque<>::iterator).
      70                 :            :    */
      71                 :            :   typedef typename KeyVec::const_iterator key_iterator;
      72                 :            : 
      73                 :            :   /**An iterator over the elements in the hash_map. */
      74                 :            :   typedef typename HashMap::const_iterator const_iterator;
      75                 :            : 
      76                 :            :   // The type of the <Key, Data> values in the hashmap.
      77                 :            :   using value_type = typename HashMap::value_type;
      78                 :            : 
      79                 :            :   /**
      80                 :            :    * Returns an iterator to the begining of the HashMap.
      81                 :            :    * Acts like a hash_map::const_iterator.
      82                 :            :    */
      83                 :     341835 :   const_iterator begin() const{
      84                 :     341835 :     return d_hashMap.begin();
      85                 :            :   }
      86                 :            :   /**
      87                 :            :    * Returns an iterator to the end of the HashMap.
      88                 :            :    * Acts like a hash_map::const_iterator.
      89                 :            :    */
      90                 : 1032304916 :   const_iterator end() const{
      91                 : 1032304916 :     return d_hashMap.end();
      92                 :            :   }
      93                 :            : 
      94                 :            :   /**
      95                 :            :    * Returns an iterator to the Key k of the map.
      96                 :            :    * See hash_map::find()
      97                 :            :    */
      98                 : 1031962929 :   const_iterator find(const Key& k) const{
      99                 : 1031962929 :     return d_hashMap.find(k);
     100                 :            :   }
     101                 :            : 
     102                 :            :   /** Returns an iterator to the start of the set of keys. */
     103                 :        792 :   key_iterator key_begin() const{
     104                 :        792 :     return d_keys.begin();
     105                 :            :   }
     106                 :            :   /** Returns an iterator to the end of the set of keys. */
     107                 :        792 :   key_iterator key_end() const{
     108                 :        792 :     return d_keys.end();
     109                 :            :   }
     110                 :            : 
     111                 :            :   /** Returns true if the map is empty. */
     112                 :  112789553 :   bool empty() const { return d_keys.empty(); }
     113                 :            :   /** Returns the number of elements in the map. */
     114                 :  264478143 :   size_t size() const { return d_keys.size(); }
     115                 :            : 
     116                 :            :   /** Returns true if k is a mapped key. */
     117                 :  309176093 :   bool contains(const Key& k) const {
     118                 :  309176093 :     return find(k) != end();
     119                 :            :   }
     120                 :            : 
     121                 :            :   /**
     122                 :            :    * Returns a reference the data mapped by k.
     123                 :            :    * This must succeed.
     124                 :            :    */
     125                 :  177377054 :   const Data& operator[](const Key& k) const {
     126                 :  177377054 :     const_iterator ci = find(k);
     127 [ -  + ][ -  + ]:  177377054 :     Assert(ci != end());
                 [ -  - ]
     128                 :  177377054 :     return (*ci).second;
     129                 :            :   }
     130                 :            : 
     131                 :            :   /**
     132                 :            :    * Inserts an element into the map, and pushes its key to the front
     133                 :            :    * of the stack. The key inserted must be not be currently mapped.
     134                 :            :    */
     135                 :            :   void push_front(const Key& k, const Data& d){
     136                 :            :     Assert(!contains(k));
     137                 :            :     d_hashMap.insert(std::make_pair(k, d));
     138                 :            :     d_keys.push_front(k);
     139                 :            :   }
     140                 :            : 
     141                 :            :   /**
     142                 :            :    * Inserts an element into the map, and pushes its key onto the
     143                 :            :    * back on the stack.  The key inserted must be not be currently mapped.
     144                 :            :    */
     145                 :  130385383 :   void push_back(const Key& k, const Data& d){
     146 [ -  + ][ -  + ]:  130385383 :     Assert(!contains(k));
                 [ -  - ]
     147                 :  130385383 :     d_hashMap.insert(std::make_pair(k, d));
     148                 :  130385383 :     d_keys.push_back(k);
     149                 :  130385383 :   }
     150                 :            : 
     151                 :            :   /**
     152                 :            :    * Pops the key at the front of the list off and removes its key from the map.
     153                 :            :    */
     154                 :            :   void pop_front(){
     155                 :            :     Assert(!empty());
     156                 :            :     const Key& front = d_keys.front();
     157                 :            :     d_hashMap.erase(front);
     158                 :            : 
     159                 :            :     Trace("TrailHashMap") <<"TrailHashMap pop_front " << size() << std::endl;
     160                 :            :     d_keys.pop_front();
     161                 :            :   }
     162                 :            : 
     163                 :            :   /**
     164                 :            :    * Pops the key at the back of the stack off and removes its key from the map.
     165                 :            :    */
     166                 :  112789553 :   void pop_back(){
     167 [ -  + ][ -  + ]:  112789553 :     Assert(!empty());
                 [ -  - ]
     168                 :  112789553 :     const Key& back = d_keys.back();
     169                 :  112789553 :     d_hashMap.erase(back);
     170                 :            : 
     171         [ +  - ]:  112789553 :     Trace("TrailHashMap") <<"TrailHashMap pop_back " << size() << std::endl;
     172                 :  112789553 :     d_keys.pop_back();
     173                 :  112789553 :   }
     174                 :            : 
     175                 :            :   /**
     176                 :            :    * Pops the back of the stack until the size is below s.
     177                 :            :    */
     178                 :    7358332 :   void pop_to_size(size_t s){
     179         [ +  + ]:  120147885 :     while(size() > s){
     180                 :  112789553 :       pop_back();
     181                 :            :     }
     182                 :    7358332 :   }
     183                 :            : };/* class TrailHashMap<> */
     184                 :            : 
     185                 :            : template <class Key, class Data, class HashFcn>
     186                 :            : class CDInsertHashMap : public ContextObj {
     187                 :            : private:
     188                 :            :   typedef InsertHashMap<Key, Data, HashFcn> IHM;
     189                 :            : 
     190                 :            :   /** An InsertHashMap that backs all of the data. */
     191                 :            :   IHM* d_insertMap;
     192                 :            : 
     193                 :            :   /** For restores, we need to keep track of the previous size. */
     194                 :            :   size_t d_size;
     195                 :            : 
     196                 :            :   /**
     197                 :            :    * Private copy constructor used only by save().  d_insertMap is
     198                 :            :    * not copied: only the base class information and
     199                 :            :    * d_size are needed in restore.
     200                 :            :    */
     201                 :    7360062 :   CDInsertHashMap(const CDInsertHashMap& l)
     202                 :    7360062 :       : ContextObj(l), d_insertMap(nullptr), d_size(l.d_size)
     203                 :            :   {
     204         [ +  - ]:   14720124 :     Trace("CDInsertHashMap") << "copy ctor: " << this
     205                 :    7360062 :                     << " from " << &l
     206                 :          0 :                     << " size " << d_size << std::endl;
     207                 :    7360062 :   }
     208                 :            :   CDInsertHashMap& operator=(const CDInsertHashMap&) = delete;
     209                 :            : 
     210                 :            :   /**
     211                 :            :    * Implementation of mandatory ContextObj method save: simply copies
     212                 :            :    * the current size information to a copy using the copy constructor (the
     213                 :            :    * pointer and the allocated size are *not* copied as they are not
     214                 :            :    * restored on a pop).  The saved information is allocated using the
     215                 :            :    * ContextMemoryManager.
     216                 :            :    */
     217                 :    7360062 :   ContextObj* save(ContextMemoryManager* pCMM) override
     218                 :            :   {
     219                 :    7360062 :     ContextObj* data = new(pCMM) CDInsertHashMap<Key, Data, HashFcn>(*this);
     220                 :    7360062 :     return data;
     221                 :            :   }
     222                 :            : protected:
     223                 :            :  /**
     224                 :            :   * Implementation of mandatory ContextObj method restore:
     225                 :            :   * restore to the previous size taking into account the number
     226                 :            :   * of new pushFront calls have happened since saving.
     227                 :            :   * The d_insertMap is untouched.
     228                 :            :   */
     229                 :    7358332 :  void restore(ContextObj* data) override
     230                 :            :  {
     231                 :    7358332 :    size_t oldSize = ((CDInsertHashMap<Key, Data, HashFcn>*)data)->d_size;
     232                 :            : 
     233                 :            :    // The size to restore to.
     234                 :    7358332 :    size_t restoreSize = oldSize;
     235                 :    7358332 :    d_insertMap->pop_to_size(restoreSize);
     236                 :    7358332 :    d_size = restoreSize;
     237 [ -  + ][ -  + ]:    7358332 :    Assert(d_insertMap->size() == d_size);
                 [ -  - ]
     238                 :    7358332 :   }
     239                 :            : public:
     240                 :            : 
     241                 :            :  /**
     242                 :            :    * Main constructor: d_insertMap starts as an empty map, with the size is 0
     243                 :            :    */
     244                 :    6586543 :  CDInsertHashMap(Context* context)
     245                 :    6586543 :      : ContextObj(context), d_insertMap(new IHM()), d_size(0)
     246                 :            :  {
     247 [ -  + ][ -  + ]:    6586543 :    Assert(d_insertMap->size() == d_size);
                 [ -  - ]
     248                 :    6586543 :  }
     249                 :            : 
     250                 :            :   /**
     251                 :            :    * Destructor: delete the d_insertMap
     252                 :            :    */
     253                 :    6544848 :   ~CDInsertHashMap() {
     254                 :    6544848 :     this->destroy();
     255         [ +  - ]:    6544848 :     delete d_insertMap;
     256                 :   13089696 :   }
     257                 :            : 
     258                 :            :   /** An iterator over the elements in the hash_map. */
     259                 :            :   typedef typename IHM::const_iterator const_iterator;
     260                 :            : 
     261                 :            :   /**
     262                 :            :    * An iterator over a list of keys.
     263                 :            :    * Use this to efficiently iterate over the elements.
     264                 :            :    * (See std::deque<>::iterator).
     265                 :            :    */
     266                 :            :   typedef typename IHM::key_iterator key_iterator;
     267                 :            : 
     268                 :            :   // The type of the <key, data> values in the hashmap.
     269                 :            :   using value_type = typename IHM::value_type;
     270                 :            : 
     271                 :            :   /** Returns true if the map is empty in the current context. */
     272                 :          0 :   bool empty() const{
     273                 :          0 :     return d_size == 0;
     274                 :            :   }
     275                 :            : 
     276                 :            :   /** Returns true the size of the map in the current context. */
     277                 :   25959214 :   size_t size() const {
     278                 :   25959214 :     return d_size;
     279                 :            :   }
     280                 :            : 
     281                 :            :   /**
     282                 :            :    * Inserts an element into the map.
     283                 :            :    * The key inserted must be not be currently mapped.
     284                 :            :    * This is implemented using d_insertMap.push_back().
     285                 :            :    */
     286                 :  130385383 :   void insert(const Key& k, const Data& d){
     287                 :  130385383 :     makeCurrent();
     288                 :  130385383 :     ++d_size;
     289                 :  130385383 :     d_insertMap->push_back(k, d);
     290 [ -  + ][ -  + ]:  130385383 :     Assert(d_insertMap->size() == d_size);
                 [ -  - ]
     291                 :  130385383 :   }
     292                 :            : 
     293                 :            :   /**
     294                 :            :    * Checks if the key k is mapped already.
     295                 :            :    * If it is, this returns false.
     296                 :            :    * Otherwise it is inserted and this returns true.
     297                 :            :    */
     298                 :   67815245 :   bool insert_safe(const Key& k, const Data& d){
     299         [ +  + ]:   67815245 :     if(contains(k)){
     300                 :     534325 :       return false;
     301                 :            :     }else{
     302                 :   67280920 :       insert(k,d);
     303                 :   67280920 :       return true;
     304                 :            :     }
     305                 :            :   }
     306                 :            : 
     307                 :            :   /** Returns true if k is a mapped key in the context. */
     308                 :  178790710 :   bool contains(const Key& k) const {
     309                 :  178790710 :     return d_insertMap->contains(k);
     310                 :            :   }
     311                 :            : 
     312                 :            :   /**
     313                 :            :    * Returns a reference the data mapped by k.
     314                 :            :    * k must be in the map in this context.
     315                 :            :    */
     316                 :  177377054 :   const Data& operator[](const Key& k) const {
     317                 :  177377054 :     return (*d_insertMap)[k];
     318                 :            :   }
     319                 :            : 
     320                 :            :    /**
     321                 :            :     * Returns a const_iterator to the value_type if k is a mapped key in
     322                 :            :     * the context.
     323                 :            :     */
     324                 :  545409782 :   const_iterator find(const Key& k) const {
     325                 :  545409782 :     return d_insertMap->find(k);
     326                 :            :   }
     327                 :            : 
     328                 :            :   /**
     329                 :            :    * Returns an iterator to the begining of the map.
     330                 :            :    * Acts like a hash_map::const_iterator.
     331                 :            :    */
     332                 :     341835 :   const_iterator begin() const{
     333                 :     341835 :     return d_insertMap->begin();
     334                 :            :   }
     335                 :            : 
     336                 :            :   /**
     337                 :            :    * Returns an iterator to the end of the map.
     338                 :            :    * Acts like a hash_map::const_iterator.
     339                 :            :    */
     340                 :  545751769 :   const_iterator end() const{
     341                 :  545751769 :     return d_insertMap->end();
     342                 :            :   }
     343                 :            : 
     344                 :            :   /** Returns an iterator to the start of the set of keys. */
     345                 :        792 :   key_iterator key_begin() const{
     346                 :        792 :     return d_insertMap->key_begin();
     347                 :            :   }
     348                 :            :   /** Returns an iterator to the end of the set of keys. */
     349                 :        792 :   key_iterator key_end() const{
     350                 :        792 :     return d_insertMap->key_end();
     351                 :            :   }
     352                 :            : };/* class CDInsertHashMap<> */
     353                 :            : 
     354                 :            : template <class Data, class HashFcn>
     355                 :            : class CDInsertHashMap<internal::NodeTemplate<false>, Data, HashFcn>
     356                 :            :     : public ContextObj
     357                 :            : {
     358                 :            :   /* CDInsertHashMap is challenging to get working with TNode.
     359                 :            :    * Consider using CDHashMap<TNode,...> instead.
     360                 :            :    *
     361                 :            :    * Explanation:
     362                 :            :    * CDInsertHashMap uses keys for deallocation.
     363                 :            :    * If the key is a TNode and the backing (the hard node reference)
     364                 :            :    * for the key in another data structure removes the key at the same context
     365                 :            :    * the ref count could drop to 0.  The key would then not be eligible to be
     366                 :            :    * hashed. Getting the order right with a guarantee is too hard.
     367                 :            :    */
     368                 :            : 
     369                 :            :   static_assert(sizeof(Data) == 0,
     370                 :            :                 "Cannot create a CDInsertHashMap with TNode keys");
     371                 :            : };
     372                 :            : 
     373                 :            : }  // namespace context
     374                 :            : }  // namespace cvc5
     375                 :            : 
     376                 :            : #endif