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
/*++
Copyright (c) 2006 Microsoft Corporation
Module Name:
nat_set.h
Abstract:
Set of natural number with fast reset method.
Author:
Leonardo de Moura (leonardo) 2007-03-27.
Revision History:
--*/
#pragma once
#include <climits>
#include "util/vector.h"
class nat_set {
unsigned m_curr_timestamp;
svector<unsigned> m_timestamps;
public:
nat_set(unsigned s = 0):
m_curr_timestamp(0),
m_timestamps() {
if (s > 0) {
m_timestamps.resize(s, 0);
}
}
// A nat_set is a function from [0..s-1] -> boolean.
// This method sets the domain of this function.
void set_domain(unsigned s) {
m_timestamps.resize(s, 0);
}
unsigned get_domain() const {
return m_timestamps.size();
}
// Assure that v is in the domain of the set.
void assure_domain(unsigned v) {
if (v >= get_domain()) {
set_domain(v+1);
}
}
bool contains(unsigned v) const {
return m_timestamps[v] > m_curr_timestamp;
}
void insert(unsigned v) {
m_timestamps[v] = m_curr_timestamp + 1;
}
void remove(unsigned v) {
m_timestamps[v] = m_curr_timestamp;
}
void reset() {
m_curr_timestamp++;
if (m_curr_timestamp == UINT_MAX) {
m_timestamps.fill(0);
m_curr_timestamp = 0;
}
}
bool empty() const {
for (auto const& t : m_timestamps)
if (t > m_curr_timestamp)
return false;
return true;
}
};