GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/attribute_black.cpp Lines: 47 47 100.0 %
Date: 2021-03-22 Branches: 95 294 32.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file attribute_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Tim King, 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 Black box testing of CVC4::Attribute.
13
 **
14
 ** Black box testing of CVC4::Attribute.
15
 **/
16
17
#include <sstream>
18
#include <vector>
19
20
#include "expr/attribute.h"
21
#include "expr/node.h"
22
#include "expr/node_builder.h"
23
#include "expr/node_value.h"
24
#include "test_node.h"
25
26
namespace CVC4 {
27
28
using namespace kind;
29
using namespace smt;
30
31
namespace test {
32
33
16
class TestNodeBlackAttribute : public TestNode
34
{
35
 protected:
36
  struct PrimitiveIntAttributeId
37
  {
38
  };
39
  using PrimitiveIntAttribute =
40
      expr::Attribute<PrimitiveIntAttributeId, uint64_t>;
41
  struct TNodeAttributeId
42
  {
43
  };
44
  using TNodeAttribute = expr::Attribute<TNodeAttributeId, TNode>;
45
  struct StringAttributeId
46
  {
47
  };
48
  using StringAttribute = expr::Attribute<StringAttributeId, std::string>;
49
  struct BoolAttributeId
50
  {
51
  };
52
  using BoolAttribute = expr::Attribute<BoolAttributeId, bool>;
53
};
54
55
13
TEST_F(TestNodeBlackAttribute, ints)
56
{
57
4
  TypeNode booleanType = d_nodeManager->booleanType();
58
2
  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
59
2
  const uint64_t val = 63489;
60
2
  uint64_t data0 = 0;
61
2
  uint64_t data1 = 0;
62
63
  PrimitiveIntAttribute attr;
64
2
  ASSERT_FALSE(node->getAttribute(attr, data0));
65
2
  node->setAttribute(attr, val);
66
2
  ASSERT_TRUE(node->getAttribute(attr, data1));
67
2
  ASSERT_EQ(data1, val);
68
69
2
  delete node;
70
}
71
72
13
TEST_F(TestNodeBlackAttribute, tnodes)
73
{
74
4
  TypeNode booleanType = d_nodeManager->booleanType();
75
2
  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
76
77
4
  Node val(d_nodeManager->mkSkolem("b", booleanType));
78
4
  TNode data0;
79
4
  TNode data1;
80
81
  TNodeAttribute attr;
82
2
  ASSERT_FALSE(node->getAttribute(attr, data0));
83
2
  node->setAttribute(attr, val);
84
2
  ASSERT_TRUE(node->getAttribute(attr, data1));
85
2
  ASSERT_EQ(data1, val);
86
87
2
  delete node;
88
}
89
90
13
TEST_F(TestNodeBlackAttribute, strings)
91
{
92
4
  TypeNode booleanType = d_nodeManager->booleanType();
93
2
  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
94
95
4
  std::string val("63489");
96
4
  std::string data0;
97
4
  std::string data1;
98
99
  StringAttribute attr;
100
2
  ASSERT_FALSE(node->getAttribute(attr, data0));
101
2
  node->setAttribute(attr, val);
102
2
  ASSERT_TRUE(node->getAttribute(attr, data1));
103
2
  ASSERT_EQ(data1, val);
104
105
2
  delete node;
106
}
107
108
13
TEST_F(TestNodeBlackAttribute, bools)
109
{
110
4
  TypeNode booleanType = d_nodeManager->booleanType();
111
2
  Node* node = new Node(d_nodeManager->mkSkolem("b", booleanType));
112
113
2
  bool val = true;
114
2
  bool data0 = false;
115
2
  bool data1 = false;
116
117
  BoolAttribute attr;
118
2
  ASSERT_TRUE(node->getAttribute(attr, data0));
119
2
  ASSERT_EQ(false, data0);
120
2
  node->setAttribute(attr, val);
121
2
  ASSERT_TRUE(node->getAttribute(attr, data1));
122
2
  ASSERT_EQ(data1, val);
123
124
2
  delete node;
125
}
126
127
}  // namespace test
128
33553
}  // namespace CVC4