Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Black box testing of cvc5::context::CDList<>.
11 : : */
12 : :
13 : : #include <limits.h>
14 : :
15 : : #include <iostream>
16 : : #include <vector>
17 : :
18 : : #include "base/exception.h"
19 : : #include "context/cdlist.h"
20 : : #include "test_context.h"
21 : :
22 : : namespace cvc5::internal {
23 : :
24 : : using namespace context;
25 : :
26 : : namespace test {
27 : :
28 : : class TestObject
29 : : {
30 : : public:
31 : : // Test support for elements without default constructor
32 : : TestObject() = delete;
33 : :
34 : 5 : TestObject(bool* cleanupCalled) : d_cleanupCalled(cleanupCalled) {}
35 : :
36 : : bool* d_cleanupCalled;
37 : : };
38 : :
39 : : class TestCleanup
40 : : {
41 : : public:
42 : 2 : TestCleanup() {}
43 : 3 : void operator()(TestObject& o) { (*o.d_cleanupCalled) = true; }
44 : : };
45 : :
46 : : class TestContextBlackCDList : public TestContext
47 : : {
48 : : protected:
49 : 6 : void list_test(int n)
50 : : {
51 : 6 : list_test(n, true);
52 : 6 : list_test(n, false);
53 : 6 : }
54 : :
55 : 12 : void list_test(int32_t n, bool callDestructor)
56 : : {
57 : 12 : CDList<int32_t> list(d_context.get(), callDestructor);
58 : :
59 [ - + ][ + - ]: 12 : ASSERT_TRUE(list.empty());
60 [ + + ]: 470 : for (int32_t i = 0; i < n; ++i)
61 : : {
62 [ - + ][ + - ]: 458 : ASSERT_EQ(list.size(), (uint32_t)i);
63 : 458 : list.push_back(i);
64 [ - + ][ + - ]: 458 : ASSERT_FALSE(list.empty());
65 [ - + ][ + - ]: 458 : ASSERT_EQ(list.back(), i);
66 : 458 : int32_t i2 = 0;
67 [ + + ]: 14938 : for (CDList<int32_t>::const_iterator j = list.begin(); j != list.end();
68 : 14480 : ++j)
69 : : {
70 [ - + ][ + - ]: 14480 : ASSERT_EQ(*j, i2++);
71 : : }
72 : : }
73 [ - + ][ + - ]: 12 : ASSERT_EQ(list.size(), (uint32_t)n);
74 : :
75 [ + + ]: 470 : for (int32_t i = 0; i < n; ++i)
76 : : {
77 [ - + ][ + - ]: 458 : ASSERT_EQ(list[i], i);
78 : : }
79 [ + - ]: 12 : }
80 : : };
81 : :
82 : 4 : TEST_F(TestContextBlackCDList, CDList10) { list_test(10); }
83 : :
84 : 4 : TEST_F(TestContextBlackCDList, CDList15) { list_test(15); }
85 : :
86 : 4 : TEST_F(TestContextBlackCDList, CDList20) { list_test(20); }
87 : :
88 : 4 : TEST_F(TestContextBlackCDList, CDList35) { list_test(35); }
89 : :
90 : 4 : TEST_F(TestContextBlackCDList, CDList50) { list_test(50); }
91 : :
92 : 4 : TEST_F(TestContextBlackCDList, CDList99) { list_test(99); }
93 : :
94 : 4 : TEST_F(TestContextBlackCDList, destructor_called)
95 : : {
96 : 1 : bool shouldRemainFalse = false;
97 : 1 : bool shouldFlipToTrue = false;
98 : 1 : bool alsoFlipToTrue = false;
99 : 1 : bool shouldAlsoRemainFalse = false;
100 : 1 : bool aThirdFalse = false;
101 : :
102 : 1 : CDList<TestObject, TestCleanup> listT(d_context.get(), true, TestCleanup());
103 : 1 : CDList<TestObject, TestCleanup> listF(d_context.get(), false, TestCleanup());
104 : :
105 : 1 : TestObject shouldRemainFalseDSO(&shouldRemainFalse);
106 : 1 : TestObject shouldFlipToTrueDSO(&shouldFlipToTrue);
107 : 1 : TestObject alsoFlipToTrueDSO(&alsoFlipToTrue);
108 : 1 : TestObject shouldAlsoRemainFalseDSO(&shouldAlsoRemainFalse);
109 : 1 : TestObject aThirdFalseDSO(&aThirdFalse);
110 : :
111 : 1 : listT.push_back(shouldAlsoRemainFalseDSO);
112 : 1 : listF.push_back(shouldAlsoRemainFalseDSO);
113 : :
114 : 1 : d_context->push();
115 : :
116 : 1 : listT.push_back(shouldFlipToTrueDSO);
117 : 1 : listT.push_back(alsoFlipToTrueDSO);
118 : :
119 : 1 : listF.push_back(shouldRemainFalseDSO);
120 : 1 : listF.push_back(shouldAlsoRemainFalseDSO);
121 : 1 : listF.push_back(aThirdFalseDSO);
122 : :
123 [ - + ][ + - ]: 1 : ASSERT_EQ(shouldRemainFalse, false);
124 [ - + ][ + - ]: 1 : ASSERT_EQ(shouldFlipToTrue, false);
125 [ - + ][ + - ]: 1 : ASSERT_EQ(alsoFlipToTrue, false);
126 [ - + ][ + - ]: 1 : ASSERT_EQ(shouldAlsoRemainFalse, false);
127 [ - + ][ + - ]: 1 : ASSERT_EQ(aThirdFalse, false);
128 : :
129 : 1 : d_context->pop();
130 : :
131 [ - + ][ + - ]: 1 : ASSERT_EQ(shouldRemainFalse, false);
132 [ - + ][ + - ]: 1 : ASSERT_EQ(shouldFlipToTrue, true);
133 [ - + ][ + - ]: 1 : ASSERT_EQ(alsoFlipToTrue, true);
134 [ - + ][ + - ]: 1 : ASSERT_EQ(shouldAlsoRemainFalse, false);
135 [ - + ][ + - ]: 1 : ASSERT_EQ(aThirdFalse, false);
136 [ + - ][ + - ]: 1 : }
137 : :
138 : 4 : TEST_F(TestContextBlackCDList, empty_iterator)
139 : : {
140 : 1 : CDList<int>* list = new (true) CDList<int>(d_context.get());
141 [ - + ][ + - ]: 1 : ASSERT_EQ(list->begin(), list->end());
142 : 1 : list->deleteSelf();
143 : : }
144 : :
145 : 4 : TEST_F(TestContextBlackCDList, pop_below_level_created)
146 : : {
147 : 1 : d_context->push();
148 : 1 : CDList<int32_t> list(d_context.get());
149 : 1 : d_context->popto(0);
150 : 1 : list.push_back(42);
151 : 1 : }
152 : :
153 : 4 : TEST_F(TestContextBlackCDList, emplace_back)
154 : : {
155 : 1 : int32_t n = 10;
156 : 1 : int32_t start = 42;
157 : 1 : CDList<std::unique_ptr<int32_t>> list(d_context.get());
158 : :
159 [ + + ]: 11 : for (int32_t i = 0; i < n; i++)
160 : : {
161 : 10 : list.emplace_back(new int32_t(start + i));
162 : : }
163 [ + + ]: 11 : for (int32_t i = 0; i < n; i++)
164 : : {
165 [ - + ][ + - ]: 10 : ASSERT_EQ(*list[i], start + i);
166 : : }
167 [ - + ][ + - ]: 1 : ASSERT_EQ(list.size(), n);
168 : :
169 : 1 : d_context->push();
170 [ + + ]: 11 : for (int32_t i = 0; i < n; i++)
171 : : {
172 : 10 : list.emplace_back(new int32_t(start + n + i));
173 : : }
174 [ + + ]: 21 : for (int32_t i = 0; i < n * 2; i++)
175 : : {
176 [ - + ][ + - ]: 20 : ASSERT_EQ(*list[i], start + i);
177 : : }
178 [ - + ][ + - ]: 1 : ASSERT_EQ(list.size(), n * 2);
179 : 1 : d_context->pop();
180 : :
181 [ + + ]: 11 : for (int32_t i = 0; i < n; i++)
182 : : {
183 [ - + ][ + - ]: 10 : ASSERT_EQ(*list[i], start + i);
184 : : }
185 [ - + ][ + - ]: 1 : ASSERT_EQ(list.size(), n);
186 [ + - ]: 1 : }
187 : :
188 : : } // namespace test
189 : : } // namespace cvc5::internal
|
