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