1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Morgan Deters |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* White box testing of Node attributes. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include <string> |
17 |
|
|
18 |
|
#include "base/check.h" |
19 |
|
#include "expr/attribute.h" |
20 |
|
#include "expr/node.h" |
21 |
|
#include "expr/node_builder.h" |
22 |
|
#include "expr/node_manager.h" |
23 |
|
#include "expr/node_manager_attributes.h" |
24 |
|
#include "expr/node_value.h" |
25 |
|
#include "smt/smt_engine.h" |
26 |
|
#include "smt/smt_engine_scope.h" |
27 |
|
#include "test_node.h" |
28 |
|
#include "theory/theory.h" |
29 |
|
#include "theory/theory_engine.h" |
30 |
|
#include "theory/uf/theory_uf.h" |
31 |
|
|
32 |
|
namespace cvc5 { |
33 |
|
|
34 |
|
using namespace kind; |
35 |
|
using namespace smt; |
36 |
|
using namespace expr; |
37 |
|
using namespace expr::attr; |
38 |
|
|
39 |
|
namespace test { |
40 |
|
|
41 |
|
struct Test1; |
42 |
|
struct Test2; |
43 |
|
struct Test3; |
44 |
|
struct Test4; |
45 |
|
struct Test5; |
46 |
|
|
47 |
|
typedef Attribute<Test1, std::string> TestStringAttr1; |
48 |
|
typedef Attribute<Test2, std::string> TestStringAttr2; |
49 |
|
|
50 |
|
using TestFlag1 = Attribute<Test1, bool>; |
51 |
|
using TestFlag2 = Attribute<Test2, bool>; |
52 |
|
using TestFlag3 = Attribute<Test3, bool>; |
53 |
|
using TestFlag4 = Attribute<Test4, bool>; |
54 |
|
using TestFlag5 = Attribute<Test5, bool>; |
55 |
|
|
56 |
8 |
class TestNodeWhiteAttribute : public TestNode |
57 |
|
{ |
58 |
|
protected: |
59 |
4 |
void SetUp() override |
60 |
|
{ |
61 |
4 |
TestNode::SetUp(); |
62 |
4 |
d_booleanType.reset(new TypeNode(d_nodeManager->booleanType())); |
63 |
4 |
} |
64 |
|
std::unique_ptr<TypeNode> d_booleanType; |
65 |
|
}; |
66 |
|
|
67 |
11 |
TEST_F(TestNodeWhiteAttribute, attribute_ids) |
68 |
|
{ |
69 |
|
// Test that IDs for (a subset of) attributes in the system are |
70 |
|
// unique and that the LastAttributeId (which would be the next ID |
71 |
|
// to assign) is greater than all attribute IDs. |
72 |
|
|
73 |
|
// We used to check ID assignments explicitly. However, between |
74 |
|
// compilation modules, you don't get a strong guarantee |
75 |
|
// (initialization order is somewhat implementation-specific, and |
76 |
|
// anyway you'd have to change the tests anytime you add an |
77 |
|
// attribute). So we back off, and just test that they're unique |
78 |
|
// and that the next ID to be assigned is strictly greater than |
79 |
|
// those that have already been assigned. |
80 |
|
|
81 |
2 |
unsigned lastId = attr::LastAttributeId<std::string>::getId(); |
82 |
2 |
ASSERT_LT(VarNameAttr::s_id, lastId); |
83 |
2 |
ASSERT_LT(TestStringAttr1::s_id, lastId); |
84 |
2 |
ASSERT_LT(TestStringAttr2::s_id, lastId); |
85 |
|
|
86 |
2 |
ASSERT_NE(VarNameAttr::s_id, TestStringAttr1::s_id); |
87 |
2 |
ASSERT_NE(VarNameAttr::s_id, TestStringAttr2::s_id); |
88 |
2 |
ASSERT_NE(TestStringAttr1::s_id, TestStringAttr2::s_id); |
89 |
|
|
90 |
2 |
lastId = attr::LastAttributeId<bool>::getId(); |
91 |
2 |
ASSERT_LT(TestFlag1::s_id, lastId); |
92 |
2 |
ASSERT_LT(TestFlag2::s_id, lastId); |
93 |
2 |
ASSERT_LT(TestFlag3::s_id, lastId); |
94 |
2 |
ASSERT_LT(TestFlag4::s_id, lastId); |
95 |
2 |
ASSERT_LT(TestFlag5::s_id, lastId); |
96 |
2 |
ASSERT_NE(TestFlag1::s_id, TestFlag2::s_id); |
97 |
2 |
ASSERT_NE(TestFlag1::s_id, TestFlag3::s_id); |
98 |
2 |
ASSERT_NE(TestFlag1::s_id, TestFlag4::s_id); |
99 |
2 |
ASSERT_NE(TestFlag1::s_id, TestFlag5::s_id); |
100 |
2 |
ASSERT_NE(TestFlag2::s_id, TestFlag3::s_id); |
101 |
2 |
ASSERT_NE(TestFlag2::s_id, TestFlag4::s_id); |
102 |
2 |
ASSERT_NE(TestFlag2::s_id, TestFlag5::s_id); |
103 |
2 |
ASSERT_NE(TestFlag3::s_id, TestFlag4::s_id); |
104 |
2 |
ASSERT_NE(TestFlag3::s_id, TestFlag5::s_id); |
105 |
2 |
ASSERT_NE(TestFlag4::s_id, TestFlag5::s_id); |
106 |
|
|
107 |
2 |
lastId = attr::LastAttributeId<TypeNode>::getId(); |
108 |
2 |
ASSERT_LT(TypeAttr::s_id, lastId); |
109 |
|
} |
110 |
|
|
111 |
11 |
TEST_F(TestNodeWhiteAttribute, attributes) |
112 |
|
{ |
113 |
4 |
Node a = d_nodeManager->mkVar(*d_booleanType); |
114 |
4 |
Node b = d_nodeManager->mkVar(*d_booleanType); |
115 |
4 |
Node c = d_nodeManager->mkVar(*d_booleanType); |
116 |
4 |
Node unnamed = d_nodeManager->mkVar(*d_booleanType); |
117 |
|
|
118 |
2 |
a.setAttribute(VarNameAttr(), "a"); |
119 |
2 |
b.setAttribute(VarNameAttr(), "b"); |
120 |
2 |
c.setAttribute(VarNameAttr(), "c"); |
121 |
|
|
122 |
|
// test that all boolean flags are FALSE to start |
123 |
2 |
Debug("boolattr") << "get flag 1 on a (should be F)\n"; |
124 |
2 |
ASSERT_FALSE(a.getAttribute(TestFlag1())); |
125 |
2 |
Debug("boolattr") << "get flag 1 on b (should be F)\n"; |
126 |
2 |
ASSERT_FALSE(b.getAttribute(TestFlag1())); |
127 |
2 |
Debug("boolattr") << "get flag 1 on c (should be F)\n"; |
128 |
2 |
ASSERT_FALSE(c.getAttribute(TestFlag1())); |
129 |
2 |
Debug("boolattr") << "get flag 1 on unnamed (should be F)\n"; |
130 |
2 |
ASSERT_FALSE(unnamed.getAttribute(TestFlag1())); |
131 |
|
|
132 |
2 |
Debug("boolattr") << "get flag 2 on a (should be F)\n"; |
133 |
2 |
ASSERT_FALSE(a.getAttribute(TestFlag2())); |
134 |
2 |
Debug("boolattr") << "get flag 2 on b (should be F)\n"; |
135 |
2 |
ASSERT_FALSE(b.getAttribute(TestFlag2())); |
136 |
2 |
Debug("boolattr") << "get flag 2 on c (should be F)\n"; |
137 |
2 |
ASSERT_FALSE(c.getAttribute(TestFlag2())); |
138 |
2 |
Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; |
139 |
2 |
ASSERT_FALSE(unnamed.getAttribute(TestFlag2())); |
140 |
|
|
141 |
2 |
Debug("boolattr") << "get flag 3 on a (should be F)\n"; |
142 |
2 |
ASSERT_FALSE(a.getAttribute(TestFlag3())); |
143 |
2 |
Debug("boolattr") << "get flag 3 on b (should be F)\n"; |
144 |
2 |
ASSERT_FALSE(b.getAttribute(TestFlag3())); |
145 |
2 |
Debug("boolattr") << "get flag 3 on c (should be F)\n"; |
146 |
2 |
ASSERT_FALSE(c.getAttribute(TestFlag3())); |
147 |
2 |
Debug("boolattr") << "get flag 3 on unnamed (should be F)\n"; |
148 |
2 |
ASSERT_FALSE(unnamed.getAttribute(TestFlag3())); |
149 |
|
|
150 |
2 |
Debug("boolattr") << "get flag 4 on a (should be F)\n"; |
151 |
2 |
ASSERT_FALSE(a.getAttribute(TestFlag4())); |
152 |
2 |
Debug("boolattr") << "get flag 4 on b (should be F)\n"; |
153 |
2 |
ASSERT_FALSE(b.getAttribute(TestFlag4())); |
154 |
2 |
Debug("boolattr") << "get flag 4 on c (should be F)\n"; |
155 |
2 |
ASSERT_FALSE(c.getAttribute(TestFlag4())); |
156 |
2 |
Debug("boolattr") << "get flag 4 on unnamed (should be F)\n"; |
157 |
2 |
ASSERT_FALSE(unnamed.getAttribute(TestFlag4())); |
158 |
|
|
159 |
2 |
Debug("boolattr") << "get flag 5 on a (should be F)\n"; |
160 |
2 |
ASSERT_FALSE(a.getAttribute(TestFlag5())); |
161 |
2 |
Debug("boolattr") << "get flag 5 on b (should be F)\n"; |
162 |
2 |
ASSERT_FALSE(b.getAttribute(TestFlag5())); |
163 |
2 |
Debug("boolattr") << "get flag 5 on c (should be F)\n"; |
164 |
2 |
ASSERT_FALSE(c.getAttribute(TestFlag5())); |
165 |
2 |
Debug("boolattr") << "get flag 5 on unnamed (should be F)\n"; |
166 |
2 |
ASSERT_FALSE(unnamed.getAttribute(TestFlag5())); |
167 |
|
|
168 |
|
// test that they all HAVE the boolean attributes |
169 |
2 |
ASSERT_TRUE(a.hasAttribute(TestFlag1())); |
170 |
2 |
ASSERT_TRUE(b.hasAttribute(TestFlag1())); |
171 |
2 |
ASSERT_TRUE(c.hasAttribute(TestFlag1())); |
172 |
2 |
ASSERT_TRUE(unnamed.hasAttribute(TestFlag1())); |
173 |
|
|
174 |
2 |
ASSERT_TRUE(a.hasAttribute(TestFlag2())); |
175 |
2 |
ASSERT_TRUE(b.hasAttribute(TestFlag2())); |
176 |
2 |
ASSERT_TRUE(c.hasAttribute(TestFlag2())); |
177 |
2 |
ASSERT_TRUE(unnamed.hasAttribute(TestFlag2())); |
178 |
|
|
179 |
2 |
ASSERT_TRUE(a.hasAttribute(TestFlag3())); |
180 |
2 |
ASSERT_TRUE(b.hasAttribute(TestFlag3())); |
181 |
2 |
ASSERT_TRUE(c.hasAttribute(TestFlag3())); |
182 |
2 |
ASSERT_TRUE(unnamed.hasAttribute(TestFlag3())); |
183 |
|
|
184 |
2 |
ASSERT_TRUE(a.hasAttribute(TestFlag4())); |
185 |
2 |
ASSERT_TRUE(b.hasAttribute(TestFlag4())); |
186 |
2 |
ASSERT_TRUE(c.hasAttribute(TestFlag4())); |
187 |
2 |
ASSERT_TRUE(unnamed.hasAttribute(TestFlag4())); |
188 |
|
|
189 |
2 |
ASSERT_TRUE(a.hasAttribute(TestFlag5())); |
190 |
2 |
ASSERT_TRUE(b.hasAttribute(TestFlag5())); |
191 |
2 |
ASSERT_TRUE(c.hasAttribute(TestFlag5())); |
192 |
2 |
ASSERT_TRUE(unnamed.hasAttribute(TestFlag5())); |
193 |
|
|
194 |
|
// test two-arg version of hasAttribute() |
195 |
2 |
bool bb = false; |
196 |
2 |
Debug("boolattr") << "get flag 1 on a (should be F)\n"; |
197 |
2 |
ASSERT_TRUE(a.getAttribute(TestFlag1(), bb)); |
198 |
2 |
ASSERT_FALSE(bb); |
199 |
2 |
Debug("boolattr") << "get flag 1 on b (should be F)\n"; |
200 |
2 |
ASSERT_TRUE(b.getAttribute(TestFlag1(), bb)); |
201 |
2 |
ASSERT_FALSE(bb); |
202 |
2 |
Debug("boolattr") << "get flag 1 on c (should be F)\n"; |
203 |
2 |
ASSERT_TRUE(c.getAttribute(TestFlag1(), bb)); |
204 |
2 |
ASSERT_FALSE(bb); |
205 |
2 |
Debug("boolattr") << "get flag 1 on unnamed (should be F)\n"; |
206 |
2 |
ASSERT_TRUE(unnamed.getAttribute(TestFlag1(), bb)); |
207 |
2 |
ASSERT_FALSE(bb); |
208 |
|
|
209 |
2 |
Debug("boolattr") << "get flag 2 on a (should be F)\n"; |
210 |
2 |
ASSERT_TRUE(a.getAttribute(TestFlag2(), bb)); |
211 |
2 |
ASSERT_FALSE(bb); |
212 |
2 |
Debug("boolattr") << "get flag 2 on b (should be F)\n"; |
213 |
2 |
ASSERT_TRUE(b.getAttribute(TestFlag2(), bb)); |
214 |
2 |
ASSERT_FALSE(bb); |
215 |
2 |
Debug("boolattr") << "get flag 2 on c (should be F)\n"; |
216 |
2 |
ASSERT_TRUE(c.getAttribute(TestFlag2(), bb)); |
217 |
2 |
ASSERT_FALSE(bb); |
218 |
2 |
Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; |
219 |
2 |
ASSERT_TRUE(unnamed.getAttribute(TestFlag2(), bb)); |
220 |
2 |
ASSERT_FALSE(bb); |
221 |
|
|
222 |
2 |
Debug("boolattr") << "get flag 3 on a (should be F)\n"; |
223 |
2 |
ASSERT_TRUE(a.getAttribute(TestFlag3(), bb)); |
224 |
2 |
ASSERT_FALSE(bb); |
225 |
2 |
Debug("boolattr") << "get flag 3 on b (should be F)\n"; |
226 |
2 |
ASSERT_TRUE(b.getAttribute(TestFlag3(), bb)); |
227 |
2 |
ASSERT_FALSE(bb); |
228 |
2 |
Debug("boolattr") << "get flag 3 on c (should be F)\n"; |
229 |
2 |
ASSERT_TRUE(c.getAttribute(TestFlag3(), bb)); |
230 |
2 |
ASSERT_FALSE(bb); |
231 |
2 |
Debug("boolattr") << "get flag 3 on unnamed (should be F)\n"; |
232 |
2 |
ASSERT_TRUE(unnamed.getAttribute(TestFlag3(), bb)); |
233 |
2 |
ASSERT_FALSE(bb); |
234 |
|
|
235 |
2 |
Debug("boolattr") << "get flag 4 on a (should be F)\n"; |
236 |
2 |
ASSERT_TRUE(a.getAttribute(TestFlag4(), bb)); |
237 |
2 |
ASSERT_FALSE(bb); |
238 |
2 |
Debug("boolattr") << "get flag 4 on b (should be F)\n"; |
239 |
2 |
ASSERT_TRUE(b.getAttribute(TestFlag4(), bb)); |
240 |
2 |
ASSERT_FALSE(bb); |
241 |
2 |
Debug("boolattr") << "get flag 4 on c (should be F)\n"; |
242 |
2 |
ASSERT_TRUE(c.getAttribute(TestFlag4(), bb)); |
243 |
2 |
ASSERT_FALSE(bb); |
244 |
2 |
Debug("boolattr") << "get flag 4 on unnamed (should be F)\n"; |
245 |
2 |
ASSERT_TRUE(unnamed.getAttribute(TestFlag4(), bb)); |
246 |
2 |
ASSERT_FALSE(bb); |
247 |
|
|
248 |
2 |
Debug("boolattr") << "get flag 5 on a (should be F)\n"; |
249 |
2 |
ASSERT_TRUE(a.getAttribute(TestFlag5(), bb)); |
250 |
2 |
ASSERT_FALSE(bb); |
251 |
2 |
Debug("boolattr") << "get flag 5 on b (should be F)\n"; |
252 |
2 |
ASSERT_TRUE(b.getAttribute(TestFlag5(), bb)); |
253 |
2 |
ASSERT_FALSE(bb); |
254 |
2 |
Debug("boolattr") << "get flag 5 on c (should be F)\n"; |
255 |
2 |
ASSERT_TRUE(c.getAttribute(TestFlag5(), bb)); |
256 |
2 |
ASSERT_FALSE(bb); |
257 |
2 |
Debug("boolattr") << "get flag 5 on unnamed (should be F)\n"; |
258 |
2 |
ASSERT_TRUE(unnamed.getAttribute(TestFlag5(), bb)); |
259 |
2 |
ASSERT_FALSE(bb); |
260 |
|
|
261 |
|
// setting boolean flags |
262 |
2 |
Debug("boolattr") << "set flag 1 on a to T\n"; |
263 |
2 |
a.setAttribute(TestFlag1(), true); |
264 |
2 |
Debug("boolattr") << "set flag 1 on b to F\n"; |
265 |
2 |
b.setAttribute(TestFlag1(), false); |
266 |
2 |
Debug("boolattr") << "set flag 1 on c to F\n"; |
267 |
2 |
c.setAttribute(TestFlag1(), false); |
268 |
2 |
Debug("boolattr") << "set flag 1 on unnamed to T\n"; |
269 |
2 |
unnamed.setAttribute(TestFlag1(), true); |
270 |
|
|
271 |
2 |
Debug("boolattr") << "set flag 2 on a to F\n"; |
272 |
2 |
a.setAttribute(TestFlag2(), false); |
273 |
2 |
Debug("boolattr") << "set flag 2 on b to T\n"; |
274 |
2 |
b.setAttribute(TestFlag2(), true); |
275 |
2 |
Debug("boolattr") << "set flag 2 on c to T\n"; |
276 |
2 |
c.setAttribute(TestFlag2(), true); |
277 |
2 |
Debug("boolattr") << "set flag 2 on unnamed to F\n"; |
278 |
2 |
unnamed.setAttribute(TestFlag2(), false); |
279 |
|
|
280 |
2 |
Debug("boolattr") << "set flag 3 on a to T\n"; |
281 |
2 |
a.setAttribute(TestFlag3(), true); |
282 |
2 |
Debug("boolattr") << "set flag 3 on b to T\n"; |
283 |
2 |
b.setAttribute(TestFlag3(), true); |
284 |
2 |
Debug("boolattr") << "set flag 3 on c to T\n"; |
285 |
2 |
c.setAttribute(TestFlag3(), true); |
286 |
2 |
Debug("boolattr") << "set flag 3 on unnamed to T\n"; |
287 |
2 |
unnamed.setAttribute(TestFlag3(), true); |
288 |
|
|
289 |
2 |
Debug("boolattr") << "set flag 4 on a to T\n"; |
290 |
2 |
a.setAttribute(TestFlag4(), true); |
291 |
2 |
Debug("boolattr") << "set flag 4 on b to T\n"; |
292 |
2 |
b.setAttribute(TestFlag4(), true); |
293 |
2 |
Debug("boolattr") << "set flag 4 on c to T\n"; |
294 |
2 |
c.setAttribute(TestFlag4(), true); |
295 |
2 |
Debug("boolattr") << "set flag 4 on unnamed to T\n"; |
296 |
2 |
unnamed.setAttribute(TestFlag4(), true); |
297 |
|
|
298 |
2 |
Debug("boolattr") << "set flag 5 on a to T\n"; |
299 |
2 |
a.setAttribute(TestFlag5(), true); |
300 |
2 |
Debug("boolattr") << "set flag 5 on b to T\n"; |
301 |
2 |
b.setAttribute(TestFlag5(), true); |
302 |
2 |
Debug("boolattr") << "set flag 5 on c to F\n"; |
303 |
2 |
c.setAttribute(TestFlag5(), false); |
304 |
2 |
Debug("boolattr") << "set flag 5 on unnamed to T\n"; |
305 |
2 |
unnamed.setAttribute(TestFlag5(), true); |
306 |
|
|
307 |
2 |
ASSERT_EQ(a.getAttribute(VarNameAttr()), "a"); |
308 |
2 |
ASSERT_NE(a.getAttribute(VarNameAttr()), "b"); |
309 |
2 |
ASSERT_NE(a.getAttribute(VarNameAttr()), "c"); |
310 |
2 |
ASSERT_NE(a.getAttribute(VarNameAttr()), ""); |
311 |
|
|
312 |
2 |
ASSERT_NE(b.getAttribute(VarNameAttr()), "a"); |
313 |
2 |
ASSERT_EQ(b.getAttribute(VarNameAttr()), "b"); |
314 |
2 |
ASSERT_NE(b.getAttribute(VarNameAttr()), "c"); |
315 |
2 |
ASSERT_NE(b.getAttribute(VarNameAttr()), ""); |
316 |
|
|
317 |
2 |
ASSERT_NE(c.getAttribute(VarNameAttr()), "a"); |
318 |
2 |
ASSERT_NE(c.getAttribute(VarNameAttr()), "b"); |
319 |
2 |
ASSERT_EQ(c.getAttribute(VarNameAttr()), "c"); |
320 |
2 |
ASSERT_NE(c.getAttribute(VarNameAttr()), ""); |
321 |
|
|
322 |
2 |
ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a"); |
323 |
2 |
ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b"); |
324 |
2 |
ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c"); |
325 |
2 |
ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), ""); |
326 |
|
|
327 |
2 |
ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr())); |
328 |
|
|
329 |
2 |
ASSERT_FALSE(a.hasAttribute(TestStringAttr1())); |
330 |
2 |
ASSERT_FALSE(b.hasAttribute(TestStringAttr1())); |
331 |
2 |
ASSERT_FALSE(c.hasAttribute(TestStringAttr1())); |
332 |
2 |
ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr1())); |
333 |
|
|
334 |
2 |
ASSERT_FALSE(a.hasAttribute(TestStringAttr2())); |
335 |
2 |
ASSERT_FALSE(b.hasAttribute(TestStringAttr2())); |
336 |
2 |
ASSERT_FALSE(c.hasAttribute(TestStringAttr2())); |
337 |
2 |
ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr2())); |
338 |
|
|
339 |
2 |
Debug("boolattr") << "get flag 1 on a (should be T)\n"; |
340 |
2 |
ASSERT_TRUE(a.getAttribute(TestFlag1())); |
341 |
2 |
Debug("boolattr") << "get flag 1 on b (should be F)\n"; |
342 |
2 |
ASSERT_FALSE(b.getAttribute(TestFlag1())); |
343 |
2 |
Debug("boolattr") << "get flag 1 on c (should be F)\n"; |
344 |
2 |
ASSERT_FALSE(c.getAttribute(TestFlag1())); |
345 |
2 |
Debug("boolattr") << "get flag 1 on unnamed (should be T)\n"; |
346 |
2 |
ASSERT_TRUE(unnamed.getAttribute(TestFlag1())); |
347 |
|
|
348 |
2 |
Debug("boolattr") << "get flag 2 on a (should be F)\n"; |
349 |
2 |
ASSERT_FALSE(a.getAttribute(TestFlag2())); |
350 |
2 |
Debug("boolattr") << "get flag 2 on b (should be T)\n"; |
351 |
2 |
ASSERT_TRUE(b.getAttribute(TestFlag2())); |
352 |
2 |
Debug("boolattr") << "get flag 2 on c (should be T)\n"; |
353 |
2 |
ASSERT_TRUE(c.getAttribute(TestFlag2())); |
354 |
2 |
Debug("boolattr") << "get flag 2 on unnamed (should be F)\n"; |
355 |
2 |
ASSERT_FALSE(unnamed.getAttribute(TestFlag2())); |
356 |
|
|
357 |
2 |
Debug("boolattr") << "get flag 3 on a (should be T)\n"; |
358 |
2 |
ASSERT_TRUE(a.getAttribute(TestFlag3())); |
359 |
2 |
Debug("boolattr") << "get flag 3 on b (should be T)\n"; |
360 |
2 |
ASSERT_TRUE(b.getAttribute(TestFlag3())); |
361 |
2 |
Debug("boolattr") << "get flag 3 on c (should be T)\n"; |
362 |
2 |
ASSERT_TRUE(c.getAttribute(TestFlag3())); |
363 |
2 |
Debug("boolattr") << "get flag 3 on unnamed (should be T)\n"; |
364 |
2 |
ASSERT_TRUE(unnamed.getAttribute(TestFlag3())); |
365 |
|
|
366 |
2 |
Debug("boolattr") << "get flag 4 on a (should be T)\n"; |
367 |
2 |
ASSERT_TRUE(a.getAttribute(TestFlag4())); |
368 |
2 |
Debug("boolattr") << "get flag 4 on b (should be T)\n"; |
369 |
2 |
ASSERT_TRUE(b.getAttribute(TestFlag4())); |
370 |
2 |
Debug("boolattr") << "get flag 4 on c (should be T)\n"; |
371 |
2 |
ASSERT_TRUE(c.getAttribute(TestFlag4())); |
372 |
2 |
Debug("boolattr") << "get flag 4 on unnamed (should be T)\n"; |
373 |
2 |
ASSERT_TRUE(unnamed.getAttribute(TestFlag4())); |
374 |
|
|
375 |
2 |
Debug("boolattr") << "get flag 5 on a (should be T)\n"; |
376 |
2 |
ASSERT_TRUE(a.getAttribute(TestFlag5())); |
377 |
2 |
Debug("boolattr") << "get flag 5 on b (should be T)\n"; |
378 |
2 |
ASSERT_TRUE(b.getAttribute(TestFlag5())); |
379 |
2 |
Debug("boolattr") << "get flag 5 on c (should be F)\n"; |
380 |
2 |
ASSERT_FALSE(c.getAttribute(TestFlag5())); |
381 |
2 |
Debug("boolattr") << "get flag 5 on unnamed (should be T)\n"; |
382 |
2 |
ASSERT_TRUE(unnamed.getAttribute(TestFlag5())); |
383 |
|
|
384 |
2 |
a.setAttribute(TestStringAttr1(), "foo"); |
385 |
2 |
b.setAttribute(TestStringAttr1(), "bar"); |
386 |
2 |
c.setAttribute(TestStringAttr1(), "baz"); |
387 |
|
|
388 |
2 |
ASSERT_EQ(a.getAttribute(VarNameAttr()), "a"); |
389 |
2 |
ASSERT_NE(a.getAttribute(VarNameAttr()), "b"); |
390 |
2 |
ASSERT_NE(a.getAttribute(VarNameAttr()), "c"); |
391 |
2 |
ASSERT_NE(a.getAttribute(VarNameAttr()), ""); |
392 |
|
|
393 |
2 |
ASSERT_NE(b.getAttribute(VarNameAttr()), "a"); |
394 |
2 |
ASSERT_EQ(b.getAttribute(VarNameAttr()), "b"); |
395 |
2 |
ASSERT_NE(b.getAttribute(VarNameAttr()), "c"); |
396 |
2 |
ASSERT_NE(b.getAttribute(VarNameAttr()), ""); |
397 |
|
|
398 |
2 |
ASSERT_NE(c.getAttribute(VarNameAttr()), "a"); |
399 |
2 |
ASSERT_NE(c.getAttribute(VarNameAttr()), "b"); |
400 |
2 |
ASSERT_EQ(c.getAttribute(VarNameAttr()), "c"); |
401 |
2 |
ASSERT_NE(c.getAttribute(VarNameAttr()), ""); |
402 |
|
|
403 |
2 |
ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a"); |
404 |
2 |
ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b"); |
405 |
2 |
ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c"); |
406 |
2 |
ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), ""); |
407 |
|
|
408 |
2 |
ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr())); |
409 |
|
|
410 |
2 |
ASSERT_TRUE(a.hasAttribute(TestStringAttr1())); |
411 |
2 |
ASSERT_TRUE(b.hasAttribute(TestStringAttr1())); |
412 |
2 |
ASSERT_TRUE(c.hasAttribute(TestStringAttr1())); |
413 |
2 |
ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr1())); |
414 |
|
|
415 |
2 |
ASSERT_FALSE(a.hasAttribute(TestStringAttr2())); |
416 |
2 |
ASSERT_FALSE(b.hasAttribute(TestStringAttr2())); |
417 |
2 |
ASSERT_FALSE(c.hasAttribute(TestStringAttr2())); |
418 |
2 |
ASSERT_FALSE(unnamed.hasAttribute(TestStringAttr2())); |
419 |
|
|
420 |
2 |
a.setAttribute(VarNameAttr(), "b"); |
421 |
2 |
b.setAttribute(VarNameAttr(), "c"); |
422 |
2 |
c.setAttribute(VarNameAttr(), "a"); |
423 |
|
|
424 |
2 |
ASSERT_EQ(c.getAttribute(VarNameAttr()), "a"); |
425 |
2 |
ASSERT_NE(c.getAttribute(VarNameAttr()), "b"); |
426 |
2 |
ASSERT_NE(c.getAttribute(VarNameAttr()), "c"); |
427 |
2 |
ASSERT_NE(c.getAttribute(VarNameAttr()), ""); |
428 |
|
|
429 |
2 |
ASSERT_NE(a.getAttribute(VarNameAttr()), "a"); |
430 |
2 |
ASSERT_EQ(a.getAttribute(VarNameAttr()), "b"); |
431 |
2 |
ASSERT_NE(a.getAttribute(VarNameAttr()), "c"); |
432 |
2 |
ASSERT_NE(a.getAttribute(VarNameAttr()), ""); |
433 |
|
|
434 |
2 |
ASSERT_NE(b.getAttribute(VarNameAttr()), "a"); |
435 |
2 |
ASSERT_NE(b.getAttribute(VarNameAttr()), "b"); |
436 |
2 |
ASSERT_EQ(b.getAttribute(VarNameAttr()), "c"); |
437 |
2 |
ASSERT_NE(b.getAttribute(VarNameAttr()), ""); |
438 |
|
|
439 |
2 |
ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "a"); |
440 |
2 |
ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "b"); |
441 |
2 |
ASSERT_NE(unnamed.getAttribute(VarNameAttr()), "c"); |
442 |
2 |
ASSERT_EQ(unnamed.getAttribute(VarNameAttr()), ""); |
443 |
|
|
444 |
2 |
ASSERT_FALSE(unnamed.hasAttribute(VarNameAttr())); |
445 |
|
} |
446 |
|
} // namespace test |
447 |
17767 |
} // namespace cvc5 |