Branch data     Line data    Source code

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