GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/context/cdhashset.h Lines: 37 42 88.1 %
Date: 2021-03-23 Branches: 4 44 9.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cdhashset.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Morgan Deters, Tim King, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Context-dependent set class.
13
 **
14
 ** Context-dependent set class.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__CONTEXT__CDHASHSET_H
20
#define CVC4__CONTEXT__CDHASHSET_H
21
22
#include "base/check.h"
23
#include "context/cdinsert_hashmap.h"
24
#include "context/context.h"
25
26
namespace CVC4 {
27
namespace context {
28
29
template <class V, class HashFcn>
30
10102423
class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn> {
31
  typedef CDInsertHashMap<V, bool, HashFcn> super;
32
33
  // no copy or assignment
34
  CDHashSet(const CDHashSet&) = delete;
35
  CDHashSet& operator=(const CDHashSet&) = delete;
36
37
public:
38
39
  // ensure these are publicly accessible
40
5789
  static void* operator new(size_t size, bool b) {
41
5789
    return ContextObj::operator new(size, b);
42
  }
43
44
  static void operator delete(void* pMem, bool b) {
45
    return ContextObj::operator delete(pMem, b);
46
  }
47
48
5768
  void deleteSelf() {
49
5768
    this->ContextObj::deleteSelf();
50
5768
  }
51
52
  static void operator delete(void* pMem) {
53
    AlwaysAssert(false) << "It is not allowed to delete a ContextObj this way!";
54
  }
55
56
711920
  CDHashSet(Context* context) :
57
711920
    super(context) {
58
711920
  }
59
60
6790
  size_t size() const {
61
6790
    return super::size();
62
  }
63
64
47
  bool empty() const {
65
47
    return super::empty();
66
  }
67
68
17658162
  bool insert(const V& v) {
69
17658162
    return super::insert_safe(v, true);
70
  }
71
72
697683
  bool contains(const V& v) const {
73
697683
    return super::contains(v);
74
  }
75
76
  class const_iterator {
77
    typename super::const_iterator d_it;
78
79
  public:
80
81
82915432
    const_iterator(const typename super::const_iterator& it) : d_it(it) {}
82
    const_iterator(const const_iterator& it) : d_it(it.d_it) {}
83
84
    // Default constructor
85
    const_iterator() {}
86
87
    // (Dis)equality
88
4912755
    bool operator==(const const_iterator& i) const {
89
4912755
      return d_it == i.d_it;
90
    }
91
36547677
    bool operator!=(const const_iterator& i) const {
92
36547677
      return d_it != i.d_it;
93
    }
94
95
    // Dereference operators.
96
2779
    V operator*() const {
97
2779
      return (*d_it).first;
98
    }
99
100
    // Prefix increment
101
2779
    const_iterator& operator++() {
102
2779
      ++d_it;
103
2779
      return *this;
104
    }
105
106
    // Postfix increment: requires a Proxy object to hold the
107
    // intermediate value for dereferencing
108
    class Proxy {
109
      const V& d_val;
110
111
    public:
112
113
      Proxy(const V& v) : d_val(v) {}
114
115
      V operator*() const {
116
        return d_val;
117
      }
118
      V* operator->() const { return &d_val; }
119
    };/* class CDSet<>::iterator::Proxy */
120
121
    // Actual postfix increment: returns Proxy with the old value.
122
    // Now, an expression like *i++ will return the current *i, and
123
    // then advance the orderedIterator.  However, don't try to use
124
    // Proxy for anything else.
125
    const Proxy operator++(int) {
126
      Proxy e(*(*this));
127
      ++(*this);
128
      return e;
129
    }
130
  };/* class CDSet<>::iterator */
131
132
973
  const_iterator begin() const {
133
973
    return const_iterator(super::begin());
134
  }
135
136
41457779
  const_iterator end() const {
137
41457779
    return const_iterator(super::end());
138
  }
139
140
41456680
  const_iterator find(const V& v) const {
141
41456680
    return const_iterator(super::find(v));
142
  }
143
144
  typedef typename super::key_iterator key_iterator;
145
603
  key_iterator key_begin() const {
146
603
    return super::key_begin();
147
  }
148
603
  key_iterator key_end() const {
149
603
    return super::key_end();
150
  }
151
152
  void insertAtContextLevelZero(const V& v) {
153
    return super::insertAtContextLevelZero(v, true);
154
  }
155
156
};/* class CDHashSet */
157
158
}/* CVC4::context namespace */
159
}/* CVC4 namespace */
160
161
#endif /* CVC4__CONTEXT__CDHASHSET_H */