blob: 7032f76ba2ffa65eb27bc11a78f73fa3d9498ef4 (
plain)
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
|
/********************* */
/*! \file cdset.h
** \verbatim
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** 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/cdmap.h"
#include "util/Assert.h"
namespace CVC4 {
namespace context {
template <class V, class HashFcn>
class CDSet : protected CDMap<V, V, HashFcn> {
typedef CDMap<V, V, HashFcn> super;
public:
CDSet(Context* context) :
super(context) {
}
size_t size() const {
return super::size();
}
size_t count(const V& v) const {
return super::count(v);
}
bool insert(const V& v) {
return super::insert(v, v);
}
bool contains(const V& v) {
return find(v) != end();
}
// FIXME: no erase(), too much hassle to implement efficiently...
class iterator {
typename super::iterator d_it;
public:
iterator(const typename super::iterator& it) : d_it(it) {}
iterator(const iterator& it) : d_it(it.d_it) {}
// Default constructor
iterator() {}
// (Dis)equality
bool operator==(const iterator& i) const {
return d_it == i.d_it;
}
bool operator!=(const iterator& i) const {
return d_it != i.d_it;
}
// Dereference operators.
V operator*() const {
return (*d_it).first;
}
// Prefix increment
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 */
typedef iterator const_iterator;
const_iterator begin() const {
return iterator(super::begin());
}
const_iterator end() const {
return iterator(super::end());
}
const_iterator find(const V& v) const {
return iterator(super::find(v));
}
};/* class CDSet */
}/* CVC4::context namespace */
}/* CVC4 namespace */
#endif /* __CVC4__CONTEXT__CDSET_H */
|
