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