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 solver functions of the C API.
11 : : */
12 : :
13 : : extern "C" {
14 : : #include <cvc5/c/cvc5.h>
15 : : }
16 : :
17 : : #include <cvc5/c/cvc5.h>
18 : :
19 : : #include <cmath>
20 : : #include <fstream>
21 : :
22 : : #include "base/check.h"
23 : : #include "base/output.h"
24 : : #include "gtest/gtest.h"
25 : :
26 : : namespace cvc5::internal::test {
27 : :
28 : : class TestCApiBlackSolver : public ::testing::Test
29 : : {
30 : : protected:
31 : 21609 : void SetUp() override
32 : : {
33 : 21609 : d_tm = cvc5_term_manager_new();
34 : 21609 : d_solver = cvc5_new(d_tm);
35 : 21609 : d_bool = cvc5_get_boolean_sort(d_tm);
36 : 21609 : d_int = cvc5_get_integer_sort(d_tm);
37 : 21609 : d_real = cvc5_get_real_sort(d_tm);
38 : 21609 : d_str = cvc5_get_string_sort(d_tm);
39 : 21609 : d_uninterpreted = cvc5_mk_uninterpreted_sort(d_tm, "u");
40 : 21609 : }
41 : 21283 : void TearDown() override
42 : : {
43 : 21283 : cvc5_delete(d_solver);
44 : 21283 : cvc5_term_manager_delete(d_tm);
45 : 21283 : }
46 : :
47 : : /**
48 : : * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks
49 : : * some simple separation logic constraints.
50 : : */
51 : 674 : void check_simple_separation_constraints()
52 : : {
53 : : // declare the separation heap
54 : 674 : cvc5_declare_sep_heap(d_solver, d_int, d_int);
55 : 674 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
56 : 674 : Cvc5Term p = cvc5_mk_const(d_tm, d_int, "p");
57 : 674 : std::vector<Cvc5Term> args = {p, x};
58 : : Cvc5Term heap =
59 : 674 : cvc5_mk_term(d_tm, CVC5_KIND_SEP_PTO, args.size(), args.data());
60 : 674 : cvc5_assert_formula(d_solver, heap);
61 : 674 : Cvc5Term nil = cvc5_mk_sep_nil(d_tm, d_int);
62 : 674 : args = {nil, cvc5_mk_integer_int64(d_tm, 5)};
63 : 674 : cvc5_assert_formula(
64 : : d_solver,
65 : 674 : cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
66 : 674 : cvc5_check_sat(d_solver);
67 : 674 : }
68 : :
69 : : Cvc5TermManager* d_tm;
70 : : Cvc5* d_solver;
71 : : Cvc5Sort d_bool;
72 : : Cvc5Sort d_int;
73 : : Cvc5Sort d_real;
74 : : Cvc5Sort d_str;
75 : : Cvc5Sort d_uninterpreted;
76 : : };
77 : :
78 : 1306 : TEST_F(TestCApiBlackSolver, pow2_large1)
79 : : {
80 : : // Based on https://github.com/cvc5/cvc5-projects/issues/371
81 : 327 : Cvc5Sort s4 = cvc5_mk_array_sort(d_tm, d_str, d_int);
82 : 327 : Cvc5Sort s7 = cvc5_mk_array_sort(d_tm, d_int, d_str);
83 : 327 : Cvc5Term t10 = cvc5_mk_integer(d_tm, "68038927088685865242724985643");
84 : 327 : Cvc5Term t74 = cvc5_mk_integer(d_tm, "8416288636405");
85 : 327 : Cvc5DatatypeConstructorDecl cons1 = cvc5_mk_dt_cons_decl(d_tm, "_x109");
86 : 327 : cvc5_dt_cons_decl_add_selector(cons1, "_x108", s7);
87 : 327 : Cvc5DatatypeConstructorDecl cons2 = cvc5_mk_dt_cons_decl(d_tm, "_x113");
88 : 327 : cvc5_dt_cons_decl_add_selector(cons2, "_x110", s4);
89 : 327 : cvc5_dt_cons_decl_add_selector(cons2, "_x111", d_int);
90 : 327 : cvc5_dt_cons_decl_add_selector(cons2, "_x112", s7);
91 : 327 : std::vector<Cvc5DatatypeConstructorDecl> ctors = {cons1, cons2};
92 : 327 : Cvc5Sort s11 = cvc5_declare_dt(d_solver, "_x107", ctors.size(), ctors.data());
93 : 327 : Cvc5Term t82 = cvc5_mk_const(d_tm, s11, "_x114");
94 : 327 : std::vector<Cvc5Term> args = {t10};
95 : 327 : Cvc5Term t180 = cvc5_mk_term(d_tm, CVC5_KIND_POW2, args.size(), args.data());
96 : 327 : args = {t74, t180};
97 : 327 : Cvc5Term t258 = cvc5_mk_term(d_tm, CVC5_KIND_GEQ, args.size(), args.data());
98 : 327 : cvc5_assert_formula(d_solver, t258);
99 : 327 : ASSERT_DEATH(cvc5_simplify(d_solver, t82, true),
100 : : "can only be a positive integral constant below");
101 [ + - ][ + - ]: 326 : }
102 : :
103 : 1302 : TEST_F(TestCApiBlackSolver, pow2_large2)
104 : : {
105 : : // Based on https://github.com/cvc5/cvc5-projects/issues/333
106 : 326 : Cvc5Term t1 = cvc5_mk_bv_uint64(d_tm, 63, ~(((uint64_t)1) << 62));
107 : 326 : std::vector<Cvc5Term> args = {t1};
108 : : Cvc5Term t2 =
109 : 326 : cvc5_mk_term(d_tm, CVC5_KIND_BITVECTOR_UBV_TO_INT, args.size(), args.data());
110 : 326 : args = {t2};
111 : 326 : Cvc5Term t3 = cvc5_mk_term(d_tm, CVC5_KIND_POW2, args.size(), args.data());
112 : 326 : args = {t3, t2};
113 : : Cvc5Term t4 =
114 : 326 : cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data());
115 : 326 : std::vector<Cvc5Term> assumptions = {t4};
116 : 326 : ASSERT_DEATH(
117 : : cvc5_check_sat_assuming(d_solver, assumptions.size(), assumptions.data()),
118 : : "can only be a positive integral constant below");
119 [ + - ][ + - ]: 325 : }
120 : :
121 : 1300 : TEST_F(TestCApiBlackSolver, pow2_large3)
122 : : {
123 : : // Based on https://github.com/cvc5/cvc5-projects/issues/339
124 : 325 : Cvc5Term t203 = cvc5_mk_integer(d_tm, "6135470354240554220207");
125 : 325 : std::vector<Cvc5Term> args = {t203};
126 : 325 : Cvc5Term t262 = cvc5_mk_term(d_tm, CVC5_KIND_POW2, args.size(), args.data());
127 : 325 : args = {t262};
128 : 325 : std::vector<uint32_t> idxs = {49};
129 : 650 : Cvc5Term t536 = cvc5_mk_term_from_op(
130 : : d_tm,
131 : 325 : cvc5_mk_op(d_tm, CVC5_KIND_INT_TO_BITVECTOR, idxs.size(), idxs.data()),
132 : : args.size(),
133 : 325 : args.data());
134 : : // should not throw an exception, will not simplify.
135 : 325 : cvc5_simplify(d_solver, t536, false);
136 : 325 : }
137 : :
138 : 1294 : TEST_F(TestCApiBlackSolver, simplify)
139 : : {
140 : 325 : Cvc5Sort bv_sort = cvc5_mk_bv_sort(d_tm, 32);
141 : 325 : std::vector<Cvc5Sort> domain = {bv_sort, bv_sort};
142 : : Cvc5Sort fun_sort1 =
143 : 325 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), bv_sort);
144 : 325 : domain = {d_uninterpreted};
145 : : Cvc5Sort fun_sort2 =
146 : 325 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
147 : :
148 : 325 : Cvc5DatatypeDecl decl = cvc5_mk_dt_decl(d_tm, "list", false);
149 : 325 : Cvc5DatatypeConstructorDecl cons = cvc5_mk_dt_cons_decl(d_tm, "cons");
150 : 325 : cvc5_dt_cons_decl_add_selector(cons, "head", d_int);
151 : 325 : cvc5_dt_cons_decl_add_selector_self(cons, "tail");
152 : 325 : cvc5_dt_decl_add_constructor(decl, cons);
153 : 325 : Cvc5DatatypeConstructorDecl nil = cvc5_mk_dt_cons_decl(d_tm, "nil");
154 : 325 : cvc5_dt_decl_add_constructor(decl, nil);
155 : 325 : Cvc5Sort list = cvc5_mk_dt_sort(d_tm, decl);
156 : :
157 : 325 : Cvc5Term x = cvc5_mk_const(d_tm, bv_sort, "x");
158 : 325 : (void)cvc5_simplify(d_solver, x, false);
159 : :
160 : 325 : ASSERT_DEATH(cvc5_simplify(nullptr, x, false), "unexpected NULL argument");
161 : 324 : ASSERT_DEATH(cvc5_simplify(d_solver, nullptr, false), "invalid term");
162 : :
163 : 323 : Cvc5Term a = cvc5_mk_const(d_tm, bv_sort, "a");
164 : 323 : (void)cvc5_simplify(d_solver, a, false);
165 : 323 : Cvc5Term b = cvc5_mk_const(d_tm, bv_sort, "b");
166 : 323 : (void)cvc5_simplify(d_solver, b, false);
167 : 323 : std::vector<Cvc5Term> args = {x, x};
168 : : Cvc5Term x_eq_x =
169 : 323 : cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
170 : 323 : (void)cvc5_simplify(d_solver, x_eq_x, false);
171 [ - + ][ + - ]: 323 : ASSERT_TRUE(cvc5_term_is_disequal(cvc5_mk_true(d_tm), x_eq_x));
172 [ - + ]: 323 : ASSERT_TRUE(cvc5_term_is_equal(cvc5_mk_true(d_tm),
173 [ + - ]: 323 : cvc5_simplify(d_solver, x_eq_x, false)));
174 : 323 : args = {x, b};
175 : : Cvc5Term x_eq_b =
176 : 323 : cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
177 : 323 : (void)cvc5_simplify(d_solver, x_eq_b, false);
178 [ - + ][ + - ]: 323 : ASSERT_TRUE(cvc5_term_is_disequal(cvc5_mk_true(d_tm), x_eq_b));
179 [ - + ]: 323 : ASSERT_TRUE(cvc5_term_is_disequal(cvc5_mk_true(d_tm),
180 [ + - ]: 323 : cvc5_simplify(d_solver, x_eq_b, false)));
181 : :
182 : 323 : Cvc5Term i1 = cvc5_mk_const(d_tm, d_int, "i1");
183 : 323 : (void)cvc5_simplify(d_solver, i1, false);
184 : 323 : args = {i1, cvc5_mk_integer(d_tm, "23")};
185 : 323 : Cvc5Term i2 = cvc5_mk_term(d_tm, CVC5_KIND_MULT, args.size(), args.data());
186 : 323 : (void)cvc5_simplify(d_solver, i2, false);
187 [ - + ][ + - ]: 323 : ASSERT_TRUE(cvc5_term_is_disequal(i1, i2));
188 [ - + ][ + - ]: 323 : ASSERT_TRUE(cvc5_term_is_disequal(i1, cvc5_simplify(d_solver, i2, false)));
189 : :
190 : 323 : args = {i1, cvc5_mk_integer(d_tm, "0")};
191 : 323 : Cvc5Term i3 = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
192 : 323 : (void)cvc5_simplify(d_solver, i3, false);
193 [ - + ][ + - ]: 323 : ASSERT_TRUE(cvc5_term_is_disequal(i1, i3));
194 [ - + ][ + - ]: 323 : ASSERT_TRUE(cvc5_term_is_equal(i1, cvc5_simplify(d_solver, i3, false)));
195 : :
196 : 323 : Cvc5Datatype list_dt = cvc5_sort_get_datatype(list);
197 : 0 : args = {
198 : 323 : cvc5_dt_cons_get_term(cvc5_dt_get_constructor_by_name(list_dt, "nil"))};
199 : 0 : args = {
200 : 323 : cvc5_dt_cons_get_term(cvc5_dt_get_constructor_by_name(list_dt, "cons")),
201 : 323 : cvc5_mk_integer(d_tm, "0"),
202 : 323 : cvc5_mk_term(
203 : 646 : d_tm, CVC5_KIND_APPLY_CONSTRUCTOR, args.size(), args.data())};
204 : : Cvc5Term dt1 =
205 : 323 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_CONSTRUCTOR, args.size(), args.data());
206 : 323 : (void)cvc5_simplify(d_solver, dt1, false);
207 : :
208 : 323 : args = {cvc5_dt_sel_get_term(cvc5_dt_cons_get_selector_by_name(
209 : : cvc5_dt_get_constructor_by_name(list_dt, "cons"), "head")),
210 : 323 : dt1};
211 : : Cvc5Term dt2 =
212 : 323 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_SELECTOR, args.size(), args.data());
213 : 323 : (void)cvc5_simplify(d_solver, dt2, false);
214 : :
215 : 323 : Cvc5Term b1 = cvc5_mk_var(d_tm, bv_sort, "b1");
216 : 323 : (void)cvc5_simplify(d_solver, b1, false);
217 : 323 : Cvc5Term b2 = cvc5_mk_var(d_tm, bv_sort, "b1");
218 : 323 : (void)cvc5_simplify(d_solver, b2, false);
219 : 323 : Cvc5Term b3 = cvc5_mk_var(d_tm, d_uninterpreted, "b3");
220 : 323 : (void)cvc5_simplify(d_solver, b3, false);
221 : 323 : Cvc5Term v1 = cvc5_mk_const(d_tm, bv_sort, "v1");
222 : 323 : (void)cvc5_simplify(d_solver, v1, false);
223 : 323 : Cvc5Term v2 = cvc5_mk_const(d_tm, d_int, "v2");
224 : 323 : (void)cvc5_simplify(d_solver, v2, false);
225 : 323 : Cvc5Term f1 = cvc5_mk_const(d_tm, fun_sort1, "f1");
226 : 323 : (void)cvc5_simplify(d_solver, f1, false);
227 : 323 : Cvc5Term f2 = cvc5_mk_const(d_tm, fun_sort2, "f1");
228 : 323 : (void)cvc5_simplify(d_solver, f2, false);
229 : :
230 : 323 : std::vector<Cvc5Term> funs = {f1, f2};
231 : 323 : std::vector<size_t> nvars = {2, 1};
232 : 323 : std::vector<Cvc5Term> vars1 = {b1, b2};
233 : 323 : std::vector<Cvc5Term> vars2 = {b3};
234 : 323 : std::vector<const Cvc5Term*> vars = {vars1.data(), vars2.data()};
235 : 323 : std::vector<Cvc5Term> terms = {v1, v2};
236 : 646 : cvc5_define_funs_rec(d_solver,
237 : : funs.size(),
238 : 323 : funs.data(),
239 : : nvars.data(),
240 : : vars.data(),
241 : 323 : terms.data(),
242 : : false);
243 : 323 : (void)cvc5_simplify(d_solver, f1, false);
244 : 323 : (void)cvc5_simplify(d_solver, f2, false);
245 : :
246 : 323 : Cvc5TermManager* tm = cvc5_term_manager_new();
247 : 323 : Cvc5* slv = cvc5_new(tm);
248 : 323 : ASSERT_DEATH(cvc5_simplify(slv, x, false),
249 : : "term is not associated with the term manager of this solver");
250 : 322 : cvc5_delete(slv);
251 : 322 : cvc5_term_manager_delete(tm);
252 [ + - ]: 322 : }
253 : :
254 : 1288 : TEST_F(TestCApiBlackSolver, simplify_apply_subs)
255 : : {
256 : 322 : cvc5_set_option(d_solver, "incremental", "true");
257 : 322 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
258 : 322 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
259 : 322 : std::vector<Cvc5Term> args = {x, zero};
260 : 322 : Cvc5Term eq = cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
261 : 322 : cvc5_assert_formula(d_solver, eq);
262 : 322 : cvc5_check_sat(d_solver);
263 : :
264 [ - + ][ + - ]: 322 : ASSERT_TRUE(cvc5_term_is_equal(cvc5_simplify(d_solver, x, false), x));
265 [ - + ][ + - ]: 322 : ASSERT_TRUE(cvc5_term_is_equal(cvc5_simplify(d_solver, x, true), zero));
266 [ + - ]: 322 : }
267 : :
268 : 1282 : TEST_F(TestCApiBlackSolver, assert_formula)
269 : : {
270 : 322 : ASSERT_DEATH(cvc5_assert_formula(nullptr, cvc5_mk_true(d_tm)),
271 : : "unexpected NULL argument");
272 : 321 : ASSERT_DEATH(cvc5_assert_formula(d_solver, nullptr), "invalid term");
273 : :
274 : 320 : cvc5_assert_formula(d_solver, cvc5_mk_true(d_tm));
275 : :
276 : 320 : Cvc5TermManager* tm = cvc5_term_manager_new();
277 : 320 : Cvc5* slv = cvc5_new(tm);
278 : 320 : ASSERT_DEATH(cvc5_assert_formula(slv, cvc5_mk_true(d_tm)),
279 : : "term is not associated with the term manager of this solver");
280 : 319 : cvc5_delete(slv);
281 : 319 : cvc5_term_manager_delete(tm);
282 : : }
283 : :
284 : 1272 : TEST_F(TestCApiBlackSolver, check_sat)
285 : : {
286 : 319 : ASSERT_DEATH(cvc5_check_sat(nullptr), "unexpected NULL argument");
287 : :
288 : 318 : cvc5_set_option(d_solver, "incremental", "false");
289 : 318 : cvc5_check_sat(d_solver);
290 : 318 : ASSERT_DEATH(cvc5_check_sat(d_solver), "cannot make multiple queries");
291 : : }
292 : :
293 : 1258 : TEST_F(TestCApiBlackSolver, check_sat_assuming)
294 : : {
295 : 317 : std::vector<Cvc5Term> assumptions = {nullptr};
296 : 317 : ASSERT_DEATH(
297 : : cvc5_check_sat_assuming(d_solver, assumptions.size(), assumptions.data()),
298 : : "invalid term at index 0");
299 : 316 : assumptions = {cvc5_mk_true(d_tm)};
300 : 316 : ASSERT_DEATH(
301 : : cvc5_check_sat_assuming(nullptr, assumptions.size(), assumptions.data()),
302 : : "unexpected NULL argument");
303 : 315 : ASSERT_DEATH(cvc5_check_sat_assuming(d_solver, 0, nullptr),
304 : : "unexpected NULL argument");
305 : :
306 : 314 : cvc5_set_option(d_solver, "incremental", "false");
307 : 314 : cvc5_check_sat_assuming(d_solver, assumptions.size(), assumptions.data());
308 : 314 : ASSERT_DEATH(
309 : : cvc5_check_sat_assuming(d_solver, assumptions.size(), assumptions.data()),
310 : : "cannot make multiple queries");
311 : :
312 : 313 : Cvc5TermManager* tm = cvc5_term_manager_new();
313 : 313 : Cvc5* slv = cvc5_new(tm);
314 : 313 : ASSERT_DEATH(
315 : : cvc5_check_sat_assuming(slv, assumptions.size(), assumptions.data()),
316 : : "expected a term associated with the term manager of this solver");
317 : : ;
318 : 312 : cvc5_delete(slv);
319 : 312 : cvc5_term_manager_delete(tm);
320 [ + - ]: 312 : }
321 : :
322 : 1248 : TEST_F(TestCApiBlackSolver, check_sat_assuming1)
323 : : {
324 : 312 : Cvc5Term x = cvc5_mk_const(d_tm, d_bool, "x");
325 : 312 : Cvc5Term y = cvc5_mk_const(d_tm, d_bool, "y");
326 : 312 : std::vector<Cvc5Term> args = {x, y};
327 : 312 : Cvc5Term z = cvc5_mk_term(d_tm, CVC5_KIND_AND, args.size(), args.data());
328 : 312 : cvc5_set_option(d_solver, "incremental", "true");
329 : 312 : std::vector<Cvc5Term> assumptions = {cvc5_mk_true(d_tm)};
330 : 312 : cvc5_check_sat_assuming(d_solver, assumptions.size(), assumptions.data());
331 : 312 : cvc5_check_sat_assuming(d_solver, assumptions.size(), assumptions.data());
332 : 312 : assumptions = {z};
333 : 312 : cvc5_check_sat_assuming(d_solver, assumptions.size(), assumptions.data());
334 : 312 : }
335 : :
336 : 1248 : TEST_F(TestCApiBlackSolver, check_sat_assuming2)
337 : : {
338 : 312 : cvc5_set_option(d_solver, "incremental", "true");
339 : :
340 : 312 : std::vector<Cvc5Sort> domain = {d_uninterpreted};
341 : : Cvc5Sort u_to_int_sort =
342 : 312 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
343 : 312 : domain = {d_int};
344 : : Cvc5Sort int_pred_sort =
345 : 312 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool);
346 : :
347 : : // Constants
348 : 312 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
349 : 312 : Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y");
350 : : // Functions
351 : 312 : Cvc5Term f = cvc5_mk_const(d_tm, u_to_int_sort, "f");
352 : 312 : Cvc5Term p = cvc5_mk_const(d_tm, int_pred_sort, "p");
353 : : // Values
354 : 312 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
355 : 312 : Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1);
356 : : // Terms
357 : 312 : std::vector<Cvc5Term> args = {f, x};
358 : : Cvc5Term f_x =
359 : 312 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
360 : 312 : args = {f, y};
361 : : Cvc5Term f_y =
362 : 312 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
363 : 312 : args = {f_x, f_y};
364 : 312 : Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
365 : 312 : args = {p, zero};
366 : : Cvc5Term p_0 =
367 : 312 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
368 : 312 : args = {p, f_y};
369 : : Cvc5Term p_f_y =
370 : 312 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
371 : : // Assertions
372 : 312 : args = {zero, f_x};
373 : 312 : Cvc5Term args1 = cvc5_mk_term(d_tm, CVC5_KIND_LEQ, args.size(), args.data());
374 : 312 : args = {zero, f_y};
375 : 312 : Cvc5Term args2 = cvc5_mk_term(d_tm, CVC5_KIND_LEQ, args.size(), args.data());
376 : 312 : args = {sum, one};
377 : 312 : Cvc5Term args3 = cvc5_mk_term(d_tm, CVC5_KIND_LEQ, args.size(), args.data());
378 : 312 : args = {p_0};
379 : 0 : args = {args1,
380 : : args2,
381 : : args3,
382 : 312 : cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()),
383 : 312 : p_f_y};
384 : : Cvc5Term assertions =
385 : 312 : cvc5_mk_term(d_tm, CVC5_KIND_AND, args.size(), args.data());
386 : :
387 : 312 : std::vector<Cvc5Term> assumptions = {cvc5_mk_true(d_tm)};
388 : 312 : (void)cvc5_check_sat_assuming(
389 : 312 : d_solver, assumptions.size(), assumptions.data());
390 : 312 : cvc5_assert_formula(d_solver, assertions);
391 : 312 : args = {x, y};
392 : : Cvc5Term dist =
393 : 312 : cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data());
394 : 312 : assumptions = {dist};
395 : 312 : (void)cvc5_check_sat_assuming(
396 : 312 : d_solver, assumptions.size(), assumptions.data());
397 : 312 : assumptions = {cvc5_mk_false(d_tm), dist};
398 : 312 : }
399 : :
400 : 1238 : TEST_F(TestCApiBlackSolver, declare_datatype)
401 : : {
402 : 312 : Cvc5DatatypeConstructorDecl nil = cvc5_mk_dt_cons_decl(d_tm, "lin");
403 : 312 : std::vector<Cvc5DatatypeConstructorDecl> ctors = {nil};
404 : 312 : (void)cvc5_declare_dt(d_solver, "", ctors.size(), ctors.data());
405 : :
406 : 312 : nil = cvc5_mk_dt_cons_decl(d_tm, "nil");
407 : 312 : ctors = {nil};
408 : 312 : (void)cvc5_declare_dt(d_solver, "a", ctors.size(), ctors.data());
409 : :
410 : 312 : Cvc5DatatypeConstructorDecl cons = cvc5_mk_dt_cons_decl(d_tm, "cons");
411 : 312 : nil = cvc5_mk_dt_cons_decl(d_tm, "nil");
412 : 312 : ctors = {cons, nil};
413 : 312 : (void)cvc5_declare_dt(d_solver, "b", ctors.size(), ctors.data());
414 : :
415 : 312 : cons = cvc5_mk_dt_cons_decl(d_tm, "cons");
416 : 312 : nil = cvc5_mk_dt_cons_decl(d_tm, "nil");
417 : 312 : ctors = {cons, nil};
418 : 312 : (void)cvc5_declare_dt(d_solver, "", ctors.size(), ctors.data());
419 : :
420 : 312 : cons = cvc5_mk_dt_cons_decl(d_tm, "cons");
421 : 312 : nil = cvc5_mk_dt_cons_decl(d_tm, "nil");
422 : 312 : ctors = {cons, nil};
423 : 312 : ASSERT_DEATH(cvc5_declare_dt(nullptr, "c", ctors.size(), ctors.data()),
424 : : "unexpected NULL argument");
425 : 311 : ctors = {nullptr};
426 : 311 : ASSERT_DEATH(cvc5_declare_dt(d_solver, "c", ctors.size(), ctors.data()),
427 : : "invalid datatype constructor declaration at index 0");
428 : :
429 : : // must have at least one constructor
430 : 310 : ctors = {};
431 : 310 : ASSERT_DEATH(cvc5_declare_dt(d_solver, "c", ctors.size(), ctors.data()),
432 : : "expected a datatype declaration with at least one constructor");
433 : : // constructors may not be reused
434 : 309 : Cvc5DatatypeConstructorDecl ctor1 = cvc5_mk_dt_cons_decl(d_tm, "_x21");
435 : 309 : Cvc5DatatypeConstructorDecl ctor2 = cvc5_mk_dt_cons_decl(d_tm, "_x31");
436 : 309 : ctors = {ctor1, ctor2};
437 : 309 : (void)cvc5_declare_dt(d_solver, "_x17", ctors.size(), ctors.data());
438 : 309 : ASSERT_DEATH(cvc5_declare_dt(d_solver, "_x86", ctors.size(), ctors.data()),
439 : : "cannot use a constructor for multiple datatypes");
440 : :
441 : 308 : Cvc5TermManager* tm = cvc5_term_manager_new();
442 : 308 : Cvc5* slv = cvc5_new(tm);
443 : 308 : nil = cvc5_mk_dt_cons_decl(d_tm, "nil");
444 : 308 : ctors = {nil};
445 : 308 : ASSERT_DEATH(cvc5_declare_dt(slv, "a", ctors.size(), ctors.data()),
446 : : "expected a datatype constructor declaration associated with "
447 : : "the term manager of this solver");
448 : 307 : cvc5_delete(slv);
449 : 307 : cvc5_term_manager_delete(tm);
450 [ + - ]: 307 : }
451 : :
452 : 1228 : TEST_F(TestCApiBlackSolver, dt_get_arity)
453 : : {
454 : : std::vector<Cvc5DatatypeConstructorDecl> ctors = {
455 : 307 : cvc5_mk_dt_cons_decl(d_tm, "_x21"), cvc5_mk_dt_cons_decl(d_tm, "_x31")};
456 : 307 : Cvc5Sort s3 = cvc5_declare_dt(d_solver, "_x17", ctors.size(), ctors.data());
457 [ - + ][ + - ]: 307 : ASSERT_EQ(cvc5_sort_dt_get_arity(s3), 0);
458 [ + - ]: 307 : }
459 : :
460 : 1218 : TEST_F(TestCApiBlackSolver, declare_fun)
461 : : {
462 : 307 : ASSERT_DEATH(cvc5_declare_fun(nullptr, "b", 0, nullptr, d_bool, true),
463 : : "unexpected NULL argument");
464 : 306 : ASSERT_DEATH(cvc5_declare_fun(d_solver, "b", 0, nullptr, nullptr, true),
465 : : "invalid sort");
466 : :
467 : 305 : Cvc5Sort bv_sort = cvc5_mk_bv_sort(d_tm, 32);
468 : 305 : std::vector<Cvc5Sort> domain = {d_uninterpreted};
469 : : Cvc5Sort fun_sort =
470 : 305 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
471 : 305 : (void)cvc5_declare_fun(d_solver, "f1", 0, nullptr, bv_sort, true);
472 : 305 : domain = {bv_sort, d_int};
473 : 305 : (void)cvc5_declare_fun(
474 : 305 : d_solver, "f3", domain.size(), domain.data(), bv_sort, true);
475 : 305 : ASSERT_DEATH(cvc5_declare_fun(d_solver, "f3", 0, nullptr, fun_sort, true),
476 : : "invalid argument");
477 : : // functions as arguments is allowed
478 : 304 : domain = {bv_sort, fun_sort};
479 : 304 : (void)cvc5_declare_fun(
480 : 304 : d_solver, "f4", domain.size(), domain.data(), bv_sort, true);
481 : 304 : domain = {bv_sort, bv_sort};
482 : 304 : ASSERT_DEATH(
483 : : cvc5_declare_fun(
484 : : d_solver, "f5", domain.size(), domain.data(), fun_sort, true),
485 : : "invalid argument");
486 : :
487 : 303 : Cvc5TermManager* tm = cvc5_term_manager_new();
488 : 303 : Cvc5* slv = cvc5_new(tm);
489 : 303 : ASSERT_DEATH(cvc5_declare_fun(slv, "f1", 0, nullptr, bv_sort, true),
490 : : "sort is not associated with the term manager of this solver");
491 : 302 : cvc5_delete(slv);
492 : 302 : cvc5_term_manager_delete(tm);
493 : : }
494 : :
495 : 1206 : TEST_F(TestCApiBlackSolver, declare_fun_fresh)
496 : : {
497 : : // std::vector<Cvc5Sort> domain =
498 : 302 : Cvc5Term t1 = cvc5_declare_fun(d_solver, "b", 0, nullptr, d_bool, true);
499 : 302 : Cvc5Term t2 = cvc5_declare_fun(d_solver, "b", 0, nullptr, d_bool, false);
500 : 302 : Cvc5Term t3 = cvc5_declare_fun(d_solver, "b", 0, nullptr, d_bool, false);
501 [ - + ][ + - ]: 302 : ASSERT_FALSE(cvc5_term_is_equal(t1, t2));
502 [ - + ][ + - ]: 302 : ASSERT_FALSE(cvc5_term_is_equal(t1, t3));
503 [ - + ][ + - ]: 302 : ASSERT_TRUE(cvc5_term_is_equal(t2, t3));
504 : 302 : Cvc5Term t4 = cvc5_declare_fun(d_solver, "c", 0, nullptr, d_bool, false);
505 [ - + ][ + - ]: 302 : ASSERT_FALSE(cvc5_term_is_equal(t2, t4));
506 : 302 : Cvc5Term t5 = cvc5_declare_fun(d_solver, "b", 0, nullptr, d_int, false);
507 [ - + ][ + - ]: 302 : ASSERT_FALSE(cvc5_term_is_equal(t2, t5));
508 : :
509 : 302 : Cvc5TermManager* tm = cvc5_term_manager_new();
510 : 302 : Cvc5* slv = cvc5_new(tm);
511 : 302 : ASSERT_DEATH(cvc5_declare_fun(slv, "b", 0, nullptr, d_int, false),
512 : : "sort is not associated with the term manager of this solver");
513 : : ;
514 : 301 : cvc5_delete(slv);
515 : 301 : cvc5_term_manager_delete(tm);
516 : : }
517 : :
518 : 1200 : TEST_F(TestCApiBlackSolver, declare_sort)
519 : : {
520 : 301 : ASSERT_DEATH(cvc5_declare_sort(nullptr, "s", 0, true),
521 : : "unexpected NULL argument");
522 : 300 : ASSERT_DEATH(cvc5_declare_sort(d_solver, nullptr, 0, true),
523 : : "unexpected NULL argument");
524 : 299 : (void)cvc5_declare_sort(d_solver, "s", 0, true);
525 : 299 : (void)cvc5_declare_sort(d_solver, "s", 2, true);
526 : 299 : (void)cvc5_declare_sort(d_solver, "", 2, true);
527 : : }
528 : :
529 : 1192 : TEST_F(TestCApiBlackSolver, declare_sort_fresh)
530 : : {
531 : 299 : ASSERT_DEATH(cvc5_declare_sort(nullptr, "b", 0, true),
532 : : "unexpected NULL argument");
533 : 298 : ASSERT_DEATH(cvc5_declare_sort(d_solver, nullptr, 0, true),
534 : : "unexpected NULL argument");
535 : :
536 : 297 : Cvc5Sort s1 = cvc5_declare_sort(d_solver, "b", 0, true);
537 : 297 : Cvc5Sort s2 = cvc5_declare_sort(d_solver, "b", 0, false);
538 : 297 : Cvc5Sort s3 = cvc5_declare_sort(d_solver, "b", 0, false);
539 [ - + ][ + - ]: 297 : ASSERT_FALSE(cvc5_sort_is_equal(s1, s2));
540 [ - + ][ + - ]: 297 : ASSERT_FALSE(cvc5_sort_is_equal(s1, s3));
541 [ - + ][ + - ]: 297 : ASSERT_TRUE(cvc5_sort_is_equal(s2, s3));
542 : :
543 : 297 : Cvc5Sort s4 = cvc5_declare_sort(d_solver, "c", 0, false);
544 [ - + ][ + - ]: 297 : ASSERT_FALSE(cvc5_sort_is_equal(s2, s4));
545 : :
546 : 297 : Cvc5Sort s5 = cvc5_declare_sort(d_solver, "b", 1, false);
547 [ - + ][ + - ]: 297 : ASSERT_FALSE(cvc5_sort_is_equal(s2, s5));
548 : : }
549 : :
550 : 1164 : TEST_F(TestCApiBlackSolver, define_fun)
551 : : {
552 : 297 : Cvc5Sort bv_sort = cvc5_mk_bv_sort(d_tm, 32);
553 : 297 : std::vector<Cvc5Sort> domain = {d_uninterpreted};
554 : : Cvc5Sort fun_sort =
555 : 297 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
556 : :
557 : 297 : Cvc5Term b1 = cvc5_mk_var(d_tm, bv_sort, "b1");
558 : 297 : Cvc5Term b2 = cvc5_mk_var(d_tm, d_int, "b2");
559 : 297 : Cvc5Term b3 = cvc5_mk_var(d_tm, fun_sort, "b3");
560 : 297 : Cvc5Term v1 = cvc5_mk_const(d_tm, bv_sort, "v1");
561 : 297 : Cvc5Term v2 = cvc5_mk_const(d_tm, fun_sort, "v2");
562 : :
563 : 297 : ASSERT_DEATH(cvc5_define_fun(nullptr, "f", 0, nullptr, bv_sort, v1, false),
564 : : "unexpected NULL argument");
565 : 296 : ASSERT_DEATH(cvc5_define_fun(d_solver, "f", 0, nullptr, nullptr, v1, false),
566 : : "invalid sort");
567 : 295 : ASSERT_DEATH(
568 : : cvc5_define_fun(d_solver, "f", 0, nullptr, bv_sort, nullptr, false),
569 : : "invalid term");
570 : :
571 : 294 : (void)cvc5_define_fun(d_solver, "f", 0, nullptr, bv_sort, v1, false);
572 : 294 : std::vector<Cvc5Term> vars = {b1, b2};
573 : 294 : (void)cvc5_define_fun(
574 : 294 : d_solver, "f", vars.size(), vars.data(), bv_sort, v1, false);
575 : 294 : vars = {v1, b2};
576 : 294 : ASSERT_DEATH(cvc5_define_fun(
577 : : d_solver, "f", vars.size(), vars.data(), bv_sort, v1, false),
578 : : "invalid bound variable");
579 : 293 : vars = {b1};
580 : 293 : ASSERT_DEATH(cvc5_define_fun(
581 : : d_solver, "f", vars.size(), vars.data(), bv_sort, v2, false),
582 : : "invalid sort of function body");
583 : 292 : ASSERT_DEATH(
584 : : cvc5_define_fun(
585 : : d_solver, "f", vars.size(), vars.data(), fun_sort, v2, false),
586 : : "invalid argument");
587 : : // b3 has function sort, which is allowed as an argument
588 : 291 : vars = {b1, b3};
589 : 291 : (void)cvc5_define_fun(
590 : 291 : d_solver, "f", vars.size(), vars.data(), bv_sort, v1, false);
591 : :
592 : 291 : Cvc5TermManager* tm = cvc5_term_manager_new();
593 : 291 : Cvc5* slv = cvc5_new(tm);
594 : 291 : Cvc5Sort bv_sort2 = cvc5_mk_bv_sort(tm, 32);
595 : 291 : Cvc5Term v12 = cvc5_mk_const(tm, bv_sort2, "v1");
596 : 291 : Cvc5Term b12 = cvc5_mk_var(tm, bv_sort2, "b1");
597 : 291 : Cvc5Term b22 = cvc5_mk_var(tm, cvc5_get_integer_sort(tm), "b2");
598 : 291 : vars = {};
599 : 291 : ASSERT_DEATH(
600 : : cvc5_define_fun(slv, "f", vars.size(), vars.data(), bv_sort, v12, false),
601 : : "sort is not associated with the term manager of this solver");
602 : 290 : ASSERT_DEATH(
603 : : cvc5_define_fun(slv, "f", vars.size(), vars.data(), bv_sort2, v1, false),
604 : : "term is not associated with the term manager of this solver");
605 : 289 : vars = {b1, b22};
606 : 289 : ASSERT_DEATH(
607 : : cvc5_define_fun(slv, "f", vars.size(), vars.data(), bv_sort2, v12, false),
608 : : "expected a term associated with the term manager of this solver");
609 : 288 : vars = {b12, b2};
610 : 288 : ASSERT_DEATH(
611 : : cvc5_define_fun(slv, "f", vars.size(), vars.data(), bv_sort2, v12, false),
612 : : "expected a term associated with the term manager of this solver");
613 : 287 : vars = {b12, b22};
614 : 287 : ASSERT_DEATH(
615 : : cvc5_define_fun(slv, "f", vars.size(), vars.data(), bv_sort, v12, false),
616 : : "sort is not associated with the term manager of this solver");
617 : 286 : ASSERT_DEATH(
618 : : cvc5_define_fun(slv, "f", vars.size(), vars.data(), bv_sort2, v1, false),
619 : : "term is not associated with the term manager of this solver");
620 : 285 : cvc5_delete(slv);
621 : 285 : cvc5_term_manager_delete(tm);
622 [ + - ]: 285 : }
623 : :
624 : 1140 : TEST_F(TestCApiBlackSolver, define_fun_global)
625 : : {
626 : 285 : Cvc5Term btrue = cvc5_mk_true(d_tm);
627 : : // (define-fun f () Bool true)
628 : 285 : Cvc5Term f = cvc5_define_fun(d_solver, "f", 0, nullptr, d_bool, btrue, true);
629 : 285 : Cvc5Term b = cvc5_mk_var(d_tm, d_bool, "b");
630 : : // (define-fun g (b Bool) Bool b)
631 : 285 : std::vector<Cvc5Term> vars = {b};
632 : : Cvc5Term g =
633 : 285 : cvc5_define_fun(d_solver, "g", vars.size(), vars.data(), d_bool, b, true);
634 : :
635 : : // (assert (or (not f) (not (g true))))
636 : 285 : std::vector<Cvc5Term> args = {f};
637 : 285 : Cvc5Term fnot = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data());
638 : 285 : args = {g, btrue};
639 : : Cvc5Term app =
640 : 285 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
641 : 285 : args = {app};
642 : 285 : Cvc5Term appnot = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data());
643 : :
644 : 285 : args = {fnot, appnot};
645 : 285 : cvc5_assert_formula(
646 : 285 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data()));
647 : 285 : Cvc5Result res = cvc5_check_sat(d_solver);
648 [ - + ][ + - ]: 285 : ASSERT_TRUE(cvc5_result_is_unsat(res));
649 : :
650 : 285 : cvc5_reset_assertions(d_solver);
651 : 285 : cvc5_result_release(res);
652 : : // (assert (or (not f) (not (g true))))
653 : 285 : cvc5_assert_formula(
654 : 285 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data()));
655 : 285 : res = cvc5_check_sat(d_solver);
656 [ - + ][ + - ]: 285 : ASSERT_TRUE(cvc5_result_is_unsat(res));
657 [ + - ][ + - ]: 285 : }
658 : :
659 : 1100 : TEST_F(TestCApiBlackSolver, define_fun_rec)
660 : : {
661 : 285 : Cvc5Sort bv_sort = cvc5_mk_bv_sort(d_tm, 32);
662 : 285 : std::vector<Cvc5Sort> domain = {bv_sort, bv_sort};
663 : : Cvc5Sort fun_sort1 =
664 : 285 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), bv_sort);
665 : 285 : domain = {d_uninterpreted};
666 : : Cvc5Sort fun_sort2 =
667 : 285 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
668 : :
669 : 285 : Cvc5Term b1 = cvc5_mk_var(d_tm, bv_sort, "b1");
670 : 285 : Cvc5Term b11 = cvc5_mk_var(d_tm, bv_sort, "b1");
671 : 285 : Cvc5Term b2 = cvc5_mk_var(d_tm, d_int, "b2");
672 : 285 : Cvc5Term b3 = cvc5_mk_var(d_tm, fun_sort2, "b3");
673 : 285 : Cvc5Term v1 = cvc5_mk_const(d_tm, bv_sort, "v1");
674 : 285 : Cvc5Term v2 = cvc5_mk_const(d_tm, d_int, "v1");
675 : 285 : Cvc5Term v3 = cvc5_mk_const(d_tm, fun_sort2, "v3");
676 : 285 : Cvc5Term f1 = cvc5_mk_const(d_tm, fun_sort1, "f1");
677 : 285 : Cvc5Term f2 = cvc5_mk_const(d_tm, fun_sort2, "f2");
678 : 285 : Cvc5Term f3 = cvc5_mk_const(d_tm, bv_sort, "f3");
679 : :
680 : 285 : (void)cvc5_define_fun_rec(d_solver, "f", 0, nullptr, bv_sort, v1, false);
681 : 285 : std::vector<Cvc5Term> vars = {b1, b2};
682 : 285 : (void)cvc5_define_fun_rec(
683 : 285 : d_solver, "f", vars.size(), vars.data(), bv_sort, v1, false);
684 : 285 : vars = {b1, b11};
685 : 285 : (void)cvc5_define_fun_rec_from_const(
686 : 285 : d_solver, f1, vars.size(), vars.data(), v1, false);
687 : :
688 : : // b3 has function sort, which is allowed as an argument
689 : 285 : vars = {b1, b3};
690 : 285 : (void)cvc5_define_fun_rec(
691 : 285 : d_solver, "f", vars.size(), vars.data(), bv_sort, v1, false);
692 : :
693 : 285 : ASSERT_DEATH(
694 : : cvc5_define_fun_rec(nullptr, "f", 0, nullptr, bv_sort, v1, false),
695 : : "unexpected NULL argument");
696 : 284 : ASSERT_DEATH(
697 : : cvc5_define_fun_rec(d_solver, nullptr, 0, nullptr, bv_sort, v1, false),
698 : : "unexpected NULL argument");
699 : 283 : ASSERT_DEATH(
700 : : cvc5_define_fun_rec(d_solver, "f", 0, nullptr, nullptr, v1, false),
701 : : "invalid sort");
702 : 282 : ASSERT_DEATH(
703 : : cvc5_define_fun_rec(d_solver, "f", 0, nullptr, bv_sort, nullptr, false),
704 : : "invalid term");
705 : :
706 : 281 : vars = {b1};
707 : 281 : ASSERT_DEATH(cvc5_define_fun_rec(
708 : : d_solver, "f", vars.size(), vars.data(), bv_sort, v3, false),
709 : : "invalid sort");
710 : 280 : vars = {b1, v2};
711 : 280 : ASSERT_DEATH(cvc5_define_fun_rec(
712 : : d_solver, "f", vars.size(), vars.data(), bv_sort, v1, false),
713 : : "invalid bound variable");
714 : 279 : vars = {b1};
715 : 279 : ASSERT_DEATH(
716 : : cvc5_define_fun_rec(
717 : : d_solver, "f", vars.size(), vars.data(), fun_sort2, v3, false),
718 : : "invalid argument");
719 : :
720 : 278 : ASSERT_DEATH(
721 : : cvc5_define_fun_rec_from_const(nullptr, f1, 0, nullptr, v1, false),
722 : : "unexpected NULL argument");
723 : 277 : ASSERT_DEATH(
724 : : cvc5_define_fun_rec_from_const(d_solver, nullptr, 0, nullptr, v1, false),
725 : : "invalid term");
726 : 276 : ASSERT_DEATH(
727 : : cvc5_define_fun_rec_from_const(d_solver, f1, 0, nullptr, nullptr, false),
728 : : "invalid term");
729 : :
730 : 275 : vars = {b1};
731 : 275 : ASSERT_DEATH(cvc5_define_fun_rec_from_const(
732 : : d_solver, f1, vars.size(), vars.data(), v1, false),
733 : : "invalid size of argument 'bound_vars'");
734 : 274 : ASSERT_DEATH(cvc5_define_fun_rec_from_const(
735 : : d_solver, f2, vars.size(), vars.data(), v2, false),
736 : : "invalid sort");
737 : 273 : ASSERT_DEATH(cvc5_define_fun_rec_from_const(
738 : : d_solver, f3, vars.size(), vars.data(), v1, false),
739 : : "invalid argument");
740 : 272 : vars = {b1, b11};
741 : 272 : ASSERT_DEATH(cvc5_define_fun_rec_from_const(
742 : : d_solver, f1, vars.size(), vars.data(), v2, false),
743 : : "invalid sort");
744 : 271 : ASSERT_DEATH(cvc5_define_fun_rec_from_const(
745 : : d_solver, f1, vars.size(), vars.data(), v3, false),
746 : : "invalid sort");
747 : :
748 : 270 : Cvc5TermManager* tm = cvc5_term_manager_new();
749 : 270 : Cvc5* slv = cvc5_new(tm);
750 : 270 : Cvc5Sort bv_sort2 = cvc5_mk_bv_sort(tm, 32);
751 : 270 : Cvc5Term b12 = cvc5_mk_var(tm, bv_sort2, "b1");
752 : 270 : Cvc5Term b22 = cvc5_mk_var(tm, cvc5_get_integer_sort(tm), "b2");
753 : 270 : Cvc5Term v12 = cvc5_mk_const(tm, bv_sort2, "v1");
754 : 270 : vars = {};
755 : 270 : ASSERT_DEATH(
756 : : cvc5_define_fun_rec(
757 : : d_solver, "f", vars.size(), vars.data(), bv_sort2, v12, false),
758 : : "term is not associated with the term manager of this solver");
759 : 269 : ASSERT_DEATH(cvc5_define_fun_rec(
760 : : slv, "f", vars.size(), vars.data(), bv_sort, v12, false),
761 : : "sort is not associated with the term manager of this solver");
762 : 268 : ASSERT_DEATH(cvc5_define_fun_rec(
763 : : slv, "f", vars.size(), vars.data(), bv_sort2, v1, false),
764 : : "term is not associated with the term manager of this solver");
765 : 267 : vars = {b12, b22};
766 : 267 : (void)cvc5_define_fun_rec(
767 : 267 : slv, "f", vars.size(), vars.data(), bv_sort2, v12, false);
768 : 267 : vars = {b1, b22};
769 : 267 : ASSERT_DEATH(
770 : : cvc5_define_fun_rec(
771 : : slv, "f", vars.size(), vars.data(), bv_sort2, v12, false),
772 : : "expected a term associated with the term manager of this solver");
773 : 266 : vars = {b12, b2};
774 : 266 : ASSERT_DEATH(
775 : : cvc5_define_fun_rec(
776 : : slv, "f", vars.size(), vars.data(), bv_sort2, v12, false),
777 : : "expected a term associated with the term manager of this solver");
778 : 265 : cvc5_delete(slv);
779 : 265 : cvc5_term_manager_delete(tm);
780 [ + - ][ + - ]: 265 : }
781 : :
782 : 1056 : TEST_F(TestCApiBlackSolver, define_fun_rec_wrong_logic)
783 : : {
784 : 265 : cvc5_set_logic(d_solver, "QF_BV");
785 : 265 : Cvc5Sort bv_sort = cvc5_mk_bv_sort(d_tm, 32);
786 : 265 : std::vector<Cvc5Sort> domain = {bv_sort, bv_sort};
787 : : Cvc5Sort fun_sort =
788 : 265 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), bv_sort);
789 : 265 : Cvc5Term b = cvc5_mk_var(d_tm, bv_sort, "b");
790 : 265 : Cvc5Term v = cvc5_mk_var(d_tm, bv_sort, "v");
791 : 265 : Cvc5Term f = cvc5_mk_var(d_tm, fun_sort, "f");
792 : 265 : std::vector<Cvc5Term> vars = {};
793 : 265 : ASSERT_DEATH(cvc5_define_fun_rec(
794 : : d_solver, "f", vars.size(), vars.data(), bv_sort, v, false),
795 : : "require a logic with quantifiers");
796 : 264 : vars = {b, b};
797 : 264 : ASSERT_DEATH(cvc5_define_fun_rec_from_const(
798 : : d_solver, f, vars.size(), vars.data(), v, false),
799 : : "require a logic with quantifiers");
800 [ + - ][ + - ]: 263 : }
801 : :
802 : 1048 : TEST_F(TestCApiBlackSolver, define_fun_rec_global)
803 : : {
804 : 263 : cvc5_push(d_solver, 1);
805 : 263 : Cvc5Term btrue = cvc5_mk_true(d_tm);
806 : : // (define-fun f () Bool true)
807 : : Cvc5Term f =
808 : 263 : cvc5_define_fun_rec(d_solver, "f", 0, nullptr, d_bool, btrue, true);
809 : 263 : Cvc5Term b = cvc5_mk_var(d_tm, d_bool, "b");
810 : : // (define-fun g (b Bool) Bool b)
811 : 263 : std::vector<Cvc5Sort> domain = {d_bool};
812 : 263 : Cvc5Term ff = cvc5_mk_const(
813 : 263 : d_tm, cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool), "g");
814 : 263 : std::vector<Cvc5Term> vars = {b};
815 : 263 : Cvc5Term g = cvc5_define_fun_rec_from_const(
816 : 263 : d_solver, ff, vars.size(), vars.data(), b, true);
817 : :
818 : : // (assert (or (not f) (not (g true))))
819 : 263 : std::vector<Cvc5Term> args = {f};
820 : 263 : Cvc5Term fnot = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data());
821 : 263 : args = {g, btrue};
822 : : Cvc5Term app =
823 : 263 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
824 : 263 : args = {app};
825 : 263 : Cvc5Term appnot = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data());
826 : 263 : args = {fnot, appnot};
827 : 263 : cvc5_assert_formula(
828 : 263 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data()));
829 : 263 : Cvc5Result res = cvc5_check_sat(d_solver);
830 [ - + ][ + - ]: 263 : ASSERT_TRUE(cvc5_result_is_unsat(res));
831 : 263 : cvc5_pop(d_solver, 1);
832 : : // (assert (or (not f) (not (g true))))
833 : 263 : cvc5_assert_formula(
834 : 263 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data()));
835 : 263 : res = cvc5_check_sat(d_solver);
836 [ - + ][ + - ]: 263 : ASSERT_TRUE(cvc5_result_is_unsat(res));
837 : :
838 : 263 : Cvc5TermManager* tm = cvc5_term_manager_new();
839 : 263 : Cvc5* slv = cvc5_new(tm);
840 : 263 : Cvc5Term bb = cvc5_mk_var(tm, cvc5_get_boolean_sort(tm), "b");
841 : 263 : domain = {d_bool};
842 : 263 : vars = {bb};
843 : 263 : ASSERT_DEATH(
844 : : cvc5_define_fun_rec_from_const(
845 : : slv,
846 : : cvc5_mk_const(
847 : : d_tm,
848 : : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool),
849 : : "g"),
850 : : vars.size(),
851 : : vars.data(),
852 : : bb,
853 : : true),
854 : : "term is not associated with the term manager of this solver");
855 : 262 : vars = {b};
856 : 262 : domain = {cvc5_get_boolean_sort(tm)};
857 : 262 : ASSERT_DEATH(
858 : : cvc5_define_fun_rec_from_const(
859 : : slv,
860 : : cvc5_mk_const(
861 : : tm,
862 : : cvc5_mk_fun_sort(
863 : : tm, domain.size(), domain.data(), cvc5_get_boolean_sort(tm)),
864 : : "g"),
865 : : vars.size(),
866 : : vars.data(),
867 : : bb,
868 : : true),
869 : : "invalid sort of parameter");
870 : 261 : cvc5_delete(slv);
871 : 261 : cvc5_term_manager_delete(tm);
872 [ + - ][ + - ]: 261 : }
[ + - ]
873 : :
874 : 1024 : TEST_F(TestCApiBlackSolver, define_funs_rec)
875 : : {
876 : 261 : Cvc5Sort bv_sort = cvc5_mk_bv_sort(d_tm, 32);
877 : 261 : std::vector<Cvc5Sort> domain = {bv_sort, bv_sort};
878 : : Cvc5Sort fun_sort1 =
879 : 261 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), bv_sort);
880 : 261 : domain = {d_uninterpreted};
881 : : Cvc5Sort fun_sort2 =
882 : 261 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
883 : 261 : Cvc5Term b1 = cvc5_mk_var(d_tm, bv_sort, "b1");
884 : 261 : Cvc5Term b11 = cvc5_mk_var(d_tm, bv_sort, "b1");
885 : 261 : Cvc5Term b2 = cvc5_mk_var(d_tm, d_int, "b2");
886 : 261 : Cvc5Term b4 = cvc5_mk_var(d_tm, d_uninterpreted, "b4");
887 : 261 : Cvc5Term v1 = cvc5_mk_const(d_tm, bv_sort, "v1");
888 : 261 : Cvc5Term v2 = cvc5_mk_const(d_tm, d_int, "v2");
889 : 261 : Cvc5Term v4 = cvc5_mk_const(d_tm, d_uninterpreted, "v4");
890 : 261 : Cvc5Term f1 = cvc5_mk_const(d_tm, fun_sort1, "f1");
891 : 261 : Cvc5Term f2 = cvc5_mk_const(d_tm, fun_sort2, "f2");
892 : 261 : Cvc5Term f3 = cvc5_mk_const(d_tm, bv_sort, "f3");
893 : :
894 : 261 : std::vector<Cvc5Term> funs = {f1, f2};
895 : 261 : std::vector<size_t> nvars = {2, 1};
896 : 261 : std::vector<Cvc5Term> vars1 = {b1, b11};
897 : 261 : std::vector<Cvc5Term> vars2 = {b4};
898 : 261 : std::vector<const Cvc5Term*> vars = {vars1.data(), vars2.data()};
899 : 261 : std::vector<Cvc5Term> terms = {v1, v2};
900 : :
901 : 522 : cvc5_define_funs_rec(d_solver,
902 : : funs.size(),
903 : 261 : funs.data(),
904 : : nvars.data(),
905 : : vars.data(),
906 : 261 : terms.data(),
907 : : false);
908 : 261 : vars1 = {v1, b11};
909 : 261 : vars = {vars1.data(), vars2.data()};
910 : 261 : ASSERT_DEATH(cvc5_define_funs_rec(d_solver,
911 : : funs.size(),
912 : : funs.data(),
913 : : nvars.data(),
914 : : vars.data(),
915 : : terms.data(),
916 : : false),
917 : : "invalid bound variable");
918 : 260 : funs = {f1, f3};
919 : 260 : vars1 = {b1, b11};
920 : 260 : vars = {vars1.data(), vars2.data()};
921 : 260 : ASSERT_DEATH(cvc5_define_funs_rec(d_solver,
922 : : funs.size(),
923 : : funs.data(),
924 : : nvars.data(),
925 : : vars.data(),
926 : : terms.data(),
927 : : false),
928 : : "invalid argument");
929 : 259 : funs = {f1, f2};
930 : 259 : vars1 = {b1};
931 : 259 : vars = {vars1.data(), vars2.data()};
932 : 259 : nvars = {1, 1};
933 : 259 : ASSERT_DEATH(cvc5_define_funs_rec(d_solver,
934 : : funs.size(),
935 : : funs.data(),
936 : : nvars.data(),
937 : : vars.data(),
938 : : terms.data(),
939 : : false),
940 : : "invalid size of argument");
941 : 258 : vars1 = {b1, b2};
942 : 258 : vars = {vars1.data(), vars2.data()};
943 : 258 : nvars = {2, 1};
944 : 258 : ASSERT_DEATH(cvc5_define_funs_rec(d_solver,
945 : : funs.size(),
946 : : funs.data(),
947 : : nvars.data(),
948 : : vars.data(),
949 : : terms.data(),
950 : : false),
951 : : "invalid sort");
952 : 257 : vars1 = {b1, b11};
953 : 257 : vars = {vars1.data(), vars2.data()};
954 : 257 : terms = {v1, v4};
955 : 257 : ASSERT_DEATH(cvc5_define_funs_rec(d_solver,
956 : : funs.size(),
957 : : funs.data(),
958 : : nvars.data(),
959 : : vars.data(),
960 : : terms.data(),
961 : : false),
962 : : "invalid sort");
963 : :
964 : 256 : Cvc5TermManager* tm = cvc5_term_manager_new();
965 : 256 : Cvc5* slv = cvc5_new(tm);
966 : 256 : Cvc5Sort uninterpreted2 = cvc5_mk_uninterpreted_sort(tm, "u");
967 : 256 : Cvc5Sort bv_sort2 = cvc5_mk_bv_sort(tm, 32);
968 : :
969 : 256 : domain = {bv_sort2, bv_sort2};
970 : : Cvc5Sort fun_sort12 =
971 : 256 : cvc5_mk_fun_sort(tm, domain.size(), domain.data(), bv_sort2);
972 : 256 : domain = {uninterpreted2};
973 : 512 : Cvc5Sort fun_sort22 = cvc5_mk_fun_sort(
974 : 256 : tm, domain.size(), domain.data(), cvc5_get_integer_sort(tm));
975 : :
976 : 256 : Cvc5Term b12 = cvc5_mk_var(tm, bv_sort2, "b1");
977 : 256 : Cvc5Term b112 = cvc5_mk_var(tm, bv_sort2, "b1");
978 : 256 : Cvc5Term b42 = cvc5_mk_var(tm, uninterpreted2, "b4");
979 : 256 : Cvc5Term v12 = cvc5_mk_const(tm, bv_sort2, "v1");
980 : 256 : Cvc5Term v22 = cvc5_mk_const(tm, cvc5_get_integer_sort(tm), "v2");
981 : 256 : Cvc5Term f12 = cvc5_mk_const(tm, fun_sort12, "f1");
982 : 256 : Cvc5Term f22 = cvc5_mk_const(tm, fun_sort22, "f2");
983 : :
984 : 256 : funs = {f12, f22};
985 : 256 : nvars = {2, 1};
986 : 256 : vars1 = {b12, b112};
987 : 256 : vars2 = {b42};
988 : 256 : vars = {vars1.data(), vars2.data()};
989 : 256 : terms = {v12, v22};
990 : 512 : cvc5_define_funs_rec(slv,
991 : : funs.size(),
992 : 256 : funs.data(),
993 : : nvars.data(),
994 : : vars.data(),
995 : 256 : terms.data(),
996 : : false);
997 : 256 : funs = {f1, f22};
998 : 256 : ASSERT_DEATH(
999 : : cvc5_define_funs_rec(slv,
1000 : : funs.size(),
1001 : : funs.data(),
1002 : : nvars.data(),
1003 : : vars.data(),
1004 : : terms.data(),
1005 : : false),
1006 : : "expected a term associated with the term manager of this solver");
1007 : 255 : funs = {f12, f22};
1008 : 255 : vars1 = {b1, b112};
1009 : 255 : vars = {vars1.data(), vars2.data()};
1010 : 255 : ASSERT_DEATH(
1011 : : cvc5_define_funs_rec(slv,
1012 : : funs.size(),
1013 : : funs.data(),
1014 : : nvars.data(),
1015 : : vars.data(),
1016 : : terms.data(),
1017 : : false),
1018 : : "expected a term associated with the term manager of this solver");
1019 : 254 : vars1 = {b12, b11};
1020 : 254 : vars = {vars1.data(), vars2.data()};
1021 : 254 : ASSERT_DEATH(
1022 : : cvc5_define_funs_rec(slv,
1023 : : funs.size(),
1024 : : funs.data(),
1025 : : nvars.data(),
1026 : : vars.data(),
1027 : : terms.data(),
1028 : : false),
1029 : : "expected a term associated with the term manager of this solver");
1030 : 253 : vars2 = {b42};
1031 : 253 : vars = {vars1.data(), vars2.data()};
1032 : 253 : terms = {v1, v22};
1033 : 253 : ASSERT_DEATH(
1034 : : cvc5_define_funs_rec(slv,
1035 : : funs.size(),
1036 : : funs.data(),
1037 : : nvars.data(),
1038 : : vars.data(),
1039 : : terms.data(),
1040 : : false),
1041 : : "expected a term associated with the term manager of this solver");
1042 : 252 : terms = {v12, v2};
1043 : 252 : ASSERT_DEATH(
1044 : : cvc5_define_funs_rec(slv,
1045 : : funs.size(),
1046 : : funs.data(),
1047 : : nvars.data(),
1048 : : vars.data(),
1049 : : terms.data(),
1050 : : false),
1051 : : "expected a term associated with the term manager of this solver");
1052 : 251 : cvc5_delete(slv);
1053 : 251 : cvc5_term_manager_delete(tm);
1054 [ + - ][ + - ]: 251 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
1055 : :
1056 : 1002 : TEST_F(TestCApiBlackSolver, define_funs_rec_wrong_logic)
1057 : : {
1058 : 251 : cvc5_set_logic(d_solver, "QF_BV");
1059 : 251 : Cvc5Sort bv_sort = cvc5_mk_bv_sort(d_tm, 32);
1060 : 251 : std::vector<Cvc5Sort> domain = {bv_sort, bv_sort};
1061 : : Cvc5Sort fun_sort1 =
1062 : 251 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), bv_sort);
1063 : 251 : domain = {d_uninterpreted};
1064 : : Cvc5Sort fun_sort2 =
1065 : 251 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
1066 : 251 : Cvc5Term b = cvc5_mk_var(d_tm, bv_sort, "b");
1067 : 251 : Cvc5Term u = cvc5_mk_var(d_tm, d_uninterpreted, "u");
1068 : 251 : Cvc5Term v1 = cvc5_mk_const(d_tm, bv_sort, "v1");
1069 : 251 : Cvc5Term v2 = cvc5_mk_const(d_tm, d_int, "v2");
1070 : 251 : Cvc5Term f1 = cvc5_mk_const(d_tm, fun_sort1, "f1");
1071 : 251 : Cvc5Term f2 = cvc5_mk_const(d_tm, fun_sort2, "f2");
1072 : :
1073 : 251 : std::vector<Cvc5Term> funs = {f1, f2};
1074 : 251 : std::vector<size_t> nvars = {2, 1};
1075 : 251 : std::vector<Cvc5Term> vars1 = {b, b};
1076 : 251 : std::vector<Cvc5Term> vars2 = {u};
1077 : 251 : std::vector<const Cvc5Term*> vars = {vars1.data(), vars2.data()};
1078 : 251 : std::vector<Cvc5Term> terms = {v1, v2};
1079 : :
1080 : 251 : ASSERT_DEATH(cvc5_define_funs_rec(d_solver,
1081 : : funs.size(),
1082 : : funs.data(),
1083 : : nvars.data(),
1084 : : vars.data(),
1085 : : terms.data(),
1086 : : false),
1087 : : "require a logic with quantifiers");
1088 [ + - ][ + - ]: 250 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
1089 : :
1090 : 1000 : TEST_F(TestCApiBlackSolver, define_funs_rec_global)
1091 : : {
1092 : 250 : std::vector<Cvc5Sort> domain = {d_bool};
1093 : : Cvc5Sort fun_sort =
1094 : 250 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool);
1095 : 250 : cvc5_push(d_solver, 1);
1096 : :
1097 : 250 : Cvc5Term btrue = cvc5_mk_true(d_tm);
1098 : 250 : Cvc5Term b = cvc5_mk_var(d_tm, d_bool, "b");
1099 : 250 : Cvc5Term g = cvc5_mk_const(d_tm, fun_sort, "g");
1100 : : // (define-funs-rec ((g ((b Bool)) Bool)) (b))
1101 : 250 : std::vector<Cvc5Term> funs = {g};
1102 : 250 : std::vector<size_t> nvars = {1};
1103 : 250 : std::vector<Cvc5Term> vars1 = {b};
1104 : 250 : std::vector<const Cvc5Term*> vars = {vars1.data()};
1105 : 250 : std::vector<Cvc5Term> terms = {b};
1106 : :
1107 : 500 : cvc5_define_funs_rec(d_solver,
1108 : : funs.size(),
1109 : 250 : funs.data(),
1110 : : nvars.data(),
1111 : : vars.data(),
1112 : 250 : terms.data(),
1113 : : true);
1114 : :
1115 : : // (assert (not (g true)))
1116 : 250 : std::vector<Cvc5Term> args = {g, btrue};
1117 : 250 : Cvc5Term t = cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1118 : 250 : args = {t};
1119 : 250 : cvc5_assert_formula(
1120 : 250 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()));
1121 : 250 : Cvc5Result res = cvc5_check_sat(d_solver);
1122 [ - + ][ + - ]: 250 : ASSERT_TRUE(cvc5_result_is_unsat(res));
1123 : 250 : cvc5_pop(d_solver, 1);
1124 : : // (assert (not (g true)))
1125 : 250 : cvc5_assert_formula(
1126 : 250 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()));
1127 : 250 : res = cvc5_check_sat(d_solver);
1128 [ - + ][ + - ]: 250 : ASSERT_TRUE(cvc5_result_is_unsat(res));
1129 [ + - ][ + - ]: 250 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ]
1130 : :
1131 : 996 : TEST_F(TestCApiBlackSolver, get_assertions)
1132 : : {
1133 : 250 : Cvc5Term a = cvc5_mk_const(d_tm, d_bool, "a");
1134 : 250 : Cvc5Term b = cvc5_mk_const(d_tm, d_bool, "b");
1135 : 250 : cvc5_assert_formula(d_solver, a);
1136 : 250 : cvc5_assert_formula(d_solver, b);
1137 : : size_t size;
1138 : 250 : auto res = cvc5_get_assertions(d_solver, &size);
1139 [ - + ][ + - ]: 250 : ASSERT_EQ(size, 2);
1140 [ - + ][ + - ]: 250 : ASSERT_TRUE(cvc5_term_is_equal(a, res[0]));
1141 [ - + ][ + - ]: 250 : ASSERT_TRUE(cvc5_term_is_equal(b, res[1]));
1142 : 250 : ASSERT_DEATH(cvc5_get_assertions(nullptr, &size), "unexpected NULL argument");
1143 : 249 : ASSERT_DEATH(cvc5_get_assertions(d_solver, nullptr),
1144 : : "unexpected NULL argument");
1145 : : }
1146 : :
1147 : 986 : TEST_F(TestCApiBlackSolver, get_info)
1148 : : {
1149 [ - + ][ + - ]: 248 : ASSERT_EQ(cvc5_get_info(d_solver, "name"), std::string("\"cvc5\""));
1150 : 248 : ASSERT_DEATH(cvc5_get_info(d_solver, "asdf"), "unrecognized flag");
1151 : 247 : ASSERT_DEATH(cvc5_get_info(nullptr, "name"), "unexpected NULL argument");
1152 : 246 : ASSERT_DEATH(cvc5_get_info(d_solver, nullptr), "unexpected NULL argument");
1153 : : }
1154 : :
1155 : 974 : TEST_F(TestCApiBlackSolver, get_option)
1156 : : {
1157 [ - + ][ + - ]: 245 : ASSERT_EQ(cvc5_get_option(d_solver, "incremental"), std::string("true"));
1158 : 245 : ASSERT_DEATH(cvc5_get_option(d_solver, "asdf"), "Unrecognized option");
1159 : 244 : ASSERT_DEATH(cvc5_get_option(nullptr, "incremental"),
1160 : : "unexpected NULL argument");
1161 : 243 : ASSERT_DEATH(cvc5_get_option(d_solver, nullptr), "unexpected NULL argument");
1162 : : }
1163 : :
1164 : 964 : TEST_F(TestCApiBlackSolver, get_option_names)
1165 : : {
1166 : : size_t size;
1167 : 242 : auto names = cvc5_get_option_names(d_solver, &size);
1168 [ - + ][ + - ]: 242 : ASSERT_TRUE(size > 100);
1169 : 242 : bool found_verbose = false;
1170 : 242 : bool found_foobar = false;
1171 [ + + ]: 128260 : for (size_t i = 0; i < size; ++i)
1172 : : {
1173 [ + + ]: 128018 : if (names[i] == std::string("verbose"))
1174 : : {
1175 : 242 : found_verbose = true;
1176 : : }
1177 [ - + ]: 127776 : else if (std::string(names[i]) == "foobar")
1178 : : {
1179 : 0 : found_foobar = true;
1180 : : }
1181 : : }
1182 [ - + ][ + - ]: 242 : ASSERT_TRUE(found_verbose);
1183 [ - + ][ + - ]: 242 : ASSERT_FALSE(found_foobar);
1184 : 242 : ASSERT_DEATH(cvc5_get_option_names(nullptr, &size),
1185 : : "unexpected NULL argument");
1186 : 241 : ASSERT_DEATH(cvc5_get_option_names(d_solver, nullptr),
1187 : : "unexpected NULL argument");
1188 : : }
1189 : :
1190 : 952 : TEST_F(TestCApiBlackSolver, get_option_info)
1191 : : {
1192 : : Cvc5OptionInfo info;
1193 : 240 : ASSERT_DEATH(cvc5_get_option_info(nullptr, "verbose", &info),
1194 : : "unexpected NULL argument");
1195 : 239 : ASSERT_DEATH(cvc5_get_option_info(d_solver, nullptr, &info),
1196 : : "unexpected NULL argument");
1197 : 238 : ASSERT_DEATH(cvc5_get_option_info(d_solver, "verbose", nullptr),
1198 : : "unexpected NULL argument");
1199 : 237 : ASSERT_DEATH(cvc5_get_option_info(d_solver, "asdf-invalid", &info),
1200 : : "Unrecognized option");
1201 : :
1202 : 236 : cvc5_set_option(d_solver, "verbosity", "2");
1203 : :
1204 : 236 : cvc5_get_option_info(d_solver, "verbose", &info);
1205 [ - + ][ + - ]: 472 : ASSERT_EQ(info.name, std::string("verbose"));
1206 [ - + ][ + - ]: 236 : ASSERT_EQ(info.num_aliases, 0);
1207 [ - + ][ + - ]: 236 : ASSERT_EQ(info.category, CVC5_OPTION_CATEGORY_COMMON);
1208 [ - + ][ + - ]: 236 : ASSERT_FALSE(info.is_set_by_user);
1209 [ - + ][ + - ]: 236 : ASSERT_EQ(info.kind, CVC5_OPTION_INFO_VOID);
1210 [ - + ]: 236 : ASSERT_EQ(cvc5_option_info_to_string(&info),
1211 [ + - ]: 236 : std::string("OptionInfo{ verbose | void }"));
1212 : :
1213 : : // bool kind
1214 : 236 : cvc5_get_option_info(d_solver, "print-success", &info);
1215 [ - + ][ + - ]: 472 : ASSERT_EQ(info.name, std::string("print-success"));
1216 [ - + ][ + - ]: 236 : ASSERT_EQ(info.num_aliases, 0);
1217 [ - + ][ + - ]: 236 : ASSERT_EQ(info.kind, CVC5_OPTION_INFO_BOOL);
1218 [ - + ][ + - ]: 236 : ASSERT_EQ(info.category, CVC5_OPTION_CATEGORY_COMMON);
1219 [ - + ][ + - ]: 236 : ASSERT_FALSE(info.is_set_by_user);
1220 [ - + ][ + - ]: 236 : ASSERT_EQ(info.info_bool.dflt, false);
1221 [ - + ][ + - ]: 236 : ASSERT_EQ(info.info_bool.cur, false);
1222 [ - + ]: 236 : ASSERT_EQ(cvc5_option_info_to_string(&info),
1223 : : std::string(
1224 [ + - ]: 236 : "OptionInfo{ print-success | bool | false | default false }"));
1225 : :
1226 : : // int64 kind
1227 : 236 : cvc5_get_option_info(d_solver, "verbosity", &info);
1228 [ - + ][ + - ]: 472 : ASSERT_EQ(info.name, std::string("verbosity"));
1229 [ - + ][ + - ]: 236 : ASSERT_EQ(info.num_aliases, 0);
1230 [ - + ][ + - ]: 236 : ASSERT_EQ(info.category, CVC5_OPTION_CATEGORY_COMMON);
1231 [ - + ][ + - ]: 236 : ASSERT_TRUE(info.is_set_by_user);
1232 [ - + ][ + - ]: 236 : ASSERT_EQ(info.kind, CVC5_OPTION_INFO_INT64);
1233 [ - + ][ + - ]: 236 : ASSERT_EQ(info.info_int.dflt, 0);
1234 [ - + ][ + - ]: 236 : ASSERT_EQ(info.info_int.cur, 2);
1235 [ + - ][ + - ]: 236 : ASSERT_FALSE(info.info_int.has_min || info.info_int.has_max);
[ - + ][ + - ]
1236 [ - + ]: 236 : ASSERT_EQ(
1237 : : cvc5_option_info_to_string(&info),
1238 : : std::string(
1239 [ + - ]: 236 : "OptionInfo{ verbosity | set by user | int64_t | 2 | default 0 }"));
1240 : :
1241 : : // uint64 kind
1242 : 236 : cvc5_get_option_info(d_solver, "rlimit", &info);
1243 [ - + ][ + - ]: 472 : ASSERT_EQ(info.name, std::string("rlimit"));
1244 [ - + ][ + - ]: 236 : ASSERT_EQ(info.num_aliases, 0);
1245 [ - + ][ + - ]: 236 : ASSERT_EQ(info.category, CVC5_OPTION_CATEGORY_COMMON);
1246 [ - + ][ + - ]: 236 : ASSERT_FALSE(info.is_set_by_user);
1247 [ - + ][ + - ]: 236 : ASSERT_EQ(info.kind, CVC5_OPTION_INFO_UINT64);
1248 [ - + ][ + - ]: 236 : ASSERT_EQ(info.info_uint.dflt, 0);
1249 [ - + ][ + - ]: 236 : ASSERT_EQ(info.info_uint.cur, 0);
1250 [ + - ][ + - ]: 236 : ASSERT_FALSE(info.info_uint.has_min || info.info_uint.has_max);
[ - + ][ + - ]
1251 [ - + ]: 236 : ASSERT_EQ(cvc5_option_info_to_string(&info),
1252 [ + - ]: 236 : std::string("OptionInfo{ rlimit | uint64_t | 0 | default 0 }"));
1253 : :
1254 : : // double kind
1255 : 236 : cvc5_get_option_info(d_solver, "random-freq", &info);
1256 [ - + ][ + - ]: 472 : ASSERT_EQ(info.name, std::string("random-freq"));
1257 [ - + ][ + - ]: 236 : ASSERT_EQ(info.num_aliases, 1);
1258 [ - + ][ + - ]: 472 : ASSERT_EQ(info.aliases[0], std::string("random-frequency"));
1259 [ - + ][ + - ]: 236 : ASSERT_EQ(info.category, CVC5_OPTION_CATEGORY_EXPERT);
1260 [ - + ][ + - ]: 236 : ASSERT_FALSE(info.is_set_by_user);
1261 [ - + ][ + - ]: 236 : ASSERT_EQ(info.kind, CVC5_OPTION_INFO_DOUBLE);
1262 [ - + ][ + - ]: 236 : ASSERT_EQ(info.info_double.dflt, 0.0);
1263 [ - + ][ + - ]: 236 : ASSERT_EQ(info.info_double.cur, 0.0);
1264 [ + - ][ + - ]: 236 : ASSERT_TRUE(info.info_double.has_min && info.info_double.has_max);
[ - + ][ + - ]
1265 [ - + ][ + - ]: 236 : ASSERT_EQ(info.info_double.min, 0.0);
1266 [ - + ][ + - ]: 236 : ASSERT_EQ(info.info_double.min, 0.0);
1267 [ - + ]: 236 : ASSERT_EQ(cvc5_option_info_to_string(&info),
1268 : : std::string("OptionInfo{ random-freq, random-frequency | double | "
1269 [ + - ]: 236 : "0 | default 0 | 0 <= x <= 1 }"));
1270 : :
1271 : : // string kind
1272 : 236 : cvc5_get_option_info(d_solver, "force-logic", &info);
1273 [ - + ][ + - ]: 472 : ASSERT_EQ(info.name, std::string("force-logic"));
1274 [ - + ][ + - ]: 236 : ASSERT_EQ(info.num_aliases, 0);
1275 [ - + ][ + - ]: 236 : ASSERT_EQ(info.category, CVC5_OPTION_CATEGORY_COMMON);
1276 [ - + ][ + - ]: 236 : ASSERT_FALSE(info.is_set_by_user);
1277 [ - + ][ + - ]: 236 : ASSERT_EQ(info.kind, CVC5_OPTION_INFO_STR);
1278 [ - + ][ + - ]: 472 : ASSERT_EQ(info.info_str.dflt, std::string(""));
1279 [ - + ][ + - ]: 472 : ASSERT_EQ(info.info_str.cur, std::string(""));
1280 [ - + ]: 236 : ASSERT_EQ(
1281 : : cvc5_option_info_to_string(&info),
1282 [ + - ]: 236 : std::string("OptionInfo{ force-logic | string | \"\" | default \"\" }"));
1283 : :
1284 : : // mode option
1285 : 236 : cvc5_get_option_info(d_solver, "simplification", &info);
1286 [ - + ][ + - ]: 472 : ASSERT_EQ(info.name, std::string("simplification"));
1287 [ - + ][ + - ]: 236 : ASSERT_EQ(info.num_aliases, 1);
1288 [ - + ][ + - ]: 472 : ASSERT_EQ(info.aliases[0], std::string("simplification-mode"));
1289 [ - + ][ + - ]: 236 : ASSERT_EQ(info.category, CVC5_OPTION_CATEGORY_REGULAR);
1290 [ - + ][ + - ]: 236 : ASSERT_FALSE(info.is_set_by_user);
1291 [ - + ][ + - ]: 236 : ASSERT_EQ(info.kind, CVC5_OPTION_INFO_MODES);
1292 [ - + ][ + - ]: 472 : ASSERT_EQ(info.info_mode.dflt, std::string("batch"));
1293 [ - + ][ + - ]: 472 : ASSERT_EQ(info.info_mode.cur, std::string("batch"));
1294 [ - + ][ + - ]: 236 : ASSERT_EQ(info.info_mode.num_modes, 2);
1295 : 708 : ASSERT_TRUE((info.info_mode.modes[0] == std::string("batch"))
1296 [ + - ]: 236 : || (info.info_mode.modes[1] == std::string("batch")));
1297 : 1180 : ASSERT_TRUE((info.info_mode.modes[0] == std::string("none"))
1298 [ + - ]: 236 : || (info.info_mode.modes[1] == std::string("none")));
1299 [ - + ]: 236 : ASSERT_EQ(cvc5_option_info_to_string(&info),
1300 : : std::string("OptionInfo{ simplification, simplification-mode | "
1301 [ + - ]: 236 : "mode | batch | default batch | modes: batch, none }"));
1302 : : }
1303 : :
1304 : 938 : TEST_F(TestCApiBlackSolver, get_unsat_assumptions1)
1305 : : {
1306 : 236 : cvc5_set_option(d_solver, "incremental", "false");
1307 : 236 : std::vector<Cvc5Term> assumptions = {cvc5_mk_false(d_tm)};
1308 : 236 : cvc5_check_sat_assuming(d_solver, assumptions.size(), assumptions.data());
1309 : : size_t size;
1310 : 236 : ASSERT_DEATH(cvc5_get_unsat_assumptions(nullptr, &size),
1311 : : "unexpected NULL argument");
1312 : 235 : ASSERT_DEATH(cvc5_get_unsat_assumptions(d_solver, nullptr),
1313 : : "unexpected NULL argument");
1314 : 234 : ASSERT_DEATH(cvc5_get_unsat_assumptions(d_solver, &size),
1315 : : "cannot get unsat assumptions");
1316 [ + - ]: 233 : }
1317 : :
1318 : 930 : TEST_F(TestCApiBlackSolver, get_unsat_assumptions2)
1319 : : {
1320 : 233 : cvc5_set_option(d_solver, "incremental", "false");
1321 : 233 : cvc5_set_option(d_solver, "produce-unsat-assumptions", "false");
1322 : 233 : std::vector<Cvc5Term> assumptions = {cvc5_mk_false(d_tm)};
1323 : 233 : cvc5_check_sat_assuming(d_solver, assumptions.size(), assumptions.data());
1324 : : size_t size;
1325 : 233 : ASSERT_DEATH(cvc5_get_unsat_assumptions(d_solver, &size),
1326 : : "cannot get unsat assumptions");
1327 [ + - ]: 232 : }
1328 : :
1329 : 926 : TEST_F(TestCApiBlackSolver, get_unsat_assumptions3)
1330 : : {
1331 : 232 : cvc5_set_option(d_solver, "incremental", "true");
1332 : 232 : cvc5_set_option(d_solver, "produce-unsat-assumptions", "true");
1333 : 232 : std::vector<Cvc5Term> assumptions = {cvc5_mk_false(d_tm)};
1334 : 232 : cvc5_check_sat_assuming(d_solver, assumptions.size(), assumptions.data());
1335 : : size_t size;
1336 : 232 : const Cvc5Term* res = cvc5_get_unsat_assumptions(d_solver, &size);
1337 [ - + ][ + - ]: 232 : ASSERT_EQ(size, 1);
1338 [ - + ][ + - ]: 232 : ASSERT_TRUE(cvc5_term_is_equal(res[0], cvc5_mk_false(d_tm)));
1339 : 232 : assumptions = {cvc5_mk_true(d_tm)};
1340 : 232 : cvc5_check_sat_assuming(d_solver, assumptions.size(), assumptions.data());
1341 : 232 : ASSERT_DEATH(cvc5_get_unsat_assumptions(d_solver, &size),
1342 : : "cannot get unsat assumptions");
1343 [ + - ]: 231 : }
1344 : :
1345 : 920 : TEST_F(TestCApiBlackSolver, get_unsat_core0)
1346 : : {
1347 : 231 : cvc5_set_option(d_solver, "incremental", "true");
1348 : 231 : cvc5_assert_formula(d_solver, cvc5_mk_false(d_tm));
1349 : 231 : cvc5_check_sat(d_solver);
1350 : : size_t size;
1351 : 231 : ASSERT_DEATH(cvc5_get_unsat_core(nullptr, &size), "unexpected NULL argument");
1352 : 230 : ASSERT_DEATH(cvc5_get_unsat_core(d_solver, nullptr),
1353 : : "unexpected NULL argument");
1354 : : }
1355 : :
1356 : 914 : TEST_F(TestCApiBlackSolver, get_unsat_core1)
1357 : : {
1358 : 229 : cvc5_set_option(d_solver, "incremental", "false");
1359 : 229 : cvc5_assert_formula(d_solver, cvc5_mk_false(d_tm));
1360 : 229 : cvc5_check_sat(d_solver);
1361 : : size_t size;
1362 : 229 : ASSERT_DEATH(cvc5_get_unsat_core(d_solver, &size), "cannot get unsat core");
1363 : : }
1364 : :
1365 : 910 : TEST_F(TestCApiBlackSolver, get_unsat_core2)
1366 : : {
1367 : 228 : cvc5_set_option(d_solver, "incremental", "false");
1368 : 228 : cvc5_set_option(d_solver, "produce-unsat-cores", "false");
1369 : 228 : cvc5_assert_formula(d_solver, cvc5_mk_false(d_tm));
1370 : 228 : cvc5_check_sat(d_solver);
1371 : : size_t size;
1372 : 228 : ASSERT_DEATH(cvc5_get_unsat_core(d_solver, &size), "cannot get unsat core");
1373 : : }
1374 : :
1375 : 908 : TEST_F(TestCApiBlackSolver, get_unsat_core_and_proof)
1376 : : {
1377 : 227 : cvc5_set_option(d_solver, "incremental", "true");
1378 : 227 : cvc5_set_option(d_solver, "produce-unsat-cores", "true");
1379 : 227 : cvc5_set_option(d_solver, "produce-proofs", "true");
1380 : :
1381 : 227 : std::vector<Cvc5Sort> domain = {d_uninterpreted};
1382 : : Cvc5Sort u_to_int =
1383 : 227 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
1384 : 227 : domain = {d_int};
1385 : : Cvc5Sort int_pred =
1386 : 227 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool);
1387 : :
1388 : 227 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
1389 : 227 : Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y");
1390 : 227 : Cvc5Term f = cvc5_mk_const(d_tm, u_to_int, "f");
1391 : 227 : Cvc5Term p = cvc5_mk_const(d_tm, int_pred, "p");
1392 : 227 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
1393 : 227 : Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1);
1394 : 227 : std::vector<Cvc5Term> args = {f, x};
1395 : : Cvc5Term f_x =
1396 : 227 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1397 : 227 : args = {f, y};
1398 : : Cvc5Term f_y =
1399 : 227 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1400 : 227 : args = {f_x, f_y};
1401 : 227 : Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
1402 : 227 : args = {p, zero};
1403 : : Cvc5Term p_0 =
1404 : 227 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1405 : 227 : args = {p, f_y};
1406 : : Cvc5Term p_f_y =
1407 : 227 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1408 : :
1409 : 227 : args = {zero, f_x};
1410 : 227 : cvc5_assert_formula(
1411 : 227 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
1412 : 227 : args = {zero, f_y};
1413 : 227 : cvc5_assert_formula(
1414 : 227 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
1415 : 227 : args = {sum, one};
1416 : 227 : cvc5_assert_formula(
1417 : 227 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
1418 : 227 : cvc5_assert_formula(d_solver, p_0);
1419 : 227 : args = {p_f_y};
1420 : 227 : cvc5_assert_formula(
1421 : 227 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()));
1422 [ - + ][ + - ]: 227 : ASSERT_TRUE(cvc5_result_is_unsat(cvc5_check_sat(d_solver)));
1423 : :
1424 : : size_t uc_size, proof_size;
1425 : 227 : const Cvc5Term* uc = cvc5_get_unsat_core(d_solver, &uc_size);
1426 [ - + ][ + - ]: 227 : ASSERT_TRUE(uc_size > 0);
1427 : :
1428 : 227 : (void)cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, &proof_size);
1429 : 227 : (void)cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_SAT, &proof_size);
1430 : :
1431 : 227 : cvc5_reset_assertions(d_solver);
1432 [ + + ]: 908 : for (size_t i = 0; i < uc_size; ++i)
1433 : : {
1434 : 681 : cvc5_assert_formula(d_solver, uc[i]);
1435 : : }
1436 : 227 : Cvc5Result res = cvc5_check_sat(d_solver);
1437 [ - + ][ + - ]: 227 : ASSERT_TRUE(cvc5_result_is_unsat(res));
1438 : 227 : (void)cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, &proof_size);
1439 [ + - ][ + - ]: 227 : }
1440 : :
1441 : 902 : TEST_F(TestCApiBlackSolver, get_unsat_core_lemmas1)
1442 : : {
1443 : 227 : cvc5_set_option(d_solver, "produce-unsat-cores", "true");
1444 : 227 : cvc5_set_option(d_solver, "unsat-cores-mode", "sat-proof");
1445 : :
1446 : : size_t size;
1447 : : // cannot ask before a check sat
1448 : 227 : ASSERT_DEATH(cvc5_get_unsat_core_lemmas(d_solver, &size),
1449 : : "cannot get unsat core");
1450 : :
1451 : 226 : cvc5_assert_formula(d_solver, cvc5_mk_false(d_tm));
1452 [ - + ][ + - ]: 226 : ASSERT_TRUE(cvc5_result_is_unsat(cvc5_check_sat(d_solver)));
1453 : 226 : (void)cvc5_get_unsat_core_lemmas(d_solver, &size);
1454 : :
1455 : 226 : ASSERT_DEATH(cvc5_get_unsat_core_lemmas(nullptr, &size),
1456 : : "unexpected NULL argument");
1457 : 225 : ASSERT_DEATH(cvc5_get_unsat_core_lemmas(d_solver, nullptr),
1458 : : "unexpected NULL argument");
1459 : : }
1460 : :
1461 : 896 : TEST_F(TestCApiBlackSolver, get_unsat_core_lemmas2)
1462 : : {
1463 : 224 : cvc5_set_option(d_solver, "incremental", "true");
1464 : 224 : cvc5_set_option(d_solver, "produce-unsat-cores", "true");
1465 : 224 : cvc5_set_option(d_solver, "produce-proofs", "true");
1466 : :
1467 : 224 : std::vector<Cvc5Sort> domain = {d_uninterpreted};
1468 : : Cvc5Sort u_to_int =
1469 : 224 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
1470 : 224 : domain = {d_int};
1471 : : Cvc5Sort int_pred =
1472 : 224 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool);
1473 : :
1474 : 224 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
1475 : 224 : Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y");
1476 : 224 : Cvc5Term f = cvc5_mk_const(d_tm, u_to_int, "f");
1477 : 224 : Cvc5Term p = cvc5_mk_const(d_tm, int_pred, "p");
1478 : 224 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
1479 : 224 : Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1);
1480 : 224 : std::vector<Cvc5Term> args = {f, x};
1481 : : Cvc5Term f_x =
1482 : 224 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1483 : 224 : args = {f, y};
1484 : : Cvc5Term f_y =
1485 : 224 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1486 : 224 : args = {f_x, f_y};
1487 : 224 : Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
1488 : 224 : args = {p, zero};
1489 : : Cvc5Term p_0 =
1490 : 224 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1491 : 224 : args = {p, f_y};
1492 : : Cvc5Term p_f_y =
1493 : 224 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1494 : :
1495 : 224 : args = {zero, f_x};
1496 : 224 : cvc5_assert_formula(
1497 : 224 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
1498 : 224 : args = {zero, f_y};
1499 : 224 : cvc5_assert_formula(
1500 : 224 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
1501 : 224 : args = {sum, one};
1502 : 224 : cvc5_assert_formula(
1503 : 224 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
1504 : 224 : cvc5_assert_formula(d_solver, p_0);
1505 : 224 : args = {p_f_y};
1506 : 224 : cvc5_assert_formula(
1507 : 224 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()));
1508 [ - + ][ + - ]: 224 : ASSERT_TRUE(cvc5_result_is_unsat(cvc5_check_sat(d_solver)));
1509 : :
1510 : : size_t size;
1511 : 224 : (void)cvc5_get_unsat_core_lemmas(d_solver, &size);
1512 [ + - ][ + - ]: 224 : }
1513 : :
1514 : 886 : TEST_F(TestCApiBlackSolver, get_difficulty)
1515 : : {
1516 : 224 : cvc5_set_option(d_solver, "produce-difficulty", "true");
1517 : : size_t size;
1518 : : Cvc5Term *inputs, *values;
1519 : 224 : ASSERT_DEATH(cvc5_get_difficulty(nullptr, &size, &inputs, &values),
1520 : : "unexpected NULL argument");
1521 : 223 : ASSERT_DEATH(cvc5_get_difficulty(d_solver, nullptr, &inputs, &values),
1522 : : "unexpected NULL argument");
1523 : 222 : ASSERT_DEATH(cvc5_get_difficulty(d_solver, &size, nullptr, &values),
1524 : : "unexpected NULL argument");
1525 : 221 : ASSERT_DEATH(cvc5_get_difficulty(d_solver, &size, &inputs, nullptr),
1526 : : "unexpected NULL argument");
1527 : : // cannot ask before a check sat
1528 : 220 : ASSERT_DEATH(cvc5_get_difficulty(d_solver, &size, &inputs, &values),
1529 : : "cannot get difficulty");
1530 : 219 : cvc5_check_sat(d_solver);
1531 : 219 : cvc5_get_difficulty(d_solver, &size, &inputs, &values);
1532 : : }
1533 : :
1534 : 874 : TEST_F(TestCApiBlackSolver, get_difficulty2)
1535 : : {
1536 : 219 : cvc5_check_sat(d_solver);
1537 : : size_t size;
1538 : : Cvc5Term *inputs, *values;
1539 : : // option is not set
1540 : 219 : ASSERT_DEATH(cvc5_get_difficulty(d_solver, &size, &inputs, &values),
1541 : : "Cannot get difficulty");
1542 : : }
1543 : :
1544 : 872 : TEST_F(TestCApiBlackSolver, get_difficulty3)
1545 : : {
1546 : 218 : cvc5_set_option(d_solver, "produce-difficulty", "true");
1547 : : size_t size;
1548 : : Cvc5Term *inputs, *values;
1549 : 218 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
1550 : 218 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
1551 : 218 : Cvc5Term ten = cvc5_mk_integer_int64(d_tm, 10);
1552 : 218 : std::vector<Cvc5Term> args = {x, ten};
1553 : 218 : Cvc5Term f0 = cvc5_mk_term(d_tm, CVC5_KIND_GEQ, args.size(), args.data());
1554 : 218 : args = {zero, x};
1555 : 218 : Cvc5Term f1 = cvc5_mk_term(d_tm, CVC5_KIND_GEQ, args.size(), args.data());
1556 : 218 : cvc5_assert_formula(d_solver, f0);
1557 : 218 : cvc5_assert_formula(d_solver, f1);
1558 : 218 : cvc5_check_sat(d_solver);
1559 : 218 : cvc5_get_difficulty(d_solver, &size, &inputs, &values);
1560 [ - + ][ + - ]: 218 : ASSERT_EQ(size, 2);
1561 : : // difficulty should map assertions to integer values
1562 [ + + ]: 654 : for (size_t i = 0; i < size; ++i)
1563 : : {
1564 [ + + ][ + - ]: 436 : ASSERT_TRUE(cvc5_term_is_equal(inputs[i], f0)
[ - + ]
1565 [ + - ]: 436 : || cvc5_term_is_equal(inputs[i], f1));
1566 [ - + ][ + - ]: 436 : ASSERT_EQ(cvc5_term_get_kind(values[i]), CVC5_KIND_CONST_INTEGER);
1567 : : }
1568 [ + - ]: 218 : }
1569 : :
1570 : 866 : TEST_F(TestCApiBlackSolver, get_timeout_core)
1571 : : {
1572 : 218 : cvc5_set_option(d_solver, "timeout-core-timeout", "100");
1573 : 218 : cvc5_set_option(d_solver, "produce-unsat-cores", "true");
1574 : :
1575 : 218 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
1576 : 218 : Cvc5Term tt = cvc5_mk_true(d_tm);
1577 : 218 : std::vector<Cvc5Term> args = {x, x};
1578 : 218 : args = {cvc5_mk_term(d_tm, CVC5_KIND_MULT, args.size(), args.data()),
1579 : 218 : cvc5_mk_integer(d_tm, "501240912901901249014210220059591")};
1580 : 218 : Cvc5Term hard = cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
1581 : 218 : cvc5_assert_formula(d_solver, tt);
1582 : 218 : cvc5_assert_formula(d_solver, hard);
1583 : :
1584 : : Cvc5Result result;
1585 : : size_t size;
1586 : 218 : const Cvc5Term* core = cvc5_get_timeout_core(d_solver, &result, &size);
1587 [ - + ][ + - ]: 218 : ASSERT_TRUE(cvc5_result_is_unknown(result));
1588 [ - + ][ + - ]: 218 : ASSERT_EQ(size, 1);
1589 [ - + ][ + - ]: 218 : ASSERT_TRUE(cvc5_term_is_equal(core[0], hard));
1590 : :
1591 : 218 : ASSERT_DEATH(cvc5_get_timeout_core(nullptr, &result, &size),
1592 : : "unexpected NULL argument");
1593 : 217 : ASSERT_DEATH(cvc5_get_timeout_core(d_solver, nullptr, &size),
1594 : : "unexpected NULL argument");
1595 : 216 : ASSERT_DEATH(cvc5_get_timeout_core(d_solver, &result, nullptr),
1596 : : "unexpected NULL argument");
1597 [ + - ]: 215 : }
1598 : :
1599 : 860 : TEST_F(TestCApiBlackSolver, get_timeout_core_unsat)
1600 : : {
1601 : 215 : cvc5_set_option(d_solver, "produce-unsat-cores", "true");
1602 : 215 : Cvc5Term ff = cvc5_mk_false(d_tm);
1603 : 215 : Cvc5Term tt = cvc5_mk_true(d_tm);
1604 : 215 : cvc5_assert_formula(d_solver, tt);
1605 : 215 : cvc5_assert_formula(d_solver, ff);
1606 : 215 : cvc5_assert_formula(d_solver, tt);
1607 : :
1608 : : Cvc5Result result;
1609 : : size_t size;
1610 : 215 : const Cvc5Term* core = cvc5_get_timeout_core(d_solver, &result, &size);
1611 [ - + ][ + - ]: 215 : ASSERT_TRUE(cvc5_result_is_unsat(result));
1612 [ - + ][ + - ]: 215 : ASSERT_EQ(size, 1);
1613 [ - + ][ + - ]: 215 : ASSERT_TRUE(cvc5_term_is_equal(core[0], ff));
1614 : : }
1615 : :
1616 : 860 : TEST_F(TestCApiBlackSolver, get_timeout_core_assuming)
1617 : : {
1618 : 215 : cvc5_set_option(d_solver, "produce-unsat-cores", "true");
1619 : 215 : Cvc5Term ff = cvc5_mk_false(d_tm);
1620 : 215 : Cvc5Term tt = cvc5_mk_true(d_tm);
1621 : 215 : cvc5_assert_formula(d_solver, tt);
1622 : :
1623 : 215 : std::vector<Cvc5Term> assumptions = {ff, tt};
1624 : : Cvc5Result result;
1625 : : size_t size;
1626 : 215 : const Cvc5Term* core = cvc5_get_timeout_core_assuming(
1627 : 215 : d_solver, assumptions.size(), assumptions.data(), &result, &size);
1628 [ - + ][ + - ]: 215 : ASSERT_TRUE(cvc5_result_is_unsat(result));
1629 [ - + ][ + - ]: 215 : ASSERT_EQ(size, 1);
1630 [ - + ][ + - ]: 215 : ASSERT_TRUE(cvc5_term_is_equal(core[0], ff));
1631 [ + - ]: 215 : }
1632 : :
1633 : 858 : TEST_F(TestCApiBlackSolver, get_timeout_core_assuming_empty)
1634 : : {
1635 : 215 : cvc5_set_option(d_solver, "produce-unsat-cores", "true");
1636 : 215 : std::vector<Cvc5Term> assumptions = {};
1637 : : Cvc5Result result;
1638 : : size_t size;
1639 : 215 : ASSERT_DEATH(
1640 : : cvc5_get_timeout_core_assuming(
1641 : : d_solver, assumptions.size(), assumptions.data(), &result, &size),
1642 : : "unexpected NULL argument");
1643 [ + - ]: 214 : }
1644 : :
1645 : 852 : TEST_F(TestCApiBlackSolver, get_proof_and_proof_to_string)
1646 : : {
1647 : 214 : cvc5_set_option(d_solver, "produce-proofs", "true");
1648 : :
1649 : 214 : std::vector<Cvc5Sort> domain = {d_uninterpreted};
1650 : : Cvc5Sort u_to_int =
1651 : 214 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
1652 : 214 : domain = {d_int};
1653 : : Cvc5Sort int_pred =
1654 : 214 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool);
1655 : :
1656 : 214 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
1657 : 214 : Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y");
1658 : 214 : Cvc5Term f = cvc5_mk_const(d_tm, u_to_int, "f");
1659 : 214 : Cvc5Term p = cvc5_mk_const(d_tm, int_pred, "p");
1660 : 214 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
1661 : 214 : Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1);
1662 : 214 : std::vector<Cvc5Term> args = {f, x};
1663 : : Cvc5Term f_x =
1664 : 214 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1665 : 214 : args = {f, y};
1666 : : Cvc5Term f_y =
1667 : 214 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1668 : 214 : args = {f_x, f_y};
1669 : 214 : Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
1670 : 214 : args = {p, zero};
1671 : : Cvc5Term p_0 =
1672 : 214 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1673 : 214 : args = {p, f_y};
1674 : : Cvc5Term p_f_y =
1675 : 214 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1676 : :
1677 : 214 : args = {zero, f_x};
1678 : 214 : cvc5_assert_formula(
1679 : 214 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
1680 : 214 : args = {zero, f_y};
1681 : 214 : cvc5_assert_formula(
1682 : 214 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
1683 : 214 : args = {sum, one};
1684 : 214 : cvc5_assert_formula(
1685 : 214 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
1686 : 214 : cvc5_assert_formula(d_solver, p_0);
1687 : 214 : args = {p_f_y};
1688 : 214 : cvc5_assert_formula(
1689 : 214 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()));
1690 [ - + ][ + - ]: 214 : ASSERT_TRUE(cvc5_result_is_unsat(cvc5_check_sat(d_solver)));
1691 : :
1692 : : size_t size;
1693 : 214 : ASSERT_DEATH(cvc5_get_proof(nullptr, CVC5_PROOF_COMPONENT_FULL, &size),
1694 : : "unexpected NULL");
1695 : 213 : ASSERT_DEATH(cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, nullptr),
1696 : : "unexpected NULL");
1697 : :
1698 : : const Cvc5Proof* proofs =
1699 : 212 : cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, &size);
1700 [ - + ][ + - ]: 212 : ASSERT_TRUE(size > 0);
1701 : :
1702 : : std::string proof_str = cvc5_proof_to_string(
1703 : 212 : d_solver, proofs[0], CVC5_PROOF_FORMAT_DEFAULT, 0, nullptr, nullptr);
1704 [ - + ][ + - ]: 212 : ASSERT_FALSE(proof_str.empty());
1705 : : proof_str = cvc5_proof_to_string(
1706 : 212 : d_solver, proofs[0], CVC5_PROOF_FORMAT_ALETHE, 0, nullptr, nullptr);
1707 [ - + ][ + - ]: 212 : ASSERT_FALSE(proof_str.empty());
1708 : 212 : proofs = cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_SAT, &size);
1709 : : proof_str = cvc5_proof_to_string(
1710 : 212 : d_solver, proofs[0], CVC5_PROOF_FORMAT_NONE, 0, nullptr, nullptr);
1711 [ - + ][ + - ]: 212 : ASSERT_FALSE(proof_str.empty());
1712 [ + - ][ + - ]: 212 : }
1713 : :
1714 : 848 : TEST_F(TestCApiBlackSolver, proof_to_string_assertion_names)
1715 : : {
1716 : 212 : cvc5_set_option(d_solver, "produce-proofs", "true");
1717 : :
1718 : 212 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
1719 : 212 : Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y");
1720 : :
1721 : 212 : std::vector<Cvc5Term> args = {x, y};
1722 : : Cvc5Term x_eq_y =
1723 : 212 : cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
1724 : 212 : args = {x_eq_y};
1725 : : Cvc5Term not_x_eq_y =
1726 : 212 : cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data());
1727 : :
1728 : 212 : cvc5_assert_formula(d_solver, x_eq_y);
1729 : 212 : cvc5_assert_formula(d_solver, not_x_eq_y);
1730 : :
1731 [ - + ][ + - ]: 212 : ASSERT_TRUE(cvc5_result_is_unsat(cvc5_check_sat(d_solver)));
1732 : :
1733 : : size_t size;
1734 : : const Cvc5Proof* proofs =
1735 : 212 : cvc5_get_proof(d_solver, CVC5_PROOF_COMPONENT_FULL, &size);
1736 [ - + ][ + - ]: 212 : ASSERT_TRUE(size > 0);
1737 : 212 : const Cvc5Term assertions[2] = {x_eq_y, not_x_eq_y};
1738 : 212 : const char* names[2] = {"as1", "as2"};
1739 : : std::string proof_str = cvc5_proof_to_string(
1740 : 212 : d_solver, proofs[0], CVC5_PROOF_FORMAT_ALETHE, 2, assertions, names);
1741 [ - + ][ + - ]: 212 : ASSERT_FALSE(proof_str.empty());
1742 [ - + ][ + - ]: 212 : ASSERT_LT(proof_str.find("as1"), std::string::npos);
1743 [ - + ][ + - ]: 212 : ASSERT_LT(proof_str.find("as2"), std::string::npos);
1744 [ + - ]: 212 : }
1745 : :
1746 : 842 : TEST_F(TestCApiBlackSolver, get_learned_literals)
1747 : : {
1748 : 212 : cvc5_set_option(d_solver, "produce-learned-literals", "true");
1749 : :
1750 : : size_t size;
1751 : : // cannot ask before a check sat
1752 : 212 : ASSERT_DEATH(
1753 : : cvc5_get_learned_literals(d_solver, CVC5_LEARNED_LIT_TYPE_INPUT, &size),
1754 : : "cannot get learned literals");
1755 : :
1756 : 211 : cvc5_check_sat(d_solver);
1757 : 211 : (void)cvc5_get_learned_literals(d_solver, CVC5_LEARNED_LIT_TYPE_INPUT, &size);
1758 : 211 : (void)cvc5_get_learned_literals(
1759 : : d_solver, CVC5_LEARNED_LIT_TYPE_PREPROCESS, &size);
1760 : :
1761 : 211 : ASSERT_DEATH(
1762 : : cvc5_get_learned_literals(nullptr, CVC5_LEARNED_LIT_TYPE_INPUT, &size),
1763 : : "unexpected NULL argument");
1764 : 210 : ASSERT_DEATH(
1765 : : cvc5_get_learned_literals(d_solver, CVC5_LEARNED_LIT_TYPE_INPUT, nullptr),
1766 : : "unexpected NULL argument");
1767 : : }
1768 : :
1769 : 836 : TEST_F(TestCApiBlackSolver, get_learned_literals2)
1770 : : {
1771 : 209 : cvc5_set_option(d_solver, "produce-learned-literals", "true");
1772 : 209 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
1773 : 209 : Cvc5Term y = cvc5_mk_const(d_tm, d_int, "y");
1774 : 209 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
1775 : 209 : Cvc5Term ten = cvc5_mk_integer_int64(d_tm, 10);
1776 : 209 : std::vector<Cvc5Term> args = {x, ten};
1777 : 209 : Cvc5Term f0 = cvc5_mk_term(d_tm, CVC5_KIND_GEQ, args.size(), args.data());
1778 : 209 : args = {zero, x};
1779 : 209 : Cvc5Term args1 = cvc5_mk_term(d_tm, CVC5_KIND_GEQ, args.size(), args.data());
1780 : 209 : args = {y, zero};
1781 : 209 : Cvc5Term args2 = cvc5_mk_term(d_tm, CVC5_KIND_GEQ, args.size(), args.data());
1782 : 209 : args = {args1, args2};
1783 : 209 : Cvc5Term f1 = cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data());
1784 : 209 : cvc5_assert_formula(d_solver, f0);
1785 : 209 : cvc5_assert_formula(d_solver, f1);
1786 : 209 : cvc5_check_sat(d_solver);
1787 : : size_t size;
1788 : 209 : (void)cvc5_get_learned_literals(d_solver, CVC5_LEARNED_LIT_TYPE_INPUT, &size);
1789 : 209 : }
1790 : :
1791 : 834 : TEST_F(TestCApiBlackSolver, get_value1)
1792 : : {
1793 : 209 : cvc5_set_option(d_solver, "produce-models", "false");
1794 : 209 : Cvc5Term t = cvc5_mk_true(d_tm);
1795 : 209 : cvc5_assert_formula(d_solver, t);
1796 : 209 : cvc5_check_sat(d_solver);
1797 : 209 : ASSERT_DEATH(cvc5_get_value(d_solver, t), "cannot get value");
1798 : : }
1799 : :
1800 : 830 : TEST_F(TestCApiBlackSolver, get_value2)
1801 : : {
1802 : 208 : cvc5_set_option(d_solver, "produce-models", "true");
1803 : 208 : Cvc5Term t = cvc5_mk_false(d_tm);
1804 : 208 : cvc5_assert_formula(d_solver, t);
1805 : 208 : cvc5_check_sat(d_solver);
1806 : 208 : ASSERT_DEATH(cvc5_get_value(d_solver, t), "cannot get value");
1807 : : }
1808 : :
1809 : 812 : TEST_F(TestCApiBlackSolver, get_value3)
1810 : : {
1811 : 207 : cvc5_set_option(d_solver, "produce-models", "true");
1812 : :
1813 : 207 : std::vector<Cvc5Sort> domain = {d_uninterpreted};
1814 : : Cvc5Sort u_to_int =
1815 : 207 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_int);
1816 : 207 : domain = {d_int};
1817 : : Cvc5Sort int_pred =
1818 : 207 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool);
1819 : :
1820 : 207 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
1821 : 207 : Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y");
1822 : 207 : Cvc5Term z = cvc5_mk_const(d_tm, d_uninterpreted, "z");
1823 : 207 : Cvc5Term f = cvc5_mk_const(d_tm, u_to_int, "f");
1824 : 207 : Cvc5Term p = cvc5_mk_const(d_tm, int_pred, "p");
1825 : 207 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
1826 : 207 : Cvc5Term one = cvc5_mk_integer_int64(d_tm, 1);
1827 : 207 : std::vector<Cvc5Term> args = {f, x};
1828 : : Cvc5Term f_x =
1829 : 207 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1830 : 207 : args = {f, y};
1831 : : Cvc5Term f_y =
1832 : 207 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1833 : 207 : args = {f_x, f_y};
1834 : 207 : Cvc5Term sum = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
1835 : 207 : args = {p, zero};
1836 : : Cvc5Term p_0 =
1837 : 207 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1838 : 207 : args = {p, f_y};
1839 : : Cvc5Term p_f_y =
1840 : 207 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
1841 : :
1842 : 207 : args = {zero, f_x};
1843 : 207 : cvc5_assert_formula(
1844 : 207 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LEQ, args.size(), args.data()));
1845 : 207 : args = {zero, f_y};
1846 : 207 : cvc5_assert_formula(
1847 : 207 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LEQ, args.size(), args.data()));
1848 : 207 : args = {sum, one};
1849 : 207 : cvc5_assert_formula(
1850 : 207 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LEQ, args.size(), args.data()));
1851 : 207 : args = {p_0};
1852 : 207 : cvc5_assert_formula(
1853 : 207 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()));
1854 : 207 : cvc5_assert_formula(d_solver, p_f_y);
1855 [ - + ][ + - ]: 207 : ASSERT_TRUE(cvc5_result_is_sat(cvc5_check_sat(d_solver)));
1856 : :
1857 : 207 : (void)cvc5_get_value(d_solver, x);
1858 : 207 : (void)cvc5_get_value(d_solver, y);
1859 : 207 : (void)cvc5_get_value(d_solver, z);
1860 : 207 : (void)cvc5_get_value(d_solver, sum);
1861 : 207 : (void)cvc5_get_value(d_solver, p_f_y);
1862 : :
1863 : 207 : ASSERT_DEATH(cvc5_get_value(nullptr, x), "unexpected NULL argument");
1864 : 206 : ASSERT_DEATH(cvc5_get_value(d_solver, nullptr), "invalid term");
1865 : :
1866 : 205 : std::vector<Cvc5Term> a = {cvc5_get_value(d_solver, x),
1867 : 410 : cvc5_get_value(d_solver, y),
1868 : 205 : cvc5_get_value(d_solver, z)};
1869 : : size_t size;
1870 : 205 : std::vector<Cvc5Term> terms = {x, y, z};
1871 : : const Cvc5Term* b =
1872 : 205 : cvc5_get_values(d_solver, terms.size(), terms.data(), &size);
1873 [ - + ][ + - ]: 205 : ASSERT_EQ(size, 3);
1874 [ - + ][ + - ]: 205 : ASSERT_TRUE(cvc5_term_is_equal(a[0], b[0]));
1875 [ - + ][ + - ]: 205 : ASSERT_TRUE(cvc5_term_is_equal(a[1], b[1]));
1876 : 205 : ASSERT_DEATH(cvc5_get_values(nullptr, terms.size(), terms.data(), &size),
1877 : : "unexpected NULL argument");
1878 : 204 : ASSERT_DEATH(cvc5_get_values(d_solver, terms.size(), nullptr, &size),
1879 : : "unexpected NULL argument");
1880 : 203 : ASSERT_DEATH(cvc5_get_values(d_solver, terms.size(), terms.data(), nullptr),
1881 : : "unexpected NULL argument");
1882 : :
1883 : 202 : Cvc5* slv = cvc5_new(d_tm);
1884 : 202 : ASSERT_DEATH(cvc5_get_value(slv, x), "cannot get value");
1885 : 201 : cvc5_delete(slv);
1886 : :
1887 : 201 : slv = cvc5_new(d_tm);
1888 : 201 : cvc5_set_option(slv, "produce-models", "true");
1889 : 201 : ASSERT_DEATH(cvc5_get_value(slv, x), "cannot get value");
1890 : 200 : cvc5_delete(slv);
1891 : :
1892 : 200 : slv = cvc5_new(d_tm);
1893 : 200 : cvc5_set_option(slv, "produce-models", "true");
1894 : 200 : cvc5_check_sat(slv);
1895 : 200 : (void)cvc5_get_value(slv, x);
1896 : 200 : cvc5_delete(slv);
1897 : :
1898 : 200 : Cvc5TermManager* tm = cvc5_term_manager_new();
1899 : 200 : slv = cvc5_new(tm);
1900 : 200 : cvc5_set_option(slv, "produce-models", "true");
1901 : 200 : cvc5_check_sat(slv);
1902 : 200 : ASSERT_DEATH(cvc5_get_value(slv, x),
1903 : : "term is not associated with the term manager of this solver");
1904 : 199 : cvc5_delete(slv);
1905 : 199 : cvc5_term_manager_delete(tm);
1906 [ + - ][ + - ]: 199 : }
1907 : :
1908 : 786 : TEST_F(TestCApiBlackSolver, get_modelDomain_elements)
1909 : : {
1910 : 199 : cvc5_set_option(d_solver, "produce-models", "true");
1911 : 199 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
1912 : 199 : Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y");
1913 : 199 : Cvc5Term z = cvc5_mk_const(d_tm, d_uninterpreted, "z");
1914 : 199 : std::vector<Cvc5Term> args = {x, y, z};
1915 : 199 : Cvc5Term f = cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data());
1916 : 199 : cvc5_assert_formula(d_solver, f);
1917 : 199 : cvc5_check_sat(d_solver);
1918 : : size_t size;
1919 : 199 : (void)cvc5_get_model_domain_elements(d_solver, d_uninterpreted, &size);
1920 [ - + ][ + - ]: 199 : ASSERT_TRUE(size >= 3);
1921 : 199 : ASSERT_DEATH(cvc5_get_model_domain_elements(nullptr, d_uninterpreted, &size),
1922 : : "unexpected NULL argument");
1923 : 198 : ASSERT_DEATH(cvc5_get_model_domain_elements(d_solver, nullptr, &size),
1924 : : "invalid sort");
1925 : 197 : ASSERT_DEATH(
1926 : : cvc5_get_model_domain_elements(d_solver, d_uninterpreted, nullptr),
1927 : : "unexpected NULL argument");
1928 : 196 : ASSERT_DEATH(cvc5_get_model_domain_elements(d_solver, d_int, &size),
1929 : : "expected an uninterpreted sort");
1930 : :
1931 : 195 : Cvc5TermManager* tm = cvc5_term_manager_new();
1932 : 195 : Cvc5* slv = cvc5_new(tm);
1933 : 195 : cvc5_set_option(slv, "produce-models", "true");
1934 : 195 : cvc5_check_sat(slv);
1935 : 195 : ASSERT_DEATH(cvc5_get_model_domain_elements(slv, d_uninterpreted, &size),
1936 : : "sort is not associated with the term manager of this solver");
1937 : 194 : cvc5_delete(slv);
1938 : 194 : cvc5_term_manager_delete(tm);
1939 [ + - ]: 194 : }
1940 : :
1941 : 776 : TEST_F(TestCApiBlackSolver, getModel_domain_elements2)
1942 : : {
1943 : 194 : cvc5_set_option(d_solver, "produce-models", "true");
1944 : 194 : cvc5_set_option(d_solver, "finite-model-find", "true");
1945 : 194 : Cvc5Term x = cvc5_mk_var(d_tm, d_uninterpreted, "x");
1946 : 194 : Cvc5Term y = cvc5_mk_var(d_tm, d_uninterpreted, "y");
1947 : 194 : std::vector<Cvc5Term> args = {x, y};
1948 : 194 : Cvc5Term eq = cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
1949 : : Cvc5Term bvl =
1950 : 194 : cvc5_mk_term(d_tm, CVC5_KIND_VARIABLE_LIST, args.size(), args.data());
1951 : 194 : args = {bvl, eq};
1952 : 194 : Cvc5Term f = cvc5_mk_term(d_tm, CVC5_KIND_FORALL, args.size(), args.data());
1953 : 194 : cvc5_assert_formula(d_solver, f);
1954 : 194 : cvc5_check_sat(d_solver);
1955 : : size_t size;
1956 : 194 : (void)cvc5_get_model_domain_elements(d_solver, d_uninterpreted, &size);
1957 : : // a model for the above must interpret u as size 1
1958 [ - + ][ + - ]: 194 : ASSERT_EQ(size, 1);
1959 [ + - ]: 194 : }
1960 : :
1961 : 770 : TEST_F(TestCApiBlackSolver, is_model_core_symbol)
1962 : : {
1963 : 194 : cvc5_set_option(d_solver, "produce-models", "true");
1964 : 194 : cvc5_set_option(d_solver, "model-cores", "simple");
1965 : 194 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
1966 : 194 : Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y");
1967 : 194 : Cvc5Term z = cvc5_mk_const(d_tm, d_uninterpreted, "z");
1968 : 194 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
1969 : 194 : std::vector<Cvc5Term> args = {x, y};
1970 : 194 : args = {cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data())};
1971 : 194 : Cvc5Term f = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data());
1972 : 194 : cvc5_assert_formula(d_solver, f);
1973 : 194 : cvc5_check_sat(d_solver);
1974 [ - + ][ + - ]: 194 : ASSERT_TRUE(cvc5_is_model_core_symbol(d_solver, x));
1975 [ - + ][ + - ]: 194 : ASSERT_TRUE(cvc5_is_model_core_symbol(d_solver, y));
1976 [ - + ][ + - ]: 194 : ASSERT_FALSE(cvc5_is_model_core_symbol(d_solver, z));
1977 : :
1978 : 194 : ASSERT_DEATH(cvc5_is_model_core_symbol(nullptr, x),
1979 : : "unexpected NULL argument");
1980 [ - + ][ + - ]: 193 : ASSERT_FALSE(cvc5_is_model_core_symbol(d_solver, nullptr));
1981 : 193 : ASSERT_DEATH(cvc5_is_model_core_symbol(d_solver, zero),
1982 : : "expected a free constant");
1983 : :
1984 : 192 : Cvc5TermManager* tm = cvc5_term_manager_new();
1985 : 192 : Cvc5* slv = cvc5_new(tm);
1986 : 192 : cvc5_set_option(slv, "produce-models", "true");
1987 : 192 : cvc5_check_sat(slv);
1988 : 192 : ASSERT_DEATH(cvc5_is_model_core_symbol(slv, x),
1989 : : "term is not associated with the term manager of this solver");
1990 : 191 : cvc5_delete(slv);
1991 : 191 : cvc5_term_manager_delete(tm);
1992 [ + - ]: 191 : }
1993 : :
1994 : 758 : TEST_F(TestCApiBlackSolver, get_model)
1995 : : {
1996 : 191 : cvc5_set_option(d_solver, "produce-models", "true");
1997 : 191 : Cvc5Term x = cvc5_mk_const(d_tm, d_uninterpreted, "x");
1998 : 191 : Cvc5Term y = cvc5_mk_const(d_tm, d_uninterpreted, "y");
1999 : 191 : std::vector<Cvc5Term> args = {x, y};
2000 : 191 : args = {cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data())};
2001 : 191 : Cvc5Term f = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data());
2002 : 191 : cvc5_assert_formula(d_solver, f);
2003 : 191 : cvc5_check_sat(d_solver);
2004 : :
2005 : 191 : std::vector<Cvc5Sort> sorts = {d_uninterpreted};
2006 : 191 : std::vector<Cvc5Term> terms = {x, y};
2007 : 382 : (void)cvc5_get_model(
2008 : 382 : d_solver, sorts.size(), sorts.data(), terms.size(), terms.data());
2009 : :
2010 : 191 : ASSERT_DEATH(
2011 : : cvc5_get_model(
2012 : : nullptr, sorts.size(), sorts.data(), terms.size(), terms.data()),
2013 : : "unexpected NULL argument");
2014 : 190 : ASSERT_DEATH(cvc5_get_model(
2015 : : d_solver, sorts.size(), nullptr, terms.size(), terms.data()),
2016 : : "unexpected NULL argument");
2017 : 189 : ASSERT_DEATH(cvc5_get_model(
2018 : : d_solver, sorts.size(), sorts.data(), terms.size(), nullptr),
2019 : : "unexpected NULL argument");
2020 : 188 : terms.push_back(nullptr);
2021 : 188 : ASSERT_DEATH(
2022 : : cvc5_get_model(
2023 : : d_solver, sorts.size(), sorts.data(), terms.size(), terms.data()),
2024 : : "");
2025 [ + - ][ + - ]: 188 : }
[ + - ]
2026 : :
2027 : 750 : TEST_F(TestCApiBlackSolver, get_model2)
2028 : : {
2029 : 188 : cvc5_set_option(d_solver, "produce-models", "true");
2030 : 188 : std::vector<Cvc5Sort> sorts;
2031 : 188 : std::vector<Cvc5Term> terms;
2032 : 188 : ASSERT_DEATH(
2033 : : cvc5_get_model(
2034 : : d_solver, sorts.size(), sorts.data(), terms.size(), terms.data()),
2035 : : "unexpected NULL argument");
2036 [ + - ][ + - ]: 187 : }
2037 : :
2038 : 744 : TEST_F(TestCApiBlackSolver, get_model3)
2039 : : {
2040 : 187 : cvc5_set_option(d_solver, "produce-models", "true");
2041 : 187 : std::vector<Cvc5Sort> sorts;
2042 : 187 : std::vector<Cvc5Term> terms;
2043 : 187 : cvc5_check_sat(d_solver);
2044 : 187 : ASSERT_DEATH(
2045 : : cvc5_get_model(
2046 : : d_solver, sorts.size(), sorts.data(), terms.size(), terms.data()),
2047 : : "unexpected NULL argument");
2048 : 186 : sorts.push_back(d_int);
2049 : 186 : ASSERT_DEATH(
2050 : : cvc5_get_model(
2051 : : d_solver, sorts.size(), sorts.data(), terms.size(), terms.data()),
2052 : : "unexpected NULL argument");
2053 [ + - ][ + - ]: 185 : }
2054 : :
2055 : 732 : TEST_F(TestCApiBlackSolver, get_quantifier_elimination)
2056 : : {
2057 : 185 : Cvc5Term x = cvc5_mk_var(d_tm, d_bool, "x");
2058 : 185 : std::vector<Cvc5Term> args = {x};
2059 : : Cvc5Term vlist =
2060 : 185 : cvc5_mk_term(d_tm, CVC5_KIND_VARIABLE_LIST, args.size(), args.data());
2061 : 185 : args = {x, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data())};
2062 : 185 : Cvc5Term b = cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data());
2063 : 185 : args = {vlist, b};
2064 : : Cvc5Term forall =
2065 : 185 : cvc5_mk_term(d_tm, CVC5_KIND_FORALL, args.size(), args.data());
2066 : :
2067 : 185 : ASSERT_DEATH(cvc5_get_quantifier_elimination(nullptr, forall),
2068 : : "unexpected NULL argument");
2069 : 184 : ASSERT_DEATH(cvc5_get_quantifier_elimination(d_solver, nullptr),
2070 : : "invalid term");
2071 : 183 : ASSERT_DEATH(cvc5_get_quantifier_elimination(d_solver, cvc5_mk_false(d_tm)),
2072 : : "Expecting a quantified formula");
2073 : 182 : (void)cvc5_get_quantifier_elimination(d_solver, forall);
2074 : :
2075 : 182 : Cvc5TermManager* tm = cvc5_term_manager_new();
2076 : 182 : Cvc5* slv = cvc5_new(tm);
2077 : 182 : cvc5_check_sat(slv);
2078 : 182 : ASSERT_DEATH(cvc5_get_quantifier_elimination(slv, forall),
2079 : : "term is not associated with the term manager of this solver");
2080 : 181 : cvc5_delete(slv);
2081 : 181 : cvc5_term_manager_delete(tm);
2082 [ + - ]: 181 : }
2083 : :
2084 : 716 : TEST_F(TestCApiBlackSolver, get_quantifier_elimination_disjunct)
2085 : : {
2086 : 181 : Cvc5Term x = cvc5_mk_var(d_tm, d_bool, "x");
2087 : 181 : std::vector<Cvc5Term> args = {x};
2088 : : Cvc5Term vlist =
2089 : 181 : cvc5_mk_term(d_tm, CVC5_KIND_VARIABLE_LIST, args.size(), args.data());
2090 : 181 : args = {x, cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data())};
2091 : 181 : Cvc5Term b = cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data());
2092 : 181 : args = {vlist, b};
2093 : : Cvc5Term forall =
2094 : 181 : cvc5_mk_term(d_tm, CVC5_KIND_FORALL, args.size(), args.data());
2095 : :
2096 : 181 : ASSERT_DEATH(cvc5_get_quantifier_elimination_disjunct(nullptr, forall),
2097 : : "unexpected NULL argument");
2098 : 180 : ASSERT_DEATH(cvc5_get_quantifier_elimination_disjunct(d_solver, nullptr),
2099 : : "invalid term");
2100 : 179 : ASSERT_DEATH(
2101 : : cvc5_get_quantifier_elimination_disjunct(d_solver, cvc5_mk_false(d_tm)),
2102 : : "Expecting a quantified formula");
2103 : 178 : (void)cvc5_get_quantifier_elimination_disjunct(d_solver, forall);
2104 : :
2105 : 178 : Cvc5TermManager* tm = cvc5_term_manager_new();
2106 : 178 : Cvc5* slv = cvc5_new(tm);
2107 : 178 : cvc5_check_sat(slv);
2108 : 178 : ASSERT_DEATH(cvc5_get_quantifier_elimination(slv, forall),
2109 : : "term is not associated with the term manager of this solver");
2110 : 177 : cvc5_delete(slv);
2111 : 177 : cvc5_term_manager_delete(tm);
2112 [ + - ]: 177 : }
2113 : :
2114 : 700 : TEST_F(TestCApiBlackSolver, declare_sep_heap)
2115 : : {
2116 : 177 : cvc5_set_logic(d_solver, "ALL");
2117 : 177 : cvc5_set_option(d_solver, "incremental", "false");
2118 : 177 : cvc5_declare_sep_heap(d_solver, d_int, d_int);
2119 : : // cannot declare separation logic heap more than once
2120 : 177 : ASSERT_DEATH(cvc5_declare_sep_heap(d_solver, d_int, d_int),
2121 : : "cannot declare heap types");
2122 : :
2123 : 176 : Cvc5TermManager* tm = cvc5_term_manager_new();
2124 : : // no logic set yet
2125 : 176 : Cvc5* slv = cvc5_new(tm);
2126 : 176 : ASSERT_DEATH(cvc5_declare_sep_heap(d_solver, d_int, d_int),
2127 : : "cannot declare heap types");
2128 : 175 : cvc5_delete(slv);
2129 : :
2130 : 175 : slv = cvc5_new(tm);
2131 : 175 : cvc5_set_logic(slv, "ALL");
2132 : 175 : ASSERT_DEATH(cvc5_declare_sep_heap(slv, cvc5_get_integer_sort(tm), d_int),
2133 : : "sort is not associated with the term manager of this solver");
2134 : 174 : cvc5_delete(slv);
2135 : :
2136 : 174 : slv = cvc5_new(tm);
2137 : 174 : cvc5_set_logic(slv, "ALL");
2138 : 174 : ASSERT_DEATH(cvc5_declare_sep_heap(slv, d_int, cvc5_get_integer_sort(tm)),
2139 : : "sort is not associated with the term manager of this solver");
2140 : 173 : cvc5_delete(slv);
2141 : 173 : cvc5_term_manager_delete(tm);
2142 : : }
2143 : :
2144 : 690 : TEST_F(TestCApiBlackSolver, get_value_sep_heap1)
2145 : : {
2146 : 173 : cvc5_set_logic(d_solver, "QF_BV");
2147 : 173 : cvc5_set_option(d_solver, "incremental", "false");
2148 : 173 : cvc5_set_option(d_solver, "produce-models", "true");
2149 : 173 : Cvc5Term t = cvc5_mk_true(d_tm);
2150 : 173 : cvc5_assert_formula(d_solver, t);
2151 : 173 : ASSERT_DEATH(cvc5_get_value_sep_heap(d_solver),
2152 : : "cannot obtain separation logic expressions");
2153 : : }
2154 : :
2155 : 686 : TEST_F(TestCApiBlackSolver, get_value_sep_heap2)
2156 : : {
2157 : 172 : cvc5_set_logic(d_solver, "ALL");
2158 : 172 : cvc5_set_option(d_solver, "incremental", "false");
2159 : 172 : cvc5_set_option(d_solver, "produce-models", "false");
2160 : 172 : check_simple_separation_constraints();
2161 : 172 : ASSERT_DEATH(cvc5_get_value_sep_heap(d_solver),
2162 : : "cannot get separation heap term");
2163 : : }
2164 : :
2165 : 682 : TEST_F(TestCApiBlackSolver, get_value_sep_heap3)
2166 : : {
2167 : 171 : cvc5_set_logic(d_solver, "ALL");
2168 : 171 : cvc5_set_option(d_solver, "incremental", "false");
2169 : 171 : cvc5_set_option(d_solver, "produce-models", "true");
2170 : 171 : Cvc5Term t = cvc5_mk_false(d_tm);
2171 : 171 : cvc5_assert_formula(d_solver, t);
2172 : 171 : cvc5_check_sat(d_solver);
2173 : 171 : ASSERT_DEATH(cvc5_get_value_sep_heap(d_solver), "after SAT or UNKNOWN");
2174 : : }
2175 : :
2176 : 678 : TEST_F(TestCApiBlackSolver, get_value_sep_heap4)
2177 : : {
2178 : 170 : cvc5_set_logic(d_solver, "ALL");
2179 : 170 : cvc5_set_option(d_solver, "incremental", "false");
2180 : 170 : cvc5_set_option(d_solver, "produce-models", "true");
2181 : 170 : Cvc5Term t = cvc5_mk_true(d_tm);
2182 : 170 : cvc5_assert_formula(d_solver, t);
2183 : 170 : cvc5_check_sat(d_solver);
2184 : 170 : ASSERT_DEATH(cvc5_get_value_sep_heap(d_solver), "Failed to obtain heap/nil");
2185 : : }
2186 : :
2187 : 676 : TEST_F(TestCApiBlackSolver, get_value_sep_heap5)
2188 : : {
2189 : 169 : cvc5_set_logic(d_solver, "ALL");
2190 : 169 : cvc5_set_option(d_solver, "incremental", "false");
2191 : 169 : cvc5_set_option(d_solver, "produce-models", "true");
2192 : 169 : check_simple_separation_constraints();
2193 : 169 : (void)cvc5_get_value_sep_heap(d_solver);
2194 : 169 : }
2195 : :
2196 : 674 : TEST_F(TestCApiBlackSolver, get_value_sep_nil1)
2197 : : {
2198 : 169 : cvc5_set_logic(d_solver, "QF_BV");
2199 : 169 : cvc5_set_option(d_solver, "incremental", "false");
2200 : 169 : cvc5_set_option(d_solver, "produce-models", "true");
2201 : 169 : Cvc5Term t = cvc5_mk_true(d_tm);
2202 : 169 : cvc5_assert_formula(d_solver, t);
2203 : 169 : ASSERT_DEATH(cvc5_get_value_sep_nil(d_solver),
2204 : : "cannot obtain separation logic expressions");
2205 : : }
2206 : :
2207 : 670 : TEST_F(TestCApiBlackSolver, get_value_sep_nil2)
2208 : : {
2209 : 168 : cvc5_set_logic(d_solver, "ALL");
2210 : 168 : cvc5_set_option(d_solver, "incremental", "false");
2211 : 168 : cvc5_set_option(d_solver, "produce-models", "false");
2212 : 168 : check_simple_separation_constraints();
2213 : 168 : ASSERT_DEATH(cvc5_get_value_sep_nil(d_solver), "cannot get separation nil");
2214 : : }
2215 : :
2216 : 666 : TEST_F(TestCApiBlackSolver, get_value_sep_nil3)
2217 : : {
2218 : 167 : cvc5_set_logic(d_solver, "ALL");
2219 : 167 : cvc5_set_option(d_solver, "incremental", "false");
2220 : 167 : cvc5_set_option(d_solver, "produce-models", "true");
2221 : 167 : Cvc5Term t = cvc5_mk_false(d_tm);
2222 : 167 : cvc5_assert_formula(d_solver, t);
2223 : 167 : cvc5_check_sat(d_solver);
2224 : 167 : ASSERT_DEATH(cvc5_get_value_sep_nil(d_solver), "after SAT or UNKNOWN");
2225 : : }
2226 : :
2227 : 662 : TEST_F(TestCApiBlackSolver, get_value_sep_nil4)
2228 : : {
2229 : 166 : cvc5_set_logic(d_solver, "ALL");
2230 : 166 : cvc5_set_option(d_solver, "incremental", "false");
2231 : 166 : cvc5_set_option(d_solver, "produce-models", "true");
2232 : 166 : Cvc5Term t = cvc5_mk_true(d_tm);
2233 : 166 : cvc5_assert_formula(d_solver, t);
2234 : 166 : cvc5_check_sat(d_solver);
2235 : 166 : ASSERT_DEATH(cvc5_get_value_sep_nil(d_solver),
2236 : : "Failed to obtain heap/nil expressions");
2237 : : }
2238 : :
2239 : 660 : TEST_F(TestCApiBlackSolver, get_value_sep_nil5)
2240 : : {
2241 : 165 : cvc5_set_logic(d_solver, "ALL");
2242 : 165 : cvc5_set_option(d_solver, "incremental", "false");
2243 : 165 : cvc5_set_option(d_solver, "produce-models", "true");
2244 : 165 : check_simple_separation_constraints();
2245 : 165 : cvc5_get_value_sep_nil(d_solver);
2246 : 165 : }
2247 : :
2248 : 656 : TEST_F(TestCApiBlackSolver, push1)
2249 : : {
2250 : 165 : cvc5_set_option(d_solver, "incremental", "true");
2251 : 165 : cvc5_push(d_solver, 1);
2252 : 165 : ASSERT_DEATH(cvc5_set_option(d_solver, "incremental", "false"),
2253 : : "is already fully initialized");
2254 : 164 : ASSERT_DEATH(cvc5_set_option(d_solver, "incremental", "true"),
2255 : : "is already fully initialized");
2256 : : }
2257 : :
2258 : 650 : TEST_F(TestCApiBlackSolver, push2)
2259 : : {
2260 : 163 : cvc5_set_option(d_solver, "incremental", "false");
2261 : 163 : ASSERT_DEATH(cvc5_push(d_solver, 1), "cannot push");
2262 : : }
2263 : :
2264 : 646 : TEST_F(TestCApiBlackSolver, push3)
2265 : : {
2266 : 162 : cvc5_set_option(d_solver, "incremental", "false");
2267 : 162 : ASSERT_DEATH(cvc5_push(nullptr, 1), "unexpected NULL argument");
2268 : : }
2269 : :
2270 : 642 : TEST_F(TestCApiBlackSolver, pop1)
2271 : : {
2272 : 161 : cvc5_set_option(d_solver, "incremental", "false");
2273 : 161 : ASSERT_DEATH(cvc5_pop(d_solver, 1), "cannot pop");
2274 : : }
2275 : :
2276 : 638 : TEST_F(TestCApiBlackSolver, pop2)
2277 : : {
2278 : 160 : cvc5_set_option(d_solver, "incremental", "true");
2279 : 160 : ASSERT_DEATH(cvc5_pop(d_solver, 1), "cannot pop");
2280 : : }
2281 : :
2282 : 634 : TEST_F(TestCApiBlackSolver, pop3)
2283 : : {
2284 : 159 : cvc5_set_option(d_solver, "incremental", "true");
2285 : 159 : cvc5_push(d_solver, 1);
2286 : 159 : cvc5_pop(d_solver, 1);
2287 : 159 : ASSERT_DEATH(cvc5_pop(d_solver, 1), "cannot pop");
2288 : : }
2289 : :
2290 : 630 : TEST_F(TestCApiBlackSolver, pop4)
2291 : : {
2292 : 158 : cvc5_set_option(d_solver, "incremental", "false");
2293 : 158 : ASSERT_DEATH(cvc5_pop(nullptr, 1), "unexpected NULL argument");
2294 : : }
2295 : :
2296 : 612 : TEST_F(TestCApiBlackSolver, set_info)
2297 : : {
2298 : 157 : ASSERT_DEATH(cvc5_set_info(d_solver, "cvc5-lagic", "QF_BV"),
2299 : : "unrecognized keyword");
2300 : 156 : ASSERT_DEATH(cvc5_set_info(d_solver, "cvc2-logic", "QF_BV"),
2301 : : "unrecognized keyword");
2302 : 155 : ASSERT_DEATH(cvc5_set_info(d_solver, "cvc5-logic", "asdf"),
2303 : : "unrecognized keyword");
2304 : :
2305 : 154 : ASSERT_DEATH(cvc5_set_info(nullptr, "source", "asdf"),
2306 : : "unexpected NULL argument");
2307 : 153 : ASSERT_DEATH(cvc5_set_info(d_solver, nullptr, "asdf"),
2308 : : "unexpected NULL argument");
2309 : 152 : ASSERT_DEATH(cvc5_set_info(d_solver, "source", nullptr),
2310 : : "unexpected NULL argument");
2311 : :
2312 : 151 : cvc5_set_info(d_solver, "source", "asdf");
2313 : 151 : cvc5_set_info(d_solver, "category", "asdf");
2314 : 151 : cvc5_set_info(d_solver, "difficulty", "asdf");
2315 : 151 : cvc5_set_info(d_solver, "filename", "asdf");
2316 : 151 : cvc5_set_info(d_solver, "license", "asdf");
2317 : 151 : cvc5_set_info(d_solver, "name", "asdf");
2318 : 151 : cvc5_set_info(d_solver, "notes", "asdf");
2319 : :
2320 : 151 : cvc5_set_info(d_solver, "smt-lib-version", "2");
2321 : 151 : cvc5_set_info(d_solver, "smt-lib-version", "2.0");
2322 : 151 : cvc5_set_info(d_solver, "smt-lib-version", "2.5");
2323 : 151 : cvc5_set_info(d_solver, "smt-lib-version", "2.6");
2324 : 151 : ASSERT_DEATH(cvc5_set_info(d_solver, "smt-lib-version", ".0"),
2325 : : "invalid argument");
2326 : :
2327 : 150 : cvc5_set_info(d_solver, "status", "sat");
2328 : 150 : cvc5_set_info(d_solver, "status", "unsat");
2329 : 150 : cvc5_set_info(d_solver, "status", "unknown");
2330 : 150 : ASSERT_DEATH(cvc5_set_info(d_solver, "status", "asdf"), "invalid argument");
2331 : : }
2332 : :
2333 : 588 : TEST_F(TestCApiBlackSolver, set_logic)
2334 : : {
2335 : 149 : ASSERT_DEATH(cvc5_set_logic(nullptr, "AUFLIRA"), "unexpected NULL argument");
2336 : 148 : ASSERT_DEATH(cvc5_set_logic(d_solver, nullptr), "unexpected NULL argument");
2337 : :
2338 : 147 : cvc5_set_logic(d_solver, "AUFLIRA");
2339 : :
2340 : 147 : ASSERT_DEATH(cvc5_set_logic(d_solver, "AF_BV"), "logic is already set");
2341 : 146 : cvc5_assert_formula(d_solver, cvc5_mk_true(d_tm));
2342 : 146 : ASSERT_DEATH(cvc5_set_logic(d_solver, "AUFLIRA"), "logic is already set");
2343 : : }
2344 : :
2345 : 578 : TEST_F(TestCApiBlackSolver, is_logic_set)
2346 : : {
2347 : 145 : ASSERT_DEATH(cvc5_is_logic_set(nullptr), "unexpected NULL argument");
2348 [ - + ][ + - ]: 144 : ASSERT_FALSE(cvc5_is_logic_set(d_solver));
2349 : 144 : cvc5_set_logic(d_solver, "QF_BV");
2350 [ - + ][ + - ]: 144 : ASSERT_TRUE(cvc5_is_logic_set(d_solver));
2351 : : }
2352 : :
2353 : 572 : TEST_F(TestCApiBlackSolver, get_logic)
2354 : : {
2355 : 144 : ASSERT_DEATH(cvc5_get_logic(nullptr), "unexpected NULL argument");
2356 : 143 : ASSERT_DEATH(cvc5_get_logic(d_solver), "logic has not yet been set");
2357 : 142 : cvc5_set_logic(d_solver, "QF_BV");
2358 [ - + ][ + - ]: 142 : ASSERT_EQ(cvc5_get_logic(d_solver), std::string("QF_BV"));
2359 : : }
2360 : :
2361 : 564 : TEST_F(TestCApiBlackSolver, set_option)
2362 : : {
2363 : 142 : cvc5_set_option(d_solver, "bv-sat-solver", "minisat");
2364 : 142 : ASSERT_DEATH(cvc5_set_option(d_solver, "bv-sat-solver", "1"),
2365 : : "unknown option");
2366 : 141 : cvc5_assert_formula(d_solver, cvc5_mk_true(d_tm));
2367 : 141 : ASSERT_DEATH(cvc5_set_option(d_solver, "bv-sat-solver", "minisat"),
2368 : : "fully initialized");
2369 : : }
2370 : :
2371 : 554 : TEST_F(TestCApiBlackSolver, reset_assertions)
2372 : : {
2373 : 140 : ASSERT_DEATH(cvc5_set_option(nullptr, "incremental", "true"),
2374 : : "unexpected NULL argument");
2375 : 139 : ASSERT_DEATH(cvc5_set_option(d_solver, nullptr, "true"),
2376 : : "unexpected NULL argument");
2377 : 138 : ASSERT_DEATH(cvc5_set_option(d_solver, "incremental", nullptr),
2378 : : "unexpected NULL argument");
2379 : :
2380 : 137 : cvc5_set_option(d_solver, "incremental", "true");
2381 : :
2382 : 137 : Cvc5Sort bv_sort = cvc5_mk_bv_sort(d_tm, 4);
2383 : 137 : Cvc5Term one = cvc5_mk_bv_uint64(d_tm, 4, 1);
2384 : 137 : Cvc5Term x = cvc5_mk_const(d_tm, bv_sort, "x");
2385 : 274 : std::vector<Cvc5Term> args = {x, one};
2386 : : Cvc5Term ule =
2387 : 137 : cvc5_mk_term(d_tm, CVC5_KIND_BITVECTOR_ULE, args.size(), args.data());
2388 : 137 : args = {one, x};
2389 : : Cvc5Term srem =
2390 : 137 : cvc5_mk_term(d_tm, CVC5_KIND_BITVECTOR_SREM, args.size(), args.data());
2391 : 137 : cvc5_push(d_solver, 4);
2392 : 137 : args = {srem, one};
2393 : : Cvc5Term slt =
2394 : 137 : cvc5_mk_term(d_tm, CVC5_KIND_BITVECTOR_SLT, args.size(), args.data());
2395 : 137 : cvc5_reset_assertions(d_solver);
2396 : 137 : args = {slt, ule};
2397 : 137 : cvc5_check_sat_assuming(d_solver, args.size(), args.data());
2398 : : }
2399 : :
2400 : 538 : TEST_F(TestCApiBlackSolver, declare_sygus_var)
2401 : : {
2402 : 137 : cvc5_set_option(d_solver, "sygus", "true");
2403 : :
2404 : 137 : std::vector<Cvc5Sort> domain = {d_int};
2405 : : Cvc5Sort fun_sort =
2406 : 137 : cvc5_mk_fun_sort(d_tm, domain.size(), domain.data(), d_bool);
2407 : :
2408 : 137 : (void)cvc5_declare_sygus_var(d_solver, "", d_bool);
2409 : 137 : (void)cvc5_declare_sygus_var(d_solver, "", fun_sort);
2410 : 137 : (void)cvc5_declare_sygus_var(d_solver, "b", d_bool);
2411 : :
2412 : 137 : ASSERT_DEATH(cvc5_declare_sygus_var(nullptr, "", d_bool),
2413 : : "unexpected NULL argument");
2414 : 136 : ASSERT_DEATH(cvc5_declare_sygus_var(d_solver, nullptr, d_bool),
2415 : : "unexpected NULL argument");
2416 : 135 : ASSERT_DEATH(cvc5_declare_sygus_var(d_solver, "", nullptr), "invalid sort");
2417 : :
2418 : 134 : Cvc5* slv = cvc5_new(d_tm);
2419 : 134 : ASSERT_DEATH(cvc5_declare_sygus_var(slv, "", d_bool), "cannot call");
2420 : 133 : cvc5_delete(slv);
2421 : :
2422 : 133 : Cvc5TermManager* tm = cvc5_term_manager_new();
2423 : 133 : slv = cvc5_new(tm);
2424 : 133 : cvc5_set_option(slv, "sygus", "true");
2425 : 133 : ASSERT_DEATH(cvc5_declare_sygus_var(slv, "", d_bool),
2426 : : "sort is not associated with the term manager of this solver");
2427 : 132 : cvc5_delete(slv);
2428 : 132 : cvc5_term_manager_delete(tm);
2429 [ + - ]: 132 : }
2430 : :
2431 : 512 : TEST_F(TestCApiBlackSolver, mk_grammar)
2432 : : {
2433 : 132 : Cvc5Term bt = cvc5_mk_true(d_tm);
2434 : 132 : Cvc5Term bv = cvc5_mk_var(d_tm, d_bool, "b");
2435 : 132 : Cvc5Term iv = cvc5_mk_var(d_tm, d_int, "i");
2436 : :
2437 : 132 : std::vector<Cvc5Term> bvars;
2438 : 132 : std::vector<Cvc5Term> symbols = {iv};
2439 : 264 : (void)cvc5_mk_grammar(
2440 : 264 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
2441 : 132 : bvars = {bv};
2442 : 264 : (void)cvc5_mk_grammar(
2443 : 264 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
2444 : :
2445 : 132 : ASSERT_DEATH(
2446 : : cvc5_mk_grammar(
2447 : : nullptr, bvars.size(), bvars.data(), symbols.size(), symbols.data()),
2448 : : "unexpected NULL argument");
2449 : 131 : ASSERT_DEATH(
2450 : : cvc5_mk_grammar(
2451 : : d_solver, bvars.size(), bvars.data(), symbols.size(), nullptr),
2452 : : "unexpected NULL argument");
2453 : :
2454 : 130 : symbols = {nullptr};
2455 : 130 : ASSERT_DEATH(
2456 : : cvc5_mk_grammar(
2457 : : d_solver, bvars.size(), bvars.data(), symbols.size(), nullptr),
2458 : : "unexpected NULL argument");
2459 : 129 : bvars = {nullptr};
2460 : 129 : symbols = {iv};
2461 : 129 : ASSERT_DEATH(
2462 : : cvc5_mk_grammar(
2463 : : d_solver, bvars.size(), bvars.data(), symbols.size(), nullptr),
2464 : : "unexpected NULL argument");
2465 : 128 : bvars = {};
2466 : 128 : symbols = {bt};
2467 : 128 : ASSERT_DEATH(
2468 : : cvc5_mk_grammar(
2469 : : d_solver, bvars.size(), bvars.data(), symbols.size(), nullptr),
2470 : : "unexpected NULL argument");
2471 : 127 : bvars = {bt};
2472 : 127 : symbols = {iv};
2473 : 127 : ASSERT_DEATH(
2474 : : cvc5_mk_grammar(
2475 : : d_solver, bvars.size(), bvars.data(), symbols.size(), nullptr),
2476 : : "unexpected NULL argument");
2477 : :
2478 : 126 : Cvc5TermManager* tm = cvc5_term_manager_new();
2479 : 126 : Cvc5* slv = cvc5_new(tm);
2480 : 126 : bvars = {};
2481 : 126 : symbols = {iv};
2482 : 126 : ASSERT_DEATH(
2483 : : cvc5_mk_grammar(
2484 : : slv, bvars.size(), bvars.data(), symbols.size(), symbols.data()),
2485 : : "expected a term associated with the term manager of this solver");
2486 : 125 : bvars = {bv};
2487 : 125 : symbols = {cvc5_mk_var(tm, cvc5_get_integer_sort(tm), "")};
2488 : 125 : ASSERT_DEATH(
2489 : : cvc5_mk_grammar(
2490 : : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data()),
2491 : : "expected a term associated with the term manager of this solver");
2492 : 124 : cvc5_delete(slv);
2493 : 124 : cvc5_term_manager_delete(tm);
2494 [ + - ][ + - ]: 124 : }
2495 : :
2496 : 484 : TEST_F(TestCApiBlackSolver, synth_fun)
2497 : : {
2498 : 124 : cvc5_set_option(d_solver, "sygus", "true");
2499 : :
2500 : 124 : Cvc5Term x = cvc5_mk_var(d_tm, d_bool, "");
2501 : 124 : Cvc5Term start1 = cvc5_mk_var(d_tm, d_bool, "");
2502 : 124 : Cvc5Term start2 = cvc5_mk_var(d_tm, d_int, "");
2503 : :
2504 : 124 : std::vector<Cvc5Term> bvars{x};
2505 : 124 : std::vector<Cvc5Term> symbols{start1};
2506 : 248 : Cvc5Grammar g1 = cvc5_mk_grammar(
2507 : 248 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
2508 : :
2509 : 124 : (void)cvc5_synth_fun(d_solver, "", 0, nullptr, d_bool);
2510 : 124 : (void)cvc5_synth_fun(d_solver, "f1", bvars.size(), bvars.data(), d_bool);
2511 : 124 : ASSERT_DEATH(cvc5_synth_fun_with_grammar(
2512 : : d_solver, "f2", bvars.size(), bvars.data(), d_bool, g1),
2513 : : "invalid grammar");
2514 : :
2515 : 123 : cvc5_grammar_add_rule(g1, start1, cvc5_mk_false(d_tm));
2516 : :
2517 : 123 : symbols = {start2};
2518 : 246 : Cvc5Grammar g2 = cvc5_mk_grammar(
2519 : 246 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
2520 : 123 : cvc5_grammar_add_rule(g2, start2, cvc5_mk_integer_int64(d_tm, 0));
2521 : :
2522 : 123 : cvc5_synth_fun_with_grammar(
2523 : 123 : d_solver, "f2", bvars.size(), bvars.data(), d_bool, g1);
2524 : 123 : ASSERT_DEATH(cvc5_synth_fun_with_grammar(
2525 : : nullptr, "f2", bvars.size(), bvars.data(), d_bool, g1),
2526 : : "unexpected NULL argument");
2527 : 122 : ASSERT_DEATH(cvc5_synth_fun_with_grammar(
2528 : : d_solver, "f2", bvars.size(), bvars.data(), nullptr, g1),
2529 : : "invalid sort");
2530 : 121 : ASSERT_DEATH(cvc5_synth_fun_with_grammar(
2531 : : d_solver, "f2", bvars.size(), bvars.data(), d_bool, nullptr),
2532 : : "invalid grammar");
2533 : :
2534 : 120 : ASSERT_DEATH(cvc5_synth_fun_with_grammar(
2535 : : d_solver, "f6", bvars.size(), bvars.data(), d_bool, g2),
2536 : : "invalid Start symbol");
2537 : :
2538 : 119 : Cvc5TermManager* tm = cvc5_term_manager_new();
2539 : 119 : Cvc5* slv = cvc5_new(tm);
2540 : 119 : ASSERT_DEATH(
2541 : : cvc5_synth_fun_with_grammar(
2542 : : slv, "f8", bvars.size(), bvars.data(), d_bool, g1),
2543 : : "expected a term associated with the term manager of this solver");
2544 : 118 : cvc5_delete(slv);
2545 : 118 : cvc5_term_manager_delete(tm);
2546 [ + - ][ + - ]: 118 : }
2547 : :
2548 : 454 : TEST_F(TestCApiBlackSolver, declare_pool)
2549 : : {
2550 : 118 : Cvc5Sort set_sort = cvc5_mk_set_sort(d_tm, d_int);
2551 : 118 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
2552 : 118 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
2553 : 118 : Cvc5Term y = cvc5_mk_const(d_tm, d_int, "y");
2554 : : // declare a pool with initial value { 0, x, y }
2555 : 118 : std::vector<Cvc5Term> args = {zero, x, y};
2556 : : Cvc5Term p =
2557 : 118 : cvc5_declare_pool(d_solver, "p", d_int, args.size(), args.data());
2558 : : // pool should have the same sort
2559 [ - + ][ + - ]: 118 : ASSERT_TRUE(cvc5_sort_is_equal(cvc5_term_get_sort(p), set_sort));
2560 : :
2561 : 118 : ASSERT_DEATH(cvc5_declare_pool(nullptr, "p", d_int, args.size(), args.data()),
2562 : : "unexpected NULL argument");
2563 : 117 : ASSERT_DEATH(
2564 : : cvc5_declare_pool(d_solver, nullptr, d_int, args.size(), args.data()),
2565 : : "unexpected NULL argument");
2566 : 116 : ASSERT_DEATH(
2567 : : cvc5_declare_pool(d_solver, "p", nullptr, args.size(), args.data()),
2568 : : "invalid sort");
2569 : :
2570 : : // no init values is allowed
2571 : 115 : (void)cvc5_declare_pool(d_solver, "p", d_int, 0, nullptr);
2572 : :
2573 : 115 : args = {nullptr, x, y};
2574 : 115 : ASSERT_DEATH(
2575 : : cvc5_declare_pool(d_solver, "p", d_int, args.size(), args.data()),
2576 : : "invalid term at index 0");
2577 : 114 : args = {zero, nullptr, y};
2578 : 114 : ASSERT_DEATH(
2579 : : cvc5_declare_pool(d_solver, "p", d_int, args.size(), args.data()),
2580 : : "invalid term at index 1");
2581 : 113 : args = {zero, x, nullptr};
2582 : 113 : ASSERT_DEATH(
2583 : : cvc5_declare_pool(d_solver, "p", d_int, args.size(), args.data()),
2584 : : "invalid term at index 2");
2585 : :
2586 : 112 : Cvc5TermManager* tm = cvc5_term_manager_new();
2587 : 112 : Cvc5* slv = cvc5_new(tm);
2588 : 112 : args = {zero, x, y};
2589 : 112 : Cvc5Term zero2 = cvc5_mk_integer_int64(tm, 0);
2590 : 112 : Cvc5Term x2 = cvc5_mk_const(tm, cvc5_get_integer_sort(tm), "x");
2591 : 112 : Cvc5Term y2 = cvc5_mk_const(tm, cvc5_get_integer_sort(tm), "y");
2592 : 112 : std::vector<Cvc5Term> args2 = {zero2, x2, y2};
2593 : 112 : ASSERT_DEATH(cvc5_declare_pool(slv, "p", d_int, args2.size(), args2.data()),
2594 : : "sort is not associated with the term manager of this solver");
2595 : 111 : ASSERT_DEATH(
2596 : : cvc5_declare_pool(
2597 : : slv, "p", cvc5_get_integer_sort(tm), args.size(), args.data()),
2598 : : "expected a term associated with the term manager of this solver");
2599 : 110 : args2 = {zero2, x, y2};
2600 : 110 : ASSERT_DEATH(
2601 : : cvc5_declare_pool(
2602 : : slv, "p", cvc5_get_integer_sort(tm), args2.size(), args2.data()),
2603 : : "expected a term associated with the term manager of this solver");
2604 : 109 : cvc5_delete(slv);
2605 : 109 : cvc5_term_manager_delete(tm);
2606 [ + - ]: 109 : }
2607 : :
2608 : 430 : TEST_F(TestCApiBlackSolver, declare_oracle_fun_unsat)
2609 : : {
2610 : 109 : cvc5_set_option(d_solver, "oracles", "true");
2611 : : // f is the function implementing (lambda ((x Int)) (+ x 1))
2612 : 109 : std::vector<Cvc5Sort> sorts = {d_int};
2613 : 218 : Cvc5Term f = cvc5_declare_oracle_fun(
2614 : : d_solver,
2615 : : "f",
2616 : : sorts.size(),
2617 : 109 : sorts.data(),
2618 : : d_int,
2619 : 109 : d_tm,
2620 : 109 : [](size_t size, const Cvc5Term* input, void* state) {
2621 : 109 : Cvc5TermManager* ctm = static_cast<Cvc5TermManager*>(state);
2622 [ + - ]: 109 : if (cvc5_term_is_uint32_value(input[0]))
2623 : : {
2624 : 218 : return cvc5_mk_integer_int64(
2625 : 109 : ctm, cvc5_term_get_uint32_value(input[0]) + 1);
2626 : : }
2627 : 0 : return cvc5_mk_integer_int64(ctm, 0);
2628 : : });
2629 : :
2630 : 109 : Cvc5Term three = cvc5_mk_integer_int64(d_tm, 3);
2631 : 109 : Cvc5Term five = cvc5_mk_integer_int64(d_tm, 5);
2632 : 109 : std::vector<Cvc5Term> args = {f, three};
2633 : 109 : args = {cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()),
2634 : 109 : five};
2635 : 109 : cvc5_assert_formula(
2636 : 109 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
2637 : : // (f 3) = 5
2638 [ - + ][ + - ]: 109 : ASSERT_TRUE(cvc5_result_is_unsat(cvc5_check_sat(d_solver)));
2639 : :
2640 : 109 : Cvc5TermManager* tm = cvc5_term_manager_new();
2641 : 109 : Cvc5* slv = cvc5_new(tm);
2642 : 109 : cvc5_set_option(slv, "oracles", "true");
2643 : 109 : Cvc5Sort int_sort = cvc5_get_integer_sort(tm);
2644 : 109 : std::vector<Cvc5Sort> sorts2 = {int_sort};
2645 [ - - ]: 109 : ASSERT_DEATH(
2646 : : cvc5_declare_oracle_fun(
2647 : : slv,
2648 : : "f",
2649 : : sorts.size(),
2650 : : sorts.data(),
2651 : : int_sort,
2652 : : tm,
2653 : : [](size_t size, const Cvc5Term* input, void* state) {
2654 : : Cvc5TermManager* ctm = static_cast<Cvc5TermManager*>(state);
2655 : : if (cvc5_term_is_uint32_value(input[0]))
2656 : : {
2657 : : return cvc5_mk_integer_int64(
2658 : : ctm, cvc5_term_get_uint32_value(input[0]) + 1);
2659 : : }
2660 : : return cvc5_mk_integer_int64(ctm, 0);
2661 : : }),
2662 : : "expected a sort associated with the term manager of this solver");
2663 [ - - ]: 108 : ASSERT_DEATH(cvc5_declare_oracle_fun(
2664 : : slv,
2665 : : "f",
2666 : : sorts2.size(),
2667 : : sorts2.data(),
2668 : : d_int,
2669 : : tm,
2670 : : [](size_t size, const Cvc5Term* input, void* state) {
2671 : : Cvc5TermManager* ctm =
2672 : : static_cast<Cvc5TermManager*>(state);
2673 : : if (cvc5_term_is_uint32_value(input[0]))
2674 : : {
2675 : : return cvc5_mk_integer_int64(
2676 : : ctm, cvc5_term_get_uint32_value(input[0]) + 1);
2677 : : }
2678 : : return cvc5_mk_integer_int64(ctm, 0);
2679 : : }),
2680 : : "sort is not associated with the term manager of this solver");
2681 : : // this cannot be caught during declaration, is caught during check-sat
2682 : 214 : Cvc5Term f2 = cvc5_declare_oracle_fun(
2683 : : slv,
2684 : : "f",
2685 : : sorts2.size(),
2686 : 107 : sorts2.data(),
2687 : : int_sort,
2688 : 107 : d_tm,
2689 : 1 : [](size_t size, const Cvc5Term* input, void* state) {
2690 : 1 : Cvc5TermManager* ctm = static_cast<Cvc5TermManager*>(state);
2691 [ + - ]: 1 : if (cvc5_term_is_uint32_value(input[0]))
2692 : : {
2693 : 2 : return cvc5_mk_integer_int64(
2694 : 1 : ctm, cvc5_term_get_uint32_value(input[0]) + 1);
2695 : : }
2696 : 0 : return cvc5_mk_integer_int64(ctm, 0);
2697 : : });
2698 : 107 : Cvc5Term three2 = cvc5_mk_integer_int64(tm, 3);
2699 : 107 : Cvc5Term five2 = cvc5_mk_integer_int64(tm, 5);
2700 : 107 : std::vector<Cvc5Term> args2 = {f2, three2};
2701 : 107 : args2 = {cvc5_mk_term(tm, CVC5_KIND_APPLY_UF, args2.size(), args2.data()),
2702 : 107 : five2};
2703 : 107 : cvc5_assert_formula(
2704 : 107 : slv, cvc5_mk_term(tm, CVC5_KIND_EQUAL, args2.size(), args2.data()));
2705 : : // (f 3) = 5
2706 : 107 : ASSERT_DEATH(cvc5_check_sat(slv),
2707 : : "Evaluated an oracle call that is not associated with the term "
2708 : : "manager of this solver");
2709 : 106 : cvc5_delete(slv);
2710 : 106 : cvc5_term_manager_delete(tm);
2711 [ + - ][ + - ]: 106 : }
2712 : :
2713 : 424 : TEST_F(TestCApiBlackSolver, declare_oracle_fun_sat)
2714 : : {
2715 : 106 : cvc5_set_option(d_solver, "oracles", "true");
2716 : 106 : cvc5_set_option(d_solver, "produce-models", "true");
2717 : : // f is the function implementing (lambda ((x Int)) (% x 10))
2718 : 106 : std::vector<Cvc5Sort> sorts = {d_int};
2719 : 212 : Cvc5Term f = cvc5_declare_oracle_fun(
2720 : : d_solver,
2721 : : "f",
2722 : : sorts.size(),
2723 : 106 : sorts.data(),
2724 : : d_int,
2725 : 106 : d_tm,
2726 : 848 : [](size_t size, const Cvc5Term* input, void* state) {
2727 [ - + ][ - + ]: 848 : Assert(size == 1);
[ - - ]
2728 : 848 : Cvc5TermManager* ctm = static_cast<Cvc5TermManager*>(state);
2729 [ + - ]: 848 : if (cvc5_term_is_uint32_value(input[0]))
2730 : : {
2731 : 1696 : return cvc5_mk_integer_int64(
2732 : 848 : ctm, cvc5_term_get_uint32_value(input[0]) % 10);
2733 : : }
2734 : 0 : return cvc5_mk_integer_int64(ctm, 0);
2735 : : });
2736 : 106 : Cvc5Term seven = cvc5_mk_integer_int64(d_tm, 7);
2737 : 106 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
2738 : 106 : std::vector<Cvc5Term> args = {x, cvc5_mk_integer_int64(d_tm, 0)};
2739 : 106 : Cvc5Term lb = cvc5_mk_term(d_tm, CVC5_KIND_GEQ, args.size(), args.data());
2740 : 106 : cvc5_assert_formula(d_solver, lb);
2741 : 106 : args = {x, cvc5_mk_integer_int64(d_tm, 100)};
2742 : 106 : Cvc5Term ub = cvc5_mk_term(d_tm, CVC5_KIND_LEQ, args.size(), args.data());
2743 : 106 : cvc5_assert_formula(d_solver, ub);
2744 : 106 : args = {f, x};
2745 : 106 : args = {cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data()),
2746 : 106 : seven};
2747 : 106 : Cvc5Term eq = cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
2748 : 106 : cvc5_assert_formula(d_solver, eq);
2749 : : // x >= 0 ^ x <= 100 ^ (f x) = 7
2750 [ - + ][ + - ]: 106 : ASSERT_TRUE(cvc5_result_is_sat(cvc5_check_sat(d_solver)));
2751 : 106 : Cvc5Term xval = cvc5_get_value(d_solver, x);
2752 [ - + ][ + - ]: 106 : ASSERT_TRUE(cvc5_term_is_uint32_value(xval));
2753 [ - + ][ + - ]: 106 : ASSERT_TRUE(cvc5_term_get_uint32_value(xval) % 10 == 7);
2754 [ + - ][ + - ]: 106 : }
2755 : :
2756 : 424 : TEST_F(TestCApiBlackSolver, declare_oracle_fun_sat2)
2757 : : {
2758 : 106 : cvc5_set_option(d_solver, "oracles", "true");
2759 : 106 : cvc5_set_option(d_solver, "produce-models", "true");
2760 : : // f is the function implementing (lambda ((x Int) (y Int)) (= x y))
2761 : 106 : std::vector<Cvc5Sort> sorts = {d_int, d_int};
2762 : 212 : Cvc5Term eq = cvc5_declare_oracle_fun(
2763 : : d_solver,
2764 : : "eq",
2765 : : sorts.size(),
2766 : 106 : sorts.data(),
2767 : : d_bool,
2768 : 106 : d_tm,
2769 : 212 : [](size_t size, const Cvc5Term* input, void* state) {
2770 [ - + ][ - + ]: 212 : Assert(size == 2);
[ - - ]
2771 : 424 : return cvc5_mk_boolean(static_cast<Cvc5TermManager*>(state),
2772 : 212 : cvc5_term_is_equal(input[0], input[1]));
2773 : : });
2774 : 106 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
2775 : 106 : Cvc5Term y = cvc5_mk_const(d_tm, d_int, "y");
2776 : 106 : std::vector<Cvc5Term> args = {eq, x, y};
2777 : 106 : args = {cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data())};
2778 : 106 : Cvc5Term neq = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data());
2779 : 106 : cvc5_assert_formula(d_solver, neq);
2780 : : // (not (eq x y))
2781 [ - + ][ + - ]: 106 : ASSERT_TRUE(cvc5_result_is_sat(cvc5_check_sat(d_solver)));
2782 : 106 : Cvc5Term xval = cvc5_get_value(d_solver, x);
2783 : 106 : Cvc5Term yval = cvc5_get_value(d_solver, y);
2784 [ - + ][ + - ]: 106 : ASSERT_TRUE(cvc5_term_is_disequal(xval, yval));
2785 [ + - ][ + - ]: 106 : }
2786 : :
2787 : 416 : TEST_F(TestCApiBlackSolver, declare_oracle_fun_error1)
2788 : : {
2789 : 106 : cvc5_set_option(d_solver, "oracles", "true");
2790 : 106 : std::vector<Cvc5Sort> sorts = {d_int, d_int};
2791 : 106 : ASSERT_DEATH(cvc5_declare_oracle_fun(
2792 : : nullptr,
2793 : : "eq",
2794 : : sorts.size(),
2795 : : sorts.data(),
2796 : : d_bool,
2797 : : d_tm,
2798 : : [](size_t size, const Cvc5Term* input, void* state) {
2799 : : Assert(size == 2);
2800 : : return cvc5_mk_boolean(
2801 : : static_cast<Cvc5TermManager*>(state),
2802 : : cvc5_term_is_equal(input[0], input[1]));
2803 : : }),
2804 : : "unexpected NULL argument");
2805 : 105 : ASSERT_DEATH(cvc5_declare_oracle_fun(
2806 : : d_solver,
2807 : : nullptr,
2808 : : sorts.size(),
2809 : : sorts.data(),
2810 : : d_bool,
2811 : : d_tm,
2812 : : [](size_t size, const Cvc5Term* input, void* state) {
2813 : : Assert(size == 2);
2814 : : return cvc5_mk_boolean(
2815 : : static_cast<Cvc5TermManager*>(state),
2816 : : cvc5_term_is_equal(input[0], input[1]));
2817 : : }),
2818 : : "unexpected NULL argument");
2819 : 104 : ASSERT_DEATH(cvc5_declare_oracle_fun(
2820 : : d_solver,
2821 : : "eq",
2822 : : 0,
2823 : : nullptr,
2824 : : d_bool,
2825 : : d_tm,
2826 : : [](size_t size, const Cvc5Term* input, void* state) {
2827 : : Assert(size == 2);
2828 : : return cvc5_mk_boolean(
2829 : : static_cast<Cvc5TermManager*>(state),
2830 : : cvc5_term_is_equal(input[0], input[1]));
2831 : : }),
2832 : : "");
2833 : 104 : ASSERT_DEATH(cvc5_declare_oracle_fun(
2834 : : d_solver,
2835 : : "eq",
2836 : : sorts.size(),
2837 : : sorts.data(),
2838 : : nullptr,
2839 : : d_tm,
2840 : : [](size_t size, const Cvc5Term* input, void* state) {
2841 : : Assert(size == 2);
2842 : : return cvc5_mk_boolean(
2843 : : static_cast<Cvc5TermManager*>(state),
2844 : : cvc5_term_is_equal(input[0], input[1]));
2845 : : }),
2846 : : "invalid sort");
2847 : : // this won't die when declaring the function, only when the actual oracle
2848 : : // fun is called
2849 : 206 : (void)cvc5_declare_oracle_fun(
2850 : : d_solver,
2851 : : "eq",
2852 : : sorts.size(),
2853 : 103 : sorts.data(),
2854 : : d_bool,
2855 : : nullptr,
2856 : 0 : [](size_t size, const Cvc5Term* input, void* state) {
2857 : 0 : Assert(size == 2);
2858 : 0 : return cvc5_mk_boolean(static_cast<Cvc5TermManager*>(state),
2859 : 0 : cvc5_term_is_equal(input[0], input[1]));
2860 : : });
2861 : 103 : ASSERT_DEATH(
2862 : : cvc5_declare_oracle_fun(
2863 : : d_solver, "eq", sorts.size(), sorts.data(), d_bool, d_tm, nullptr),
2864 : : "unexpected NULL argument");
2865 [ + - ]: 102 : }
2866 : :
2867 : 406 : TEST_F(TestCApiBlackSolver, declare_oracle_fun_error2)
2868 : : {
2869 : 102 : std::vector<Cvc5Sort> sorts = {d_int};
2870 : : // cannot declare without option
2871 : 102 : ASSERT_DEATH(cvc5_declare_oracle_fun(
2872 : : d_solver,
2873 : : "f",
2874 : : sorts.size(),
2875 : : sorts.data(),
2876 : : d_int,
2877 : : d_tm,
2878 : : [](size_t size, const Cvc5Term* input, void* state) {
2879 : : Assert(size == 2);
2880 : : return cvc5_mk_integer_int64(
2881 : : static_cast<Cvc5TermManager*>(state), 0);
2882 : : }),
2883 : : "unless oracles is enabled");
2884 [ + - ]: 101 : }
2885 : :
2886 : 386 : TEST_F(TestCApiBlackSolver, get_interpolant)
2887 : : {
2888 : 101 : cvc5_set_logic(d_solver, "QF_LIA");
2889 : 101 : cvc5_set_option(d_solver, "produce-interpolants", "true");
2890 : 101 : cvc5_set_option(d_solver, "incremental", "false");
2891 : :
2892 : 101 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
2893 : 101 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
2894 : 101 : Cvc5Term y = cvc5_mk_const(d_tm, d_int, "y");
2895 : 101 : Cvc5Term z = cvc5_mk_const(d_tm, d_int, "z");
2896 : :
2897 : : // Assumptions for interpolation: x + y > 0 /\ x < 0
2898 : 101 : std::vector<Cvc5Term> args = {x, y};
2899 : 101 : Cvc5Term add = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
2900 : 101 : args = {add, zero};
2901 : 101 : cvc5_assert_formula(
2902 : 101 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
2903 : 101 : args = {x, zero};
2904 : 101 : cvc5_assert_formula(
2905 : 101 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LT, args.size(), args.data()));
2906 : :
2907 : : // Conjecture for interpolation: y + z > 0 \/ z < 0
2908 : 101 : args = {y, z};
2909 : 101 : add = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
2910 : 101 : args = {add, zero};
2911 : 101 : Cvc5Term gt = cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data());
2912 : 101 : args = {z, zero};
2913 : 101 : Cvc5Term lt = cvc5_mk_term(d_tm, CVC5_KIND_LT, args.size(), args.data());
2914 : 101 : args = {gt, lt};
2915 : 101 : Cvc5Term conj = cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data());
2916 : :
2917 : : // Call the interpolation api, while the resulting interpolant is the output
2918 : 101 : Cvc5Term output = cvc5_get_interpolant(d_solver, conj);
2919 : : // We expect the resulting output to be a boolean formula
2920 [ - + ][ + - ]: 101 : ASSERT_TRUE(cvc5_sort_is_boolean(cvc5_term_get_sort(output)));
2921 : :
2922 : 101 : ASSERT_DEATH(cvc5_get_interpolant(nullptr, conj), "unexpected NULL argument");
2923 : 100 : ASSERT_DEATH(cvc5_get_interpolant(d_solver, nullptr), "invalid term");
2924 : :
2925 : : // try with a grammar, a simple grammar admitting true
2926 : 99 : Cvc5Term ttrue = cvc5_mk_true(d_tm);
2927 : 99 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
2928 : 99 : std::vector<Cvc5Term> symbols = {start};
2929 : : Cvc5Grammar g =
2930 : 99 : cvc5_mk_grammar(d_solver, 0, nullptr, symbols.size(), symbols.data());
2931 : :
2932 : 99 : args = {zero, zero};
2933 : : Cvc5Term conj2 =
2934 : 99 : cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
2935 : 99 : ASSERT_DEATH(cvc5_get_interpolant_with_grammar(d_solver, conj2, g),
2936 : : "invalid grammar, must have at least one rule");
2937 : 98 : cvc5_grammar_add_rule(g, start, ttrue);
2938 : :
2939 : : // Call the interpolation api, while the resulting interpolant is the output
2940 : 98 : Cvc5Term output2 = cvc5_get_interpolant_with_grammar(d_solver, conj2, g);
2941 : : // interpolant must be true
2942 [ - + ][ + - ]: 98 : ASSERT_TRUE(cvc5_term_is_equal(output2, ttrue));
2943 : :
2944 : 98 : ASSERT_DEATH(cvc5_get_interpolant_with_grammar(nullptr, conj2, g),
2945 : : "unexpected NULL argument");
2946 : 97 : ASSERT_DEATH(cvc5_get_interpolant_with_grammar(d_solver, nullptr, g),
2947 : : "invalid term");
2948 : 96 : ASSERT_DEATH(cvc5_get_interpolant_with_grammar(d_solver, conj2, nullptr),
2949 : : "invalid grammar");
2950 : :
2951 : 95 : Cvc5TermManager* tm = cvc5_term_manager_new();
2952 : 95 : Cvc5* slv = cvc5_new(tm);
2953 : 95 : cvc5_set_option(slv, "produce-interpolants", "true");
2954 : 95 : Cvc5Term zzero = cvc5_mk_integer_int64(tm, 0);
2955 : 95 : Cvc5Term sstart = cvc5_mk_var(tm, cvc5_get_boolean_sort(tm), "start");
2956 : 95 : std::vector<Cvc5Term> ssymbols = {sstart};
2957 : : Cvc5Grammar gg =
2958 : 95 : cvc5_mk_grammar(slv, 0, nullptr, ssymbols.size(), ssymbols.data());
2959 : 95 : cvc5_grammar_add_rule(gg, sstart, cvc5_mk_true(tm));
2960 : 95 : std::vector<Cvc5Term> aargs = {zzero, zzero};
2961 : : Cvc5Term cconj2 =
2962 : 95 : cvc5_mk_term(tm, CVC5_KIND_EQUAL, aargs.size(), aargs.data());
2963 : 95 : (void)cvc5_get_interpolant_with_grammar(slv, cconj2, gg);
2964 : 95 : ASSERT_DEATH(cvc5_get_interpolant(slv, conj2),
2965 : : "term is not associated with the term manager of this solver");
2966 : 94 : ASSERT_DEATH(cvc5_get_interpolant_with_grammar(slv, conj2, gg),
2967 : : "term is not associated with the term manager of this solver");
2968 : 93 : ASSERT_DEATH(
2969 : : cvc5_get_interpolant_with_grammar(slv, cconj2, g),
2970 : : "grammar is not associated with the term manager of this solver");
2971 : 92 : cvc5_delete(slv);
2972 : 92 : cvc5_term_manager_delete(tm);
2973 [ + - ]: 92 : }
2974 : :
2975 : 362 : TEST_F(TestCApiBlackSolver, get_interpolant_next)
2976 : : {
2977 : 92 : cvc5_set_logic(d_solver, "QF_LIA");
2978 : 92 : cvc5_set_option(d_solver, "produce-interpolants", "true");
2979 : 92 : cvc5_set_option(d_solver, "incremental", "true");
2980 : :
2981 : 92 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
2982 : 92 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
2983 : 92 : Cvc5Term y = cvc5_mk_const(d_tm, d_int, "y");
2984 : 92 : Cvc5Term z = cvc5_mk_const(d_tm, d_int, "z");
2985 : :
2986 : : // Assumptions for interpolation: x + y > 0 /\ x < 0
2987 : 92 : std::vector<Cvc5Term> args = {x, y};
2988 : 92 : Cvc5Term add = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
2989 : 92 : args = {add, zero};
2990 : 92 : cvc5_assert_formula(
2991 : 92 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
2992 : 92 : args = {x, zero};
2993 : 92 : cvc5_assert_formula(
2994 : 92 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_LT, args.size(), args.data()));
2995 : : // Conjecture for interpolation: y + z > 0 \/ z < 0
2996 : 92 : args = {y, z};
2997 : 92 : add = cvc5_mk_term(d_tm, CVC5_KIND_ADD, args.size(), args.data());
2998 : 92 : args = {add, zero};
2999 : 92 : Cvc5Term gt = cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data());
3000 : 92 : args = {z, zero};
3001 : 92 : Cvc5Term lt = cvc5_mk_term(d_tm, CVC5_KIND_LT, args.size(), args.data());
3002 : 92 : args = {gt, lt};
3003 : 92 : Cvc5Term conj = cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data());
3004 : :
3005 : 92 : Cvc5Term output = cvc5_get_interpolant(d_solver, conj);
3006 : 92 : Cvc5Term output2 = cvc5_get_interpolant_next(d_solver);
3007 : :
3008 : 92 : ASSERT_DEATH(cvc5_get_interpolant(nullptr, conj), "unexpected NULL argument");
3009 : 91 : ASSERT_DEATH(cvc5_get_interpolant(d_solver, nullptr), "invalid term");
3010 : :
3011 : 90 : ASSERT_DEATH(cvc5_get_interpolant_next(nullptr), "unexpected NULL argument");
3012 : :
3013 : : // We expect the next output to be distinct
3014 [ - + ][ + - ]: 89 : ASSERT_TRUE(cvc5_term_is_disequal(output, output2));
3015 [ + - ]: 89 : }
3016 : :
3017 : 338 : TEST_F(TestCApiBlackSolver, get_abduct)
3018 : : {
3019 : 89 : cvc5_set_logic(d_solver, "QF_LIA");
3020 : 89 : cvc5_set_option(d_solver, "produce-abducts", "true");
3021 : 89 : cvc5_set_option(d_solver, "incremental", "false");
3022 : :
3023 : 89 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
3024 : 89 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
3025 : 89 : Cvc5Term y = cvc5_mk_const(d_tm, d_int, "y");
3026 : :
3027 : : // Assumptions for abduction: x > 0
3028 : 89 : std::vector<Cvc5Term> args = {x, zero};
3029 : 89 : cvc5_assert_formula(
3030 : 89 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
3031 : : // Conjecture for abduction: y > 0
3032 : 89 : args = {y, zero};
3033 : 89 : Cvc5Term conj = cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data());
3034 : : // Call the abduction api, while the resulting abduct is the output
3035 : 89 : Cvc5Term output = cvc5_get_abduct(d_solver, conj);
3036 : : // We expect the resulting output to be a boolean formula
3037 [ - + ][ + - ]: 89 : ASSERT_TRUE(cvc5_sort_is_boolean(cvc5_term_get_sort(output)));
3038 : :
3039 : 89 : ASSERT_DEATH(cvc5_get_abduct(nullptr, conj), "unexpected NULL argument");
3040 : 88 : ASSERT_DEATH(cvc5_get_abduct(d_solver, nullptr), "invalid term");
3041 : :
3042 : : // try with a grammar, a simple grammar admitting true
3043 : 87 : Cvc5Term ttrue = cvc5_mk_true(d_tm);
3044 : 87 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
3045 : 87 : std::vector<Cvc5Term> symbols = {start};
3046 : : Cvc5Grammar g =
3047 : 87 : cvc5_mk_grammar(d_solver, 0, nullptr, symbols.size(), symbols.data());
3048 : 87 : args = {x, zero};
3049 : 87 : Cvc5Term conj2 = cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data());
3050 : 87 : ASSERT_DEATH(cvc5_get_abduct_with_grammar(d_solver, conj2, g),
3051 : : "invalid grammar, must have at least one rule");
3052 : 86 : cvc5_grammar_add_rule(g, start, ttrue);
3053 : :
3054 : : // Call the abduction api, while the resulting abduct is the output
3055 : 86 : Cvc5Term output2 = cvc5_get_abduct_with_grammar(d_solver, conj2, g);
3056 : : // abduct must be true
3057 [ - + ][ + - ]: 86 : ASSERT_TRUE(cvc5_term_is_equal(output2, ttrue));
3058 : :
3059 : 86 : ASSERT_DEATH(cvc5_get_abduct_with_grammar(nullptr, conj2, g),
3060 : : "unexpected NULL argument");
3061 : 85 : ASSERT_DEATH(cvc5_get_abduct_with_grammar(d_solver, nullptr, g),
3062 : : "invalid term");
3063 : 84 : ASSERT_DEATH(cvc5_get_abduct_with_grammar(d_solver, conj2, nullptr),
3064 : : "invalid grammar");
3065 : :
3066 : 83 : Cvc5TermManager* tm = cvc5_term_manager_new();
3067 : 83 : Cvc5* slv = cvc5_new(tm);
3068 : 83 : cvc5_set_option(slv, "produce-abducts", "true");
3069 : 83 : Cvc5Sort int_sort = cvc5_get_integer_sort(tm);
3070 : 83 : Cvc5Term zzero = cvc5_mk_integer_int64(tm, 0);
3071 : 83 : Cvc5Term xx = cvc5_mk_const(tm, int_sort, "x");
3072 : 83 : Cvc5Term yy = cvc5_mk_const(tm, int_sort, "y");
3073 : 83 : Cvc5Term sstart = cvc5_mk_var(tm, cvc5_get_boolean_sort(tm), "start");
3074 : 83 : args = {xx, yy};
3075 : 83 : Cvc5Term add = cvc5_mk_term(tm, CVC5_KIND_ADD, args.size(), args.data());
3076 : 83 : args = {add, zzero};
3077 : 83 : cvc5_assert_formula(slv,
3078 : 83 : cvc5_mk_term(tm, CVC5_KIND_GT, args.size(), args.data()));
3079 : 83 : std::vector<Cvc5Term> ssymbols = {sstart};
3080 : : Cvc5Grammar gg =
3081 : 83 : cvc5_mk_grammar(slv, 0, nullptr, ssymbols.size(), ssymbols.data());
3082 : 83 : cvc5_grammar_add_rule(gg, sstart, cvc5_mk_true(tm));
3083 : 83 : std::vector<Cvc5Term> aargs = {zzero, zzero};
3084 : : Cvc5Term cconj2 =
3085 : 83 : cvc5_mk_term(tm, CVC5_KIND_EQUAL, aargs.size(), aargs.data());
3086 : 83 : (void)cvc5_get_abduct_with_grammar(slv, cconj2, gg);
3087 : 83 : ASSERT_DEATH(cvc5_get_abduct(slv, conj2),
3088 : : "term is not associated with the term manager of this solver");
3089 : 82 : ASSERT_DEATH(cvc5_get_abduct_with_grammar(slv, conj2, gg),
3090 : : "term is not associated with the term manager of this solver");
3091 : 81 : ASSERT_DEATH(
3092 : : cvc5_get_abduct_with_grammar(slv, cconj2, g),
3093 : : "grammar is not associated with the term manager of this solver");
3094 : 80 : cvc5_delete(slv);
3095 : 80 : cvc5_term_manager_delete(tm);
3096 [ + - ]: 80 : }
3097 : :
3098 : 318 : TEST_F(TestCApiBlackSolver, get_abduct2)
3099 : : {
3100 : 80 : cvc5_set_logic(d_solver, "QF_LIA");
3101 : 80 : cvc5_set_option(d_solver, "incremental", "false");
3102 : :
3103 : 80 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
3104 : 80 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
3105 : 80 : Cvc5Term y = cvc5_mk_const(d_tm, d_int, "y");
3106 : : // Assumptions for abduction: x > 0
3107 : 80 : std::vector<Cvc5Term> args = {x, zero};
3108 : 80 : cvc5_assert_formula(
3109 : 80 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
3110 : : // Conjecture for abduction: y > 0
3111 : 80 : args = {y, zero};
3112 : 80 : Cvc5Term conj = cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data());
3113 : : // Fails due to option not set
3114 : 80 : ASSERT_DEATH(cvc5_get_abduct(d_solver, conj), "unless abducts are enabled");
3115 [ + - ]: 79 : }
3116 : :
3117 : 310 : TEST_F(TestCApiBlackSolver, get_abduct_next)
3118 : : {
3119 : 79 : cvc5_set_logic(d_solver, "QF_LIA");
3120 : 79 : cvc5_set_option(d_solver, "produce-abducts", "true");
3121 : 79 : cvc5_set_option(d_solver, "incremental", "true");
3122 : :
3123 : 79 : Cvc5Term zero = cvc5_mk_integer_int64(d_tm, 0);
3124 : 79 : Cvc5Term x = cvc5_mk_const(d_tm, d_int, "x");
3125 : 79 : Cvc5Term y = cvc5_mk_const(d_tm, d_int, "y");
3126 : :
3127 : : // Assumptions for abduction: x > 0
3128 : 79 : std::vector<Cvc5Term> args = {x, zero};
3129 : 79 : cvc5_assert_formula(
3130 : 79 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data()));
3131 : : // Conjecture for abduction: y > 0
3132 : 79 : args = {y, zero};
3133 : 79 : Cvc5Term conj = cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data());
3134 : : // Call the abduction api, while the resulting abduct is the output
3135 : 79 : Cvc5Term output = cvc5_get_abduct(d_solver, conj);
3136 : 79 : Cvc5Term output2 = cvc5_get_abduct_next(d_solver);
3137 : :
3138 : 79 : ASSERT_DEATH(cvc5_get_abduct(nullptr, conj), "unexpected NULL argument");
3139 : 78 : ASSERT_DEATH(cvc5_get_abduct(d_solver, nullptr), "invalid term");
3140 : :
3141 : 77 : ASSERT_DEATH(cvc5_get_abduct_next(nullptr), "unexpected NULL argument");
3142 : :
3143 : : // should produce a different output
3144 [ - + ][ + - ]: 76 : ASSERT_TRUE(cvc5_term_is_disequal(output, output2));
3145 [ + - ]: 76 : }
3146 : :
3147 : 302 : TEST_F(TestCApiBlackSolver, block_model1)
3148 : : {
3149 : 76 : Cvc5Term x = cvc5_mk_const(d_tm, d_bool, "x");
3150 : 76 : std::vector<Cvc5Term> args = {x, x};
3151 : 76 : cvc5_assert_formula(
3152 : 76 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
3153 : 76 : cvc5_check_sat(d_solver);
3154 : 76 : ASSERT_DEATH(cvc5_block_model(d_solver, CVC5_BLOCK_MODELS_MODE_LITERALS),
3155 : : "cannot get value");
3156 [ + - ]: 75 : }
3157 : :
3158 : 298 : TEST_F(TestCApiBlackSolver, block_model2)
3159 : : {
3160 : 75 : cvc5_set_option(d_solver, "produce-models", "true");
3161 : 75 : Cvc5Term x = cvc5_mk_const(d_tm, d_bool, "x");
3162 : 75 : std::vector<Cvc5Term> args = {x, x};
3163 : 75 : cvc5_assert_formula(
3164 : 75 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
3165 : 75 : ASSERT_DEATH(cvc5_block_model(d_solver, CVC5_BLOCK_MODELS_MODE_LITERALS),
3166 : : "after SAT or UNKNOWN");
3167 [ + - ]: 74 : }
3168 : :
3169 : 294 : TEST_F(TestCApiBlackSolver, block_model3)
3170 : : {
3171 : 74 : cvc5_set_option(d_solver, "produce-models", "true");
3172 : 74 : Cvc5Term x = cvc5_mk_const(d_tm, d_bool, "x");
3173 : 74 : std::vector<Cvc5Term> args = {x, x};
3174 : 74 : cvc5_assert_formula(
3175 : 74 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
3176 : 74 : cvc5_check_sat(d_solver);
3177 : 74 : cvc5_block_model(d_solver, CVC5_BLOCK_MODELS_MODE_LITERALS);
3178 : 74 : ASSERT_DEATH(cvc5_block_model(nullptr, CVC5_BLOCK_MODELS_MODE_LITERALS),
3179 : : "unexpected NULL argument");
3180 [ + - ]: 73 : }
3181 : :
3182 : 284 : TEST_F(TestCApiBlackSolver, block_model_values1)
3183 : : {
3184 : 73 : cvc5_set_option(d_solver, "produce-models", "true");
3185 : 73 : Cvc5Term x = cvc5_mk_const(d_tm, d_bool, "x");
3186 : 73 : std::vector<Cvc5Term> args = {x, x};
3187 : 73 : cvc5_assert_formula(
3188 : 73 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
3189 : 73 : cvc5_check_sat(d_solver);
3190 : 73 : args = {cvc5_mk_true(d_tm)};
3191 : 73 : cvc5_block_model_values(d_solver, args.size(), args.data());
3192 : :
3193 : 73 : ASSERT_DEATH(cvc5_block_model_values(nullptr, args.size(), args.data()),
3194 : : "unexpected NULL argument");
3195 : 72 : ASSERT_DEATH(cvc5_block_model_values(d_solver, 0, nullptr),
3196 : : "unexpected NULL argument");
3197 : 71 : args = {nullptr};
3198 : 71 : ASSERT_DEATH(cvc5_block_model_values(d_solver, args.size(), args.data()),
3199 : : "invalid term at index 0");
3200 : :
3201 : 70 : Cvc5TermManager* tm = cvc5_term_manager_new();
3202 : 70 : Cvc5* slv = cvc5_new(tm);
3203 : 70 : cvc5_set_option(slv, "produce-models", "true");
3204 : 70 : cvc5_check_sat(slv);
3205 : 70 : args = {cvc5_mk_true(d_tm)};
3206 : 70 : ASSERT_DEATH(
3207 : : cvc5_block_model_values(slv, args.size(), args.data()),
3208 : : "expected a term associated with the term manager of this solver");
3209 : 69 : cvc5_delete(slv);
3210 : 69 : cvc5_term_manager_delete(tm);
3211 [ + - ]: 69 : }
3212 : :
3213 : 276 : TEST_F(TestCApiBlackSolver, block_model_values2)
3214 : : {
3215 : 69 : cvc5_set_option(d_solver, "produce-models", "true");
3216 : 69 : Cvc5Term x = cvc5_mk_const(d_tm, d_bool, "x");
3217 : 69 : std::vector<Cvc5Term> args = {x, x};
3218 : 69 : cvc5_assert_formula(
3219 : 69 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
3220 : 69 : cvc5_check_sat(d_solver);
3221 : 69 : args = {x};
3222 : 69 : cvc5_block_model_values(d_solver, args.size(), args.data());
3223 : 69 : }
3224 : :
3225 : 274 : TEST_F(TestCApiBlackSolver, block_model_values3)
3226 : : {
3227 : 69 : Cvc5Term x = cvc5_mk_const(d_tm, d_bool, "x");
3228 : 69 : std::vector<Cvc5Term> args = {x, x};
3229 : 69 : cvc5_assert_formula(
3230 : 69 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
3231 : 69 : cvc5_check_sat(d_solver);
3232 : 69 : args = {x};
3233 : 69 : ASSERT_DEATH(cvc5_block_model_values(d_solver, args.size(), args.data()),
3234 : : "cannot get value");
3235 [ + - ]: 68 : }
3236 : :
3237 : 270 : TEST_F(TestCApiBlackSolver, block_model_values4)
3238 : : {
3239 : 68 : cvc5_set_option(d_solver, "produce-models", "true");
3240 : 68 : Cvc5Term x = cvc5_mk_const(d_tm, d_bool, "x");
3241 : 68 : std::vector<Cvc5Term> args = {x, x};
3242 : 68 : cvc5_assert_formula(
3243 : 68 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
3244 : 68 : args = {x};
3245 : 68 : ASSERT_DEATH(cvc5_block_model_values(d_solver, args.size(), args.data()),
3246 : : "SAT or UNKNOWN response");
3247 [ + - ]: 67 : }
3248 : :
3249 : 268 : TEST_F(TestCApiBlackSolver, block_model_values5)
3250 : : {
3251 : 67 : cvc5_set_option(d_solver, "produce-models", "true");
3252 : 67 : Cvc5Term x = cvc5_mk_const(d_tm, d_bool, "x");
3253 : 67 : std::vector<Cvc5Term> args = {x, x};
3254 : 67 : cvc5_assert_formula(
3255 : 67 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
3256 : 67 : cvc5_check_sat(d_solver);
3257 : 67 : args = {x};
3258 : 67 : cvc5_block_model_values(d_solver, args.size(), args.data());
3259 : 67 : }
3260 : :
3261 : 264 : TEST_F(TestCApiBlackSolver, get_instantiations)
3262 : : {
3263 : 67 : std::vector<Cvc5Sort> sorts = {d_int};
3264 : : Cvc5Term p =
3265 : 67 : cvc5_declare_fun(d_solver, "p", sorts.size(), sorts.data(), d_bool, true);
3266 : 67 : Cvc5Term x = cvc5_mk_var(d_tm, d_int, "x");
3267 : 67 : std::vector<Cvc5Term> args = {x};
3268 : : Cvc5Term bvl =
3269 : 67 : cvc5_mk_term(d_tm, CVC5_KIND_VARIABLE_LIST, args.size(), args.data());
3270 : 67 : args = {p, x};
3271 : : Cvc5Term app =
3272 : 67 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
3273 : 67 : args = {bvl, app};
3274 : 67 : Cvc5Term q = cvc5_mk_term(d_tm, CVC5_KIND_FORALL, args.size(), args.data());
3275 : 67 : cvc5_assert_formula(d_solver, q);
3276 : 67 : Cvc5Term five = cvc5_mk_integer_int64(d_tm, 5);
3277 : 67 : args = {p, five};
3278 : 67 : args = {cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data())};
3279 : 67 : Cvc5Term app2 = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data());
3280 : 67 : cvc5_assert_formula(d_solver, app2);
3281 : 67 : ASSERT_DEATH(cvc5_get_instantiations(d_solver),
3282 : : "after a UNSAT, SAT or UNKNOWN response");
3283 : 66 : cvc5_check_sat(d_solver);
3284 : 66 : cvc5_get_instantiations(d_solver);
3285 : 66 : ASSERT_DEATH(cvc5_get_instantiations(nullptr), "unexpected NULL argument");
3286 [ + - ][ + - ]: 65 : }
3287 : :
3288 : 254 : TEST_F(TestCApiBlackSolver, add_sygus_constraint)
3289 : : {
3290 : 65 : cvc5_set_option(d_solver, "sygus", "true");
3291 : 65 : Cvc5Term tbool = cvc5_mk_true(d_tm);
3292 : :
3293 : 65 : cvc5_add_sygus_constraint(d_solver, tbool);
3294 : 65 : ASSERT_DEATH(cvc5_add_sygus_constraint(nullptr, tbool),
3295 : : "unexpected NULL argument");
3296 : 64 : ASSERT_DEATH(cvc5_add_sygus_constraint(d_solver, nullptr), "invalid term");
3297 : :
3298 : 63 : Cvc5TermManager* tm = cvc5_term_manager_new();
3299 : 63 : Cvc5* slv = cvc5_new(tm);
3300 : 63 : cvc5_set_option(slv, "sygus", "true");
3301 : 63 : ASSERT_DEATH(cvc5_add_sygus_constraint(slv, tbool),
3302 : : "term is not associated with the term manager of this solver");
3303 : 62 : cvc5_delete(slv);
3304 : 62 : cvc5_term_manager_delete(tm);
3305 : : }
3306 : :
3307 : 244 : TEST_F(TestCApiBlackSolver, get_sygus_constraints)
3308 : : {
3309 : 62 : cvc5_set_option(d_solver, "sygus", "true");
3310 : 62 : Cvc5Term ttrue = cvc5_mk_true(d_tm);
3311 : 62 : Cvc5Term tfalse = cvc5_mk_false(d_tm);
3312 : 62 : cvc5_add_sygus_constraint(d_solver, ttrue);
3313 : 62 : cvc5_add_sygus_constraint(d_solver, tfalse);
3314 : : size_t size;
3315 : 62 : const Cvc5Term* constraints = cvc5_get_sygus_constraints(d_solver, &size);
3316 [ - + ][ + - ]: 62 : ASSERT_TRUE(cvc5_term_is_equal(ttrue, constraints[0]));
3317 [ - + ][ + - ]: 62 : ASSERT_TRUE(cvc5_term_is_equal(tfalse, constraints[1]));
3318 : 62 : ASSERT_DEATH(cvc5_get_sygus_constraints(nullptr, &size),
3319 : : "unexpected NULL argument");
3320 : 61 : ASSERT_DEATH(cvc5_get_sygus_constraints(d_solver, nullptr),
3321 : : "unexpected NULL argument");
3322 : : }
3323 : :
3324 : 232 : TEST_F(TestCApiBlackSolver, add_sygus_assume)
3325 : : {
3326 : 60 : cvc5_set_option(d_solver, "sygus", "true");
3327 : 60 : Cvc5Term tbool = cvc5_mk_false(d_tm);
3328 : 60 : Cvc5Term tint = cvc5_mk_integer_int64(d_tm, 1);
3329 : :
3330 : 60 : cvc5_add_sygus_assume(d_solver, tbool);
3331 : 60 : ASSERT_DEATH(cvc5_add_sygus_assume(nullptr, tbool),
3332 : : "unexpected NULL argument");
3333 : 59 : ASSERT_DEATH(cvc5_add_sygus_assume(d_solver, nullptr), "invalid term");
3334 : 58 : ASSERT_DEATH(cvc5_add_sygus_assume(d_solver, tint), "invalid argument");
3335 : :
3336 : 57 : Cvc5TermManager* tm = cvc5_term_manager_new();
3337 : 57 : Cvc5* slv = cvc5_new(tm);
3338 : 57 : cvc5_set_option(slv, "sygus", "true");
3339 : 57 : ASSERT_DEATH(cvc5_add_sygus_assume(slv, tbool),
3340 : : "term is not associated with the term manager of this solver");
3341 : 56 : cvc5_delete(slv);
3342 : 56 : cvc5_term_manager_delete(tm);
3343 : : }
3344 : :
3345 : 220 : TEST_F(TestCApiBlackSolver, get_sygus_assumptions)
3346 : : {
3347 : 56 : cvc5_set_option(d_solver, "sygus", "true");
3348 : 56 : Cvc5Term ttrue = cvc5_mk_true(d_tm);
3349 : 56 : Cvc5Term tfalse = cvc5_mk_false(d_tm);
3350 : 56 : cvc5_add_sygus_assume(d_solver, ttrue);
3351 : 56 : cvc5_add_sygus_assume(d_solver, tfalse);
3352 : 56 : cvc5_add_sygus_assume(d_solver, ttrue);
3353 : 56 : cvc5_add_sygus_assume(d_solver, tfalse);
3354 : : size_t size;
3355 : 56 : const Cvc5Term* assumptions = cvc5_get_sygus_assumptions(d_solver, &size);
3356 [ - + ][ + - ]: 56 : ASSERT_TRUE(cvc5_term_is_equal(ttrue, assumptions[0]));
3357 [ - + ][ + - ]: 56 : ASSERT_TRUE(cvc5_term_is_equal(tfalse, assumptions[1]));
3358 : 56 : ASSERT_DEATH(cvc5_get_sygus_assumptions(nullptr, &size),
3359 : : "unexpected NULL argument");
3360 : 55 : ASSERT_DEATH(cvc5_get_sygus_assumptions(d_solver, nullptr),
3361 : : "unexpected NULL argument");
3362 : : }
3363 : :
3364 : 180 : TEST_F(TestCApiBlackSolver, add_sygus_inv_constraint)
3365 : : {
3366 : 54 : cvc5_set_option(d_solver, "sygus", "true");
3367 : 54 : Cvc5Term tint = cvc5_mk_integer_int64(d_tm, 1);
3368 : :
3369 : 54 : std::vector<Cvc5Sort> domain = {d_real};
3370 : 54 : Cvc5Term inv = cvc5_declare_fun(
3371 : 54 : d_solver, "inv", domain.size(), domain.data(), d_bool, true);
3372 : 54 : Cvc5Term pre = cvc5_declare_fun(
3373 : 54 : d_solver, "pre", domain.size(), domain.data(), d_bool, true);
3374 : 54 : domain = {d_real, d_real};
3375 : 54 : Cvc5Term trans = cvc5_declare_fun(
3376 : 54 : d_solver, "trans", domain.size(), domain.data(), d_bool, true);
3377 : 54 : domain = {d_real};
3378 : 54 : Cvc5Term post = cvc5_declare_fun(
3379 : 54 : d_solver, "post", domain.size(), domain.data(), d_bool, true);
3380 : :
3381 : 54 : Cvc5Term inv1 = cvc5_declare_fun(
3382 : 54 : d_solver, "inv1", domain.size(), domain.data(), d_real, true);
3383 : 54 : domain = {d_bool, d_real};
3384 : 54 : Cvc5Term trans1 = cvc5_declare_fun(
3385 : 54 : d_solver, "trans1", domain.size(), domain.data(), d_bool, true);
3386 : 54 : domain = {d_real, d_bool};
3387 : 54 : Cvc5Term trans2 = cvc5_declare_fun(
3388 : 54 : d_solver, "trans2", domain.size(), domain.data(), d_bool, true);
3389 : 54 : domain = {d_real, d_real};
3390 : 54 : Cvc5Term trans3 = cvc5_declare_fun(
3391 : 54 : d_solver, "trans3", domain.size(), domain.data(), d_real, true);
3392 : :
3393 : 54 : cvc5_add_sygus_inv_constraint(d_solver, inv, pre, trans, post);
3394 : :
3395 : 54 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(nullptr, inv, pre, trans, post),
3396 : : "unexpected NULL argument");
3397 : 53 : ASSERT_DEATH(
3398 : : cvc5_add_sygus_inv_constraint(d_solver, nullptr, pre, trans, post),
3399 : : "invalid term");
3400 : 52 : ASSERT_DEATH(
3401 : : cvc5_add_sygus_inv_constraint(d_solver, inv, nullptr, trans, post),
3402 : : "invalid term");
3403 : 51 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(d_solver, inv, pre, nullptr, post),
3404 : : "invalid term");
3405 : 50 : ASSERT_DEATH(
3406 : : cvc5_add_sygus_inv_constraint(d_solver, inv, pre, trans, nullptr),
3407 : : "invalid term");
3408 : :
3409 : 49 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(d_solver, tint, pre, trans, post),
3410 : : "invalid argument");
3411 : 48 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(d_solver, inv1, pre, trans, post),
3412 : : "invalid argument");
3413 : 47 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(d_solver, inv, trans, trans, post),
3414 : : "have the same sort");
3415 : 46 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(d_solver, inv, pre, tint, post),
3416 : : "expected the sort of trans");
3417 : 45 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(d_solver, inv, pre, pre, post),
3418 : : "expected the sort of trans");
3419 : 44 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(d_solver, inv, pre, trans1, post),
3420 : : "expected the sort of trans");
3421 : 43 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(d_solver, inv, pre, trans2, post),
3422 : : "expected the sort of trans");
3423 : 42 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(d_solver, inv, pre, trans3, post),
3424 : : "expected the sort of trans");
3425 : 41 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(d_solver, inv, pre, trans, trans),
3426 : : "expected inv and post to have the same sort");
3427 : :
3428 : 40 : Cvc5TermManager* tm = cvc5_term_manager_new();
3429 : 40 : Cvc5* slv = cvc5_new(tm);
3430 : 40 : cvc5_set_option(slv, "sygus", "true");
3431 : 40 : Cvc5Sort bool_sort = cvc5_get_boolean_sort(tm);
3432 : 40 : Cvc5Sort real_sort = cvc5_get_real_sort(tm);
3433 : 40 : std::vector<Cvc5Sort> domain2 = {real_sort};
3434 : 40 : Cvc5Term inv22 = cvc5_declare_fun(
3435 : 40 : slv, "inv", domain2.size(), domain2.data(), bool_sort, true);
3436 : 40 : Cvc5Term pre22 = cvc5_declare_fun(
3437 : 40 : slv, "pre", domain2.size(), domain2.data(), bool_sort, true);
3438 : 40 : domain2 = {real_sort, real_sort};
3439 : 40 : Cvc5Term trans22 = cvc5_declare_fun(
3440 : 40 : slv, "trans", domain2.size(), domain2.data(), bool_sort, true);
3441 : 40 : domain2 = {real_sort};
3442 : 40 : Cvc5Term post22 = cvc5_declare_fun(
3443 : 40 : slv, "post", domain2.size(), domain2.data(), bool_sort, true);
3444 : 40 : cvc5_add_sygus_inv_constraint(slv, inv22, pre22, trans22, post22);
3445 : 40 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(slv, inv, pre22, trans22, post22),
3446 : : "term is not associated with the term manager of this solver");
3447 : 39 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(slv, inv22, pre, trans22, post22),
3448 : : "term is not associated with the term manager of this solver");
3449 : 38 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(slv, inv22, pre22, trans, post22),
3450 : : "term is not associated with the term manager of this solver");
3451 : 37 : ASSERT_DEATH(cvc5_add_sygus_inv_constraint(slv, inv22, pre22, trans22, post),
3452 : : "term is not associated with the term manager of this solver");
3453 : 36 : cvc5_delete(slv);
3454 : 36 : cvc5_term_manager_delete(tm);
3455 [ + - ]: 36 : }
3456 : :
3457 : 140 : TEST_F(TestCApiBlackSolver, check_synth)
3458 : : {
3459 : : // requires option to be set
3460 : 36 : ASSERT_DEATH(cvc5_check_synth(d_solver),
3461 : : "cannot check for a synthesis solution");
3462 : 35 : cvc5_set_option(d_solver, "sygus", "true");
3463 : 35 : cvc5_check_synth(d_solver);
3464 : 35 : ASSERT_DEATH(cvc5_check_synth(nullptr), "unexpected NULL argument");
3465 : : }
3466 : :
3467 : 126 : TEST_F(TestCApiBlackSolver, get_synth_solution)
3468 : : {
3469 : 34 : cvc5_set_option(d_solver, "sygus", "true");
3470 : 34 : cvc5_set_option(d_solver, "incremental", "false");
3471 : :
3472 : 34 : Cvc5Term x = cvc5_mk_false(d_tm);
3473 : 34 : Cvc5Term f = cvc5_synth_fun(d_solver, "f", 0, nullptr, d_bool);
3474 : :
3475 : 34 : ASSERT_DEATH(cvc5_get_synth_solution(d_solver, f), "not in a state");
3476 : :
3477 : 33 : Cvc5SynthResult res = cvc5_check_synth(d_solver);
3478 [ - + ][ + - ]: 33 : ASSERT_TRUE(cvc5_synth_result_has_solution(res));
3479 : :
3480 : 33 : cvc5_get_synth_solution(d_solver, f);
3481 : 33 : cvc5_get_synth_solution(d_solver, f);
3482 : :
3483 : 33 : ASSERT_DEATH(cvc5_get_synth_solution(nullptr, f), "unexpected NULL argument");
3484 : 32 : ASSERT_DEATH(cvc5_get_synth_solution(d_solver, nullptr), "invalid term");
3485 : 31 : ASSERT_DEATH(cvc5_get_synth_solution(d_solver, x),
3486 : : "synthesis solution not found for given term");
3487 : :
3488 : 30 : Cvc5TermManager* tm = cvc5_term_manager_new();
3489 : 30 : Cvc5* slv = cvc5_new(tm);
3490 : 30 : ASSERT_DEATH(cvc5_get_synth_solution(slv, f),
3491 : : "term is not associated with the term manager of this solver");
3492 : 29 : cvc5_delete(slv);
3493 : 29 : cvc5_term_manager_delete(tm);
3494 : : }
3495 : :
3496 : 104 : TEST_F(TestCApiBlackSolver, get_synth_solutions)
3497 : : {
3498 : 29 : cvc5_set_option(d_solver, "sygus", "true");
3499 : 29 : cvc5_set_option(d_solver, "incremental", "false");
3500 : :
3501 : 29 : Cvc5Term x = cvc5_mk_false(d_tm);
3502 : 29 : Cvc5Term f = cvc5_synth_fun(d_solver, "f", 0, nullptr, d_bool);
3503 : :
3504 : 29 : std::vector<Cvc5Term> args{f};
3505 : 29 : ASSERT_DEATH(cvc5_get_synth_solutions(d_solver, args.size(), args.data()),
3506 : : "not in a state");
3507 : :
3508 : 28 : cvc5_check_synth(d_solver);
3509 : :
3510 : 28 : cvc5_get_synth_solutions(d_solver, args.size(), args.data());
3511 : 28 : args = {f, f};
3512 : 28 : cvc5_get_synth_solutions(d_solver, args.size(), args.data());
3513 : :
3514 : 28 : ASSERT_DEATH(cvc5_get_synth_solutions(d_solver, 0, nullptr),
3515 : : "unexpected NULL argument");
3516 : 27 : ASSERT_DEATH(cvc5_get_synth_solutions(nullptr, args.size(), args.data()),
3517 : : "unexpected NULL argument");
3518 : 26 : args = {nullptr};
3519 : 26 : ASSERT_DEATH(cvc5_get_synth_solutions(d_solver, args.size(), args.data()),
3520 : : "invalid term at index 0");
3521 : 25 : args = {x};
3522 : 25 : ASSERT_DEATH(cvc5_get_synth_solutions(d_solver, args.size(), args.data()),
3523 : : "synthesis solution not found for term at index 0");
3524 : :
3525 : 24 : Cvc5TermManager* tm = cvc5_term_manager_new();
3526 : 24 : Cvc5* slv = cvc5_new(tm);
3527 : 24 : ASSERT_DEATH(
3528 : : cvc5_get_synth_solutions(slv, args.size(), args.data()),
3529 : : "expected a term associated with the term manager of this solver");
3530 : 23 : cvc5_delete(slv);
3531 : 23 : cvc5_term_manager_delete(tm);
3532 [ + - ]: 23 : }
3533 : :
3534 : 90 : TEST_F(TestCApiBlackSolver, check_synth_next)
3535 : : {
3536 : 23 : cvc5_set_option(d_solver, "sygus", "true");
3537 : 23 : cvc5_set_option(d_solver, "incremental", "true");
3538 : :
3539 : 23 : Cvc5Term f = cvc5_synth_fun(d_solver, "f", 0, nullptr, d_bool);
3540 : :
3541 : 23 : Cvc5SynthResult res = cvc5_check_synth(d_solver);
3542 [ - + ][ + - ]: 23 : ASSERT_TRUE(cvc5_synth_result_has_solution(res));
3543 : :
3544 : 23 : std::vector<Cvc5Term> args{f};
3545 : 23 : cvc5_get_synth_solutions(d_solver, args.size(), args.data());
3546 : :
3547 : 23 : res = cvc5_check_synth_next(d_solver);
3548 [ - + ][ + - ]: 23 : ASSERT_TRUE(cvc5_synth_result_has_solution(res));
3549 : 23 : cvc5_get_synth_solutions(d_solver, args.size(), args.data());
3550 : :
3551 : 23 : ASSERT_DEATH(cvc5_check_synth_next(nullptr), "unexpected NULL argument");
3552 : : }
3553 : :
3554 : 86 : TEST_F(TestCApiBlackSolver, check_synth_next2)
3555 : : {
3556 : 22 : cvc5_set_option(d_solver, "sygus", "true");
3557 : 22 : cvc5_set_option(d_solver, "incremental", "false");
3558 : 22 : (void)cvc5_synth_fun(d_solver, "f", 0, nullptr, d_bool);
3559 : 22 : cvc5_check_synth(d_solver);
3560 : 22 : ASSERT_DEATH(cvc5_check_synth_next(d_solver),
3561 : : "cannot check for a next synthesis solution");
3562 : : }
3563 : :
3564 : 82 : TEST_F(TestCApiBlackSolver, check_synth_next3)
3565 : : {
3566 : 21 : cvc5_set_option(d_solver, "sygus", "true");
3567 : 21 : cvc5_set_option(d_solver, "incremental", "true");
3568 : 21 : (void)cvc5_synth_fun(d_solver, "f", 0, nullptr, d_bool);
3569 : 21 : ASSERT_DEATH(cvc5_check_synth_next(d_solver), "unless immediately preceded");
3570 : : }
3571 : :
3572 : 68 : TEST_F(TestCApiBlackSolver, find_synth)
3573 : : {
3574 : 20 : cvc5_set_option(d_solver, "sygus", "true");
3575 : 20 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
3576 : 20 : std::vector<Cvc5Term> symbols = {start};
3577 : : Cvc5Grammar g =
3578 : 20 : cvc5_mk_grammar(d_solver, 0, nullptr, symbols.size(), symbols.data());
3579 : :
3580 : 20 : ASSERT_DEATH(
3581 : : cvc5_synth_fun_with_grammar(d_solver, "f", 0, nullptr, d_bool, g),
3582 : : "invalid grammar");
3583 : :
3584 : 19 : Cvc5Term ttrue = cvc5_mk_true(d_tm);
3585 : 19 : Cvc5Term tfalse = cvc5_mk_false(d_tm);
3586 : 19 : cvc5_grammar_add_rule(g, start, ttrue);
3587 : 19 : cvc5_grammar_add_rule(g, start, tfalse);
3588 : 19 : (void)cvc5_synth_fun_with_grammar(d_solver, "f", 0, nullptr, d_bool, g);
3589 : :
3590 : : // should enumerate based on the grammar of the function to synthesize above
3591 : 19 : Cvc5Term t = cvc5_find_synth(d_solver, CVC5_FIND_SYNTH_TARGET_ENUM);
3592 [ + - ][ + - ]: 19 : ASSERT_TRUE(t && cvc5_sort_is_boolean(cvc5_term_get_sort(t)));
[ - + ][ + - ]
3593 : :
3594 : 19 : ASSERT_DEATH(cvc5_find_synth(nullptr, CVC5_FIND_SYNTH_TARGET_ENUM),
3595 : : "unexpected NULL argument");
3596 : 18 : ASSERT_DEATH(cvc5_find_synth(d_solver, static_cast<Cvc5FindSynthTarget>(125)),
3597 : : "invalid find synthesis target");
3598 : :
3599 : 17 : ASSERT_DEATH(
3600 : : cvc5_find_synth_with_grammar(nullptr, CVC5_FIND_SYNTH_TARGET_ENUM, g),
3601 : : "unexpected NULL argument");
3602 : 16 : ASSERT_DEATH(cvc5_find_synth_with_grammar(
3603 : : d_solver, static_cast<Cvc5FindSynthTarget>(125), g),
3604 : : "invalid find synthesis target");
3605 : 15 : ASSERT_DEATH(cvc5_find_synth_with_grammar(
3606 : : d_solver, CVC5_FIND_SYNTH_TARGET_ENUM, nullptr),
3607 : : "invalid grammar");
3608 [ + - ]: 14 : }
3609 : :
3610 : 54 : TEST_F(TestCApiBlackSolver, find_synth2)
3611 : : {
3612 : 14 : cvc5_set_option(d_solver, "sygus", "true");
3613 : 14 : cvc5_set_option(d_solver, "incremental", "true");
3614 : :
3615 : 14 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
3616 : 14 : std::vector<Cvc5Term> symbols = {start};
3617 : : Cvc5Grammar g =
3618 : 14 : cvc5_mk_grammar(d_solver, 0, nullptr, symbols.size(), symbols.data());
3619 : 14 : Cvc5Term ttrue = cvc5_mk_true(d_tm);
3620 : 14 : Cvc5Term tfalse = cvc5_mk_false(d_tm);
3621 : 14 : cvc5_grammar_add_rule(g, start, ttrue);
3622 : 14 : cvc5_grammar_add_rule(g, start, tfalse);
3623 : :
3624 : : // should enumerate true/false
3625 : : Cvc5Term t =
3626 : 14 : cvc5_find_synth_with_grammar(d_solver, CVC5_FIND_SYNTH_TARGET_ENUM, g);
3627 [ + - ][ + - ]: 14 : ASSERT_TRUE(t && cvc5_sort_is_boolean(cvc5_term_get_sort(t)));
[ - + ][ + - ]
3628 : 14 : t = cvc5_find_synth_next(d_solver);
3629 [ + - ][ + - ]: 14 : ASSERT_TRUE(t && cvc5_sort_is_boolean(cvc5_term_get_sort(t)));
[ - + ][ + - ]
3630 : :
3631 : 14 : ASSERT_DEATH(cvc5_find_synth_next(nullptr), "unexpected NULL argument");
3632 [ + - ]: 13 : }
3633 : :
3634 : 50 : TEST_F(TestCApiBlackSolver, get_statistics)
3635 : : {
3636 : 13 : ASSERT_DEATH(cvc5_get_statistics(nullptr), "unexpected NULL argument");
3637 : :
3638 : : // do some reasoning to make sure we have statistics
3639 : : {
3640 : 12 : Cvc5Sort s2 = cvc5_mk_array_sort(d_tm, d_int, d_int);
3641 : 12 : Cvc5Term t1 = cvc5_mk_const(d_tm, d_int, "i");
3642 : 12 : Cvc5Term t2 = cvc5_mk_const(d_tm, s2, "a");
3643 : 12 : std::vector<Cvc5Term> args = {t2, t1};
3644 : 12 : args = {cvc5_mk_term(d_tm, CVC5_KIND_SELECT, args.size(), args.data()), t1};
3645 : 12 : cvc5_assert_formula(
3646 : : d_solver,
3647 : 12 : cvc5_mk_term(d_tm, CVC5_KIND_DISTINCT, args.size(), args.data()));
3648 : 12 : cvc5_check_sat(d_solver);
3649 : 12 : }
3650 : 12 : Cvc5Statistics stats = cvc5_get_statistics(d_solver);
3651 : 12 : (void)cvc5_stats_to_string(stats);
3652 : :
3653 : 12 : Cvc5Stat stat1 = cvc5_stats_get(stats, "global::totalTime");
3654 [ - + ][ + - ]: 12 : ASSERT_FALSE(cvc5_stat_is_internal(stat1));
3655 [ - + ][ + - ]: 12 : ASSERT_FALSE(cvc5_stat_is_default(stat1));
3656 [ - + ][ + - ]: 12 : ASSERT_TRUE(cvc5_stat_is_string(stat1));
3657 : 12 : (void)cvc5_stat_to_string(stat1);
3658 : :
3659 : 12 : std::string time = cvc5_stat_get_string(stat1);
3660 [ - + ][ + - ]: 12 : ASSERT_TRUE(time.rfind("ms") == time.size() - 2); // ends with "ms"
3661 [ - + ][ + - ]: 12 : ASSERT_FALSE(cvc5_stat_is_double(stat1));
3662 : :
3663 : 12 : Cvc5Stat stat2 = cvc5_stats_get(stats, "resource::resourceUnitsUsed");
3664 [ - + ][ + - ]: 12 : ASSERT_TRUE(cvc5_stat_is_internal(stat2));
3665 [ - + ][ + - ]: 12 : ASSERT_FALSE(cvc5_stat_is_default(stat2));
3666 [ - + ][ + - ]: 12 : ASSERT_TRUE(cvc5_stat_is_int(stat2));
3667 [ - + ][ + - ]: 12 : ASSERT_TRUE(cvc5_stat_get_int(stat2) >= 0);
3668 : 12 : (void)cvc5_stat_to_string(stat2);
3669 : :
3670 : 12 : cvc5_stats_iter_init(stats, true, true);
3671 : 12 : bool hasstats = false;
3672 [ + + ]: 6168 : while (cvc5_stats_iter_has_next(stats))
3673 : : {
3674 : 6156 : hasstats = true;
3675 : : const char* name;
3676 : 6156 : Cvc5Stat stat = cvc5_stats_iter_next(stats, &name);
3677 : 6156 : (void)cvc5_stat_to_string(stat);
3678 [ + + ]: 6156 : if (name == std::string("theory::arrays::avgIndexListLength"))
3679 : : {
3680 [ - + ][ + - ]: 12 : ASSERT_TRUE(cvc5_stat_is_internal(stat));
3681 [ - + ][ + - ]: 12 : ASSERT_TRUE(cvc5_stat_is_double(stat));
3682 [ - + ][ + - ]: 12 : ASSERT_TRUE(std::isnan(cvc5_stat_get_double(stat)));
3683 : : }
3684 : : }
3685 [ - + ][ + - ]: 12 : ASSERT_TRUE(hasstats);
3686 : : }
3687 : :
3688 : 48 : TEST_F(TestCApiBlackSolver, print_statistics_safe)
3689 : : {
3690 : 12 : testing::internal::CaptureStdout();
3691 : 12 : cvc5_print_stats_safe(d_solver, STDOUT_FILENO);
3692 : 12 : testing::internal::GetCapturedStdout();
3693 : 12 : }
3694 : :
3695 : : namespace {
3696 : 12 : const Cvc5Term* plugin_unsat_check(size_t* size, void* state)
3697 : : {
3698 [ + - ]: 12 : static thread_local std::vector<Cvc5Term> lemmas;
3699 : : // add the "false" lemma.
3700 : 12 : Cvc5Term flem = cvc5_mk_false(static_cast<Cvc5TermManager*>(state));
3701 : 12 : lemmas = {flem};
3702 : 12 : *size = lemmas.size();
3703 : 12 : return lemmas.data();
3704 : : }
3705 : 24 : const char* plugin_unsat_get_name() { return "PluginUnsat"; }
3706 : : } // namespace
3707 : :
3708 : 48 : TEST_F(TestCApiBlackSolver, plugin_unsat)
3709 : : {
3710 : 12 : Cvc5Plugin plugin{&plugin_unsat_check,
3711 : : nullptr,
3712 : : nullptr,
3713 : : &plugin_unsat_get_name,
3714 : 12 : d_tm,
3715 : : nullptr,
3716 : 12 : nullptr};
3717 : 12 : cvc5_add_plugin(d_solver, &plugin);
3718 [ - + ][ + - ]: 12 : ASSERT_TRUE(plugin.get_name() == std::string("PluginUnsat"));
3719 : : // should be unsat since the plugin above asserts "false" as a lemma
3720 [ - + ][ + - ]: 12 : ASSERT_TRUE(cvc5_result_is_unsat(cvc5_check_sat(d_solver)));
3721 : : }
3722 : :
3723 : : namespace {
3724 : 36 : void plugin_listen_notify_sat_clause(const Cvc5Term clause, void* state)
3725 : : {
3726 : 36 : *static_cast<bool*>(state) = true;
3727 : 36 : }
3728 : 48 : void plugin_listen_notify_theory_lemma(const Cvc5Term lemma, void* state)
3729 : : {
3730 : 48 : *static_cast<bool*>(state) = true;
3731 : 48 : }
3732 : 12 : const char* plugin_listen_get_name() { return "PluginListen"; }
3733 : : } // namespace
3734 : :
3735 : 48 : TEST_F(TestCApiBlackSolver, plugin_listen)
3736 : : {
3737 : : bool clause_seen, lemma_seen;
3738 : 12 : Cvc5Plugin plugin{nullptr,
3739 : : &plugin_listen_notify_sat_clause,
3740 : : &plugin_listen_notify_theory_lemma,
3741 : : &plugin_listen_get_name,
3742 : : nullptr,
3743 : : &clause_seen,
3744 : 12 : &lemma_seen};
3745 : :
3746 : : // NOTE: this shouldn't be necessary but ensures notify_sat_clause is called
3747 : : // here.
3748 : 12 : cvc5_set_option(d_solver, "plugin-notify-sat-clause-in-solve", "false");
3749 : 12 : cvc5_add_plugin(d_solver, &plugin);
3750 : 12 : Cvc5Sort string_sort = cvc5_get_string_sort(d_tm);
3751 : 12 : Cvc5Term x = cvc5_mk_const(d_tm, string_sort, "x");
3752 : 12 : Cvc5Term y = cvc5_mk_const(d_tm, string_sort, "y");
3753 : 12 : std::vector<Cvc5Term> args{x, y};
3754 : : Cvc5Term ctn1 =
3755 : 12 : cvc5_mk_term(d_tm, CVC5_KIND_STRING_CONTAINS, args.size(), args.data());
3756 : 12 : args = {y, x};
3757 : : Cvc5Term ctn2 =
3758 : 12 : cvc5_mk_term(d_tm, CVC5_KIND_STRING_CONTAINS, args.size(), args.data());
3759 : 12 : args = {ctn1, ctn2};
3760 : 12 : cvc5_assert_formula(
3761 : 12 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data()));
3762 : 12 : args = {x};
3763 : : Cvc5Term lx =
3764 : 12 : cvc5_mk_term(d_tm, CVC5_KIND_STRING_LENGTH, args.size(), args.data());
3765 : 12 : args = {y};
3766 : : Cvc5Term ly =
3767 : 12 : cvc5_mk_term(d_tm, CVC5_KIND_STRING_LENGTH, args.size(), args.data());
3768 : 12 : args = {lx, ly};
3769 : 12 : Cvc5Term lc = cvc5_mk_term(d_tm, CVC5_KIND_GT, args.size(), args.data());
3770 : 12 : cvc5_assert_formula(d_solver, lc);
3771 [ - + ][ + - ]: 12 : ASSERT_TRUE(cvc5_result_is_sat(cvc5_check_sat(d_solver)));
3772 : : // above input formulas should induce a theory lemma and SAT clause learning
3773 [ - + ][ + - ]: 12 : ASSERT_TRUE(lemma_seen);
3774 [ - + ][ + - ]: 12 : ASSERT_TRUE(clause_seen);
3775 [ + - ]: 12 : }
3776 : :
3777 : 44 : TEST_F(TestCApiBlackSolver, tuple_project)
3778 : : {
3779 : 12 : std::vector<Cvc5Term> args = {cvc5_mk_string(d_tm, "Z", false)};
3780 : : std::vector<Cvc5Term> elements = {
3781 : 12 : cvc5_mk_true(d_tm),
3782 : 24 : cvc5_mk_integer_int64(d_tm, 3),
3783 : 24 : cvc5_mk_string(d_tm, "C", false),
3784 : 12 : cvc5_mk_term(d_tm, CVC5_KIND_SET_SINGLETON, args.size(), args.data())};
3785 : :
3786 : 12 : Cvc5Term tuple = cvc5_mk_tuple(d_tm, elements.size(), elements.data());
3787 : :
3788 : 12 : std::vector<uint32_t> indices1 = {};
3789 : 12 : std::vector<uint32_t> indices2 = {0};
3790 : 12 : std::vector<uint32_t> indices3 = {0, 1};
3791 : 12 : std::vector<uint32_t> indices4 = {0, 0, 2, 2, 3, 3, 0};
3792 : 12 : std::vector<uint32_t> indices5 = {4};
3793 : 12 : std::vector<uint32_t> indices6 = {0, 4};
3794 : :
3795 : 12 : args = {tuple};
3796 : 24 : (void)cvc5_mk_term_from_op(
3797 : : d_tm,
3798 : : cvc5_mk_op(
3799 : 12 : d_tm, CVC5_KIND_TUPLE_PROJECT, indices1.size(), indices1.data()),
3800 : : args.size(),
3801 : 12 : args.data());
3802 : 24 : (void)cvc5_mk_term_from_op(
3803 : : d_tm,
3804 : : cvc5_mk_op(
3805 : 12 : d_tm, CVC5_KIND_TUPLE_PROJECT, indices2.size(), indices2.data()),
3806 : : args.size(),
3807 : 12 : args.data());
3808 : 24 : (void)cvc5_mk_term_from_op(
3809 : : d_tm,
3810 : : cvc5_mk_op(
3811 : 12 : d_tm, CVC5_KIND_TUPLE_PROJECT, indices3.size(), indices3.data()),
3812 : : args.size(),
3813 : 12 : args.data());
3814 : 24 : (void)cvc5_mk_term_from_op(
3815 : : d_tm,
3816 : : cvc5_mk_op(
3817 : 12 : d_tm, CVC5_KIND_TUPLE_PROJECT, indices4.size(), indices4.data()),
3818 : : args.size(),
3819 : 12 : args.data());
3820 : :
3821 : 12 : ASSERT_DEATH(
3822 : : cvc5_mk_term_from_op(
3823 : : d_tm,
3824 : : cvc5_mk_op(
3825 : : d_tm, CVC5_KIND_TUPLE_PROJECT, indices5.size(), indices5.data()),
3826 : : args.size(),
3827 : : args.data()),
3828 : : "Project index 4");
3829 : 11 : ASSERT_DEATH(
3830 : : cvc5_mk_term_from_op(
3831 : : d_tm,
3832 : : cvc5_mk_op(
3833 : : d_tm, CVC5_KIND_TUPLE_PROJECT, indices6.size(), indices6.data()),
3834 : : args.size(),
3835 : : args.data()),
3836 : : "Project index 4");
3837 : :
3838 : 10 : std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
3839 : :
3840 : : Cvc5Op op =
3841 : 10 : cvc5_mk_op(d_tm, CVC5_KIND_TUPLE_PROJECT, indices.size(), indices.data());
3842 : : Cvc5Term projection =
3843 : 10 : cvc5_mk_term_from_op(d_tm, op, args.size(), args.data());
3844 : :
3845 : 10 : Cvc5Datatype datatype = cvc5_sort_get_datatype(cvc5_term_get_sort(tuple));
3846 : 10 : Cvc5DatatypeConstructor cons = cvc5_dt_get_constructor(datatype, 0);
3847 : :
3848 [ + + ]: 70 : for (size_t i = 0; i < indices.size(); i++)
3849 : : {
3850 : 60 : args = {cvc5_dt_sel_get_term(cvc5_dt_cons_get_selector(cons, indices[i])),
3851 : 60 : tuple};
3852 : : Cvc5Term selected =
3853 : 60 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_SELECTOR, args.size(), args.data());
3854 : 60 : Cvc5Term simplified = cvc5_simplify(d_solver, selected, false);
3855 [ - + ][ + - ]: 60 : ASSERT_TRUE(cvc5_term_is_equal(elements[indices[i]], simplified));
3856 : : }
3857 : :
3858 [ - + ]: 20 : ASSERT_EQ(
3859 : : std::string(
3860 : : "((_ tuple.project 0 3 2 0 1 2) (tuple true 3 \"C\" (set.singleton "
3861 : : "\"Z\")))"),
3862 [ + - ]: 10 : cvc5_term_to_string(projection));
3863 [ + - ][ + - ]: 10 : }
[ + - ][ + - ]
[ + - ][ + - ]
[ + - ][ + - ]
3864 : :
3865 : 40 : TEST_F(TestCApiBlackSolver, vertical_bars)
3866 : : {
3867 : 10 : Cvc5Term a = cvc5_declare_fun(d_solver, "|a |", 0, nullptr, d_real, true);
3868 [ - + ][ + - ]: 20 : ASSERT_EQ(std::string("|a |"), cvc5_term_to_string(a));
3869 : : }
3870 : :
3871 : 40 : TEST_F(TestCApiBlackSolver, get_version)
3872 : : {
3873 : 10 : std::cout << cvc5_get_version(d_solver) << std::endl;
3874 : 10 : }
3875 : :
3876 : 40 : TEST_F(TestCApiBlackSolver, multiple_solvers)
3877 : : {
3878 : : Cvc5Term zero, value1, value2;
3879 : : Cvc5Term deffun;
3880 : : {
3881 : 10 : Cvc5* s1 = cvc5_new(d_tm);
3882 : 10 : cvc5_set_logic(s1, "ALL");
3883 : 10 : cvc5_set_option(s1, "produce-models", "true");
3884 : 10 : Cvc5Term fun1 = cvc5_declare_fun(s1, "f1", 0, nullptr, d_int, true);
3885 : 10 : Cvc5Term x = cvc5_mk_var(d_tm, d_int, "x");
3886 : 10 : zero = cvc5_mk_integer_int64(d_tm, 0);
3887 : 10 : std::vector<Cvc5Term> args = {x};
3888 : : deffun =
3889 : 10 : cvc5_define_fun(s1, "f", args.size(), args.data(), d_int, zero, true);
3890 : 10 : args = {fun1, zero};
3891 : 10 : cvc5_assert_formula(
3892 : 10 : s1, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
3893 : 10 : cvc5_check_sat(s1);
3894 : 10 : value1 = cvc5_get_value(s1, fun1);
3895 : 10 : cvc5_delete(s1);
3896 : 10 : }
3897 [ - + ][ + - ]: 10 : ASSERT_TRUE(cvc5_term_is_equal(zero, value1));
3898 : : {
3899 : 10 : Cvc5* s2 = cvc5_new(d_tm);
3900 : 10 : cvc5_set_logic(s2, "ALL");
3901 : 10 : cvc5_set_option(s2, "produce-models", "true");
3902 : 10 : Cvc5Term fun2 = cvc5_declare_fun(s2, "f2", 0, nullptr, d_int, true);
3903 : 10 : std::vector<Cvc5Term> args = {fun2, value1};
3904 : 10 : cvc5_assert_formula(
3905 : 10 : s2, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
3906 : 10 : cvc5_check_sat(s2);
3907 : 10 : value2 = cvc5_get_value(s2, fun2);
3908 : 10 : cvc5_delete(s2);
3909 : 10 : }
3910 [ - + ][ + - ]: 10 : ASSERT_TRUE(cvc5_term_is_equal(value1, value2));
3911 : : {
3912 : 10 : Cvc5* s3 = cvc5_new(d_tm);
3913 : 10 : cvc5_set_logic(s3, "ALL");
3914 : 10 : cvc5_set_option(s3, "produce-models", "true");
3915 : 10 : Cvc5Term fun3 = cvc5_declare_fun(s3, "f3", 0, nullptr, d_int, true);
3916 : 10 : std::vector<Cvc5Term> args = {deffun, zero};
3917 : : Cvc5Term apply =
3918 : 10 : cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data());
3919 : 10 : args = {fun3, apply};
3920 : 10 : cvc5_assert_formula(
3921 : 10 : s3, cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data()));
3922 : 10 : cvc5_check_sat(s3);
3923 : 10 : Cvc5Term value3 = cvc5_get_value(s3, fun3);
3924 [ - + ][ + - ]: 10 : ASSERT_TRUE(cvc5_term_is_equal(value1, value3));
3925 : 10 : cvc5_delete(s3);
3926 [ + - ]: 10 : }
3927 : : }
3928 : :
3929 : : #ifdef CVC5_USE_COCOA
3930 : :
3931 : 40 : TEST_F(TestCApiBlackSolver, basic_finite_field)
3932 : : {
3933 : 10 : cvc5_set_option(d_solver, "produce-models", "true");
3934 : :
3935 : 10 : Cvc5Sort ff_sort = cvc5_mk_ff_sort(d_tm, "5", 10);
3936 : 10 : Cvc5Term a = cvc5_mk_const(d_tm, ff_sort, "a");
3937 : 10 : Cvc5Term b = cvc5_mk_const(d_tm, ff_sort, "b");
3938 [ - + ][ + - ]: 20 : ASSERT_EQ(std::string("5"), cvc5_sort_ff_get_size(ff_sort));
3939 : :
3940 : 10 : std::vector<Cvc5Term> args = {a, b};
3941 : 0 : args = {
3942 : 10 : cvc5_mk_term(d_tm, CVC5_KIND_FINITE_FIELD_MULT, args.size(), args.data()),
3943 : 10 : cvc5_mk_ff_elem(d_tm, "1", ff_sort, 10)};
3944 : 10 : Cvc5Term inv = cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
3945 : 10 : args = {a, cvc5_mk_ff_elem(d_tm, "2", ff_sort, 10)};
3946 : : Cvc5Term a_is_two =
3947 : 10 : cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
3948 : :
3949 : 10 : cvc5_assert_formula(d_solver, inv);
3950 : 10 : cvc5_assert_formula(d_solver, a_is_two);
3951 [ - + ][ + - ]: 10 : ASSERT_TRUE(cvc5_result_is_sat(cvc5_check_sat(d_solver)));
3952 [ - + ]: 10 : ASSERT_EQ(cvc5_term_get_ff_value(cvc5_get_value(d_solver, a)),
3953 [ + - ]: 10 : std::string("2"));
3954 [ - + ]: 10 : ASSERT_EQ(cvc5_term_get_ff_value(cvc5_get_value(d_solver, b)),
3955 [ + - ]: 10 : std::string("-2"));
3956 : :
3957 : 10 : args = {b, cvc5_mk_ff_elem(d_tm, "2", ff_sort, 10)};
3958 : : Cvc5Term b_is_two =
3959 : 10 : cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
3960 : 10 : cvc5_assert_formula(d_solver, b_is_two);
3961 [ - + ][ + - ]: 10 : ASSERT_FALSE(cvc5_result_is_sat(cvc5_check_sat(d_solver)));
3962 : : }
3963 : :
3964 : 40 : TEST_F(TestCApiBlackSolver, basic_finite_field_base)
3965 : : {
3966 : 10 : cvc5_set_option(d_solver, "produce-models", "true");
3967 : :
3968 : 10 : Cvc5Sort ff_sort = cvc5_mk_ff_sort(d_tm, "101", 2);
3969 : 10 : Cvc5Term a = cvc5_mk_const(d_tm, ff_sort, "a");
3970 : 10 : Cvc5Term b = cvc5_mk_const(d_tm, ff_sort, "b");
3971 [ - + ][ + - ]: 20 : ASSERT_EQ(std::string("5"), cvc5_sort_ff_get_size(ff_sort));
3972 : :
3973 : 10 : std::vector<Cvc5Term> args = {a, b};
3974 : 0 : args = {
3975 : 10 : cvc5_mk_term(d_tm, CVC5_KIND_FINITE_FIELD_MULT, args.size(), args.data()),
3976 : 10 : cvc5_mk_ff_elem(d_tm, "1", ff_sort, 3)};
3977 : 10 : Cvc5Term inv = cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
3978 : :
3979 : 10 : args = {a, cvc5_mk_ff_elem(d_tm, "10", ff_sort, 2)};
3980 : : Cvc5Term a_is_two =
3981 : 10 : cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
3982 : :
3983 : 10 : cvc5_assert_formula(d_solver, inv);
3984 : 10 : cvc5_assert_formula(d_solver, a_is_two);
3985 [ - + ][ + - ]: 10 : ASSERT_TRUE(cvc5_result_is_sat(cvc5_check_sat(d_solver)));
3986 [ - + ]: 10 : ASSERT_EQ(cvc5_term_get_ff_value(cvc5_get_value(d_solver, a)),
3987 [ + - ]: 10 : std::string("2"));
3988 [ - + ]: 10 : ASSERT_EQ(cvc5_term_get_ff_value(cvc5_get_value(d_solver, b)),
3989 [ + - ]: 10 : std::string("-2"));
3990 : :
3991 : 10 : args = {b, cvc5_mk_ff_elem(d_tm, "2", ff_sort, 10)};
3992 : : Cvc5Term b_is_two =
3993 : 10 : cvc5_mk_term(d_tm, CVC5_KIND_EQUAL, args.size(), args.data());
3994 : 10 : cvc5_assert_formula(d_solver, b_is_two);
3995 [ - + ][ + - ]: 10 : ASSERT_FALSE(cvc5_result_is_sat(cvc5_check_sat(d_solver)));
3996 : : }
3997 : : #endif // CVC5_USE_COCOA
3998 : :
3999 : 22 : TEST_F(TestCApiBlackSolver, output1)
4000 : : {
4001 : 10 : ASSERT_DEATH(cvc5_is_output_on(nullptr, "inst"), "unexpected NULL argument");
4002 : 9 : ASSERT_DEATH(cvc5_is_output_on(d_solver, nullptr),
4003 : : "unexpected NULL argument");
4004 : 8 : ASSERT_DEATH(cvc5_is_output_on(d_solver, "foo-invalid"),
4005 : : "invalid output tag");
4006 : :
4007 : 7 : ASSERT_DEATH(cvc5_get_output(nullptr, "inst", "<stdout>"),
4008 : : "unexpected NULL argument");
4009 : 6 : ASSERT_DEATH(cvc5_get_output(d_solver, nullptr, "<stdout>"),
4010 : : "unexpected NULL argument");
4011 : 5 : ASSERT_DEATH(cvc5_get_output(d_solver, "inst", nullptr),
4012 : : "unexpected NULL argument");
4013 : 4 : ASSERT_DEATH(cvc5_get_output(d_solver, "foo-invalid", "<stdout>"),
4014 : : "invalid output tag");
4015 : :
4016 : 3 : ASSERT_DEATH(cvc5_close_output(nullptr, "<stdout>"),
4017 : : "unexpected NULL argument");
4018 : 2 : ASSERT_DEATH(cvc5_close_output(d_solver, nullptr),
4019 : : "unexpected NULL argument");
4020 : : // should not fail
4021 : 1 : cvc5_close_output(d_solver, "<stdout>");
4022 : : }
4023 : :
4024 : 4 : TEST_F(TestCApiBlackSolver, output2)
4025 : : {
4026 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_is_output_on(d_solver, "inst"));
4027 : : // noop if output tag is not enabled
4028 : 1 : cvc5_get_output(d_solver, "inst", "<stdout>");
4029 : 1 : cvc5_set_option(d_solver, "output", "inst");
4030 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_is_output_on(d_solver, "inst"));
4031 : 1 : cvc5_get_output(d_solver, "inst", "<stdout>");
4032 : : }
4033 : :
4034 : 4 : TEST_F(TestCApiBlackSolver, output3)
4035 : : {
4036 : 1 : cvc5_set_option(d_solver, "output", "post-asserts");
4037 : 1 : cvc5_get_output(d_solver, "post-asserts", "<stdout>");
4038 : :
4039 : 1 : testing::internal::CaptureStdout();
4040 : :
4041 : 1 : std::vector<Cvc5Term> vars = {cvc5_mk_var(d_tm, d_bool, "b")};
4042 : 1 : Cvc5Term g = cvc5_define_fun(
4043 : 1 : d_solver, "g", vars.size(), vars.data(), d_bool, vars[0], true);
4044 : 1 : std::vector<Cvc5Term> args = {g, cvc5_mk_true(d_tm)};
4045 : 1 : args = {cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data())};
4046 : 1 : Cvc5Term appnot = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data());
4047 : 1 : args = {cvc5_define_fun(
4048 : 1 : d_solver, "f", 0, nullptr, d_bool, cvc5_mk_true(d_tm), true)};
4049 : 1 : args = {cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()), appnot};
4050 : 1 : cvc5_assert_formula(
4051 : 1 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data()));
4052 : 1 : cvc5_check_sat(d_solver);
4053 : :
4054 : 1 : std::string out = testing::internal::GetCapturedStdout();
4055 : 1 : std::stringstream expected;
4056 : 1 : expected << ";; post-asserts start" << std::endl;
4057 : 1 : expected << "(set-logic ALL)" << std::endl;
4058 : 1 : expected << "(define-fun f () Bool true)" << std::endl;
4059 : 1 : expected << "(define-fun g ((b Bool)) Bool b)" << std::endl;
4060 : 1 : expected << "(assert false)" << std::endl;
4061 : 1 : expected << "(check-sat)" << std::endl;
4062 : 1 : expected << ";; post-asserts end" << std::endl;
4063 [ - + ][ + - ]: 2 : ASSERT_EQ(out, expected.str());
4064 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
4065 : :
4066 : 4 : TEST_F(TestCApiBlackSolver, output4)
4067 : : {
4068 : 1 : const char* filename = "foo.out";
4069 : 1 : cvc5_set_option(d_solver, "output", "post-asserts");
4070 : 1 : cvc5_get_output(d_solver, "post-asserts", filename);
4071 : :
4072 : 1 : std::vector<Cvc5Term> vars = {cvc5_mk_var(d_tm, d_bool, "b")};
4073 : 1 : Cvc5Term g = cvc5_define_fun(
4074 : 1 : d_solver, "g", vars.size(), vars.data(), d_bool, vars[0], true);
4075 : 1 : std::vector<Cvc5Term> args = {g, cvc5_mk_true(d_tm)};
4076 : 1 : args = {cvc5_mk_term(d_tm, CVC5_KIND_APPLY_UF, args.size(), args.data())};
4077 : 1 : Cvc5Term appnot = cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data());
4078 : 1 : args = {cvc5_define_fun(
4079 : 1 : d_solver, "f", 0, nullptr, d_bool, cvc5_mk_true(d_tm), true)};
4080 : 1 : args = {cvc5_mk_term(d_tm, CVC5_KIND_NOT, args.size(), args.data()), appnot};
4081 : 1 : cvc5_assert_formula(
4082 : 1 : d_solver, cvc5_mk_term(d_tm, CVC5_KIND_OR, args.size(), args.data()));
4083 : 1 : cvc5_check_sat(d_solver);
4084 : :
4085 : 1 : cvc5_close_output(d_solver, filename);
4086 : 1 : std::ifstream in(filename);
4087 : 1 : std::stringstream out;
4088 : 1 : out << in.rdbuf();
4089 : 1 : std::stringstream expected;
4090 : 1 : expected << ";; post-asserts start" << std::endl;
4091 : 1 : expected << "(set-logic ALL)" << std::endl;
4092 : 1 : expected << "(define-fun f () Bool true)" << std::endl;
4093 : 1 : expected << "(define-fun g ((b Bool)) Bool b)" << std::endl;
4094 : 1 : expected << "(assert false)" << std::endl;
4095 : 1 : expected << "(check-sat)" << std::endl;
4096 : 1 : expected << ";; post-asserts end" << std::endl;
4097 [ - + ][ + - ]: 2 : ASSERT_EQ(out.str(), expected.str());
4098 : 1 : std::remove(filename);
4099 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
[ + - ]
4100 : : } // namespace cvc5::internal::test
|
