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