GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/attribute_white.cpp Lines: 314 314 100.0 %
Date: 2021-03-23 Branches: 1007 3526 28.6 %

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