GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_sets_type_rules_white.cpp Lines: 32 32 100.0 %
Date: 2021-03-22 Branches: 104 315 33.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sets_type_rules_white.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz, Mudathir Mohamed
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 sets typing rules
13
 **/
14
15
#include "expr/dtype.h"
16
#include "test_api.h"
17
#include "test_node.h"
18
19
namespace CVC4 {
20
21
using namespace CVC4::api;
22
23
namespace test {
24
25
4
class TestTheoryWhiteSetsTypeRuleApi : public TestApi
26
{
27
};
28
8
class TestTheoryWhiteSetsTypeRuleInternal : public TestNode
29
{
30
};
31
32
12
TEST_F(TestTheoryWhiteSetsTypeRuleInternal, is_comparable_to)
33
{
34
4
  TypeNode setRealType = d_nodeManager->mkSetType(d_nodeManager->realType());
35
4
  TypeNode setIntType = d_nodeManager->mkSetType(d_nodeManager->integerType());
36
2
  ASSERT_FALSE(setIntType.isComparableTo(setRealType));
37
2
  ASSERT_FALSE(setIntType.isSubtypeOf(setRealType));
38
2
  ASSERT_FALSE(setRealType.isComparableTo(setIntType));
39
2
  ASSERT_FALSE(setRealType.isComparableTo(setIntType));
40
}
41
42
12
TEST_F(TestTheoryWhiteSetsTypeRuleApi, singleton_term)
43
{
44
4
  Sort realSort = d_solver.getRealSort();
45
4
  Sort intSort = d_solver.getIntegerSort();
46
4
  Term emptyReal = d_solver.mkEmptySet(d_solver.mkSetSort(realSort));
47
4
  Term integerOne = d_solver.mkInteger(1);
48
4
  Term realOne = d_solver.mkReal(1);
49
4
  Term singletonInt = d_solver.mkTerm(api::SINGLETON, integerOne);
50
4
  Term singletonReal = d_solver.mkTerm(api::SINGLETON, realOne);
51
  // (union
52
  //    (singleton (singleton_op Int) 1)
53
  //    (as emptyset (Set Real)))
54
4
  ASSERT_THROW(d_solver.mkTerm(UNION, singletonInt, emptyReal),
55
2
               CVC4ApiException);
56
  // (union
57
  //    (singleton (singleton_op Real) 1)
58
  //    (as emptyset (Set Real)))
59
2
  ASSERT_NO_THROW(d_solver.mkTerm(UNION, singletonReal, emptyReal));
60
}
61
62
12
TEST_F(TestTheoryWhiteSetsTypeRuleInternal, singleton_node)
63
{
64
  Node singletonInt =
65
4
      d_nodeManager->mkConst(SingletonOp(d_nodeManager->integerType()));
66
  Node singletonReal =
67
4
      d_nodeManager->mkConst(SingletonOp(d_nodeManager->realType()));
68
4
  Node intConstant = d_nodeManager->mkConst(Rational(1));
69
4
  Node realConstant = d_nodeManager->mkConst(Rational(1, 5));
70
  // (singleton (singleton_op Real) 1)
71
2
  ASSERT_NO_THROW(
72
      d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant));
73
  // (singleton (singleton_op Int) (/ 1 5))
74
2
  ASSERT_DEATH(
75
      d_nodeManager->mkSingleton(d_nodeManager->integerType(), realConstant),
76
      "Invalid operands for mkSingleton");
77
78
4
  Node n = d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant);
79
  // the type of (singleton (singleton_op Real) 1) is (Set Real)
80
2
  ASSERT_TRUE(n.getType()
81
2
              == d_nodeManager->mkSetType(d_nodeManager->realType()));
82
  // (singleton (singleton_op Real) 1) is a constant in normal form
83
2
  ASSERT_TRUE(n.isConst());
84
}
85
}  // namespace test
86
27424
}  // namespace CVC4