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