1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
|
/********************* */
/*! \file cdhashset.h
** \verbatim
** Original author: Dejan Jovanović <dejan.jovanovic@gmail.com>
** Major contributors: Tim King <taking@cs.nyu.edu>, Morgan Deters <mdeters@cs.nyu.edu>
** Minor contributors (to current version): François Bobot <francois@bobot.eu>
** This file is part of the CVC4 project.
** Copyright (c) 2009-2013 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Context-dependent set class.
**
** Context-dependent set class.
**/
#include "cvc4_private.h"
#ifndef __CVC4__CONTEXT__CDSET_H
#define __CVC4__CONTEXT__CDSET_H
#include "context/context.h"
#include "context/cdinsert_hashmap.h"
#include "util/cvc4_assert.h"
namespace CVC4 {
namespace context {
template <class V, class HashFcn>
class CDHashSet : protected CDInsertHashMap<V, bool, HashFcn> {
typedef CDInsertHashMap<V, bool, HashFcn> super;
public:
// ensure these are publicly accessible
static void* operator new(size_t size, bool b) {
return ContextObj::operator new(size, b);
}
static void operator delete(void* pMem, bool b) {
return ContextObj::operator delete(pMem, b);
}
void deleteSelf() {
this->ContextObj::deleteSelf();
}
static void operator delete(void* pMem) {
AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!");
}
CDHashSet(Context* context) :
super(context) {
}
size_t size() const {
return super::size();
}
bool insert(const V& v) {
return super::insert_safe(v, true);
}
bool contains(const V& v) {
return super::contains(v);
}
class const_iterator {
typename super::const_iterator d_it;
public:
const_iterator(const typename super::const_iterator& it) : d_it(it) {}
const_iterator(const const_iterator& it) : d_it(it.d_it) {}
// Default constructor
const_iterator() {}
// (Dis)equality
bool operator==(const const_iterator& i) const {
return d_it == i.d_it;
}
bool operator!=(const const_iterator& i) const {
return d_it != i.d_it;
}
// Dereference operators.
V operator*() const {
return (*d_it).first;
}
// Prefix increment
const_iterator& operator++() {
++d_it;
return *this;
}
// Postfix increment: requires a Proxy object to hold the
// intermediate value for dereferencing
class Proxy {
const V& d_val;
public:
Proxy(const V& v) : d_val(v) {}
V operator*() const {
return d_val;
}
};/* class CDSet<>::iterator::Proxy */
// Actual postfix increment: returns Proxy with the old value.
// Now, an expression like *i++ will return the current *i, and
// then advance the orderedIterator. However, don't try to use
// Proxy for anything else.
const Proxy operator++(int) {
Proxy e(*(*this));
++(*this);
return e;
}
};/* class CDSet<>::iterator */
const_iterator begin() const {
return const_iterator(super::begin());
}
const_iterator end() const {
return const_iterator(super::end());
}
const_iterator find(const V& v) const {
return const_iterator(super::find(v));
}
typedef typename super::key_iterator key_iterator;
key_iterator key_begin() const {
return super::key_begin();
}
key_iterator key_end() const {
return super::key_end();
}
void insertAtContextLevelZero(const V& v) {
return super::insertAtContextLevelZero(v, true);
}
};/* class CDSet */
}/* CVC4::context namespace */
}/* CVC4 namespace */
#endif /* __CVC4__CONTEXT__CDSET_H */
|
