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