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
|
#include <cxxtest/TestSuite.h>
#include <vector>
#include <iostream>
#include <limits.h>
#include "memory.h"
#include "context/context.h"
#include "context/cdvector.h"
using namespace std;
using namespace CVC4::context;
using namespace CVC4::test;
struct DtorSensitiveObject {
bool& d_dtorCalled;
DtorSensitiveObject(bool& dtorCalled) : d_dtorCalled(dtorCalled) {}
~DtorSensitiveObject() { d_dtorCalled = true; }
};
class CDListBlack : public CxxTest::TestSuite {
private:
Context* d_context;
public:
void setUp() {
d_context = new Context();
}
void tearDown() {
delete d_context;
}
void testCDVector17() { vectorTest(17); }
void testCDVector31() { vectorTest(31); }
void testCDVector191() { vectorTest(113); }
void vectorTest(unsigned P){
vectorTest(P, 2);
vectorTest(P, 5);
vectorTest(P, P/3 + 1);
}
void vectorTest(unsigned P, unsigned m){
for(unsigned g=2; g< P; g++){
vectorTest(P, g, m, 1, false);
vectorTest(P, g, m, 3, false);
}
}
vector<unsigned> copy(CDVector<unsigned>& v){
vector<unsigned> ret;
for(unsigned i=0; i < v.size(); ++i){
ret.push_back(v[i]);
}
return ret;
}
void equal(vector<unsigned>& copy, CDVector<unsigned>& v){
TS_ASSERT_EQUALS(copy.size(), v.size());
for(unsigned i = 0; i < v.size(); ++i){
TS_ASSERT_EQUALS(copy[i], v[i]);
}
}
void vectorTest(unsigned P, unsigned g, unsigned m, unsigned r, bool callDestructor) {
CDVector<unsigned> vec(d_context, callDestructor);
vector< vector<unsigned> > copies;
copies.push_back( copy(vec) );
d_context->push();
TS_ASSERT(vec.empty());
for(unsigned i = 0; i < P; ++i){
vec.push_back(i);
TS_ASSERT_EQUALS(vec.size(), i+1);
}
TS_ASSERT(!vec.empty());
TS_ASSERT_EQUALS(vec.size(), P);
copies.push_back( copy(vec) );
d_context->push();
for(unsigned i = 0, g_i = 1; i < r*P; ++i, g_i = (g_i * g)% P){
if(i % m == 0){
copies.push_back( copy(vec) );
d_context->push();
}
vec.set(g_i, i);
TS_ASSERT_EQUALS(vec.get(g_i), i);
}
TS_ASSERT_EQUALS(vec.size(), P);
copies.push_back( copy(vec) );
while(d_context->getLevel() >= 1){
TS_ASSERT_EQUALS(vec.size(), P);
equal(copies[d_context->getLevel()], vec);
d_context->pop();
}
}
void testTreeUpdate() {
CDVector<int> vec(d_context);
vec.push_back(-1);
vec.set(0, 0);
d_context->push();
d_context->push();
vec.set(0, 1);
d_context->pop();
d_context->pop();
d_context->push();
d_context->push();
TS_ASSERT_EQUALS(vec.get(0), 0);
}
};
|
