GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/node/type_node_white.cpp Lines: 49 49 100.0 %
Date: 2021-03-23 Branches: 180 600 30.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file type_node_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Andrew Reynolds
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 TypeNode
13
 **
14
 ** White box testing of TypeNode.
15
 **/
16
17
#include <iostream>
18
#include <sstream>
19
#include <string>
20
21
#include "expr/node_manager.h"
22
#include "expr/type_node.h"
23
#include "smt/smt_engine.h"
24
#include "test_node.h"
25
26
namespace CVC4 {
27
28
using namespace kind;
29
using namespace context;
30
31
namespace test {
32
33
4
class TestNodeWhiteTypeNode : public TestNode
34
{
35
 protected:
36
2
  void SetUp() override
37
  {
38
2
    TestNode::SetUp();
39
2
    d_smt.reset(new SmtEngine(d_nodeManager.get()));
40
2
  }
41
  std::unique_ptr<SmtEngine> d_smt;
42
};
43
44
10
TEST_F(TestNodeWhiteTypeNode, sub_types)
45
{
46
4
  TypeNode realType = d_nodeManager->realType();
47
4
  TypeNode integerType = d_nodeManager->realType();
48
4
  TypeNode booleanType = d_nodeManager->booleanType();
49
4
  TypeNode arrayType = d_nodeManager->mkArrayType(realType, integerType);
50
4
  TypeNode bvType = d_nodeManager->mkBitVectorType(32);
51
52
4
  Node x = d_nodeManager->mkBoundVar("x", realType);
53
4
  Node xPos = d_nodeManager->mkNode(GT, x, d_nodeManager->mkConst(Rational(0)));
54
4
  TypeNode funtype = d_nodeManager->mkFunctionType(integerType, booleanType);
55
4
  Node lambda = d_nodeManager->mkVar("lambda", funtype);
56
4
  std::vector<Node> formals;
57
2
  formals.push_back(x);
58
2
  d_smt->defineFunction(lambda, formals, xPos);
59
60
2
  ASSERT_FALSE(realType.isComparableTo(booleanType));
61
2
  ASSERT_TRUE(realType.isComparableTo(integerType));
62
2
  ASSERT_TRUE(realType.isComparableTo(realType));
63
2
  ASSERT_FALSE(realType.isComparableTo(arrayType));
64
2
  ASSERT_FALSE(realType.isComparableTo(bvType));
65
66
2
  ASSERT_FALSE(booleanType.isComparableTo(integerType));
67
2
  ASSERT_FALSE(booleanType.isComparableTo(realType));
68
2
  ASSERT_TRUE(booleanType.isComparableTo(booleanType));
69
2
  ASSERT_FALSE(booleanType.isComparableTo(arrayType));
70
2
  ASSERT_FALSE(booleanType.isComparableTo(bvType));
71
72
2
  ASSERT_TRUE(integerType.isComparableTo(realType));
73
2
  ASSERT_TRUE(integerType.isComparableTo(integerType));
74
2
  ASSERT_FALSE(integerType.isComparableTo(booleanType));
75
2
  ASSERT_FALSE(integerType.isComparableTo(arrayType));
76
2
  ASSERT_FALSE(integerType.isComparableTo(bvType));
77
78
2
  ASSERT_FALSE(arrayType.isComparableTo(booleanType));
79
2
  ASSERT_FALSE(arrayType.isComparableTo(integerType));
80
2
  ASSERT_FALSE(arrayType.isComparableTo(realType));
81
2
  ASSERT_TRUE(arrayType.isComparableTo(arrayType));
82
2
  ASSERT_FALSE(arrayType.isComparableTo(bvType));
83
84
2
  ASSERT_FALSE(bvType.isComparableTo(booleanType));
85
2
  ASSERT_FALSE(bvType.isComparableTo(integerType));
86
2
  ASSERT_FALSE(bvType.isComparableTo(realType));
87
2
  ASSERT_FALSE(bvType.isComparableTo(arrayType));
88
2
  ASSERT_TRUE(bvType.isComparableTo(bvType));
89
90
2
  ASSERT_TRUE(realType.getBaseType() == realType);
91
2
  ASSERT_TRUE(integerType.getBaseType() == realType);
92
2
  ASSERT_TRUE(booleanType.getBaseType() == booleanType);
93
2
  ASSERT_TRUE(arrayType.getBaseType() == arrayType);
94
2
  ASSERT_TRUE(bvType.getBaseType() == bvType);
95
}
96
}  // namespace test
97
14402
}  // namespace CVC4