Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/node/attribute_black.cpp	Lines:	47	47	100.0 %
Date:	2021-09-29	Branches:	94	292	32.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Tim King, Andrew Reynolds
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Black box testing of cvc5::Attribute.
 */

#include <sstream>
#include <vector>

#include "expr/attribute.h"
#include "expr/node.h"
#include "expr/node_builder.h"
#include "expr/node_value.h"
#include "test_node.h"

namespace cvc5 {

using namespace kind;
using namespace smt;

namespace test {

class TestNodeBlackAttribute : public TestNode
{
 protected:
  struct PrimitiveIntAttributeId
  {
  };
  using PrimitiveIntAttribute =
      expr::Attribute<PrimitiveIntAttributeId, uint64_t>;
  struct TNodeAttributeId
  {
  };
  using TNodeAttribute = expr::Attribute<TNodeAttributeId, TNode>;
  struct StringAttributeId
  {
  };
  using StringAttribute = expr::Attribute<StringAttributeId, std::string>;
  struct BoolAttributeId
  {
  };
  using BoolAttribute = expr::Attribute<BoolAttributeId, bool>;
};

TEST_F(TestNodeBlackAttribute, ints)
{
  TypeNode booleanType = d_nodeManager->booleanType();
  Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));
  const uint64_t val = 63489;
  uint64_t data0 = 0;
  uint64_t data1 = 0;

  PrimitiveIntAttribute attr;
  ASSERT_FALSE(node->getAttribute(attr, data0));
  node->setAttribute(attr, val);
  ASSERT_TRUE(node->getAttribute(attr, data1));
  ASSERT_EQ(data1, val);

  delete node;
}

TEST_F(TestNodeBlackAttribute, tnodes)
{
  TypeNode booleanType = d_nodeManager->booleanType();
  Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));

  Node val(d_skolemManager->mkDummySkolem("b", booleanType));
  TNode data0;
  TNode data1;

  TNodeAttribute attr;
  ASSERT_FALSE(node->getAttribute(attr, data0));
  node->setAttribute(attr, val);
  ASSERT_TRUE(node->getAttribute(attr, data1));
  ASSERT_EQ(data1, val);

  delete node;
}

TEST_F(TestNodeBlackAttribute, strings)
{
  TypeNode booleanType = d_nodeManager->booleanType();
  Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));

  std::string val("63489");
  std::string data0;
  std::string data1;

  StringAttribute attr;
  ASSERT_FALSE(node->getAttribute(attr, data0));
  node->setAttribute(attr, val);
  ASSERT_TRUE(node->getAttribute(attr, data1));
  ASSERT_EQ(data1, val);

  delete node;
}

TEST_F(TestNodeBlackAttribute, bools)
{
  TypeNode booleanType = d_nodeManager->booleanType();
  Node* node = new Node(d_skolemManager->mkDummySkolem("b", booleanType));

  bool val = true;
  bool data0 = false;
  bool data1 = false;

  BoolAttribute attr;
  ASSERT_TRUE(node->getAttribute(attr, data0));
  ASSERT_EQ(false, data0);
  node->setAttribute(attr, val);
  ASSERT_TRUE(node->getAttribute(attr, data1));
  ASSERT_EQ(data1, val);

  delete node;
}

}  // namespace test
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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