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 set class.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5parser_public.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__CONTEXT__CDHASHSET_H
      16                 :            : #define CVC5__CONTEXT__CDHASHSET_H
      17                 :            : 
      18                 :            : #include "base/check.h"
      19                 :            : #include "context/cdinsert_hashmap.h"
      20                 :            : #include "context/context.h"
      21                 :            : 
      22                 :            : namespace cvc5::context {
      23                 :            : 
      24                 :            : template <class V, class HashFcn = std::hash<V>>
      25                 :            : class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn>
      26                 :            : {
      27                 :            :   typedef CDInsertHashMap<V, bool, HashFcn> super;
      28                 :            : 
      29                 :            :   // no copy or assignment
      30                 :            :   CDHashSet(const CDHashSet&) = delete;
      31                 :            :   CDHashSet& operator=(const CDHashSet&) = delete;
      32                 :            : 
      33                 :            :  public:
      34                 :            :   // ensure these are publicly accessible
      35                 :      29451 :   static void* operator new(size_t size, bool b)
      36                 :            :   {
      37                 :      29451 :     return ContextObj::operator new(size, b);
      38                 :            :   }
      39                 :            : 
      40                 :          0 :   static void operator delete(void* pMem, bool b)
      41                 :            :   {
      42                 :          0 :     return ContextObj::operator delete(pMem, b);
      43                 :            :   }
      44                 :            : 
      45                 :      29451 :   void deleteSelf() { this->ContextObj::deleteSelf(); }
      46                 :            : 
      47                 :          0 :   static void operator delete(CVC5_UNUSED void* pMem)
      48                 :            :   {
      49                 :          0 :     AlwaysAssert(false) << "It is not allowed to delete a ContextObj this way!";
      50                 :            :   }
      51                 :            : 
      52                 :    4357926 :   CDHashSet(Context* context) : super(context) {}
      53                 :            : 
      54                 :   12031749 :   size_t size() const { return super::size(); }
      55                 :            : 
      56                 :          0 :   bool empty() const { return super::empty(); }
      57                 :            : 
      58                 :   59219048 :   bool insert(const V& v) { return super::insert_safe(v, true); }
      59                 :            : 
      60                 :    4641803 :   bool contains(const V& v) const { return super::contains(v); }
      61                 :            : 
      62                 :            :   class const_iterator
      63                 :            :   {
      64                 :            :     typename super::const_iterator d_it;
      65                 :            : 
      66                 :            :    public:
      67                 :  362922490 :     const_iterator(const typename super::const_iterator& it) : d_it(it) {}
      68                 :            : 
      69                 :      69001 :     const_iterator() = default;
      70                 :            : 
      71                 :            :     // (Dis)equality
      72                 :   84856766 :     bool operator==(const const_iterator& i) const { return d_it == i.d_it; }
      73                 :   96827773 :     bool operator!=(const const_iterator& i) const { return d_it != i.d_it; }
      74                 :            : 
      75                 :            :     // Dereference operators.
      76                 :     243816 :     V operator*() const { return (*d_it).first; }
      77                 :            : 
      78                 :            :     // Prefix increment
      79                 :     223390 :     const_iterator& operator++()
      80                 :            :     {
      81                 :     223390 :       ++d_it;
      82                 :     223390 :       return *this;
      83                 :            :     }
      84                 :            : 
      85                 :            :     // Postfix increment: requires a Proxy object to hold the
      86                 :            :     // intermediate value for dereferencing
      87                 :            :     class Proxy
      88                 :            :     {
      89                 :            :       const V& d_val;
      90                 :            : 
      91                 :            :      public:
      92                 :            :       Proxy(const V& v) : d_val(v) {}
      93                 :            : 
      94                 :            :       V operator*() const { return d_val; }
      95                 :            :       V* operator->() const { return &d_val; }
      96                 :            :     }; /* class CDSet<>::iterator::Proxy */
      97                 :            : 
      98                 :            :     // Actual postfix increment: returns Proxy with the old value.
      99                 :            :     // Now, an expression like *i++ will return the current *i, and
     100                 :            :     // then advance the orderedIterator.  However, don't try to use
     101                 :            :     // Proxy for anything else.
     102                 :            :     const Proxy operator++(int)
     103                 :            :     {
     104                 :            :       Proxy e(*(*this));
     105                 :            :       ++(*this);
     106                 :            :       return e;
     107                 :            :     }
     108                 :            :   }; /* class CDSet<>::iterator */
     109                 :            : 
     110                 :     311785 :   const_iterator begin() const { return const_iterator(super::begin()); }
     111                 :            : 
     112                 :  181461341 :   const_iterator end() const { return const_iterator(super::end()); }
     113                 :            : 
     114                 :  181149364 :   const_iterator find(const V& v) const
     115                 :            :   {
     116                 :  181149364 :     return const_iterator(super::find(v));
     117                 :            :   }
     118                 :            : 
     119                 :            :   typedef typename super::key_iterator key_iterator;
     120                 :        631 :   key_iterator key_begin() const { return super::key_begin(); }
     121                 :        631 :   key_iterator key_end() const { return super::key_end(); }
     122                 :            : 
     123                 :            : }; /* class CDHashSet */
     124                 :            : 
     125                 :            : }  // namespace cvc5::context
     126                 :            : 
     127                 :            : #endif /* CVC5__CONTEXT__CDHASHSET_H */