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 : :
20 : : namespace cvc5::internal::test {
21 : :
22 : : class TestCApiBlackTerm : public ::testing::Test
23 : : {
24 : : protected:
25 : 2331 : void SetUp() override
26 : : {
27 : 2331 : d_tm = cvc5_term_manager_new();
28 : 2331 : d_solver = cvc5_new(d_tm);
29 : 2331 : d_bool = cvc5_get_boolean_sort(d_tm);
30 : 2331 : d_int = cvc5_get_integer_sort(d_tm);
31 : 2331 : d_real = cvc5_get_real_sort(d_tm);
32 : 2331 : d_uninterpreted = cvc5_mk_uninterpreted_sort(d_tm, "u");
33 : 2331 : }
34 : 2203 : void TearDown() override
35 : : {
36 : 2203 : cvc5_delete(d_solver);
37 : 2203 : cvc5_term_manager_delete(d_tm);
38 : 2203 : }
39 : :
40 : : Cvc5TermManager* d_tm;
41 : : Cvc5* d_solver;
42 : : Cvc5Sort d_bool;
43 : : Cvc5Sort d_int;
44 : : Cvc5Sort d_real;
45 : : Cvc5Sort d_uninterpreted;
46 : : };
47 : :
48 : 514 : TEST_F(TestCApiBlackTerm, hash)
49 : : {
50 : 129 : ASSERT_DEATH(cvc5_term_hash(nullptr), "invalid term");
51 : 128 : (void)cvc5_term_hash(cvc5_mk_integer_int64(d_tm, 2));
52 : 128 : Cvc5Term x = cvc5_mk_var(d_tm, d_int, "x");
53 : 128 : Cvc5Term y = cvc5_mk_var(d_tm, d_int, "y");
54 [ - + ][ + - ]: 128 : ASSERT_EQ(cvc5_term_hash(x), cvc5_term_hash(x));
55 [ - + ][ + - ]: 128 : ASSERT_NE(cvc5_term_hash(x), cvc5_term_hash(y));
56 : : }
57 : :
58 : 508 : TEST_F(TestCApiBlackTerm, copy_release)
59 : : {
60 : 128 : ASSERT_DEATH(cvc5_term_copy(nullptr), "invalid term");
61 : 127 : ASSERT_DEATH(cvc5_term_release(nullptr), "invalid term");
62 : 126 : Cvc5Term tint = cvc5_mk_integer_int64(d_tm, 2);
63 : 126 : size_t hash1 = cvc5_term_hash(tint);
64 : 126 : Cvc5Term tint_copy = cvc5_term_copy(tint);
65 : 126 : size_t hash2 = cvc5_term_hash(tint_copy);
66 [ - + ][ + - ]: 126 : ASSERT_EQ(hash1, hash2);
67 : 126 : cvc5_term_release(tint);
68 [ - + ][ + - ]: 126 : ASSERT_EQ(cvc5_term_hash(tint), cvc5_term_hash(tint_copy));
69 : 126 : cvc5_term_release(tint);
70 : : // we cannot reliably check that querying on the (now freed) term fails
71 : : // unless ASAN is enabled
72 : : }
73 : :
74 : 500 : TEST_F(TestCApiBlackTerm, compare)
75 : : {
76 : 126 : Cvc5Term x = cvc5_mk_var(d_tm, d_uninterpreted, "x");
77 : 126 : Cvc5Term y = cvc5_mk_var(d_tm, d_uninterpreted, "y");
78 : 126 : ASSERT_DEATH(cvc5_term_compare(x, nullptr), "invalid term");
79 : 125 : ASSERT_DEATH(cvc5_term_compare(nullptr, y), "invalid term");
80 [ - + ][ + - ]: 124 : ASSERT_FALSE(cvc5_term_is_equal(x, nullptr));
81 [ - + ][ + - ]: 124 : ASSERT_TRUE(cvc5_term_is_disequal(x, nullptr));
82 [ - + ][ + - ]: 124 : ASSERT_EQ(cvc5_term_compare(x, x), 0);
83 [ - + ][ + - ]: 124 : ASSERT_NE(cvc5_term_compare(x, y), 0);
84 : : }
85 : :
86 : 494 : TEST_F(TestCApiBlackTerm, get_id)
87 : : {
88 : 124 : ASSERT_DEATH(cvc5_term_get_id(nullptr), "invalid term");
89 : 123 : Cvc5Term x = cvc5_mk_var(d_tm, d_int, "x");
90 : 123 : Cvc5Term y = cvc5_term_copy(x);
91 : 123 : Cvc5Term z = cvc5_mk_var(d_tm, d_int, "z");
92 : 123 : (void)cvc5_term_get_id(x);
93 [ - + ][ + - ]: 123 : ASSERT_EQ(cvc5_term_get_id(x), cvc5_term_get_id(y));
94 [ - + ][ + - ]: 123 : ASSERT_NE(cvc5_term_get_id(x), cvc5_term_get_id(z));
95 : 123 : cvc5_term_release(y);
96 : : }
97 : :
98 : 490 : TEST_F(TestCApiBlackTerm, get_kind)
99 : : {
100 : 123 : std::vector<Cvc5Sort> domain = {d_uninterpreted};
101 : : Cvc5Sort fun_sort1 =
102 : 123 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
103 : 123 : domain = {d_int};
104 : : Cvc5Sort fun_sort2 =
105 : 123 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
106 : :
107 : 123 : ASSERT_DEATH(cvc5_term_get_kind(nullptr), "invalid term");
108 : :
109 : 122 : Cvc5Term x = cvc5_mk_var(d_tm, d_uninterpreted, "x");
110 [ - + ][ + - ]: 122 : ASSERT_EQ(cvc5_term_get_kind(x), CVC5_KIND_VARIABLE);
111 : 122 : Cvc5Term y = cvc5_mk_var(d_tm, d_uninterpreted, "y");
112 [ - + ][ + - ]: 122 : ASSERT_EQ(cvc5_term_get_kind(y), CVC5_KIND_VARIABLE);
113 : :
114 : 122 : Cvc5Term f = cvc5_mk_var(d_tm, fun_sort1, "f");
115 [ - + ][ + - ]: 122 : ASSERT_EQ(cvc5_term_get_kind(f), CVC5_KIND_VARIABLE);
116 : 122 : Cvc5Term p = cvc5_mk_var(d_tm, fun_sort2, "p");
117 [ - + ][ + - ]: 122 : ASSERT_EQ(cvc5_term_get_kind(p), CVC5_KIND_VARIABLE);
118 : :
119 : 122 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
120 [ - + ][ + - ]: 122 : ASSERT_EQ(cvc5_term_get_kind(zero), CVC5_KIND_CONST_INTEGER);
121 : :
122 : 122 : std::vector<Cvc5Term> args = {f, x};
123 : : Cvc5Term f_x =
124 : 122 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
125 [ - + ][ + - ]: 122 : ASSERT_EQ(cvc5_term_get_kind(f_x), CVC5_KIND_APPLY_UF);
126 : 122 : args = {f, y};
127 : : Cvc5Term f_y =
128 : 122 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
129 [ - + ][ + - ]: 122 : ASSERT_EQ(cvc5_term_get_kind(f_y), CVC5_KIND_APPLY_UF);
130 : 122 : args = {f_x, f_y};
131 : 122 : Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
132 [ - + ][ + - ]: 122 : ASSERT_EQ(cvc5_term_get_kind(sum), CVC5_KIND_ADD);
133 : 122 : args = {p, zero};
134 : : Cvc5Term p_0 =
135 : 122 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
136 [ - + ][ + - ]: 122 : ASSERT_EQ(cvc5_term_get_kind(p_0), CVC5_KIND_APPLY_UF);
137 : 122 : args = {p, f_y};
138 : : Cvc5Term p_f_y =
139 : 122 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
140 [ - + ][ + - ]: 122 : ASSERT_EQ(cvc5_term_get_kind(p_f_y), CVC5_KIND_APPLY_UF);
141 : :
142 : : // Sequence kinds do not exist internally, test that the API properly
143 : : // converts them back.
144 : 122 : Cvc5Sort seq_sort = cvc5_mk_sequence_sort(d_tm, d_int);
145 : 122 : Cvc5Term s = cvc5_mk_const(d_tm, seq_sort, "s");
146 : 122 : args = {s, s};
147 : : Cvc5Term ss =
148 : 122 : cvc5_mk_term(d_tm, CVC5_KIND_SEQ_CONCAT, args.size(), args.data());
149 [ - + ][ + - ]: 122 : ASSERT_EQ(cvc5_term_get_kind(ss), CVC5_KIND_SEQ_CONCAT);
150 [ + - ]: 122 : }
151 : :
152 : 486 : TEST_F(TestCApiBlackTerm, get_sort)
153 : : {
154 : 122 : Cvc5Sort bv_sort = cvc5_mk_bv_sort(d_tm, 8);
155 : 122 : std::vector<Cvc5Sort> domain = {bv_sort};
156 : : Cvc5Sort fun_sort1 =
157 : 122 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
158 : 122 : domain = {d_int};
159 : : Cvc5Sort fun_sort2 =
160 : 122 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool);
161 : :
162 : 122 : ASSERT_DEATH(cvc5_term_get_sort(nullptr), "invalid term");
163 : :
164 : 121 : Cvc5Term x = cvc5_mk_var(d_tm, bv_sort, "x");
165 [ - + ][ + - ]: 121 : ASSERT_TRUE(cvc5_sort_is_equal(cvc5_term_get_sort(x), bv_sort));
166 : 121 : Cvc5Term y = cvc5_mk_var(d_tm, bv_sort, "y");
167 [ - + ][ + - ]: 121 : ASSERT_TRUE(cvc5_sort_is_equal(cvc5_term_get_sort(x), cvc5_term_get_sort(y)));
168 : :
169 : 121 : Cvc5Term f = cvc5_mk_var(d_tm, fun_sort1, "f");
170 [ - + ][ + - ]: 121 : ASSERT_TRUE(cvc5_sort_is_equal(cvc5_term_get_sort(f), fun_sort1));
171 : 121 : Cvc5Term p = cvc5_mk_var(d_tm, fun_sort2, "p");
172 [ - + ][ + - ]: 121 : ASSERT_TRUE(cvc5_sort_is_equal(cvc5_term_get_sort(p), fun_sort2));
173 : :
174 : 121 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
175 [ - + ][ + - ]: 121 : ASSERT_TRUE(cvc5_sort_is_equal(cvc5_term_get_sort(zero), d_int));
176 : :
177 : 121 : std::vector<Cvc5Term> args = {f, x};
178 : : Cvc5Term f_x =
179 : 121 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
180 [ - + ][ + - ]: 121 : ASSERT_TRUE(cvc5_sort_is_equal(cvc5_term_get_sort(f_x), d_int));
181 : 121 : args = {f, y};
182 : : Cvc5Term f_y =
183 : 121 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
184 [ - + ][ + - ]: 121 : ASSERT_TRUE(cvc5_sort_is_equal(cvc5_term_get_sort(f_y), d_int));
185 : 121 : args = {f_x, f_y};
186 : 121 : Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
187 [ - + ][ + - ]: 121 : ASSERT_TRUE(cvc5_sort_is_equal(cvc5_term_get_sort(sum), d_int));
188 : 121 : args = {p, zero};
189 : : Cvc5Term p_0 =
190 : 121 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
191 [ - + ][ + - ]: 121 : ASSERT_TRUE(cvc5_sort_is_equal(cvc5_term_get_sort(p_0), d_bool));
192 : 121 : args = {p, f_y};
193 : : Cvc5Term p_f_y =
194 : 121 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
195 [ - + ][ + - ]: 121 : ASSERT_TRUE(cvc5_sort_is_equal(cvc5_term_get_sort(p_f_y), d_bool));
196 [ - + ][ + - ]: 121 : ASSERT_EQ(cvc5_term_get_kind(p_f_y), CVC5_KIND_APPLY_UF);
197 [ + - ]: 121 : }
198 : :
199 : 476 : TEST_F(TestCApiBlackTerm, get_op)
200 : : {
201 : 121 : ASSERT_DEATH(cvc5_term_has_op(nullptr), "invalid term");
202 : 120 : ASSERT_DEATH(cvc5_term_get_op(nullptr), "invalid term");
203 : :
204 : 119 : Cvc5Sort bv_sort = cvc5_mk_bv_sort(d_tm, 8);
205 : 119 : Cvc5Sort arr_sort = cvc5_mk_array_sort(d_tm, bv_sort, d_int);
206 : 119 : std::vector<Cvc5Sort> domain = {d_int};
207 : : Cvc5Sort fun_sort =
208 : 119 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), bv_sort);
209 : :
210 : 119 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
211 : 119 : Cvc5Term a = cvc5_mk_const(d_tm, arr_sort, "a");
212 : 119 : Cvc5Term b = cvc5_mk_const(d_tm, bv_sort, "b");
213 : :
214 [ - + ][ + - ]: 119 : ASSERT_FALSE(cvc5_term_has_op(x));
215 : 119 : ASSERT_DEATH(cvc5_term_get_op(x), "expected Term to have an Op");
216 : :
217 : 118 : std::vector<Cvc5Term> args = {a, b};
218 : 118 : Cvc5Term ab = cvc5_mk_term(d_tm, CVC5_KIND_SELECT, args.size(), args.data());
219 [ - + ][ + - ]: 118 : ASSERT_TRUE(cvc5_term_has_op(ab));
220 [ - + ][ + - ]: 118 : ASSERT_FALSE(cvc5_op_is_indexed(cvc5_term_get_op(ab)));
221 : :
222 : 118 : std::vector<uint32_t> idxs = {4, 0};
223 : : Cvc5Op ext =
224 : 118 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_EXTRACT, idxs.size(), idxs.data());
225 : 118 : args = {b};
226 : 118 : Cvc5Term extb = cvc5_mk_term_from_op(d_tm, ext, args.size(), args.data());
227 [ - + ][ + - ]: 118 : ASSERT_EQ(cvc5_term_get_kind(extb), CVC5_KIND_BITVECTOR_EXTRACT);
228 : : // can compare directly to a Kind (will invoke Op constructor)
229 [ - + ][ + - ]: 118 : ASSERT_TRUE(cvc5_term_has_op(extb));
230 [ - + ][ + - ]: 118 : ASSERT_TRUE(cvc5_op_is_indexed(cvc5_term_get_op(extb)));
231 [ - + ][ + - ]: 118 : ASSERT_TRUE(cvc5_op_is_equal(cvc5_term_get_op(extb), ext));
232 : :
233 : 118 : idxs = {4};
234 : : Cvc5Op bit =
235 : 118 : cvc5_mk_op(d_tm, CVC5_KIND_BITVECTOR_BIT, idxs.size(), idxs.data());
236 : 118 : Cvc5Term bitb = cvc5_mk_term_from_op(d_tm, bit, args.size(), args.data());
237 [ - + ][ + - ]: 118 : ASSERT_EQ(cvc5_term_get_kind(bitb), CVC5_KIND_BITVECTOR_BIT);
238 [ - + ][ + - ]: 118 : ASSERT_TRUE(cvc5_term_has_op(bitb));
239 [ - + ][ + - ]: 118 : ASSERT_TRUE(cvc5_op_is_equal(cvc5_term_get_op(bitb), bit));
240 [ - + ][ + - ]: 118 : ASSERT_TRUE(cvc5_op_is_indexed(cvc5_term_get_op(bitb)));
241 [ - + ][ + - ]: 118 : ASSERT_EQ(cvc5_op_get_num_indices(bit), 1);
242 [ - + ]: 118 : ASSERT_TRUE(cvc5_term_is_equal(cvc5_op_get_index(bit, 0),
243 [ + - ]: 118 : cvc5_mk_integer_int64(d_tm, 4)));
244 : :
245 : 118 : Cvc5Term f = cvc5_mk_const(d_tm, fun_sort, "f");
246 : 118 : args = {f, x};
247 : : Cvc5Term fx =
248 : 118 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
249 [ - + ][ + - ]: 118 : ASSERT_FALSE(cvc5_term_has_op(f));
250 : 118 : ASSERT_DEATH(cvc5_term_get_op(f), "expected Term to have an Op");
251 [ - + ][ + - ]: 117 : ASSERT_TRUE(cvc5_term_has_op(fx));
252 : :
253 : : // testing rebuild from op and children
254 [ - + ]: 117 : ASSERT_TRUE(cvc5_term_is_equal(
255 : : fx,
256 : : cvc5_mk_term_from_op(
257 [ + - ]: 117 : d_tm, cvc5_term_get_op(fx), args.size(), args.data())));
258 : :
259 : : // Test Datatypes Ops
260 : 117 : Cvc5Sort sort = cvc5_mk_param_sort(d_tm, "T");
261 : 117 : std::vector<Cvc5Sort> sorts = {sort};
262 : 117 : Cvc5DatatypeDecl decl = cvc5_mk_dt_decl_with_params(
263 : 117 : d_tm, "paramlist", sorts.size(), sorts.data(), false);
264 : 117 : Cvc5DatatypeConstructorDecl cons = cvc5_mk_dt_cons_decl(d_tm, "cons");
265 : 117 : cvc5_dt_cons_decl_add_selector(cons, "head", sort);
266 : 117 : cvc5_dt_cons_decl_add_selector_self(cons, "tail");
267 : 117 : cvc5_dt_decl_add_constructor(decl, cons);
268 : 117 : Cvc5DatatypeConstructorDecl nil = cvc5_mk_dt_cons_decl(d_tm, "nil");
269 : 117 : cvc5_dt_decl_add_constructor(decl, nil);
270 : 117 : Cvc5Sort list_sort = cvc5_mk_dt_sort(d_tm, decl);
271 : 117 : sorts = {d_int};
272 : : Cvc5Sort int_list_sort =
273 : 117 : cvc5_sort_instantiate(list_sort, sorts.size(), sorts.data());
274 : :
275 : 117 : Cvc5Term c = cvc5_mk_const(d_tm, int_list_sort, "c");
276 : 117 : Cvc5Datatype list = cvc5_sort_get_datatype(list_sort);
277 : : // list datatype constructor and selector operator terms
278 : : Cvc5Term cons_term =
279 : 117 : cvc5_dt_cons_get_term(cvc5_dt_get_constructor_by_name(list, "cons"));
280 : : Cvc5Term nil_term =
281 : 117 : cvc5_dt_cons_get_term(cvc5_dt_get_constructor_by_name(list, "nil"));
282 : 117 : Cvc5Term head_term = cvc5_dt_sel_get_term(cvc5_dt_get_selector(list, "head"));
283 : 117 : Cvc5Term tail_term = cvc5_dt_sel_get_term(cvc5_dt_get_selector(list, "tail"));
284 : :
285 : 117 : args = {nil_term};
286 : : Cvc5Term apply_nil_term =
287 : 117 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_CONSTRUCTOR, args.size(), args.data());
288 : 117 : args = {cons_term, cvc5_mk_integer_int64(d_tm, 0), apply_nil_term};
289 : : Cvc5Term apply_cons_term =
290 : 117 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_CONSTRUCTOR, args.size(), args.data());
291 : 117 : args = {head_term, apply_cons_term};
292 : : Cvc5Term apply_head_term =
293 : 117 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_SELECTOR, args.size(), args.data());
294 : 117 : args = {tail_term, apply_cons_term};
295 : : Cvc5Term apply_tail_term =
296 : 117 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_SELECTOR, args.size(), args.data());
297 : :
298 [ - + ][ + - ]: 117 : ASSERT_FALSE(cvc5_term_has_op(c));
299 [ - + ][ + - ]: 117 : ASSERT_TRUE(cvc5_term_has_op(apply_nil_term));
300 [ - + ][ + - ]: 117 : ASSERT_TRUE(cvc5_term_has_op(apply_cons_term));
301 [ - + ][ + - ]: 117 : ASSERT_TRUE(cvc5_term_has_op(apply_head_term));
302 [ - + ][ + - ]: 117 : ASSERT_TRUE(cvc5_term_has_op(apply_tail_term));
303 : :
304 : : // Test rebuilding
305 : 117 : args.clear();
306 [ + + ]: 351 : for (size_t i = 0, n = cvc5_term_get_num_children(apply_head_term); i < n;
307 : : ++i)
308 : : {
309 : 234 : args.push_back(cvc5_term_get_child(apply_head_term, i));
310 : : }
311 [ - + ]: 117 : ASSERT_TRUE(cvc5_term_is_equal(
312 : : apply_head_term,
313 : : cvc5_mk_term_from_op(
314 [ + - ]: 117 : d_tm, cvc5_term_get_op(apply_head_term), args.size(), args.data())));
315 : : }
316 : :
317 : 462 : TEST_F(TestCApiBlackTerm, has_get_symbol)
318 : : {
319 : 117 : ASSERT_DEATH(cvc5_term_has_symbol(nullptr), "invalid term");
320 : 116 : ASSERT_DEATH(cvc5_term_get_symbol(nullptr), "invalid term");
321 : :
322 : 115 : Cvc5Term t = cvc5_mk_true(d_tm);
323 : 115 : Cvc5Term c = cvc5_mk_const(d_tm, d_bool, "|\\|");
324 : :
325 [ - + ][ + - ]: 115 : ASSERT_FALSE(cvc5_term_has_symbol(t));
326 [ - + ][ + - ]: 115 : ASSERT_TRUE(cvc5_term_has_symbol(c));
327 : :
328 : 115 : ASSERT_DEATH(cvc5_term_get_symbol(t), "cannot get symbol");
329 [ - + ][ + - ]: 114 : ASSERT_EQ(cvc5_term_get_symbol(c), std::string("|\\|"));
330 : : }
331 : :
332 : 456 : TEST_F(TestCApiBlackTerm, assignment)
333 : : {
334 : 114 : Cvc5Term t1 = cvc5_mk_integer_int64(d_tm, 1);
335 : 114 : Cvc5Term t2 = cvc5_term_copy(t1);
336 : 114 : t2 = cvc5_mk_integer_int64(d_tm, 2);
337 [ - + ][ + - ]: 114 : ASSERT_TRUE(cvc5_term_is_equal(t1, cvc5_mk_integer_int64(d_tm, 1)));
338 [ - + ][ + - ]: 114 : ASSERT_TRUE(cvc5_term_is_equal(t2, cvc5_mk_integer_int64(d_tm, 2)));
339 [ - + ][ + - ]: 114 : ASSERT_FALSE(cvc5_term_is_equal(t1, t2));
340 : 114 : cvc5_term_release(t1);
341 [ - + ][ + - ]: 114 : ASSERT_TRUE(cvc5_term_is_equal(t1, cvc5_mk_integer_int64(d_tm, 1)));
342 [ - + ][ + - ]: 114 : ASSERT_TRUE(cvc5_term_is_equal(t2, cvc5_mk_integer_int64(d_tm, 2)));
343 [ - + ][ + - ]: 114 : ASSERT_FALSE(cvc5_term_is_equal(t1, t2));
344 : : }
345 : :
346 : 452 : TEST_F(TestCApiBlackTerm, children)
347 : : {
348 : 114 : ASSERT_DEATH(cvc5_term_get_num_children(nullptr), "invalid term");
349 : 113 : ASSERT_DEATH(cvc5_term_get_child(nullptr, 0), "invalid term");
350 : : // simple term 2+3
351 : 112 : Cvc5Term two = cvc5_mk_integer_int64(d_tm, 2);
352 : 112 : std::vector<Cvc5Term> args = {two, cvc5_mk_integer_int64(d_tm, 3)};
353 : 112 : Cvc5Term t1 = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
354 [ - + ][ + - ]: 112 : ASSERT_EQ(cvc5_term_get_num_children(t1), 2);
355 [ - + ][ + - ]: 112 : ASSERT_TRUE(cvc5_term_is_equal(cvc5_term_get_child(t1, 0), two));
356 : :
357 [ + + ]: 336 : for (size_t i = 0, n = cvc5_term_get_num_children(t1); i < n; ++i)
358 : : {
359 : 224 : (void)cvc5_term_get_child(t1, i);
360 : : }
361 : :
362 : : // apply term f(2)
363 : 112 : std::vector<Cvc5Sort> domain = {d_int};
364 : : Cvc5Sort fun_sort =
365 : 112 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
366 : 112 : Cvc5Term f = cvc5_mk_const(d_tm, fun_sort, "f");
367 : 112 : args = {f, two};
368 : : Cvc5Term t2 =
369 : 112 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
370 : : // due to our higher-order view of terms, we treat f as a child of APPLY_UF
371 [ - + ][ + - ]: 112 : ASSERT_EQ(cvc5_term_get_num_children(t2), 2);
372 [ - + ][ + - ]: 112 : ASSERT_TRUE(cvc5_term_is_equal(cvc5_term_get_child(t2, 0), f));
373 [ - + ][ + - ]: 112 : ASSERT_TRUE(cvc5_term_is_equal(cvc5_term_get_child(t2, 1), two));
374 : : }
375 : :
376 : 404 : TEST_F(TestCApiBlackTerm, get_integer)
377 : : {
378 : 112 : ASSERT_DEATH(cvc5_mk_integer(nullptr, "2"), "unexpected NULL argument");
379 : 111 : ASSERT_DEATH(cvc5_mk_integer(d_tm, nullptr), "unexpected NULL argument");
380 : :
381 : 110 : Cvc5Term int1 = cvc5_mk_integer(d_tm, "-18446744073709551616");
382 : 110 : Cvc5Term int2 = cvc5_mk_integer(d_tm, "-18446744073709551615");
383 : 110 : Cvc5Term int3 = cvc5_mk_integer(d_tm, "-4294967296");
384 : 110 : Cvc5Term int4 = cvc5_mk_integer(d_tm, "-4294967295");
385 : 110 : Cvc5Term int5 = cvc5_mk_integer(d_tm, "-10");
386 : 110 : Cvc5Term int6 = cvc5_mk_integer(d_tm, "0");
387 : 110 : Cvc5Term int7 = cvc5_mk_integer(d_tm, "10");
388 : 110 : Cvc5Term int8 = cvc5_mk_integer(d_tm, "4294967295");
389 : 110 : Cvc5Term int9 = cvc5_mk_integer(d_tm, "4294967296");
390 : 110 : Cvc5Term int10 = cvc5_mk_integer(d_tm, "18446744073709551615");
391 : 110 : Cvc5Term int11 = cvc5_mk_integer(d_tm, "18446744073709551616");
392 : 110 : Cvc5Term int12 = cvc5_mk_integer(d_tm, "-0");
393 : :
394 : 110 : ASSERT_DEATH(cvc5_mk_integer(d_tm, ""), "invalid argument");
395 : 109 : ASSERT_DEATH(cvc5_mk_integer(d_tm, "-"), "invalid argument");
396 : 108 : ASSERT_DEATH(cvc5_mk_integer(d_tm, "-1-"), "invalid argument");
397 : 107 : ASSERT_DEATH(cvc5_mk_integer(d_tm, "0.0"), "invalid argument");
398 : 106 : ASSERT_DEATH(cvc5_mk_integer(d_tm, "-0.1"), "invalid argument");
399 : 105 : ASSERT_DEATH(cvc5_mk_integer(d_tm, "012"), "invalid argument");
400 : 104 : ASSERT_DEATH(cvc5_mk_integer(d_tm, "0000"), "invalid argument");
401 : 103 : ASSERT_DEATH(cvc5_mk_integer(d_tm, "-01"), "invalid argument");
402 : 102 : ASSERT_DEATH(cvc5_mk_integer(d_tm, "-00"), "invalid argument");
403 : :
404 : 101 : ASSERT_DEATH(cvc5_term_is_int32_value(nullptr), "invalid term");
405 : 100 : ASSERT_DEATH(cvc5_term_is_uint32_value(nullptr), "invalid term");
406 : 99 : ASSERT_DEATH(cvc5_term_is_int64_value(nullptr), "invalid term");
407 : 98 : ASSERT_DEATH(cvc5_term_is_uint64_value(nullptr), "invalid term");
408 : 97 : ASSERT_DEATH(cvc5_term_is_integer_value(nullptr), "invalid term");
409 : 96 : ASSERT_DEATH(cvc5_term_get_integer_value(nullptr), "invalid term");
410 : 95 : ASSERT_DEATH(cvc5_term_get_int32_value(nullptr), "invalid term");
411 : 94 : ASSERT_DEATH(cvc5_term_get_int64_value(nullptr), "invalid term");
412 : 93 : ASSERT_DEATH(cvc5_term_get_uint32_value(nullptr), "invalid term");
413 : 92 : ASSERT_DEATH(cvc5_term_get_uint64_value(nullptr), "invalid term");
414 : 91 : ASSERT_DEATH(cvc5_term_get_real_or_integer_value_sign(nullptr),
415 : : "invalid term");
416 : :
417 [ + - ][ + - ]: 90 : ASSERT_TRUE(
[ + - ][ + - ]
[ + - ][ - + ]
418 : : !cvc5_term_is_int32_value(int1) && !cvc5_term_is_uint32_value(int1)
419 : : && !cvc5_term_is_int64_value(int1) && !cvc5_term_is_uint64_value(int1)
420 [ + - ]: 90 : && cvc5_term_is_integer_value(int1));
421 [ - + ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int1),
422 [ + - ]: 90 : std::string("-18446744073709551616"));
423 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int1), -1);
424 : :
425 [ + - ][ + - ]: 90 : ASSERT_TRUE(
[ + - ][ + - ]
[ + - ][ - + ]
426 : : !cvc5_term_is_int32_value(int2) && !cvc5_term_is_uint32_value(int2)
427 : : && !cvc5_term_is_int64_value(int2) && !cvc5_term_is_uint64_value(int2)
428 [ + - ]: 90 : && cvc5_term_is_integer_value(int2));
429 [ - + ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int2),
430 [ + - ]: 90 : std::string("-18446744073709551615"));
431 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int2), -1);
432 : :
433 [ + - ][ + - ]: 90 : ASSERT_TRUE(
[ + - ][ + - ]
[ + - ][ - + ]
434 : : !cvc5_term_is_int32_value(int3) && !cvc5_term_is_uint32_value(int3)
435 : : && cvc5_term_is_int64_value(int3) && !cvc5_term_is_uint64_value(int3)
436 [ + - ]: 90 : && cvc5_term_is_integer_value(int3));
437 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int3), std::string("-4294967296"));
438 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int3), -1);
439 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int64_value(int3), -4294967296);
440 : :
441 [ + - ][ + - ]: 90 : ASSERT_TRUE(
[ + - ][ + - ]
[ + - ][ - + ]
442 : : !cvc5_term_is_int32_value(int4) && !cvc5_term_is_uint32_value(int4)
443 : : && cvc5_term_is_int64_value(int4) && !cvc5_term_is_uint64_value(int4)
444 [ + - ]: 90 : && cvc5_term_is_integer_value(int4));
445 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int4), std::string("-4294967295"));
446 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int4), -1);
447 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int64_value(int4), -4294967295);
448 : :
449 [ + - ][ + - ]: 90 : ASSERT_TRUE(cvc5_term_is_int32_value(int5) && !cvc5_term_is_uint32_value(int5)
[ + - ][ + - ]
[ + - ][ - + ]
450 : : && cvc5_term_is_int64_value(int5)
451 : : && !cvc5_term_is_uint64_value(int5)
452 [ + - ]: 90 : && cvc5_term_is_integer_value(int5));
453 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int5), std::string("-10"));
454 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int5), -1);
455 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int32_value(int5), -10);
456 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int64_value(int5), -10);
457 : :
458 [ + - ][ + - ]: 90 : ASSERT_TRUE(cvc5_term_is_int32_value(int6) && cvc5_term_is_uint32_value(int6)
[ + - ][ + - ]
[ + - ][ - + ]
459 : : && cvc5_term_is_int64_value(int6)
460 : : && cvc5_term_is_uint64_value(int6)
461 [ + - ]: 90 : && cvc5_term_is_integer_value(int6));
462 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int6), std::string("0"));
463 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int6), 0);
464 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int32_value(int6), 0);
465 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int64_value(int6), 0);
466 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_uint32_value(int6), 0);
467 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_uint64_value(int6), 0);
468 : :
469 [ + - ][ + - ]: 90 : ASSERT_TRUE(cvc5_term_is_int32_value(int7) && cvc5_term_is_uint32_value(int7)
[ + - ][ + - ]
[ + - ][ - + ]
470 : : && cvc5_term_is_int64_value(int7)
471 : : && cvc5_term_is_uint64_value(int7)
472 [ + - ]: 90 : && cvc5_term_is_integer_value(int7));
473 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int7), std::string("10"));
474 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int7), 1);
475 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int32_value(int7), 10);
476 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int64_value(int7), 10);
477 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_uint32_value(int7), 10);
478 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_uint64_value(int7), 10);
479 : :
480 [ + - ][ + - ]: 90 : ASSERT_TRUE(!cvc5_term_is_int32_value(int8) && cvc5_term_is_uint32_value(int8)
[ + - ][ + - ]
[ + - ][ - + ]
481 : : && cvc5_term_is_int64_value(int8)
482 : : && cvc5_term_is_uint64_value(int8)
483 [ + - ]: 90 : && cvc5_term_is_integer_value(int8));
484 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int8), std::string("4294967295"));
485 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int8), 1);
486 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int64_value(int8), 4294967295);
487 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_uint32_value(int8), 4294967295);
488 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_uint64_value(int8), 4294967295);
489 : :
490 [ + - ][ + - ]: 90 : ASSERT_TRUE(
[ + - ][ + - ]
[ + - ][ - + ]
491 : : !cvc5_term_is_int32_value(int9) && !cvc5_term_is_uint32_value(int9)
492 : : && cvc5_term_is_int64_value(int9) && cvc5_term_is_uint64_value(int9)
493 [ + - ]: 90 : && cvc5_term_is_integer_value(int9));
494 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int9), std::string("4294967296"));
495 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int9), 1);
496 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int64_value(int9), 4294967296);
497 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_uint64_value(int9), 4294967296);
498 : :
499 [ + - ][ + - ]: 90 : ASSERT_TRUE(
[ + - ][ + - ]
[ + - ][ - + ]
500 : : !cvc5_term_is_int32_value(int10) && !cvc5_term_is_uint32_value(int10)
501 : : && !cvc5_term_is_int64_value(int10) && cvc5_term_is_uint64_value(int10)
502 [ + - ]: 90 : && cvc5_term_is_integer_value(int10));
503 [ - + ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int10),
504 [ + - ]: 90 : std::string("18446744073709551615"));
505 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int10), 1);
506 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_uint64_value(int10), 18446744073709551615ull);
507 : :
508 [ + - ][ + - ]: 90 : ASSERT_TRUE(
[ + - ][ + - ]
[ + - ][ - + ]
509 : : !cvc5_term_is_int32_value(int11) && !cvc5_term_is_uint32_value(int11)
510 : : && !cvc5_term_is_int64_value(int11) && !cvc5_term_is_uint64_value(int11)
511 [ + - ]: 90 : && cvc5_term_is_integer_value(int11));
512 [ - + ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int11),
513 [ + - ]: 90 : std::string("18446744073709551616"));
514 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int11), 1);
515 : :
516 [ + - ][ + - ]: 90 : ASSERT_TRUE(
[ + - ][ + - ]
[ + - ][ - + ]
517 : : cvc5_term_is_int32_value(int12) && cvc5_term_is_uint32_value(int12)
518 : : && cvc5_term_is_int64_value(int12) && cvc5_term_is_uint64_value(int12)
519 [ + - ]: 90 : && cvc5_term_is_integer_value(int12));
520 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_integer_value(int12), std::string("0"));
521 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_real_or_integer_value_sign(int12), 0);
522 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int32_value(int12), 0);
523 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_int64_value(int12), 0);
524 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_uint32_value(int12), 0);
525 [ - + ][ + - ]: 90 : ASSERT_EQ(cvc5_term_get_uint64_value(int12), 0);
526 : : }
527 : :
528 : 352 : TEST_F(TestCApiBlackTerm, get_string)
529 : : {
530 : 90 : ASSERT_DEATH(cvc5_mk_string(nullptr, "abcde", false),
531 : : "unexpected NULL argument");
532 : 89 : ASSERT_DEATH(cvc5_term_is_string_value(nullptr), "invalid term");
533 : 88 : ASSERT_DEATH(cvc5_term_get_u32string_value(nullptr), "invalid term");
534 : 87 : ASSERT_DEATH(cvc5_mk_string(d_tm, nullptr, false),
535 : : "unexpected NULL argument");
536 : 86 : Cvc5Term s1 = cvc5_mk_string(d_tm, "abcde", false);
537 [ - + ][ + - ]: 86 : ASSERT_TRUE(cvc5_term_is_string_value(s1));
538 [ - + ][ + - ]: 86 : ASSERT_EQ(cvc5_term_get_u32string_value(s1), std::u32string(U"abcde"));
539 : : }
540 : :
541 : 318 : TEST_F(TestCApiBlackTerm, get_real)
542 : : {
543 : : int32_t num32;
544 : : uint32_t den32;
545 : : int64_t num64;
546 : : uint64_t den64;
547 : :
548 : 86 : ASSERT_DEATH(cvc5_mk_real(nullptr, "2"), "unexpected NULL argument");
549 : 85 : ASSERT_DEATH(cvc5_mk_real(d_tm, nullptr), "unexpected NULL argument");
550 : :
551 : 84 : Cvc5Term real1 = cvc5_mk_real(d_tm, "0");
552 : 84 : Cvc5Term real2 = cvc5_mk_real(d_tm, ".0");
553 : 84 : Cvc5Term real3 = cvc5_mk_real(d_tm, "-17");
554 : 84 : Cvc5Term real4 = cvc5_mk_real(d_tm, "-3/5");
555 : 84 : Cvc5Term real5 = cvc5_mk_real(d_tm, "12.7");
556 : 84 : Cvc5Term real6 = cvc5_mk_real(d_tm, "1/4294967297");
557 : 84 : Cvc5Term real7 = cvc5_mk_real(d_tm, "4294967297");
558 : 84 : Cvc5Term real8 = cvc5_mk_real(d_tm, "1/18446744073709551617");
559 : 84 : Cvc5Term real9 = cvc5_mk_real(d_tm, "18446744073709551617");
560 : 84 : Cvc5Term real10 = cvc5_mk_real(d_tm, "2343.2343");
561 : :
562 : 84 : ASSERT_DEATH(cvc5_term_is_real32_value(nullptr), "invalid term");
563 : 83 : ASSERT_DEATH(cvc5_term_is_real64_value(nullptr), "invalid term");
564 : 82 : ASSERT_DEATH(cvc5_term_is_real_value(nullptr), "invalid term");
565 : 81 : ASSERT_DEATH(cvc5_term_get_real_value(nullptr), "invalid term");
566 : 80 : ASSERT_DEATH(cvc5_term_get_real32_value(nullptr, &num32, &den32),
567 : : "invalid term");
568 : 79 : ASSERT_DEATH(cvc5_term_get_real32_value(real1, nullptr, &den32),
569 : : "unexpected NULL argument");
570 : 78 : ASSERT_DEATH(cvc5_term_get_real32_value(real1, &num32, nullptr),
571 : : "unexpected NULL argument");
572 : 77 : ASSERT_DEATH(cvc5_term_get_real64_value(real1, nullptr, &den64),
573 : : "unexpected NULL argument");
574 : 76 : ASSERT_DEATH(cvc5_term_get_real64_value(real1, &num64, nullptr),
575 : : "unexpected NULL argument");
576 : 75 : ASSERT_DEATH(cvc5_term_get_real64_value(nullptr, &num64, &den64),
577 : : "invalid term");
578 : 74 : ASSERT_DEATH(cvc5_term_get_real_or_integer_value_sign(nullptr),
579 : : "invalid term");
580 : :
581 [ + - ][ + - ]: 73 : ASSERT_TRUE(cvc5_term_is_real_value(real1) && cvc5_term_is_real64_value(real1)
[ + - ][ - + ]
582 [ + - ]: 73 : && cvc5_term_is_real32_value(real1));
583 [ + - ][ + - ]: 73 : ASSERT_TRUE(cvc5_term_is_real_value(real2) && cvc5_term_is_real64_value(real2)
[ + - ][ - + ]
584 [ + - ]: 73 : && cvc5_term_is_real32_value(real2));
585 [ + - ][ + - ]: 73 : ASSERT_TRUE(cvc5_term_is_real_value(real3) && cvc5_term_is_real64_value(real3)
[ + - ][ - + ]
586 [ + - ]: 73 : && cvc5_term_is_real32_value(real3));
587 [ + - ][ + - ]: 73 : ASSERT_TRUE(cvc5_term_is_real_value(real4) && cvc5_term_is_real64_value(real4)
[ + - ][ - + ]
588 [ + - ]: 73 : && cvc5_term_is_real32_value(real4));
589 [ + - ][ + - ]: 73 : ASSERT_TRUE(cvc5_term_is_real_value(real5) && cvc5_term_is_real64_value(real5)
[ + - ][ - + ]
590 [ + - ]: 73 : && cvc5_term_is_real32_value(real5));
591 [ + - ][ + - ]: 73 : ASSERT_TRUE(cvc5_term_is_real_value(real6)
[ - + ]
592 [ + - ]: 73 : && cvc5_term_is_real64_value(real6));
593 [ + - ][ + - ]: 73 : ASSERT_TRUE(cvc5_term_is_real_value(real7)
[ - + ]
594 [ + - ]: 73 : && cvc5_term_is_real64_value(real7));
595 [ - + ][ + - ]: 73 : ASSERT_TRUE(cvc5_term_is_real_value(real8));
596 [ - + ][ + - ]: 73 : ASSERT_TRUE(cvc5_term_is_real_value(real9));
597 [ - + ][ + - ]: 73 : ASSERT_TRUE(cvc5_term_is_real_value(real10));
598 : :
599 : 73 : cvc5_term_get_real32_value(real1, &num32, &den32);
600 [ - + ][ + - ]: 73 : ASSERT_EQ(num32, 0);
601 [ - + ][ + - ]: 73 : ASSERT_EQ(den32, 1);
602 : 73 : cvc5_term_get_real64_value(real1, &num64, &den64);
603 [ - + ][ + - ]: 73 : ASSERT_EQ(num64, 0);
604 [ - + ][ + - ]: 73 : ASSERT_EQ(den64, 1);
605 [ - + ][ + - ]: 73 : ASSERT_EQ(cvc5_term_get_real_value(real1), std::string("0/1"));
606 : :
607 : 73 : cvc5_term_get_real32_value(real2, &num32, &den32);
608 [ - + ][ + - ]: 73 : ASSERT_EQ(num32, 0);
609 [ - + ][ + - ]: 73 : ASSERT_EQ(den32, 1);
610 : 73 : cvc5_term_get_real64_value(real2, &num64, &den64);
611 [ - + ][ + - ]: 73 : ASSERT_EQ(num64, 0);
612 [ - + ][ + - ]: 73 : ASSERT_EQ(den64, 1);
613 [ - + ][ + - ]: 73 : ASSERT_EQ(cvc5_term_get_real_value(real2), std::string("0/1"));
614 : :
615 : 73 : cvc5_term_get_real32_value(real3, &num32, &den32);
616 [ - + ][ + - ]: 73 : ASSERT_EQ(num32, -17);
617 [ - + ][ + - ]: 73 : ASSERT_EQ(den32, 1);
618 : 73 : cvc5_term_get_real64_value(real3, &num64, &den64);
619 [ - + ][ + - ]: 73 : ASSERT_EQ(num64, -17);
620 [ - + ][ + - ]: 73 : ASSERT_EQ(den64, 1);
621 [ - + ][ + - ]: 73 : ASSERT_EQ(cvc5_term_get_real_value(real3), std::string("-17/1"));
622 : :
623 : 73 : cvc5_term_get_real32_value(real4, &num32, &den32);
624 [ - + ][ + - ]: 73 : ASSERT_EQ(num32, -3);
625 [ - + ][ + - ]: 73 : ASSERT_EQ(den32, 5);
626 : 73 : cvc5_term_get_real64_value(real4, &num64, &den64);
627 [ - + ][ + - ]: 73 : ASSERT_EQ(num64, -3);
628 [ - + ][ + - ]: 73 : ASSERT_EQ(den64, 5);
629 [ - + ][ + - ]: 73 : ASSERT_EQ(cvc5_term_get_real_value(real4), std::string("-3/5"));
630 : :
631 : 73 : cvc5_term_get_real32_value(real5, &num32, &den32);
632 [ - + ][ + - ]: 73 : ASSERT_EQ(num32, 127);
633 [ - + ][ + - ]: 73 : ASSERT_EQ(den32, 10);
634 : 73 : cvc5_term_get_real64_value(real5, &num64, &den64);
635 [ - + ][ + - ]: 73 : ASSERT_EQ(num64, 127);
636 [ - + ][ + - ]: 73 : ASSERT_EQ(den64, 10);
637 [ - + ][ + - ]: 73 : ASSERT_EQ(cvc5_term_get_real_value(real5), std::string("127/10"));
638 : :
639 : 73 : cvc5_term_get_real64_value(real6, &num64, &den64);
640 [ - + ][ + - ]: 73 : ASSERT_EQ(num64, 1);
641 [ - + ][ + - ]: 73 : ASSERT_EQ(den64, 4294967297);
642 [ - + ][ + - ]: 73 : ASSERT_EQ(cvc5_term_get_real_value(real6), std::string("1/4294967297"));
643 : :
644 : 73 : cvc5_term_get_real64_value(real7, &num64, &den64);
645 [ - + ][ + - ]: 73 : ASSERT_EQ(num64, 4294967297);
646 [ - + ][ + - ]: 73 : ASSERT_EQ(den64, 1);
647 [ - + ][ + - ]: 73 : ASSERT_EQ(cvc5_term_get_real_value(real7), std::string("4294967297/1"));
648 : :
649 [ - + ]: 73 : ASSERT_EQ(cvc5_term_get_real_value(real8),
650 [ + - ]: 73 : std::string("1/18446744073709551617"));
651 : :
652 [ - + ]: 73 : ASSERT_EQ(cvc5_term_get_real_value(real9),
653 [ + - ]: 73 : std::string("18446744073709551617/1"));
654 : :
655 [ - + ][ + - ]: 73 : ASSERT_EQ(cvc5_term_get_real_value(real10), std::string("23432343/10000"));
656 : : }
657 : :
658 : 284 : TEST_F(TestCApiBlackTerm, get_const_array_base)
659 : : {
660 : 73 : Cvc5Sort arr_sort = cvc5_mk_array_sort(d_tm, d_int, d_int);
661 : 73 : Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1);
662 : 73 : Cvc5Term const_arr = cvc5_mk_const_array(d_tm, arr_sort, one);
663 : :
664 : 73 : ASSERT_DEATH(cvc5_term_is_const_array(nullptr), "invalid term");
665 : 72 : ASSERT_DEATH(cvc5_term_get_const_array_base(nullptr), "invalid term");
666 : :
667 [ - + ][ + - ]: 71 : ASSERT_TRUE(cvc5_term_is_const_array(const_arr));
668 [ - + ]: 71 : ASSERT_TRUE(
669 [ + - ]: 71 : cvc5_term_is_equal(cvc5_term_get_const_array_base(const_arr), one));
670 : :
671 : 71 : Cvc5Term a = cvc5_mk_const(d_tm, arr_sort, "a");
672 : 71 : ASSERT_DEATH(cvc5_term_get_const_array_base(a), "invalid argument");
673 : 70 : ASSERT_DEATH(cvc5_term_get_const_array_base(one), "invalid argument");
674 : : }
675 : :
676 : 272 : TEST_F(TestCApiBlackTerm, get_boolean_value)
677 : : {
678 : 69 : Cvc5Term b1 = cvc5_mk_true(d_tm);
679 : 69 : Cvc5Term b2 = cvc5_mk_false(d_tm);
680 : :
681 : 69 : ASSERT_DEATH(cvc5_term_is_boolean_value(nullptr), "invalid term");
682 : 68 : ASSERT_DEATH(cvc5_term_get_boolean_value(nullptr), "invalid term");
683 [ - + ][ + - ]: 67 : ASSERT_TRUE(cvc5_term_is_boolean_value(b1));
684 [ - + ][ + - ]: 67 : ASSERT_TRUE(cvc5_term_is_boolean_value(b2));
685 [ - + ][ + - ]: 67 : ASSERT_TRUE(cvc5_term_get_boolean_value(b1));
686 [ - + ][ + - ]: 67 : ASSERT_FALSE(cvc5_term_get_boolean_value(b2));
687 : : }
688 : :
689 : 264 : TEST_F(TestCApiBlackTerm, get_bv_value)
690 : : {
691 : 67 : ASSERT_DEATH(cvc5_mk_bv_uint64(nullptr, 8, 15), "unexpected NULL argument");
692 : 66 : ASSERT_DEATH(cvc5_term_is_bv_value(nullptr), "invalid term");
693 : :
694 : 65 : Cvc5Term b1 = cvc5_mk_bv_uint64(d_tm, 8, 15);
695 : 65 : Cvc5Term b2 = cvc5_mk_bv(d_tm, 8, "00001111", 2);
696 : 65 : Cvc5Term b3 = cvc5_mk_bv(d_tm, 8, "15", 10);
697 : 65 : Cvc5Term b4 = cvc5_mk_bv(d_tm, 8, "0f", 16);
698 : 65 : Cvc5Term b5 = cvc5_mk_bv(d_tm, 9, "00001111", 2);
699 : 65 : Cvc5Term b6 = cvc5_mk_bv(d_tm, 9, "15", 10);
700 : 65 : Cvc5Term b7 = cvc5_mk_bv(d_tm, 9, "0f", 16);
701 : :
702 [ - + ][ + - ]: 65 : ASSERT_TRUE(cvc5_term_is_bv_value(b1));
703 [ - + ][ + - ]: 65 : ASSERT_TRUE(cvc5_term_is_bv_value(b2));
704 [ - + ][ + - ]: 65 : ASSERT_TRUE(cvc5_term_is_bv_value(b3));
705 [ - + ][ + - ]: 65 : ASSERT_TRUE(cvc5_term_is_bv_value(b4));
706 [ - + ][ + - ]: 65 : ASSERT_TRUE(cvc5_term_is_bv_value(b5));
707 [ - + ][ + - ]: 65 : ASSERT_TRUE(cvc5_term_is_bv_value(b6));
708 [ - + ][ + - ]: 65 : ASSERT_TRUE(cvc5_term_is_bv_value(b7));
709 : :
710 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("00001111"), cvc5_term_get_bv_value(b1, 2));
711 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("15"), cvc5_term_get_bv_value(b1, 10));
712 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("f"), cvc5_term_get_bv_value(b1, 16));
713 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("00001111"), cvc5_term_get_bv_value(b2, 2));
714 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("15"), cvc5_term_get_bv_value(b2, 10));
715 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("f"), cvc5_term_get_bv_value(b2, 16));
716 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("00001111"), cvc5_term_get_bv_value(b3, 2));
717 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("15"), cvc5_term_get_bv_value(b3, 10));
718 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("f"), cvc5_term_get_bv_value(b3, 16));
719 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("00001111"), cvc5_term_get_bv_value(b4, 2));
720 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("15"), cvc5_term_get_bv_value(b4, 10));
721 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("f"), cvc5_term_get_bv_value(b4, 16));
722 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("000001111"), cvc5_term_get_bv_value(b5, 2));
723 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("15"), cvc5_term_get_bv_value(b5, 10));
724 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("f"), cvc5_term_get_bv_value(b5, 16));
725 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("000001111"), cvc5_term_get_bv_value(b6, 2));
726 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("15"), cvc5_term_get_bv_value(b6, 10));
727 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("f"), cvc5_term_get_bv_value(b6, 16));
728 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("000001111"), cvc5_term_get_bv_value(b7, 2));
729 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("15"), cvc5_term_get_bv_value(b7, 10));
730 [ - + ][ + - ]: 130 : ASSERT_EQ(std::string("f"), cvc5_term_get_bv_value(b7, 16));
731 : : }
732 : :
733 : 258 : TEST_F(TestCApiBlackTerm, is_ff_value)
734 : : {
735 : 65 : ASSERT_DEATH(cvc5_term_is_ff_value(nullptr), "invalid term");
736 : 64 : Cvc5Sort fs = cvc5_mk_ff_sort(d_tm, "7", 10);
737 : 64 : Cvc5Term fv = cvc5_mk_ff_elem(d_tm, "1", fs, 10);
738 [ - + ][ + - ]: 64 : ASSERT_TRUE(cvc5_term_is_ff_value(fv));
739 : 64 : Cvc5Term b1 = cvc5_mk_bv_uint64(d_tm, 8, 15);
740 [ - + ][ + - ]: 64 : ASSERT_FALSE(cvc5_term_is_ff_value(b1));
741 : : }
742 : :
743 : 252 : TEST_F(TestCApiBlackTerm, get_ff_value)
744 : : {
745 : 64 : ASSERT_DEATH(cvc5_term_get_ff_value(nullptr), "invalid term");
746 : 63 : Cvc5Sort fs = cvc5_mk_ff_sort(d_tm, "7", 10);
747 : 63 : Cvc5Term fv = cvc5_mk_ff_elem(d_tm, "1", fs, 10);
748 [ - + ][ + - ]: 126 : ASSERT_EQ(std::string("1"), cvc5_term_get_ff_value(fv));
749 : 63 : Cvc5Term b1 = cvc5_mk_bv_uint64(d_tm, 8, 15);
750 : 63 : ASSERT_DEATH(cvc5_term_get_ff_value(b1),
751 : : "expected Term to be a finite field value");
752 : : }
753 : :
754 : 246 : TEST_F(TestCApiBlackTerm, get_uninterpreted_sort_value)
755 : : {
756 : 62 : ASSERT_DEATH(cvc5_term_get_uninterpreted_sort_value(nullptr), "invalid term");
757 : 61 : cvc5_set_option(d_solver, "produce-models", "true");
758 : 61 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
759 : 61 : Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y");
760 : 61 : std::vector<Cvc5Term> args = {x, y};
761 : 61 : cvc5_assert_formula(
762 : 61 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
763 : 61 : Cvc5Result res = cvc5_check_sat(d_solver);
764 [ - + ][ + - ]: 61 : ASSERT_TRUE(cvc5_result_is_sat(res));
765 : 61 : Cvc5Term vx = cvc5_get_value(d_solver, x);
766 : 61 : Cvc5Term vy = cvc5_get_value(d_solver, y);
767 [ - + ][ + - ]: 61 : ASSERT_TRUE(cvc5_term_is_uninterpreted_sort_value(vx));
768 [ - + ][ + - ]: 61 : ASSERT_TRUE(cvc5_term_is_uninterpreted_sort_value(vy));
769 [ - + ]: 122 : ASSERT_EQ(std::string(cvc5_term_get_uninterpreted_sort_value(vx)),
770 [ + - ]: 61 : cvc5_term_get_uninterpreted_sort_value(vy));
771 : : }
772 : :
773 : 242 : TEST_F(TestCApiBlackTerm, is_rm_value)
774 : : {
775 : 61 : ASSERT_DEATH(cvc5_term_is_rm_value(nullptr), "invalid term");
776 [ - + ][ + - ]: 60 : ASSERT_FALSE(cvc5_term_is_rm_value(cvc5_mk_integer_int64(d_tm, 15)));
777 [ - + ]: 60 : ASSERT_TRUE(cvc5_term_is_rm_value(
778 [ + - ]: 60 : cvc5_mk_rm(d_tm, CVC5_RM_ROUND_NEAREST_TIES_TO_EVEN)));
779 [ - + ]: 60 : ASSERT_FALSE(
780 [ + - ]: 60 : cvc5_term_is_rm_value(cvc5_mk_const(d_tm, cvc5_get_rm_sort(d_tm), "")));
781 : : }
782 : :
783 : 236 : TEST_F(TestCApiBlackTerm, get_rm_value)
784 : : {
785 : 60 : ASSERT_DEATH(cvc5_term_get_rm_value(nullptr), "invalid term");
786 : 59 : ASSERT_DEATH(cvc5_term_get_rm_value(cvc5_mk_integer_int64(d_tm, 15)),
787 : : "invalid argument");
788 : :
789 [ - + ]: 58 : ASSERT_EQ(cvc5_term_get_rm_value(
790 : : cvc5_mk_rm(d_tm, CVC5_RM_ROUND_NEAREST_TIES_TO_EVEN)),
791 [ + - ]: 58 : CVC5_RM_ROUND_NEAREST_TIES_TO_EVEN);
792 [ - + ]: 58 : ASSERT_EQ(cvc5_term_get_rm_value(
793 : : cvc5_mk_rm(d_tm, CVC5_RM_ROUND_NEAREST_TIES_TO_AWAY)),
794 [ + - ]: 58 : CVC5_RM_ROUND_NEAREST_TIES_TO_AWAY);
795 [ - + ]: 58 : ASSERT_EQ(
796 : : cvc5_term_get_rm_value(cvc5_mk_rm(d_tm, CVC5_RM_ROUND_TOWARD_POSITIVE)),
797 [ + - ]: 58 : CVC5_RM_ROUND_TOWARD_POSITIVE);
798 [ - + ]: 58 : ASSERT_EQ(
799 : : cvc5_term_get_rm_value(cvc5_mk_rm(d_tm, CVC5_RM_ROUND_TOWARD_NEGATIVE)),
800 [ + - ]: 58 : CVC5_RM_ROUND_TOWARD_NEGATIVE);
801 [ - + ]: 58 : ASSERT_EQ(cvc5_term_get_rm_value(cvc5_mk_rm(d_tm, CVC5_RM_ROUND_TOWARD_ZERO)),
802 [ + - ]: 58 : CVC5_RM_ROUND_TOWARD_ZERO);
803 : : }
804 : :
805 : 226 : TEST_F(TestCApiBlackTerm, get_tuple)
806 : : {
807 : 58 : Cvc5Term t1 = cvc5_mk_integer_int64(d_tm, 15);
808 : 58 : Cvc5Term t2 = cvc5_mk_real_num_den(d_tm, 17, 25);
809 : 58 : Cvc5Term t3 = cvc5_mk_string(d_tm, "abc", false);
810 : 58 : std::vector<Cvc5Term> args = {t1, t2, t3};
811 : 58 : Cvc5Term tup = cvc5_mk_tuple(d_tm, args.size(), args.data());
812 : :
813 : : size_t size;
814 : 58 : ASSERT_DEATH(cvc5_term_get_tuple_value(nullptr, &size), "invalid term");
815 : 57 : ASSERT_DEATH(cvc5_term_get_tuple_value(tup, nullptr),
816 : : "unexpected NULL argument");
817 : 56 : ASSERT_DEATH(cvc5_term_is_tuple_value(nullptr), "invalid term");
818 : :
819 [ - + ][ + - ]: 55 : ASSERT_TRUE(cvc5_term_is_tuple_value(tup));
820 : 55 : const Cvc5Term* val = cvc5_term_get_tuple_value(tup, &size);
821 [ - + ][ + - ]: 55 : ASSERT_EQ(size, 3);
822 [ - + ][ + - ]: 55 : ASSERT_TRUE(cvc5_term_is_equal(val[0], t1));
823 [ - + ][ + - ]: 55 : ASSERT_TRUE(cvc5_term_is_equal(val[1], t2));
824 [ - + ][ + - ]: 55 : ASSERT_TRUE(cvc5_term_is_equal(val[2], t3));
825 [ + - ]: 55 : }
826 : :
827 : 200 : TEST_F(TestCApiBlackTerm, get_fp_value)
828 : : {
829 : : uint32_t ew, sw;
830 : : Cvc5Term res;
831 : 55 : Cvc5Term bv_val = cvc5_mk_bv(d_tm, 16, "0000110000000011", 2);
832 : 55 : Cvc5Term fp_val = cvc5_mk_fp(d_tm, 5, 11, bv_val);
833 : :
834 : 55 : ASSERT_DEATH(cvc5_term_is_fp_value(nullptr), "invalid term");
835 : 54 : ASSERT_DEATH(cvc5_term_is_fp_pos_zero(nullptr), "invalid term");
836 : 53 : ASSERT_DEATH(cvc5_term_is_fp_neg_zero(nullptr), "invalid term");
837 : 52 : ASSERT_DEATH(cvc5_term_is_fp_pos_inf(nullptr), "invalid term");
838 : 51 : ASSERT_DEATH(cvc5_term_is_fp_neg_inf(nullptr), "invalid term");
839 : 50 : ASSERT_DEATH(cvc5_term_is_fp_nan(nullptr), "invalid term");
840 : 49 : ASSERT_DEATH(cvc5_term_get_fp_value(nullptr, &ew, &sw, &res), "invalid term");
841 : 48 : ASSERT_DEATH(cvc5_term_get_fp_value(fp_val, nullptr, &sw, &res),
842 : : "unexpected NULL argument");
843 : 47 : ASSERT_DEATH(cvc5_term_get_fp_value(fp_val, &ew, nullptr, &res),
844 : : "unexpected NULL argument");
845 : 46 : ASSERT_DEATH(cvc5_term_get_fp_value(fp_val, &ew, &sw, nullptr),
846 : : "unexpected NULL argument");
847 : :
848 [ - + ][ + - ]: 45 : ASSERT_TRUE(cvc5_term_is_fp_value(fp_val));
849 [ - + ][ + - ]: 45 : ASSERT_FALSE(cvc5_term_is_fp_pos_zero(fp_val));
850 [ - + ][ + - ]: 45 : ASSERT_FALSE(cvc5_term_is_fp_neg_zero(fp_val));
851 [ - + ][ + - ]: 45 : ASSERT_FALSE(cvc5_term_is_fp_pos_inf(fp_val));
852 [ - + ][ + - ]: 45 : ASSERT_FALSE(cvc5_term_is_fp_neg_inf(fp_val));
853 [ - + ][ + - ]: 45 : ASSERT_FALSE(cvc5_term_is_fp_nan(fp_val));
854 : :
855 : 45 : cvc5_term_get_fp_value(fp_val, &ew, &sw, &res);
856 [ - + ][ + - ]: 45 : ASSERT_EQ(ew, 5u);
857 [ - + ][ + - ]: 45 : ASSERT_EQ(sw, 11u);
858 [ - + ][ + - ]: 45 : ASSERT_TRUE(cvc5_term_is_equal(bv_val, res));
859 : :
860 [ - + ][ + - ]: 45 : ASSERT_TRUE(cvc5_term_is_fp_pos_zero(cvc5_mk_fp_pos_zero(d_tm, 5, 11)));
861 [ - + ][ + - ]: 45 : ASSERT_TRUE(cvc5_term_is_fp_neg_zero(cvc5_mk_fp_neg_zero(d_tm, 5, 11)));
862 [ - + ][ + - ]: 45 : ASSERT_TRUE(cvc5_term_is_fp_pos_inf(cvc5_mk_fp_pos_inf(d_tm, 5, 11)));
863 [ - + ][ + - ]: 45 : ASSERT_TRUE(cvc5_term_is_fp_neg_inf(cvc5_mk_fp_neg_inf(d_tm, 5, 11)));
864 [ - + ][ + - ]: 45 : ASSERT_TRUE(cvc5_term_is_fp_nan(cvc5_mk_fp_nan(d_tm, 5, 11)));
865 : : }
866 : :
867 : 174 : TEST_F(TestCApiBlackTerm, get_set_value)
868 : : {
869 : 45 : Cvc5Sort s = cvc5_mk_set_sort(d_tm, d_int);
870 : :
871 : 45 : Cvc5Term i1 = cvc5_mk_integer_int64(d_tm, 5);
872 : 45 : Cvc5Term i2 = cvc5_mk_integer_int64(d_tm, 7);
873 : :
874 : 45 : Cvc5Term s1 = cvc5_mk_empty_set(d_tm, s);
875 : 45 : std::vector<Cvc5Term> args = {i1};
876 : : Cvc5Term s2 =
877 : 45 : cvc5_mk_term(d_tm, CVC5_KIND_SET_SINGLETON, args.size(), args.data());
878 : : Cvc5Term s3 =
879 : 45 : cvc5_mk_term(d_tm, CVC5_KIND_SET_SINGLETON, args.size(), args.data());
880 : 45 : args = {i2};
881 : : Cvc5Term s4 =
882 : 45 : cvc5_mk_term(d_tm, CVC5_KIND_SET_SINGLETON, args.size(), args.data());
883 : 45 : args = {s3, s4};
884 : 0 : args = {s2,
885 : 45 : cvc5_mk_term(d_tm, CVC5_KIND_SET_UNION, args.size(), args.data())};
886 : : Cvc5Term s5 =
887 : 45 : cvc5_mk_term(d_tm, CVC5_KIND_SET_UNION, args.size(), args.data());
888 : :
889 : 45 : ASSERT_DEATH(cvc5_term_is_set_value(nullptr), "invalid term");
890 [ - + ][ + - ]: 44 : ASSERT_TRUE(cvc5_term_is_set_value(s1));
891 [ - + ][ + - ]: 44 : ASSERT_TRUE(cvc5_term_is_set_value(s2));
892 [ - + ][ + - ]: 44 : ASSERT_TRUE(cvc5_term_is_set_value(s3));
893 [ - + ][ + - ]: 44 : ASSERT_TRUE(cvc5_term_is_set_value(s4));
894 [ - + ][ + - ]: 44 : ASSERT_FALSE(cvc5_term_is_set_value(s5));
895 : 44 : s5 = cvc5_simplify(d_solver, s5, false);
896 [ - + ][ + - ]: 44 : ASSERT_TRUE(cvc5_term_is_set_value(s5));
897 : :
898 : : size_t size;
899 : 44 : ASSERT_DEATH(cvc5_term_get_set_value(nullptr, &size), "invalid term");
900 : 43 : ASSERT_DEATH(cvc5_term_get_set_value(s1, nullptr),
901 : : "unexpected NULL argument");
902 : 42 : (void)cvc5_term_get_set_value(s1, &size);
903 [ - + ][ + - ]: 42 : ASSERT_EQ(size, 0);
904 : 42 : const Cvc5Term* res2 = cvc5_term_get_set_value(s2, &size);
905 [ - + ][ + - ]: 42 : ASSERT_EQ(size, 1);
906 [ - + ][ + - ]: 42 : ASSERT_TRUE(cvc5_term_is_equal(res2[0], i1));
907 : 42 : const Cvc5Term* res3 = cvc5_term_get_set_value(s3, &size);
908 [ - + ][ + - ]: 42 : ASSERT_EQ(size, 1);
909 [ - + ][ + - ]: 42 : ASSERT_TRUE(cvc5_term_is_equal(res3[0], i1));
910 : 42 : const Cvc5Term* res4 = cvc5_term_get_set_value(s4, &size);
911 [ - + ][ + - ]: 42 : ASSERT_EQ(size, 1);
912 [ - + ][ + - ]: 42 : ASSERT_TRUE(cvc5_term_is_equal(res4[0], i2));
913 : 42 : const Cvc5Term* res5 = cvc5_term_get_set_value(s5, &size);
914 [ - + ][ + - ]: 42 : ASSERT_EQ(size, 2);
915 [ - + ][ + - ]: 42 : ASSERT_TRUE(cvc5_term_is_equal(res5[0], i1));
916 [ - + ][ + - ]: 42 : ASSERT_TRUE(cvc5_term_is_equal(res5[1], i2));
917 [ + - ]: 42 : }
918 : :
919 : 156 : TEST_F(TestCApiBlackTerm, get_sequence_value)
920 : : {
921 : 42 : Cvc5Sort seq_sort = cvc5_mk_sequence_sort(d_tm, d_int);
922 : :
923 : 42 : Cvc5Term i1 = cvc5_mk_integer_int64(d_tm, 5);
924 : 42 : Cvc5Term i2 = cvc5_mk_integer_int64(d_tm, 7);
925 : :
926 : 42 : Cvc5Term s1 = cvc5_mk_empty_sequence(d_tm, seq_sort);
927 : 42 : std::vector<Cvc5Term> args = {i1};
928 : : Cvc5Term s2 =
929 : 42 : cvc5_mk_term(d_tm, CVC5_KIND_SEQ_UNIT, args.size(), args.data());
930 : : Cvc5Term s3 =
931 : 42 : cvc5_mk_term(d_tm, CVC5_KIND_SEQ_UNIT, args.size(), args.data());
932 : 42 : args = {i2};
933 : : Cvc5Term s4 =
934 : 42 : cvc5_mk_term(d_tm, CVC5_KIND_SEQ_UNIT, args.size(), args.data());
935 : 42 : args = {s3, s4};
936 : 0 : args = {s2,
937 : 42 : cvc5_mk_term(d_tm, CVC5_KIND_SEQ_CONCAT, args.size(), args.data())};
938 : : Cvc5Term s5 =
939 : 42 : cvc5_mk_term(d_tm, CVC5_KIND_SEQ_CONCAT, args.size(), args.data());
940 : :
941 : 42 : ASSERT_DEATH(cvc5_mk_empty_sequence(nullptr, seq_sort),
942 : : "unexpected NULL argument");
943 : 41 : ASSERT_DEATH(cvc5_mk_empty_sequence(d_tm, nullptr), "invalid sort");
944 : 40 : ASSERT_DEATH(cvc5_term_is_sequence_value(nullptr), "invalid term");
945 : :
946 [ - + ][ + - ]: 39 : ASSERT_TRUE(cvc5_term_is_sequence_value(s1));
947 [ - + ][ + - ]: 39 : ASSERT_FALSE(cvc5_term_is_sequence_value(s2));
948 [ - + ][ + - ]: 39 : ASSERT_FALSE(cvc5_term_is_sequence_value(s3));
949 [ - + ][ + - ]: 39 : ASSERT_FALSE(cvc5_term_is_sequence_value(s4));
950 [ - + ][ + - ]: 39 : ASSERT_FALSE(cvc5_term_is_sequence_value(s5));
951 : 39 : s2 = cvc5_simplify(d_solver, s2, false);
952 [ - + ][ + - ]: 39 : ASSERT_TRUE(cvc5_term_is_sequence_value(s2));
953 : 39 : s3 = cvc5_simplify(d_solver, s3, false);
954 [ - + ][ + - ]: 39 : ASSERT_TRUE(cvc5_term_is_sequence_value(s3));
955 : 39 : s4 = cvc5_simplify(d_solver, s4, false);
956 [ - + ][ + - ]: 39 : ASSERT_TRUE(cvc5_term_is_sequence_value(s4));
957 : 39 : s5 = cvc5_simplify(d_solver, s5, false);
958 [ - + ][ + - ]: 39 : ASSERT_TRUE(cvc5_term_is_sequence_value(s5));
959 : :
960 : : size_t size;
961 : 39 : ASSERT_DEATH(cvc5_term_get_sequence_value(nullptr, &size), "invalid term");
962 : 38 : ASSERT_DEATH(cvc5_term_get_sequence_value(s1, nullptr),
963 : : "unexpected NULL argument");
964 : 37 : (void)cvc5_term_get_sequence_value(s1, &size);
965 [ - + ][ + - ]: 37 : ASSERT_EQ(size, 0);
966 : 37 : const Cvc5Term* res2 = cvc5_term_get_sequence_value(s2, &size);
967 [ - + ][ + - ]: 37 : ASSERT_EQ(size, 1);
968 [ - + ][ + - ]: 37 : ASSERT_TRUE(cvc5_term_is_equal(res2[0], i1));
969 : 37 : const Cvc5Term* res3 = cvc5_term_get_sequence_value(s3, &size);
970 [ - + ][ + - ]: 37 : ASSERT_EQ(size, 1);
971 [ - + ][ + - ]: 37 : ASSERT_TRUE(cvc5_term_is_equal(res3[0], i1));
972 : 37 : const Cvc5Term* res4 = cvc5_term_get_sequence_value(s4, &size);
973 [ - + ][ + - ]: 37 : ASSERT_EQ(size, 1);
974 [ - + ][ + - ]: 37 : ASSERT_TRUE(cvc5_term_is_equal(res4[0], i2));
975 : 37 : const Cvc5Term* res5 = cvc5_term_get_sequence_value(s5, &size);
976 [ - + ][ + - ]: 37 : ASSERT_EQ(size, 3);
977 [ - + ][ + - ]: 37 : ASSERT_TRUE(cvc5_term_is_equal(res5[0], i1));
978 [ - + ][ + - ]: 37 : ASSERT_TRUE(cvc5_term_is_equal(res5[1], i1));
979 [ - + ][ + - ]: 37 : ASSERT_TRUE(cvc5_term_is_equal(res5[2], i2));
980 : :
981 : 37 : seq_sort = cvc5_mk_sequence_sort(d_tm, d_real);
982 : 37 : Cvc5Term s = cvc5_mk_empty_sequence(d_tm, seq_sort);
983 [ - + ][ + - ]: 37 : ASSERT_EQ(cvc5_term_get_kind(s), CVC5_KIND_CONST_SEQUENCE);
984 : : // empty sequence has zero elements
985 : 37 : (void)cvc5_term_get_sequence_value(s, &size);
986 [ - + ][ + - ]: 37 : ASSERT_EQ(size, 0);
987 : :
988 : : // A seq.unit app is not a constant sequence (regardless of whether it is
989 : : // applied to a constant).
990 : 37 : args = {cvc5_mk_real_int64(d_tm, 1)};
991 : : Cvc5Term su =
992 : 37 : cvc5_mk_term(d_tm, CVC5_KIND_SEQ_UNIT, args.size(), args.data());
993 : 37 : ASSERT_DEATH(cvc5_term_get_sequence_value(su, &size), "invalid argument");
994 [ + - ]: 36 : }
995 : :
996 : 126 : TEST_F(TestCApiBlackTerm, substitute)
997 : : {
998 : 36 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
999 : 36 : Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1);
1000 : 36 : Cvc5Term ttrue = cvc5_mk_true(d_tm);
1001 : 36 : std::vector<Cvc5Term> args = {x, x};
1002 : 36 : Cvc5Term xpx = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
1003 : 36 : args = {one, one};
1004 : : Cvc5Term onepone =
1005 : 36 : cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
1006 : :
1007 : 36 : ASSERT_DEATH(cvc5_term_substitute_term(nullptr, x, one), "invalid term");
1008 : 35 : ASSERT_DEATH(cvc5_term_substitute_term(xpx, nullptr, one), "invalid term");
1009 : 34 : ASSERT_DEATH(cvc5_term_substitute_term(xpx, x, nullptr), "invalid term");
1010 : :
1011 [ - + ]: 33 : ASSERT_TRUE(
1012 [ + - ]: 33 : cvc5_term_is_equal(cvc5_term_substitute_term(xpx, x, one), onepone));
1013 : : // incorrect due to type
1014 : 33 : ASSERT_DEATH(cvc5_term_substitute_term(xpx, one, ttrue),
1015 : : "expected terms of the same sort");
1016 : :
1017 : : // simultaneous substitution
1018 : 32 : Cvc5Term y = cvc5_mk_const(d_tm, d_int, "y");
1019 : 32 : args = {x, y};
1020 : 32 : Cvc5Term xpy = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
1021 : 32 : args = {y, one};
1022 : 32 : Cvc5Term xpone = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
1023 : 32 : std::vector<Cvc5Term> es = {x, y};
1024 : 32 : std::vector<Cvc5Term> rs = {y, one};
1025 [ - + ]: 32 : ASSERT_EQ(cvc5_term_substitute_terms(xpy, es.size(), es.data(), rs.data()),
1026 [ + - ]: 32 : xpone);
1027 : :
1028 : : // incorrect substitution due to types
1029 : 32 : rs[1] = ttrue;
1030 : 32 : ASSERT_DEATH(cvc5_term_substitute_terms(xpy, es.size(), es.data(), rs.data()),
1031 : : "expecting terms of the same sort at index 1");
1032 : :
1033 : : // null cannot substitute
1034 : 31 : es = {nullptr, y};
1035 : 31 : rs = {y, one};
1036 : 31 : ASSERT_DEATH(cvc5_term_substitute_terms(xpy, es.size(), es.data(), rs.data()),
1037 : : "invalid term at index 0");
1038 : 30 : es = {x, nullptr};
1039 : 30 : ASSERT_DEATH(cvc5_term_substitute_terms(xpy, es.size(), es.data(), rs.data()),
1040 : : "invalid term at index 1");
1041 : 29 : es = {x, y};
1042 : 29 : rs = {nullptr, one};
1043 : 29 : ASSERT_DEATH(cvc5_term_substitute_terms(xpy, es.size(), es.data(), rs.data()),
1044 : : "invalid term at index 0");
1045 : 28 : rs = {y, nullptr};
1046 : 28 : ASSERT_DEATH(cvc5_term_substitute_terms(xpy, es.size(), es.data(), rs.data()),
1047 : : "invalid term at index 1");
1048 [ + - ]: 27 : }
1049 : :
1050 : 94 : TEST_F(TestCApiBlackTerm, const_array)
1051 : : {
1052 : 27 : Cvc5Sort arr_sort = cvc5_mk_array_sort(d_tm, d_int, d_int);
1053 : 27 : Cvc5Term a = cvc5_mk_const(d_tm, arr_sort, "a");
1054 : 27 : Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1);
1055 : 27 : Cvc5Term two = cvc5_mk_bv_uint64(d_tm, 2, 2);
1056 : 27 : Cvc5Term i = cvc5_mk_const(d_tm, d_int, "i");
1057 : 27 : Cvc5Term const_arr = cvc5_mk_const_array(d_tm, arr_sort, one);
1058 : :
1059 : 27 : ASSERT_DEATH(cvc5_mk_const_array(nullptr, arr_sort, one),
1060 : : "unexpected NULL argument");
1061 : 26 : ASSERT_DEATH(cvc5_mk_const_array(d_tm, nullptr, one), "invalid sort");
1062 : 25 : ASSERT_DEATH(cvc5_mk_const_array(d_tm, arr_sort, nullptr), "invalid term");
1063 : 24 : ASSERT_DEATH(cvc5_mk_const_array(d_tm, arr_sort, two),
1064 : : "value does not match element sort");
1065 : 23 : ASSERT_DEATH(cvc5_mk_const_array(d_tm, arr_sort, i), "invalid argument");
1066 : :
1067 : 22 : ASSERT_DEATH(cvc5_term_get_const_array_base(nullptr), "invalid term");
1068 : :
1069 [ - + ][ + - ]: 21 : ASSERT_EQ(cvc5_term_get_kind(const_arr), CVC5_KIND_CONST_ARRAY);
1070 [ - + ]: 21 : ASSERT_TRUE(
1071 [ + - ]: 21 : cvc5_term_is_equal(cvc5_term_get_const_array_base(const_arr), one));
1072 : 21 : ASSERT_DEATH(cvc5_term_get_const_array_base(a), "invalid argument");
1073 : :
1074 : 20 : arr_sort = cvc5_mk_array_sort(d_tm, d_real, d_real);
1075 : : Cvc5Term zero_array =
1076 : 20 : cvc5_mk_const_array(d_tm, arr_sort, cvc5_mk_real_int64(d_tm, 0));
1077 : : std::vector<Cvc5Term> args = {
1078 : 20 : zero_array, cvc5_mk_real_int64(d_tm, 1), cvc5_mk_real_int64(d_tm, 2)};
1079 : : Cvc5Term stores =
1080 : 20 : cvc5_mk_term(d_tm, CVC5_KIND_STORE, args.size(), args.data());
1081 : 20 : args = {stores, cvc5_mk_real_int64(d_tm, 2), cvc5_mk_real_int64(d_tm, 3)};
1082 : 20 : stores = cvc5_mk_term(d_tm, CVC5_KIND_STORE, args.size(), args.data());
1083 : 20 : args = {stores, cvc5_mk_real_int64(d_tm, 4), cvc5_mk_real_int64(d_tm, 5)};
1084 : 20 : stores = cvc5_mk_term(d_tm, CVC5_KIND_STORE, args.size(), args.data());
1085 : : }
1086 : :
1087 : 66 : TEST_F(TestCApiBlackTerm, get_cardinality_constraint)
1088 : : {
1089 : 20 : ASSERT_DEATH(cvc5_mk_cardinality_constraint(nullptr, d_uninterpreted, 3),
1090 : : "unexpected NULL argument");
1091 : 19 : ASSERT_DEATH(cvc5_mk_cardinality_constraint(d_tm, nullptr, 3),
1092 : : "invalid sort");
1093 : 18 : ASSERT_DEATH(cvc5_term_is_cardinality_constraint(nullptr), "invalid term");
1094 : :
1095 : 17 : Cvc5Term t = cvc5_mk_cardinality_constraint(d_tm, d_uninterpreted, 3);
1096 [ - + ][ + - ]: 17 : ASSERT_TRUE(cvc5_term_is_cardinality_constraint(t));
1097 : :
1098 : : Cvc5Sort res;
1099 : : uint32_t res_upper;
1100 : 17 : ASSERT_DEATH(cvc5_term_get_cardinality_constraint(nullptr, &res, &res_upper),
1101 : : "invalid term");
1102 : 16 : ASSERT_DEATH(cvc5_term_get_cardinality_constraint(t, nullptr, &res_upper),
1103 : : "unexpected NULL argument");
1104 : 15 : ASSERT_DEATH(cvc5_term_get_cardinality_constraint(t, &res, nullptr),
1105 : : "unexpected NULL argument");
1106 : :
1107 : 14 : cvc5_term_get_cardinality_constraint(t, &res, &res_upper);
1108 [ - + ][ + - ]: 14 : ASSERT_TRUE(cvc5_sort_is_equal(res, d_uninterpreted));
1109 [ - + ][ + - ]: 14 : ASSERT_EQ(res_upper, 3);
1110 : :
1111 : 14 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
1112 [ - + ][ + - ]: 14 : ASSERT_FALSE(cvc5_term_is_cardinality_constraint(x));
1113 : 14 : ASSERT_DEATH(cvc5_term_get_cardinality_constraint(x, &res, &res_upper),
1114 : : "invalid argument");
1115 : : }
1116 : :
1117 : 40 : TEST_F(TestCApiBlackTerm, get_real_algebraic_number)
1118 : : {
1119 : 13 : cvc5_set_option(d_solver, "produce-models", "true");
1120 : 13 : cvc5_set_logic(d_solver, "QF_NRA");
1121 : 13 : Cvc5Term x = cvc5_mk_const(d_tm, d_real, "x");
1122 : 13 : Cvc5Term y = cvc5_mk_var(d_tm, d_real, "y");
1123 : 13 : std::vector<Cvc5Term> args = {x, x};
1124 : 13 : Cvc5Term x2 = cvc5_mk_term(d_tm, CVC5_KIND_MULT, args.size(), args.data());
1125 : 13 : Cvc5Term two = cvc5_mk_real_num_den(d_tm, 2, 1);
1126 : 13 : args = {x2, two};
1127 : 13 : Cvc5Term eq = cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
1128 : 13 : cvc5_assert_formula(d_solver, eq);
1129 : :
1130 : 13 : ASSERT_DEATH(cvc5_term_is_real_algebraic_number(nullptr), "invalid term");
1131 : 12 : ASSERT_DEATH(
1132 : : cvc5_term_get_real_algebraic_number_defining_polynomial(nullptr, y),
1133 : : "invalid term");
1134 : 11 : ASSERT_DEATH(
1135 : : cvc5_term_get_real_algebraic_number_defining_polynomial(x, nullptr),
1136 : : "invalid term");
1137 : 10 : ASSERT_DEATH(cvc5_term_get_real_algebraic_number_lower_bound(nullptr),
1138 : : "invalid term");
1139 : 9 : ASSERT_DEATH(cvc5_term_get_real_algebraic_number_upper_bound(nullptr),
1140 : : "invalid term");
1141 : :
1142 : : // Note that check-sat should only return "sat" if libpoly is enabled.
1143 : : // Otherwise, we do not test the following functionality.
1144 [ + - ]: 8 : if (cvc5_result_is_sat(cvc5_check_sat(d_solver)))
1145 : : {
1146 : : // We find a model for (x*x = 2), where x should be a real algebraic number.
1147 : : // We assert that its defining polynomial is non-null and its lower and
1148 : : // upper bounds are real.
1149 : 8 : Cvc5Term vx = cvc5_get_value(d_solver, x);
1150 [ - + ][ + - ]: 8 : ASSERT_TRUE(cvc5_term_is_real_algebraic_number(vx));
1151 : : Cvc5Term poly =
1152 : 8 : cvc5_term_get_real_algebraic_number_defining_polynomial(vx, y);
1153 [ - + ][ + - ]: 8 : ASSERT_NE(poly, nullptr);
1154 : :
1155 : 8 : Cvc5Term lb = cvc5_term_get_real_algebraic_number_lower_bound(vx);
1156 : 8 : Cvc5Term ub = cvc5_term_get_real_algebraic_number_upper_bound(vx);
1157 [ - + ][ + - ]: 8 : ASSERT_TRUE(cvc5_term_is_real_value(lb));
1158 [ - + ][ + - ]: 8 : ASSERT_TRUE(cvc5_term_is_real_value(ub));
1159 : : // cannot call with non-variable
1160 : 8 : Cvc5Term yc = cvc5_mk_const(d_tm, d_real, "y");
1161 : 8 : ASSERT_DEATH(
1162 : : cvc5_term_get_real_algebraic_number_defining_polynomial(vx, yc),
1163 : : "invalid argument");
1164 : : }
1165 [ + - ]: 7 : }
1166 : :
1167 : 16 : TEST_F(TestCApiBlackTerm, get_skolem)
1168 : : {
1169 : : size_t size;
1170 : 7 : ASSERT_DEATH(cvc5_term_is_skolem(nullptr), "invalid term");
1171 : 6 : ASSERT_DEATH(cvc5_term_get_skolem_id(nullptr), "invalid term");
1172 : : // ordinary variables are not skolems
1173 : 5 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
1174 [ - + ][ + - ]: 5 : ASSERT_FALSE(cvc5_term_is_skolem(x));
1175 : 5 : ASSERT_DEATH(cvc5_term_get_skolem_id(x), "invalid argument");
1176 : 4 : ASSERT_DEATH(cvc5_term_get_skolem_indices(x, &size), "invalid argument");
1177 : 3 : ASSERT_DEATH(cvc5_term_get_skolem_indices(nullptr, &size), "invalid term");
1178 : 2 : ASSERT_DEATH(cvc5_term_get_skolem_indices(x, nullptr),
1179 : : "unexpected NULL argument");
1180 : : }
1181 : :
1182 : 4 : TEST_F(TestCApiBlackTerm, term_scoped_to_string)
1183 : : {
1184 : 1 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
1185 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_term_to_string(x), std::string("x"));
1186 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_term_to_string(x), std::string("x"));
1187 : : }
1188 : :
1189 : : } // namespace cvc5::internal::test
|
