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