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