Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 the guards of the C API functions.
14 : : */
15 : :
16 : : extern "C" {
17 : : #include <cvc5/c/cvc5.h>
18 : : }
19 : :
20 : : #include "base/output.h"
21 : : #include "gtest/gtest.h"
22 : :
23 : : namespace cvc5::internal::test {
24 : :
25 : : class TestCApiBlackOp : public ::testing::Test
26 : : {
27 : : protected:
28 : 55 : void SetUp() override
29 : : {
30 : 55 : d_tm = cvc5_term_manager_new();
31 : 55 : d_bool = cvc5_get_boolean_sort(d_tm);
32 : 55 : d_int = cvc5_get_integer_sort(d_tm);
33 : 55 : d_real = cvc5_get_real_sort(d_tm);
34 : 55 : d_uninterpreted = cvc5_mk_uninterpreted_sort(d_tm, "u");
35 : 55 : }
36 : 45 : void TearDown() override { cvc5_term_manager_delete(d_tm); }
37 : :
38 : : Cvc5TermManager* d_tm;
39 : : Cvc5Sort d_bool;
40 : : Cvc5Sort d_int;
41 : : Cvc5Sort d_real;
42 : : Cvc5Sort d_uninterpreted;
43 : : };
44 : :
45 : 22 : TEST_F(TestCApiBlackOp, equal)
46 : : {
47 : 11 : std::vector<uint32_t> idxs = {4, 0};
48 : : Cvc5Op op1 =
49 : 11 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), idxs.data());
50 : 11 : idxs = {4, 1};
51 : : Cvc5Op op2 =
52 : 11 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), idxs.data());
53 [ - + ]: 11 : ASSERT_TRUE(cvc5_op_is_equal(op1, op1));
54 [ - + ]: 11 : ASSERT_TRUE(cvc5_op_is_disequal(op1, op2));
55 [ - + ]: 11 : ASSERT_FALSE(cvc5_op_is_equal(op1, nullptr));
56 [ - + ]: 11 : ASSERT_TRUE(cvc5_op_is_disequal(op1, nullptr));
57 : : }
58 : :
59 : 22 : TEST_F(TestCApiBlackOp, hash)
60 : : {
61 : 11 : ASSERT_DEATH(cvc5_op_hash(nullptr), "invalid operator");
62 : 10 : std::vector<uint32_t> idxs = {4, 0};
63 : : Cvc5Op op1 =
64 : 10 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), idxs.data());
65 : 10 : idxs = {4, 1};
66 : : Cvc5Op op2 =
67 : 10 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), idxs.data());
68 [ - + ]: 10 : ASSERT_EQ(cvc5_op_hash(op1), cvc5_op_hash(op1));
69 [ - + ]: 10 : ASSERT_NE(cvc5_op_hash(op1), cvc5_op_hash(op2));
70 : : }
71 : :
72 : 20 : TEST_F(TestCApiBlackOp, copy_release)
73 : : {
74 : 10 : ASSERT_DEATH(cvc5_op_copy(nullptr), "invalid op");
75 : 9 : ASSERT_DEATH(cvc5_op_release(nullptr), "invalid op");
76 : 8 : std::vector<uint32_t> idxs = {4, 0};
77 : : Cvc5Op op =
78 : 8 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), idxs.data());
79 : 8 : Cvc5Op op_copy = cvc5_op_copy(op);
80 : 8 : size_t hash1 = cvc5_op_hash(op);
81 : 8 : size_t hash2 = cvc5_op_hash(op_copy);
82 [ - + ]: 8 : ASSERT_EQ(hash1, hash2);
83 : 8 : cvc5_op_release(op);
84 [ - + ]: 8 : ASSERT_EQ(cvc5_op_hash(op), cvc5_op_hash(op_copy));
85 : 8 : cvc5_op_release(op);
86 : : // we cannot reliably check that querying on the (now freed) term fails
87 : : // unless ASAN is enabled
88 : : }
89 : :
90 : 16 : TEST_F(TestCApiBlackOp, get_kind)
91 : : {
92 : 8 : ASSERT_DEATH(cvc5_op_get_kind(nullptr), "invalid operator");
93 : 7 : std::vector<uint32_t> idxs = {4, 0};
94 [ - + ]: 7 : ASSERT_EQ(cvc5_op_get_kind(cvc5_mk_op(
95 : : d_tm, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), idxs.data())),
96 : : CVC5_KIND_BITVECTOR_EXTRACT);
97 : : }
98 : :
99 : 14 : TEST_F(TestCApiBlackOp, mk_op)
100 : : {
101 : 7 : std::vector<uint32_t> idxs = {4, 0};
102 : 7 : ASSERT_DEATH(
103 : : cvc5_mk_op(
104 : : nullptr, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), idxs.data()),
105 : : "unexpected NULL argument");
106 : 6 : ASSERT_DEATH(
107 : : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), nullptr),
108 : : "unexpected NULL argument");
109 : 5 : (void)cvc5_mk_op(d_tm, CVC5_KIND_ADD, 0, nullptr);
110 : 5 : idxs.push_back(2);
111 : 5 : ASSERT_DEATH(
112 : : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), idxs.data()),
113 : : "invalid number of indices");
114 : : }
115 : :
116 : 8 : TEST_F(TestCApiBlackOp, get_num_indices)
117 : : {
118 : 4 : ASSERT_DEATH(cvc5_op_get_num_indices(nullptr), "invalid operator");
119 : :
120 : : // Operators with 0 indices
121 : 3 : Cvc5Op add = cvc5_mk_op(d_tm, CVC5_KIND_ADD, 0, nullptr);
122 [ - + ]: 3 : ASSERT_EQ(cvc5_op_get_num_indices(add), 0);
123 : :
124 : : // Operators with 1 index
125 : 3 : std::vector<uint32_t> idxs = {4};
126 : : Cvc5Op divisible =
127 : 3 : cvc5_mk_op(d_tm, CVC5_KIND_DIVISIBLE, idxs.size(), idxs.data());
128 : 3 : idxs = {5};
129 : : Cvc5Op bv_repeat =
130 : 3 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_REPEAT, idxs.size(), idxs.data());
131 : 3 : idxs = {6};
132 : 3 : Cvc5Op bv_zext = cvc5_mk_op(
133 : 3 : d_tm, CVC5_KIND_BITVECTOR_ZERO_EXTEND, idxs.size(), idxs.data());
134 : 3 : idxs = {7};
135 : 3 : Cvc5Op bv_sext = cvc5_mk_op(
136 : 3 : d_tm, CVC5_KIND_BITVECTOR_SIGN_EXTEND, idxs.size(), idxs.data());
137 : 3 : idxs = {8};
138 : 3 : Cvc5Op bv_rol = cvc5_mk_op(
139 : 3 : d_tm, CVC5_KIND_BITVECTOR_ROTATE_LEFT, idxs.size(), idxs.data());
140 : 3 : idxs = {9};
141 : 3 : Cvc5Op bv_ror = cvc5_mk_op(
142 : 3 : d_tm, CVC5_KIND_BITVECTOR_ROTATE_RIGHT, idxs.size(), idxs.data());
143 : 3 : idxs = {10};
144 : : Cvc5Op int_to_bv =
145 : 3 : cvc5_mk_op(d_tm, CVC5_KIND_INT_TO_BITVECTOR, idxs.size(), idxs.data());
146 : 3 : idxs = {12};
147 : 3 : Cvc5Op iand = cvc5_mk_op(d_tm, CVC5_KIND_IAND, idxs.size(), idxs.data());
148 : 3 : idxs = {12};
149 : 3 : Cvc5Op fp_to_ubv = cvc5_mk_op(
150 : 3 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_UBV, idxs.size(), idxs.data());
151 : 3 : idxs = {13};
152 : 3 : Cvc5Op fp_to_sbv = cvc5_mk_op(
153 : 3 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_SBV, idxs.size(), idxs.data());
154 : :
155 [ - + ]: 3 : ASSERT_EQ(1, cvc5_op_get_num_indices(divisible));
156 [ - + ]: 3 : ASSERT_EQ(1, cvc5_op_get_num_indices(bv_repeat));
157 [ - + ]: 3 : ASSERT_EQ(1, cvc5_op_get_num_indices(bv_zext));
158 [ - + ]: 3 : ASSERT_EQ(1, cvc5_op_get_num_indices(bv_sext));
159 [ - + ]: 3 : ASSERT_EQ(1, cvc5_op_get_num_indices(bv_ror));
160 [ - + ]: 3 : ASSERT_EQ(1, cvc5_op_get_num_indices(bv_rol));
161 [ - + ]: 3 : ASSERT_EQ(1, cvc5_op_get_num_indices(int_to_bv));
162 [ - + ]: 3 : ASSERT_EQ(1, cvc5_op_get_num_indices(iand));
163 [ - + ]: 3 : ASSERT_EQ(1, cvc5_op_get_num_indices(fp_to_ubv));
164 [ - + ]: 3 : ASSERT_EQ(1, cvc5_op_get_num_indices(fp_to_sbv));
165 : :
166 : : // Operators with 2 indices
167 : 3 : idxs = {1, 0};
168 : : Cvc5Op bv_ext =
169 : 3 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), idxs.data());
170 : 3 : idxs = {3, 2};
171 : : Cvc5Op to_fp_from_ieee =
172 : 3 : cvc5_mk_op(d_tm,
173 : : CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
174 : : idxs.size(),
175 : 3 : idxs.data());
176 : 3 : idxs = {5, 4};
177 : 3 : Cvc5Op to_fp_from_fp = cvc5_mk_op(
178 : 3 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_FP, idxs.size(), idxs.data());
179 : 3 : idxs = {7, 6};
180 : 3 : Cvc5Op to_fp_from_real = cvc5_mk_op(
181 : 3 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_REAL, idxs.size(), idxs.data());
182 : 3 : idxs = {9, 8};
183 : 3 : Cvc5Op to_fp_from_sbv = cvc5_mk_op(
184 : 3 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_SBV, idxs.size(), idxs.data());
185 : 3 : idxs = {11, 10};
186 : 3 : Cvc5Op to_fp_from_ubv = cvc5_mk_op(
187 : 3 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_UBV, idxs.size(), idxs.data());
188 : 3 : idxs = {15, 14};
189 : : Cvc5Op regexp_loop =
190 : 3 : cvc5_mk_op(d_tm, CVC5_KIND_REGEXP_LOOP, idxs.size(), idxs.data());
191 : :
192 [ - + ]: 3 : ASSERT_EQ(2, cvc5_op_get_num_indices(bv_ext));
193 [ - + ]: 3 : ASSERT_EQ(2, cvc5_op_get_num_indices(to_fp_from_ieee));
194 [ - + ]: 3 : ASSERT_EQ(2, cvc5_op_get_num_indices(to_fp_from_fp));
195 [ - + ]: 3 : ASSERT_EQ(2, cvc5_op_get_num_indices(to_fp_from_real));
196 [ - + ]: 3 : ASSERT_EQ(2, cvc5_op_get_num_indices(to_fp_from_sbv));
197 [ - + ]: 3 : ASSERT_EQ(2, cvc5_op_get_num_indices(to_fp_from_ubv));
198 [ - + ]: 3 : ASSERT_EQ(2, cvc5_op_get_num_indices(regexp_loop));
199 : :
200 : : // Operators with n indices
201 : 3 : idxs = {0, 3, 2, 0, 1, 2};
202 : : Cvc5Op tuple_proj =
203 : 3 : cvc5_mk_op(d_tm, CVC5_KIND_TUPLE_PROJECT, idxs.size(), idxs.data());
204 [ - + ]: 3 : ASSERT_EQ(idxs.size(), cvc5_op_get_num_indices(tuple_proj));
205 : :
206 : : Cvc5Op rel_proj =
207 : 3 : cvc5_mk_op(d_tm, CVC5_KIND_RELATION_PROJECT, idxs.size(), idxs.data());
208 [ - + ]: 3 : ASSERT_EQ(idxs.size(), cvc5_op_get_num_indices(rel_proj));
209 : :
210 : : Cvc5Op table_proj =
211 : 3 : cvc5_mk_op(d_tm, CVC5_KIND_TABLE_PROJECT, idxs.size(), idxs.data());
212 [ - + ]: 3 : ASSERT_EQ(idxs.size(), cvc5_op_get_num_indices(table_proj));
213 : : }
214 : :
215 : 6 : TEST_F(TestCApiBlackOp, subscript_operator)
216 : : {
217 : : // Operators with 0 indices
218 : 3 : Cvc5Op add = cvc5_mk_op(d_tm, CVC5_KIND_ADD, 0, nullptr);
219 : 3 : ASSERT_DEATH(cvc5_op_get_index(nullptr, 0), "invalid operator");
220 : 2 : ASSERT_DEATH(cvc5_op_get_index(add, 0), "Op is not indexed");
221 : :
222 : : // Operators with 1 index
223 : 1 : std::vector<uint32_t> idxs = {4};
224 : : Cvc5Op divisible =
225 : 1 : cvc5_mk_op(d_tm, CVC5_KIND_DIVISIBLE, idxs.size(), idxs.data());
226 : 1 : idxs = {5};
227 : : Cvc5Op bv_repeat =
228 : 1 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_REPEAT, idxs.size(), idxs.data());
229 : 1 : idxs = {6};
230 : 1 : Cvc5Op bv_zext = cvc5_mk_op(
231 : 1 : d_tm, CVC5_KIND_BITVECTOR_ZERO_EXTEND, idxs.size(), idxs.data());
232 : 1 : idxs = {7};
233 : 1 : Cvc5Op bv_sext = cvc5_mk_op(
234 : 1 : d_tm, CVC5_KIND_BITVECTOR_SIGN_EXTEND, idxs.size(), idxs.data());
235 : 1 : idxs = {8};
236 : 1 : Cvc5Op bv_rol = cvc5_mk_op(
237 : 1 : d_tm, CVC5_KIND_BITVECTOR_ROTATE_LEFT, idxs.size(), idxs.data());
238 : 1 : idxs = {9};
239 : 1 : Cvc5Op bv_ror = cvc5_mk_op(
240 : 1 : d_tm, CVC5_KIND_BITVECTOR_ROTATE_RIGHT, idxs.size(), idxs.data());
241 : 1 : idxs = {10};
242 : : Cvc5Op int_to_bv =
243 : 1 : cvc5_mk_op(d_tm, CVC5_KIND_INT_TO_BITVECTOR, idxs.size(), idxs.data());
244 : 1 : idxs = {11};
245 : 1 : Cvc5Op iand = cvc5_mk_op(d_tm, CVC5_KIND_IAND, idxs.size(), idxs.data());
246 : 1 : idxs = {12};
247 : 1 : Cvc5Op fp_to_ubv = cvc5_mk_op(
248 : 1 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_UBV, idxs.size(), idxs.data());
249 : 1 : idxs = {13};
250 : 1 : Cvc5Op fp_to_sbv = cvc5_mk_op(
251 : 1 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_SBV, idxs.size(), idxs.data());
252 : 1 : idxs = {14};
253 : : Cvc5Op regexp_repeat =
254 : 1 : cvc5_mk_op(d_tm, CVC5_KIND_REGEXP_REPEAT, idxs.size(), idxs.data());
255 : :
256 [ - + ]: 1 : ASSERT_EQ(4, cvc5_term_get_uint32_value(cvc5_op_get_index(divisible, 0)));
257 [ - + ]: 1 : ASSERT_EQ(5, cvc5_term_get_uint32_value(cvc5_op_get_index(bv_repeat, 0)));
258 [ - + ]: 1 : ASSERT_EQ(6, cvc5_term_get_uint32_value(cvc5_op_get_index(bv_zext, 0)));
259 [ - + ]: 1 : ASSERT_EQ(7, cvc5_term_get_uint32_value(cvc5_op_get_index(bv_sext, 0)));
260 [ - + ]: 1 : ASSERT_EQ(8, cvc5_term_get_uint32_value(cvc5_op_get_index(bv_rol, 0)));
261 [ - + ]: 1 : ASSERT_EQ(9, cvc5_term_get_uint32_value(cvc5_op_get_index(bv_ror, 0)));
262 [ - + ]: 1 : ASSERT_EQ(10, cvc5_term_get_uint32_value(cvc5_op_get_index(int_to_bv, 0)));
263 [ - + ]: 1 : ASSERT_EQ(11, cvc5_term_get_uint32_value(cvc5_op_get_index(iand, 0)));
264 [ - + ]: 1 : ASSERT_EQ(12, cvc5_term_get_uint32_value(cvc5_op_get_index(fp_to_ubv, 0)));
265 [ - + ]: 1 : ASSERT_EQ(13, cvc5_term_get_uint32_value(cvc5_op_get_index(fp_to_sbv, 0)));
266 [ - + ]: 1 : ASSERT_EQ(14,
267 : : cvc5_term_get_uint32_value(cvc5_op_get_index(regexp_repeat, 0)));
268 : :
269 : : // Operators with 2 indices
270 : 1 : idxs = {1, 0};
271 : : Cvc5Op bv_ext =
272 : 1 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), idxs.data());
273 : 1 : idxs = {3, 2};
274 : : Cvc5Op to_fp_from_ieee =
275 : 1 : cvc5_mk_op(d_tm,
276 : : CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_IEEE_BV,
277 : : idxs.size(),
278 : 1 : idxs.data());
279 : 1 : idxs = {5, 4};
280 : 1 : Cvc5Op to_fp_from_fp = cvc5_mk_op(
281 : 1 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_FP, idxs.size(), idxs.data());
282 : 1 : idxs = {7, 6};
283 : 1 : Cvc5Op to_fp_from_real = cvc5_mk_op(
284 : 1 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_REAL, idxs.size(), idxs.data());
285 : 1 : idxs = {9, 8};
286 : 1 : Cvc5Op to_fp_from_sbv = cvc5_mk_op(
287 : 1 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_SBV, idxs.size(), idxs.data());
288 : 1 : idxs = {11, 10};
289 : 1 : Cvc5Op to_fp_from_ubv = cvc5_mk_op(
290 : 1 : d_tm, CVC5_KIND_FLOATINGPOINT_TO_FP_FROM_UBV, idxs.size(), idxs.data());
291 : 1 : idxs = {15, 14};
292 : : Cvc5Op regexp_loop =
293 : 1 : cvc5_mk_op(d_tm, CVC5_KIND_REGEXP_LOOP, idxs.size(), idxs.data());
294 : :
295 [ - + ]: 1 : ASSERT_EQ(1, cvc5_term_get_uint32_value(cvc5_op_get_index(bv_ext, 0)));
296 [ - + ]: 1 : ASSERT_EQ(0, cvc5_term_get_uint32_value(cvc5_op_get_index(bv_ext, 1)));
297 [ - + ]: 1 : ASSERT_EQ(3,
298 : : cvc5_term_get_uint32_value(cvc5_op_get_index(to_fp_from_ieee, 0)));
299 [ - + ]: 1 : ASSERT_EQ(2,
300 : : cvc5_term_get_uint32_value(cvc5_op_get_index(to_fp_from_ieee, 1)));
301 [ - + ]: 1 : ASSERT_EQ(5, cvc5_term_get_uint32_value(cvc5_op_get_index(to_fp_from_fp, 0)));
302 [ - + ]: 1 : ASSERT_EQ(4, cvc5_term_get_uint32_value(cvc5_op_get_index(to_fp_from_fp, 1)));
303 [ - + ]: 1 : ASSERT_EQ(7,
304 : : cvc5_term_get_uint32_value(cvc5_op_get_index(to_fp_from_real, 0)));
305 [ - + ]: 1 : ASSERT_EQ(6,
306 : : cvc5_term_get_uint32_value(cvc5_op_get_index(to_fp_from_real, 1)));
307 [ - + ]: 1 : ASSERT_EQ(9,
308 : : cvc5_term_get_uint32_value(cvc5_op_get_index(to_fp_from_sbv, 0)));
309 [ - + ]: 1 : ASSERT_EQ(8,
310 : : cvc5_term_get_uint32_value(cvc5_op_get_index(to_fp_from_sbv, 1)));
311 [ - + ]: 1 : ASSERT_EQ(11,
312 : : cvc5_term_get_uint32_value(cvc5_op_get_index(to_fp_from_ubv, 0)));
313 [ - + ]: 1 : ASSERT_EQ(10,
314 : : cvc5_term_get_uint32_value(cvc5_op_get_index(to_fp_from_ubv, 1)));
315 [ - + ]: 1 : ASSERT_EQ(15, cvc5_term_get_uint32_value(cvc5_op_get_index(regexp_loop, 0)));
316 [ - + ]: 1 : ASSERT_EQ(14, cvc5_term_get_uint32_value(cvc5_op_get_index(regexp_loop, 1)));
317 : :
318 : : // Operators with n indices
319 : 1 : idxs = {0, 3, 2, 0, 1, 2};
320 : : Cvc5Op tuple_proj =
321 : 1 : cvc5_mk_op(d_tm, CVC5_KIND_TUPLE_PROJECT, idxs.size(), idxs.data());
322 [ + + ]: 7 : for (size_t i = 0, size = cvc5_op_get_num_indices(tuple_proj); i < size; ++i)
323 : : {
324 [ - + ]: 6 : ASSERT_EQ(idxs[i],
325 : : cvc5_term_get_uint32_value(cvc5_op_get_index(tuple_proj, i)));
326 : : }
327 : :
328 : : Cvc5Op rel_proj =
329 : 1 : cvc5_mk_op(d_tm, CVC5_KIND_RELATION_PROJECT, idxs.size(), idxs.data());
330 [ + + ]: 7 : for (size_t i = 0, size = cvc5_op_get_num_indices(rel_proj); i < size; ++i)
331 : : {
332 [ - + ]: 6 : ASSERT_EQ(idxs[i],
333 : : cvc5_term_get_uint32_value(cvc5_op_get_index(rel_proj, i)));
334 : : }
335 : :
336 : : Cvc5Op table_proj =
337 : 1 : cvc5_mk_op(d_tm, CVC5_KIND_TABLE_PROJECT, idxs.size(), idxs.data());
338 [ + + ]: 7 : for (size_t i = 0, size = cvc5_op_get_num_indices(table_proj); i < size; ++i)
339 : : {
340 [ - + ]: 6 : ASSERT_EQ(idxs[i],
341 : : cvc5_term_get_uint32_value(cvc5_op_get_index(table_proj, i)));
342 : : }
343 : : }
344 : :
345 : 2 : TEST_F(TestCApiBlackOp, to_string)
346 : : {
347 : 1 : std::vector<uint32_t> idxs = {5};
348 : : Cvc5Op bv_repeat =
349 : 1 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_REPEAT, idxs.size(), idxs.data());
350 [ - + ]: 1 : ASSERT_EQ(cvc5_op_to_string(bv_repeat), cvc5_op_to_string(bv_repeat));
351 : : }
352 : : } // namespace cvc5::internal::test
|
