Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * The cvc5 types definitions for the C API.
11 : : */
12 : :
13 : : #include "api/c/cvc5_c_structs.h"
14 : :
15 : : #include "api/c/cvc5_checks.h"
16 : :
17 : : /* -------------------------------------------------------------------------- */
18 : : /* Cvc5TermManager struct */
19 : : /* -------------------------------------------------------------------------- */
20 : :
21 : 223362 : Cvc5Sort Cvc5TermManager::export_sort(const cvc5::Sort& sort)
22 : : {
23 [ - + ][ - + ]: 223362 : Assert(!sort.isNull());
[ - - ]
24 : 223362 : auto [it, inserted] = d_alloc_sorts.try_emplace(sort, this, sort);
25 [ + + ]: 223362 : if (!inserted)
26 : : {
27 : 10457 : copy(&it->second);
28 : : }
29 : 223362 : return &it->second;
30 : : }
31 : :
32 : 154886 : Cvc5Term Cvc5TermManager::export_term(const cvc5::Term& term)
33 : : {
34 [ - + ][ - + ]: 154886 : Assert(!term.isNull());
[ - - ]
35 : 154886 : auto [it, inserted] = d_alloc_terms.try_emplace(term, this, term);
36 [ + + ]: 154886 : if (!inserted)
37 : : {
38 : 31500 : copy(&it->second);
39 : : }
40 : 154886 : return &it->second;
41 : : }
42 : :
43 : 3756 : Cvc5Op Cvc5TermManager::export_op(const cvc5::Op& op)
44 : : {
45 [ - + ][ - + ]: 3756 : Assert(!op.isNull());
[ - - ]
46 : 3756 : auto [it, inserted] = d_alloc_ops.try_emplace(op, this, op);
47 [ + + ]: 3756 : if (!inserted)
48 : : {
49 : 661 : copy(&it->second);
50 : : }
51 : 3756 : return &it->second;
52 : : }
53 : :
54 : 2553 : Cvc5Datatype Cvc5TermManager::export_dt(const cvc5::Datatype& dt)
55 : : {
56 [ - + ][ - + ]: 2553 : Assert(!dt.isNull());
[ - - ]
57 : 2553 : auto [it, inserted] = d_alloc_dts.try_emplace(dt, this, dt);
58 [ - + ]: 2553 : if (!inserted)
59 : : {
60 : 0 : copy(&it->second);
61 : : }
62 : 2553 : return &it->second;
63 : : }
64 : :
65 : 2487 : Cvc5DatatypeConstructor Cvc5TermManager::export_dt_cons(
66 : : const cvc5::DatatypeConstructor& cons)
67 : : {
68 [ - + ][ - + ]: 2487 : Assert(!cons.isNull());
[ - - ]
69 : 2487 : auto [it, inserted] = d_alloc_dt_conss.try_emplace(cons, this, cons);
70 [ - + ]: 2487 : if (!inserted)
71 : : {
72 : 0 : copy(&it->second);
73 : : }
74 : 2487 : return &it->second;
75 : : }
76 : :
77 : 1530 : Cvc5DatatypeSelector Cvc5TermManager::export_dt_sel(
78 : : const cvc5::DatatypeSelector& sel)
79 : : {
80 [ - + ][ - + ]: 1530 : Assert(!sel.isNull());
[ - - ]
81 : 1530 : auto [it, inserted] = d_alloc_dt_sels.try_emplace(sel, this, sel);
82 [ - + ]: 1530 : if (!inserted)
83 : : {
84 : 0 : copy(&it->second);
85 : : }
86 : 1530 : return &it->second;
87 : : }
88 : :
89 : 5144 : Cvc5DatatypeDecl Cvc5TermManager::export_dt_decl(const cvc5::DatatypeDecl& decl)
90 : : {
91 [ - + ][ - + ]: 5144 : Assert(!decl.isNull());
[ - - ]
92 : 5144 : auto [it, inserted] = d_alloc_dt_decls.try_emplace(decl, this, decl);
93 [ - + ]: 5144 : if (!inserted)
94 : : {
95 : 0 : copy(&it->second);
96 : : }
97 : 5144 : return &it->second;
98 : : }
99 : :
100 : 13818 : Cvc5DatatypeConstructorDecl Cvc5TermManager::export_dt_cons_decl(
101 : : const cvc5::DatatypeConstructorDecl& decl)
102 : : {
103 [ - + ][ - + ]: 13818 : Assert(!decl.isNull());
[ - - ]
104 : 13818 : auto [it, inserted] = d_alloc_dt_cons_decls.try_emplace(decl, this, decl);
105 [ - + ]: 13818 : if (!inserted)
106 : : {
107 : 0 : copy(&it->second);
108 : : }
109 : 13818 : return &it->second;
110 : : }
111 : :
112 : 6519 : Cvc5Stat Cvc5TermManager::export_stat(const cvc5::Stat& stat)
113 : : {
114 : 6519 : d_alloc_stats.emplace_back(this, stat);
115 : 6519 : return &d_alloc_stats.back();
116 : : }
117 : :
118 : 285 : Cvc5Statistics Cvc5TermManager::export_stats(const cvc5::Statistics& stat)
119 : : {
120 : 285 : d_alloc_statistics.emplace_back(this, stat);
121 : 285 : return &d_alloc_statistics.back();
122 : : }
123 : :
124 : 489 : void Cvc5TermManager::release(cvc5_term_t* term)
125 : : {
126 [ + - ]: 489 : if (term)
127 : : {
128 : 489 : term->d_refs -= 1;
129 [ + + ]: 489 : if (term->d_refs == 0)
130 : : {
131 [ - + ][ - + ]: 126 : Assert(d_alloc_terms.find(term->d_term) != d_alloc_terms.end());
[ - - ]
132 : 126 : d_alloc_terms.erase(term->d_term);
133 : : }
134 : : }
135 : 489 : }
136 : :
137 : 31863 : cvc5_term_t* Cvc5TermManager::copy(cvc5_term_t* term)
138 : : {
139 [ + - ]: 31863 : if (term)
140 : : {
141 : 31863 : term->d_refs += 1;
142 : : }
143 : 31863 : return term;
144 : : }
145 : :
146 : 16 : void Cvc5TermManager::release(cvc5_op_t* op)
147 : : {
148 [ + - ]: 16 : if (op)
149 : : {
150 : 16 : op->d_refs -= 1;
151 [ + + ]: 16 : if (op->d_refs == 0)
152 : : {
153 [ - + ][ - + ]: 8 : Assert(d_alloc_ops.find(op->d_op) != d_alloc_ops.end());
[ - - ]
154 : 8 : d_alloc_ops.erase(op->d_op);
155 : : }
156 : : }
157 : 16 : }
158 : :
159 : 669 : cvc5_op_t* Cvc5TermManager::copy(cvc5_op_t* op)
160 : : {
161 [ + - ]: 669 : if (op)
162 : : {
163 : 669 : op->d_refs += 1;
164 : : }
165 : 669 : return op;
166 : : }
167 : :
168 : 132 : void Cvc5TermManager::release(cvc5_sort_t* sort)
169 : : {
170 [ + - ]: 132 : if (sort)
171 : : {
172 : 132 : sort->d_refs -= 1;
173 [ + + ]: 132 : if (sort->d_refs == 0)
174 : : {
175 [ - + ][ - + ]: 66 : Assert(d_alloc_sorts.find(sort->d_sort) != d_alloc_sorts.end());
[ - - ]
176 : 66 : d_alloc_sorts.erase(sort->d_sort);
177 : : }
178 : : }
179 : 132 : }
180 : :
181 : 10523 : cvc5_sort_t* Cvc5TermManager::copy(cvc5_sort_t* sort)
182 : : {
183 [ + - ]: 10523 : if (sort)
184 : : {
185 : 10523 : sort->d_refs += 1;
186 : : }
187 : 10523 : return sort;
188 : : }
189 : :
190 : 70 : void Cvc5TermManager::release(cvc5_dt_t* dt)
191 : : {
192 [ + - ]: 70 : if (dt)
193 : : {
194 : 70 : dt->d_refs -= 1;
195 [ + + ]: 70 : if (dt->d_refs == 0)
196 : : {
197 [ - + ][ - + ]: 35 : Assert(d_alloc_dts.find(dt->d_dt) != d_alloc_dts.end());
[ - - ]
198 : 35 : d_alloc_dts.erase(dt->d_dt);
199 : : }
200 : : }
201 : 70 : }
202 : :
203 : 35 : cvc5_dt_t* Cvc5TermManager::copy(cvc5_dt_t* dt)
204 : : {
205 [ + - ]: 35 : if (dt)
206 : : {
207 : 35 : dt->d_refs += 1;
208 : : }
209 : 35 : return dt;
210 : : }
211 : :
212 : 92 : void Cvc5TermManager::release(cvc5_dt_cons_t* cons)
213 : : {
214 [ + - ]: 92 : if (cons)
215 : : {
216 : 92 : cons->d_refs -= 1;
217 [ + + ]: 92 : if (cons->d_refs == 0)
218 : : {
219 [ - + ][ - + ]: 46 : Assert(d_alloc_dt_conss.find(cons->d_dt_cons) != d_alloc_dt_conss.end());
[ - - ]
220 : 46 : d_alloc_dt_conss.erase(cons->d_dt_cons);
221 : : }
222 : : }
223 : 92 : }
224 : :
225 : 46 : cvc5_dt_cons_t* Cvc5TermManager::copy(cvc5_dt_cons_t* cons)
226 : : {
227 [ + - ]: 46 : if (cons)
228 : : {
229 : 46 : cons->d_refs += 1;
230 : : }
231 : 46 : return cons;
232 : : }
233 : :
234 : 108 : void Cvc5TermManager::release(cvc5_dt_sel_t* sel)
235 : : {
236 [ + - ]: 108 : if (sel)
237 : : {
238 : 108 : sel->d_refs -= 1;
239 [ + + ]: 108 : if (sel->d_refs == 0)
240 : : {
241 [ - + ][ - + ]: 54 : Assert(d_alloc_dt_sels.find(sel->d_dt_sel) != d_alloc_dt_sels.end());
[ - - ]
242 : 54 : d_alloc_dt_sels.erase(sel->d_dt_sel);
243 : : }
244 : : }
245 : 108 : }
246 : :
247 : 54 : cvc5_dt_sel_t* Cvc5TermManager::copy(cvc5_dt_sel_t* sel)
248 : : {
249 [ + - ]: 54 : if (sel)
250 : : {
251 : 54 : sel->d_refs += 1;
252 : : }
253 : 54 : return sel;
254 : : }
255 : :
256 : 128 : void Cvc5TermManager::release(cvc5_dt_decl_t* decl)
257 : : {
258 [ + - ]: 128 : if (decl)
259 : : {
260 : 128 : decl->d_refs -= 1;
261 [ + + ]: 128 : if (decl->d_refs == 0)
262 : : {
263 [ - + ][ - + ]: 64 : Assert(d_alloc_dt_decls.find(decl->d_decl) != d_alloc_dt_decls.end());
[ - - ]
264 : 64 : d_alloc_dt_decls.erase(decl->d_decl);
265 : : }
266 : : }
267 : 128 : }
268 : :
269 : 64 : cvc5_dt_decl_t* Cvc5TermManager::copy(cvc5_dt_decl_t* decl)
270 : : {
271 [ + - ]: 64 : if (decl)
272 : : {
273 : 64 : decl->d_refs += 1;
274 : : }
275 : 64 : return decl;
276 : : }
277 : :
278 : 152 : void Cvc5TermManager::release(cvc5_dt_cons_decl_t* decl)
279 : : {
280 [ + - ]: 152 : if (decl)
281 : : {
282 : 152 : decl->d_refs -= 1;
283 [ + + ]: 152 : if (decl->d_refs == 0)
284 : : {
285 [ - + ][ - + ]: 76 : Assert(d_alloc_dt_cons_decls.find(decl->d_decl)
[ - - ]
286 : : != d_alloc_dt_cons_decls.end());
287 : 76 : d_alloc_dt_cons_decls.erase(decl->d_decl);
288 : : }
289 : : }
290 : 152 : }
291 : :
292 : 76 : cvc5_dt_cons_decl_t* Cvc5TermManager::copy(cvc5_dt_cons_decl_t* decl)
293 : : {
294 [ + - ]: 76 : if (decl)
295 : : {
296 : 76 : decl->d_refs += 1;
297 : : }
298 : 76 : return decl;
299 : : }
300 : :
301 : 267 : void Cvc5TermManager::release()
302 : : {
303 : 267 : d_alloc_sorts.clear();
304 : 267 : d_alloc_terms.clear();
305 : 267 : d_alloc_dts.clear();
306 : 267 : d_alloc_dt_conss.clear();
307 : 267 : d_alloc_dt_sels.clear();
308 : 267 : d_alloc_dt_decls.clear();
309 : 267 : d_alloc_dt_cons_decls.clear();
310 : 267 : }
311 : :
312 : : /* -------------------------------------------------------------------------- */
313 : : /* Cvc5 struct */
314 : : /* -------------------------------------------------------------------------- */
315 : :
316 : 30319 : Cvc5::~Cvc5()
317 : : {
318 [ - + ]: 30319 : if (d_output_tag_file_stream.is_open())
319 : : {
320 : 0 : d_output_tag_file_stream.close();
321 : : }
322 : : // reset redirected output stream returned by Solver::getOutput()
323 [ + + ]: 30319 : if (d_output_tag_stream)
324 : : {
325 [ - + ][ - + ]: 3 : Assert(d_output_tag_streambuf);
326 : 3 : d_output_tag_stream->rdbuf(d_output_tag_streambuf);
327 : : }
328 : 30319 : }
329 : :
330 : 14408 : Cvc5Result Cvc5::export_result(const cvc5::Result& result)
331 : : {
332 [ - + ][ - + ]: 14408 : Assert(!result.isNull());
[ - - ]
333 : 14408 : auto [it, inserted] = d_alloc_results.try_emplace(result, this, result);
334 [ + + ]: 14408 : if (!inserted)
335 : : {
336 : 1677 : copy(&it->second);
337 : : }
338 : 14408 : return &it->second;
339 : : }
340 : :
341 : 287 : void Cvc5::release(cvc5_result_t* result)
342 : : {
343 : 287 : result->d_refs -= 1;
344 [ + + ]: 287 : if (result->d_refs == 0)
345 : : {
346 [ - + ][ - + ]: 286 : Assert(d_alloc_results.find(result->d_result) != d_alloc_results.end());
[ - - ]
347 : 286 : d_alloc_results.erase(result->d_result);
348 : : }
349 : 287 : }
350 : :
351 : 1678 : cvc5_result_t* Cvc5::copy(cvc5_result_t* result)
352 : : {
353 : 1678 : result->d_refs += 1;
354 : 1678 : return result;
355 : : }
356 : :
357 : 191 : Cvc5SynthResult Cvc5::export_synth_result(const cvc5::SynthResult& result)
358 : : {
359 [ - + ][ - + ]: 191 : Assert(!result.isNull());
[ - - ]
360 : 191 : auto [it, inserted] = d_alloc_synth_results.try_emplace(result, this, result);
361 [ + + ]: 191 : if (!inserted)
362 : : {
363 : 23 : copy(&it->second);
364 : : }
365 : 191 : return &it->second;
366 : : }
367 : :
368 : 2 : void Cvc5::release(cvc5_synth_result_t* result)
369 : : {
370 : 2 : result->d_refs -= 1;
371 [ + + ]: 2 : if (result->d_refs == 0)
372 : : {
373 [ - + ][ - + ]: 1 : Assert(d_alloc_synth_results.find(result->d_result)
[ - - ]
374 : : != d_alloc_synth_results.end());
375 : 1 : d_alloc_synth_results.erase(result->d_result);
376 : : }
377 : 2 : }
378 : :
379 : 24 : cvc5_synth_result_t* Cvc5::copy(cvc5_synth_result_t* result)
380 : : {
381 : 24 : result->d_refs += 1;
382 : 24 : return result;
383 : : }
384 : :
385 : 1480 : Cvc5Proof Cvc5::export_proof(const cvc5::Proof& proof)
386 : : {
387 : 1480 : auto [it, inserted] = d_alloc_proofs.try_emplace(proof, this, proof);
388 [ - + ]: 1480 : if (!inserted)
389 : : {
390 : 0 : copy(&it->second);
391 : : }
392 : 1480 : return &it->second;
393 : : }
394 : :
395 : 2 : void Cvc5::release(cvc5_proof_t* proof)
396 : : {
397 : 2 : proof->d_refs -= 1;
398 [ + + ]: 2 : if (proof->d_refs == 0)
399 : : {
400 [ - + ][ - + ]: 1 : Assert(d_alloc_proofs.find(proof->d_proof) != d_alloc_proofs.end());
[ - - ]
401 : 1 : d_alloc_proofs.erase(proof->d_proof);
402 : : }
403 : 2 : }
404 : :
405 : 1 : cvc5_proof_t* Cvc5::copy(cvc5_proof_t* proof)
406 : : {
407 : 1 : proof->d_refs += 1;
408 : 1 : return proof;
409 : : }
410 : :
411 : 1067 : Cvc5Grammar Cvc5::export_grammar(const cvc5::Grammar& grammar)
412 : : {
413 : 1067 : auto [it, inserted] = d_alloc_grammars.try_emplace(grammar, this, grammar);
414 [ - + ]: 1067 : if (!inserted)
415 : : {
416 : 0 : copy(&it->second);
417 : : }
418 : 1067 : return &it->second;
419 : : }
420 : :
421 : 2 : void Cvc5::release(cvc5_grammar_t* grammar)
422 : : {
423 : 2 : grammar->d_refs -= 1;
424 [ + + ]: 2 : if (grammar->d_refs == 0)
425 : : {
426 [ - + ][ - + ]: 1 : Assert(d_alloc_grammars.find(grammar->d_grammar) != d_alloc_grammars.end());
[ - - ]
427 : 1 : d_alloc_grammars.erase(grammar->d_grammar);
428 : : }
429 : 2 : }
430 : :
431 : 1 : cvc5_grammar_t* Cvc5::copy(cvc5_grammar_t* grammar)
432 : : {
433 : 1 : grammar->d_refs += 1;
434 : 1 : return grammar;
435 : : }
436 : :
437 : 72 : std::vector<cvc5::Term> Cvc5::PluginCpp::check()
438 : : {
439 [ - + ][ - + ]: 72 : Assert(d_plugin);
[ - - ]
440 : 72 : std::vector<cvc5::Term> res;
441 [ + + ]: 72 : if (d_plugin->check)
442 : : {
443 : : size_t size;
444 : 12 : const Cvc5Term* terms = d_plugin->check(&size, d_plugin->d_check_state);
445 [ + + ]: 24 : for (size_t i = 0; i < size; ++i)
446 : : {
447 : 12 : res.push_back(terms[i]->d_term);
448 : : }
449 : : }
450 : 72 : return res;
451 : 0 : }
452 : :
453 : 36 : void Cvc5::PluginCpp::notifySatClause(const cvc5::Term& clause)
454 : : {
455 [ - + ][ - + ]: 36 : Assert(d_plugin);
[ - - ]
456 [ + - ]: 36 : if (d_plugin->notify_sat_clause)
457 : : {
458 : 36 : d_plugin->notify_sat_clause(d_cvc5->d_tm->export_term(clause),
459 : 36 : d_plugin->d_notify_sat_clause_state);
460 : : }
461 : 36 : }
462 : :
463 : 48 : void Cvc5::PluginCpp::notifyTheoryLemma(const cvc5::Term& lemma)
464 : : {
465 [ - + ][ - + ]: 48 : Assert(d_plugin);
[ - - ]
466 [ + - ]: 48 : if (d_plugin->notify_theory_lemma)
467 : : {
468 : 48 : d_plugin->notify_theory_lemma(d_cvc5->d_tm->export_term(lemma),
469 : 48 : d_plugin->d_notify_theory_lemma_state);
470 : : }
471 : 48 : }
472 : :
473 : 24 : std::string Cvc5::PluginCpp::getName()
474 : : {
475 [ - + ][ - + ]: 24 : Assert(d_plugin);
[ - - ]
476 [ - + ][ - + ]: 24 : Assert(d_plugin->get_name);
[ - - ]
477 : 24 : return d_plugin->get_name();
478 : : }
|
