GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/api/op_black.cpp Lines: 94 94 100.0 %
Date: 2021-03-23 Branches: 196 644 30.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file op_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Makai Mann, Aina Niemetz
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 the Op class.
13
 **/
14
15
#include "test_api.h"
16
17
namespace CVC4 {
18
19
using namespace api;
20
21
namespace test {
22
23
28
class TestApiBlackOp : public TestApi
24
{
25
};
26
27
16
TEST_F(TestApiBlackOp, getKind)
28
{
29
4
  Op x;
30
2
  x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
31
2
  ASSERT_NO_THROW(x.getKind());
32
}
33
34
16
TEST_F(TestApiBlackOp, isNull)
35
{
36
4
  Op x;
37
2
  ASSERT_TRUE(x.isNull());
38
2
  x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
39
2
  ASSERT_FALSE(x.isNull());
40
}
41
42
16
TEST_F(TestApiBlackOp, opFromKind)
43
{
44
2
  ASSERT_NO_THROW(d_solver.mkOp(PLUS));
45
4
  ASSERT_THROW(d_solver.mkOp(BITVECTOR_EXTRACT), CVC4ApiException);
46
}
47
48
16
TEST_F(TestApiBlackOp, getIndicesString)
49
{
50
4
  Op x;
51
4
  ASSERT_THROW(x.getIndices<std::string>(), CVC4ApiException);
52
53
4
  Op divisible_ot = d_solver.mkOp(DIVISIBLE, 4);
54
2
  ASSERT_TRUE(divisible_ot.isIndexed());
55
4
  std::string divisible_idx = divisible_ot.getIndices<std::string>();
56
2
  ASSERT_EQ(divisible_idx, "4");
57
58
4
  Op record_update_ot = d_solver.mkOp(RECORD_UPDATE, "test");
59
4
  std::string record_update_idx = record_update_ot.getIndices<std::string>();
60
2
  ASSERT_EQ(record_update_idx, "test");
61
4
  ASSERT_THROW(record_update_ot.getIndices<uint32_t>(), CVC4ApiException);
62
}
63
64
16
TEST_F(TestApiBlackOp, getIndicesUint)
65
{
66
4
  Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
67
2
  ASSERT_TRUE(bitvector_repeat_ot.isIndexed());
68
2
  uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices<uint32_t>();
69
2
  ASSERT_EQ(bitvector_repeat_idx, 5);
70
4
  ASSERT_THROW(
71
      (bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()),
72
2
      CVC4ApiException);
73
74
4
  Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
75
  uint32_t bitvector_zero_extend_idx =
76
2
      bitvector_zero_extend_ot.getIndices<uint32_t>();
77
2
  ASSERT_EQ(bitvector_zero_extend_idx, 6);
78
79
4
  Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
80
  uint32_t bitvector_sign_extend_idx =
81
2
      bitvector_sign_extend_ot.getIndices<uint32_t>();
82
2
  ASSERT_EQ(bitvector_sign_extend_idx, 7);
83
84
4
  Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
85
  uint32_t bitvector_rotate_left_idx =
86
2
      bitvector_rotate_left_ot.getIndices<uint32_t>();
87
2
  ASSERT_EQ(bitvector_rotate_left_idx, 8);
88
89
4
  Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
90
  uint32_t bitvector_rotate_right_idx =
91
2
      bitvector_rotate_right_ot.getIndices<uint32_t>();
92
2
  ASSERT_EQ(bitvector_rotate_right_idx, 9);
93
94
4
  Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10);
95
2
  uint32_t int_to_bitvector_idx = int_to_bitvector_ot.getIndices<uint32_t>();
96
2
  ASSERT_EQ(int_to_bitvector_idx, 10);
97
98
4
  Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11);
99
  uint32_t floatingpoint_to_ubv_idx =
100
2
      floatingpoint_to_ubv_ot.getIndices<uint32_t>();
101
2
  ASSERT_EQ(floatingpoint_to_ubv_idx, 11);
102
103
4
  Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
104
  uint32_t floatingpoint_to_sbv_idx =
105
2
      floatingpoint_to_sbv_ot.getIndices<uint32_t>();
106
2
  ASSERT_EQ(floatingpoint_to_sbv_idx, 13);
107
108
4
  Op tuple_update_ot = d_solver.mkOp(TUPLE_UPDATE, 5);
109
2
  uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>();
110
2
  ASSERT_EQ(tuple_update_idx, 5);
111
4
  ASSERT_THROW(tuple_update_ot.getIndices<std::string>(), CVC4ApiException);
112
}
113
114
16
TEST_F(TestApiBlackOp, getIndicesPairUint)
115
{
116
4
  Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
117
2
  ASSERT_TRUE(bitvector_extract_ot.isIndexed());
118
  std::pair<uint32_t, uint32_t> bitvector_extract_indices =
119
2
      bitvector_extract_ot.getIndices<std::pair<uint32_t, uint32_t>>();
120
2
  ASSERT_TRUE(
121
2
      (bitvector_extract_indices == std::pair<uint32_t, uint32_t>{4, 0}));
122
123
  Op floatingpoint_to_fp_ieee_bitvector_ot =
124
4
      d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25);
125
  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_ieee_bitvector_indices =
126
      floatingpoint_to_fp_ieee_bitvector_ot
127
2
          .getIndices<std::pair<uint32_t, uint32_t>>();
128
2
  ASSERT_TRUE((floatingpoint_to_fp_ieee_bitvector_indices
129
2
               == std::pair<uint32_t, uint32_t>{4, 25}));
130
131
  Op floatingpoint_to_fp_floatingpoint_ot =
132
4
      d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25);
133
  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_floatingpoint_indices =
134
      floatingpoint_to_fp_floatingpoint_ot
135
2
          .getIndices<std::pair<uint32_t, uint32_t>>();
136
2
  ASSERT_TRUE((floatingpoint_to_fp_floatingpoint_indices
137
2
               == std::pair<uint32_t, uint32_t>{4, 25}));
138
139
  Op floatingpoint_to_fp_real_ot =
140
4
      d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25);
141
  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_real_indices =
142
2
      floatingpoint_to_fp_real_ot.getIndices<std::pair<uint32_t, uint32_t>>();
143
2
  ASSERT_TRUE((floatingpoint_to_fp_real_indices
144
2
               == std::pair<uint32_t, uint32_t>{4, 25}));
145
146
  Op floatingpoint_to_fp_signed_bitvector_ot =
147
4
      d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25);
148
  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_signed_bitvector_indices =
149
      floatingpoint_to_fp_signed_bitvector_ot
150
2
          .getIndices<std::pair<uint32_t, uint32_t>>();
151
2
  ASSERT_TRUE((floatingpoint_to_fp_signed_bitvector_indices
152
2
               == std::pair<uint32_t, uint32_t>{4, 25}));
153
154
  Op floatingpoint_to_fp_unsigned_bitvector_ot =
155
4
      d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25);
156
  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_unsigned_bitvector_indices =
157
      floatingpoint_to_fp_unsigned_bitvector_ot
158
2
          .getIndices<std::pair<uint32_t, uint32_t>>();
159
2
  ASSERT_TRUE((floatingpoint_to_fp_unsigned_bitvector_indices
160
2
               == std::pair<uint32_t, uint32_t>{4, 25}));
161
162
  Op floatingpoint_to_fp_generic_ot =
163
4
      d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25);
164
  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_generic_indices =
165
      floatingpoint_to_fp_generic_ot
166
2
          .getIndices<std::pair<uint32_t, uint32_t>>();
167
2
  ASSERT_TRUE((floatingpoint_to_fp_generic_indices
168
2
               == std::pair<uint32_t, uint32_t>{4, 25}));
169
4
  ASSERT_THROW(floatingpoint_to_fp_generic_ot.getIndices<std::string>(),
170
2
               CVC4ApiException);
171
}
172
173
16
TEST_F(TestApiBlackOp, opScopingToString)
174
{
175
4
  Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
176
4
  std::string op_repr = bitvector_repeat_ot.toString();
177
4
  Solver solver2;
178
2
  ASSERT_EQ(bitvector_repeat_ot.toString(), op_repr);
179
}
180
}  // namespace test
181
24
}  // namespace CVC4