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 : : #ifndef CVC5__C_API__CVC5_C_TYPES_H
14 : : #define CVC5__C_API__CVC5_C_TYPES_H
15 : :
16 : : extern "C" {
17 : : #include <cvc5/c/cvc5.h>
18 : : }
19 : : #include <cvc5/cvc5.h>
20 : :
21 : : #include <fstream>
22 : :
23 : : /* -------------------------------------------------------------------------- */
24 : : /* Wrapper structs (associated with Cvc5TermManager) */
25 : : /* -------------------------------------------------------------------------- */
26 : :
27 : : /** Wrapper for cvc5 C++ terms. */
28 : : struct cvc5_term_t
29 : : {
30 : : /**
31 : : * Constructor.
32 : : * @param term The wrapped C++ term.
33 : : * @param tm The associated term manager.
34 : : */
35 : 123386 : cvc5_term_t(Cvc5TermManager* tm, const cvc5::Term& term)
36 : 123386 : : d_term(term), d_tm(tm)
37 : : {
38 : 123386 : }
39 : : /** The wrapped C++ term. */
40 : : cvc5::Term d_term;
41 : : /** External refs count. */
42 : : uint32_t d_refs = 1;
43 : : /** The associated term manager. */
44 : : Cvc5TermManager* d_tm = nullptr;
45 : : };
46 : :
47 : : /** Wrapper for cvc5 C++ operators. */
48 : : struct cvc5_op_t
49 : : {
50 : : /**
51 : : * Constructor.
52 : : * @param op The wrapped C++ operator.
53 : : * @param tm The associated term manager.
54 : : */
55 : 3095 : cvc5_op_t(Cvc5TermManager* tm, const cvc5::Op& op) : d_op(op), d_tm(tm) {}
56 : : /** The wrapped C++ op. */
57 : : cvc5::Op d_op;
58 : : /** External refs count. */
59 : : uint32_t d_refs = 1;
60 : : /** The associated term manager. */
61 : : Cvc5TermManager* d_tm = nullptr;
62 : : };
63 : :
64 : : /** Wrapper for cvc5 C++ sorts. */
65 : : struct cvc5_sort_t
66 : : {
67 : : /**
68 : : * Constructor.
69 : : * @param sort The wrapped C++ sort.
70 : : * @param tm The associated term manager.
71 : : */
72 : 212905 : cvc5_sort_t(Cvc5TermManager* tm, const cvc5::Sort& sort)
73 : 212905 : : d_sort(sort), d_tm(tm)
74 : : {
75 : 212905 : }
76 : : /** The wrapped C++ sort. */
77 : : cvc5::Sort d_sort;
78 : : /** External refs count. */
79 : : uint32_t d_refs = 1;
80 : : /** The associated term manager. */
81 : : Cvc5TermManager* d_tm = nullptr;
82 : : };
83 : :
84 : : /** Wrapper for cvc5 C++ datatypes. */
85 : : struct cvc5_dt_t
86 : : {
87 : : /**
88 : : * Constructor.
89 : : * @param tm The associated term manager.
90 : : * @param dt The wrapped C++ datatype.
91 : : */
92 : 2553 : cvc5_dt_t(Cvc5TermManager* tm, const cvc5::Datatype& dt) : d_dt(dt), d_tm(tm)
93 : : {
94 : 2553 : }
95 : : /** The wrapped C++ datatype. */
96 : : cvc5::Datatype d_dt;
97 : : /** External refs count. */
98 : : uint32_t d_refs = 1;
99 : : /** The associated term manager. */
100 : : Cvc5TermManager* d_tm = nullptr;
101 : : };
102 : :
103 : : /** Wrapper for cvc5 C++ datatype constructors. */
104 : : struct cvc5_dt_cons_t
105 : : {
106 : : /**
107 : : * Constructor.
108 : : * @param tm The associated term manager.
109 : : * @param dt The wrapped C++ datatype constructor.
110 : : */
111 : 2487 : cvc5_dt_cons_t(Cvc5TermManager* tm, const cvc5::DatatypeConstructor& cons)
112 : 2487 : : d_dt_cons(cons), d_tm(tm)
113 : : {
114 : 2487 : }
115 : : /** The wrapped C++ datatype constructor. */
116 : : cvc5::DatatypeConstructor d_dt_cons;
117 : : /** External refs count. */
118 : : uint32_t d_refs = 1;
119 : : /** The associated term manager. */
120 : : Cvc5TermManager* d_tm = nullptr;
121 : : };
122 : :
123 : : /** Wrapper for cvc5 C++ datatype selectors. */
124 : : struct cvc5_dt_sel_t
125 : : {
126 : : /**
127 : : * Constructor.
128 : : * @param tm The associated term manager.
129 : : * @param dt The wrapped C++ datatype selector.
130 : : */
131 : 1530 : cvc5_dt_sel_t(Cvc5TermManager* tm, const cvc5::DatatypeSelector& sel)
132 : 1530 : : d_dt_sel(sel), d_tm(tm)
133 : : {
134 : 1530 : }
135 : : /** The wrapped C++ datatype selector. */
136 : : cvc5::DatatypeSelector d_dt_sel;
137 : : /** External refs count. */
138 : : uint32_t d_refs = 1;
139 : : /** The associated term manager. */
140 : : Cvc5TermManager* d_tm = nullptr;
141 : : };
142 : :
143 : : /** Wrapper for cvc5 C++ datatype declarations. */
144 : : struct cvc5_dt_decl_t
145 : : {
146 : : /**
147 : : * Constructor.
148 : : * @param decl The wrapped C++ datatype declaration.
149 : : * @param tm The associated term manager.
150 : : */
151 : 5144 : cvc5_dt_decl_t(Cvc5TermManager* tm, const cvc5::DatatypeDecl& decl)
152 : 5144 : : d_decl(decl), d_tm(tm)
153 : : {
154 : 5144 : }
155 : : /** The wrapped C++ datatype declaration. */
156 : : cvc5::DatatypeDecl d_decl;
157 : : /** External refs count. */
158 : : uint32_t d_refs = 1;
159 : : /** The associated term manager. */
160 : : Cvc5TermManager* d_tm = nullptr;
161 : : };
162 : :
163 : : /** Wrapper for cvc5 C++ datatype constructor declarations. */
164 : : struct cvc5_dt_cons_decl_t
165 : : {
166 : : /**
167 : : * Constructor.
168 : : * @param decl The wrapped C++ datatype constructor declaration.
169 : : * @param tm The associated term manager.
170 : : */
171 : 13818 : cvc5_dt_cons_decl_t(Cvc5TermManager* tm,
172 : : const cvc5::DatatypeConstructorDecl& decl)
173 : 13818 : : d_decl(decl), d_tm(tm)
174 : : {
175 : 13818 : }
176 : : /** The wrapped C++ datatype constructor declaration. */
177 : : cvc5::DatatypeConstructorDecl d_decl;
178 : : /** External refs count. */
179 : : uint32_t d_refs = 1;
180 : : /** The associated term manager. */
181 : : Cvc5TermManager* d_tm = nullptr;
182 : : };
183 : :
184 : : /**
185 : : * Wrapper for cvc5 C++ term manager.
186 : : * @note Visibility of this struct is set to export for linkage of parser
187 : : * library (it needs to be able to use member functions of the struct).
188 : : */
189 : : struct CVC5_EXPORT Cvc5TermManager
190 : : {
191 : : /**
192 : : * Export C++ sort to C API.
193 : : * @param sort The sort to export.
194 : : */
195 : : Cvc5Sort export_sort(const cvc5::Sort& sort);
196 : : /**
197 : : * Export C++ term to C API.
198 : : * @param term The term to export.
199 : : */
200 : : Cvc5Term export_term(const cvc5::Term& term);
201 : : /**
202 : : * Export C++ operator to C API.
203 : : * @param op The operator to export.
204 : : */
205 : : Cvc5Op export_op(const cvc5::Op& op);
206 : : /**
207 : : * Export C++ datatype to C API.
208 : : * @param dt The datatype to export.
209 : : */
210 : : Cvc5Datatype export_dt(const cvc5::Datatype& dt);
211 : : /**
212 : : * Export C++ datatype constructor to C API.
213 : : * @param cons The datatype constructor to export.
214 : : */
215 : : Cvc5DatatypeConstructor export_dt_cons(const cvc5::DatatypeConstructor& cons);
216 : : /**
217 : : * Export C++ datatype selector to C API.
218 : : * @param sel The datatype selector to export.
219 : : */
220 : : Cvc5DatatypeSelector export_dt_sel(const cvc5::DatatypeSelector& sel);
221 : : /**
222 : : * Export C++ datatype declaration to C API.
223 : : * @param decl The datatype declaration to export.
224 : : */
225 : : Cvc5DatatypeDecl export_dt_decl(const cvc5::DatatypeDecl& decl);
226 : : /**
227 : : * Export C++ datatype constructor declaration to C API.
228 : : * @param decl The datatype constructor declaration to export.
229 : : */
230 : : Cvc5DatatypeConstructorDecl export_dt_cons_decl(
231 : : const cvc5::DatatypeConstructorDecl& decl);
232 : :
233 : : /**
234 : : * Export C++ statistic to C API.
235 : : * @param statistic The statistic to export.
236 : : */
237 : : Cvc5Stat export_stat(const cvc5::Stat& stat);
238 : :
239 : : /**
240 : : * Export C++ statistics to C API.
241 : : * @param statistics The statistics to export.
242 : : */
243 : : Cvc5Statistics export_stats(const cvc5::Statistics& stat);
244 : :
245 : : /* Manual memory management for sorts and terms. ------ */
246 : :
247 : : /**
248 : : * Decrement the external ref count of a term. If the ref count reaches zero,
249 : : * the term is released (freed).
250 : : * @param term The term to release.
251 : : */
252 : : void release(cvc5_term_t* term);
253 : : /**
254 : : * Increment the external ref count of a term.
255 : : * @param term The term to copy.
256 : : * @return The copied term.
257 : : */
258 : : cvc5_term_t* copy(cvc5_term_t* term);
259 : : /**
260 : : * Decrement the external ref count of an operator. If the ref count reaches
261 : : * zero, the operator is released (freed).
262 : : * @param op The operator to release.
263 : : */
264 : : void release(cvc5_op_t* op);
265 : : /**
266 : : * Increment the external ref count of an operator.
267 : : * @param op The operator to copy.
268 : : * @return The copied operator.
269 : : */
270 : : cvc5_op_t* copy(cvc5_op_t* term);
271 : : /**
272 : : * Decrement the external ref count of a sort. If the ref count reaches zero,
273 : : * the sort is released (freed).
274 : : * @param sort The sort to release.
275 : : */
276 : : void release(cvc5_sort_t* sort);
277 : : /**
278 : : * Increment the external ref count of a sort.
279 : : * @param sort The sort to copy.
280 : : * @return The copied sort.
281 : : */
282 : : cvc5_sort_t* copy(cvc5_sort_t* sort);
283 : : /**
284 : : * Decrement the external ref count of a datatype. If the ref count reaches
285 : : * zero, the datatype is released (freed).
286 : : * @param dt The datatype to release.
287 : : */
288 : : void release(cvc5_dt_t* dt);
289 : : /**
290 : : * Increment the external ref count of a datatype.
291 : : * @param dt The datatype to copy.
292 : : * @return The copied datatype.
293 : : */
294 : : cvc5_dt_t* copy(cvc5_dt_t* dt);
295 : : /**
296 : : * Decrement the external ref count of a datatype constructor. If the ref
297 : : * count reaches zero, the datatype constructor is released (freed).
298 : : * @param cons The datatype constructor to release.
299 : : */
300 : : void release(cvc5_dt_cons_t* cons);
301 : : /**
302 : : * Increment the external ref count of a datatype constructor.
303 : : * @param cons The datatype constructor to copy.
304 : : * @return The copied datatype constructor.
305 : : */
306 : : cvc5_dt_cons_t* copy(cvc5_dt_cons_t* cons);
307 : : /**
308 : : * Decrement the external ref count of a datatype selector. If the ref
309 : : * count reaches zero, the datatype selector is released (freed).
310 : : * @param cons The datatype selector to release.
311 : : */
312 : : void release(cvc5_dt_sel_t* sel);
313 : : /**
314 : : * Increment the external ref count of a datatype selector.
315 : : * @param cons The datatype selector to copy.
316 : : * @return The copied datatype selector.
317 : : */
318 : : cvc5_dt_sel_t* copy(cvc5_dt_sel_t* sel);
319 : : /**
320 : : * Decrement the external ref count of a datatype declaration. If the ref
321 : : * count reaches zero, the datatype declaration is released (freed).
322 : : * @param decl The datatype declaration to release.
323 : : */
324 : : void release(cvc5_dt_decl_t* decl);
325 : : /**
326 : : * Increment the external ref count of a datatype declaration.
327 : : * @param decl The datatype declaration to copy.
328 : : * @return The copied datatype declaration.
329 : : */
330 : : cvc5_dt_decl_t* copy(cvc5_dt_decl_t* decl);
331 : : /**
332 : : * Decrement the external ref count of a datatype constructor declaration. If
333 : : * the ref count reaches zero, the datatype constructor declaration is
334 : : * release (freed).
335 : : * @param decl The datatype constructor declaration to release.
336 : : */
337 : : void release(cvc5_dt_cons_decl_t* decl);
338 : : /**
339 : : * Increment the external ref count of a datatype constructor declaration.
340 : : * @param decl The datatype constructor declaration to copy.
341 : : * @return The copied datatype constructor declaration.
342 : : */
343 : : cvc5_dt_cons_decl_t* copy(cvc5_dt_cons_decl_t* decl);
344 : :
345 : : /** Release all managed objects. */
346 : : void release();
347 : :
348 : : /* ---------------------------------------------------- */
349 : :
350 : : /** The associated term manager instance. */
351 : : cvc5::TermManager d_tm;
352 : :
353 : : private:
354 : : /** Cache of allocated sorts. */
355 : : std::unordered_map<cvc5::Sort, cvc5_sort_t> d_alloc_sorts;
356 : : /** Cache of allocated terms. */
357 : : std::unordered_map<cvc5::Term, cvc5_term_t> d_alloc_terms;
358 : : /** Cache of allocated operators. */
359 : : std::unordered_map<cvc5::Op, cvc5_op_t> d_alloc_ops;
360 : : /** Cache of allocated datatypes. */
361 : : std::unordered_map<cvc5::Datatype, cvc5_dt_t> d_alloc_dts;
362 : : /** Cache of allocated datatype constructors. */
363 : : std::unordered_map<cvc5::DatatypeConstructor, cvc5_dt_cons_t>
364 : : d_alloc_dt_conss;
365 : : /** Cache of allocated datatype selectors. */
366 : : std::unordered_map<cvc5::DatatypeSelector, cvc5_dt_sel_t> d_alloc_dt_sels;
367 : : /** Cache of allocated datatype declarations. */
368 : : std::unordered_map<cvc5::DatatypeDecl, cvc5_dt_decl_t> d_alloc_dt_decls;
369 : : /** Cache of allocated datatype constructor declarations. */
370 : : std::unordered_map<cvc5::DatatypeConstructorDecl, cvc5_dt_cons_decl_t>
371 : : d_alloc_dt_cons_decls;
372 : : /** Cache of allocated statistic objects. */
373 : : std::vector<cvc5_stat_t> d_alloc_stats;
374 : : /** Cache of allocated statistics objects. */
375 : : std::vector<cvc5_stats_t> d_alloc_statistics;
376 : : };
377 : :
378 : : /* -------------------------------------------------------------------------- */
379 : : /* Wrapper structs (associated with Cvc5) */
380 : : /* -------------------------------------------------------------------------- */
381 : :
382 : : /** Wrapper for cvc5 C++ results. */
383 : : struct cvc5_result_t
384 : : {
385 : : /**
386 : : * Constructor.
387 : : * @param cvc5 The associated solver instance.
388 : : * @param result The wrapped C++ result.
389 : : */
390 : 12731 : cvc5_result_t(Cvc5* cvc5, const cvc5::Result& result)
391 : 12731 : : d_result(result), d_cvc5(cvc5)
392 : : {
393 : 12731 : }
394 : : /** The wrapped C++ result. */
395 : : cvc5::Result d_result;
396 : : /** External refs count. */
397 : : uint32_t d_refs = 1;
398 : : /** The associated solver instance. */
399 : : Cvc5* d_cvc5 = nullptr;
400 : : };
401 : :
402 : : /** Wrapper for cvc5 C++ synthesis results. */
403 : : struct cvc5_synth_result_t
404 : : {
405 : : /**
406 : : * Constructor.
407 : : * @param cvc5 The associated solver instance.
408 : : * @param result The wrapped C++ synthesis result.
409 : : */
410 : 168 : cvc5_synth_result_t(Cvc5* cvc5, const cvc5::SynthResult& result)
411 : 168 : : d_result(result), d_cvc5(cvc5)
412 : : {
413 : 168 : }
414 : : /** The wrapped C++ result. */
415 : : cvc5::SynthResult d_result;
416 : : /** External refs count. */
417 : : uint32_t d_refs = 1;
418 : : /** The associated solver instance. */
419 : : Cvc5* d_cvc5 = nullptr;
420 : : };
421 : :
422 : : /** Wrapper for cvc5 C++ proofs. */
423 : : struct cvc5_proof_t
424 : : {
425 : : /**
426 : : * Constructor.
427 : : * @param cvc5 The associated solver instance.
428 : : * @param proof The wrapped C++ proof.
429 : : */
430 : 1480 : cvc5_proof_t(Cvc5* cvc5, const cvc5::Proof& proof)
431 : 1480 : : d_proof(proof), d_cvc5(cvc5)
432 : : {
433 : 1480 : }
434 : : /** The wrapped C++ proof. */
435 : : cvc5::Proof d_proof;
436 : : /** External refs count. */
437 : : uint32_t d_refs = 1;
438 : : /** The associated solver instance. */
439 : : Cvc5* d_cvc5 = nullptr;
440 : : };
441 : :
442 : : /** Wrapper for cvc5 C++ grammars. */
443 : : struct cvc5_grammar_t
444 : : {
445 : : /**
446 : : * Constructor.
447 : : * @param cvc5 The associated solver instance.
448 : : * @param grammar The wrapped C++ grammar.
449 : : */
450 : 1067 : cvc5_grammar_t(Cvc5* cvc5, const cvc5::Grammar& grammar)
451 : 1067 : : d_grammar(grammar), d_cvc5(cvc5)
452 : : {
453 : 1067 : }
454 : : /** The wrapped C++ grammar. */
455 : : cvc5::Grammar d_grammar;
456 : : /** External refs count. */
457 : : uint32_t d_refs = 1;
458 : : /** The associated solver instance. */
459 : : Cvc5* d_cvc5 = nullptr;
460 : : };
461 : :
462 : : /** Wrapper for cvc5 C++ solver instance. */
463 : : struct Cvc5
464 : : {
465 : : /**
466 : : * Constructor.
467 : : * @param tm The associated term manager instance.
468 : : */
469 : 30944 : Cvc5(Cvc5TermManager* tm) : d_solver(tm->d_tm), d_tm(tm) {}
470 : :
471 : : /** Destructor. */
472 : : ~Cvc5();
473 : :
474 : : /**
475 : : * Export C++ result to C API.
476 : : * @param result The result to export.
477 : : */
478 : : Cvc5Result export_result(const cvc5::Result& result);
479 : : /**
480 : : * Decrement the external ref count of a result. If the ref count reaches
481 : : * zero, the result is released (freed).
482 : : * @param result The result to release.
483 : : */
484 : : void release(cvc5_result_t* result);
485 : : /**
486 : : * Increment the external ref count of a result.
487 : : * @param result The result to copy.
488 : : * @return The copied result.
489 : : */
490 : : cvc5_result_t* copy(cvc5_result_t* result);
491 : :
492 : : /**
493 : : * Export C++ synthesis result to C API.
494 : : * @param result Thesynthesis result to export.
495 : : */
496 : : Cvc5SynthResult export_synth_result(const cvc5::SynthResult& result);
497 : : /**
498 : : * Decrement the external ref count of a synthesis result. If the ref count
499 : : * reaches zero, the result is released (freed).
500 : : * @param result The result to release.
501 : : */
502 : : void release(cvc5_synth_result_t* result);
503 : : /**
504 : : * Increment the external ref count of a synthesis result.
505 : : * @param result The synthesis result to copy.
506 : : * @return The copied synthesis result.
507 : : */
508 : : cvc5_synth_result_t* copy(cvc5_synth_result_t* result);
509 : :
510 : : /**
511 : : * Export C++ proof to C API.
512 : : * @param proof The proof to export.
513 : : */
514 : : Cvc5Proof export_proof(const cvc5::Proof& proof);
515 : : /**
516 : : * Decrement the external ref count of a proof. If the ref count reaches
517 : : * zero, the proof is released (freed).
518 : : * @param proof The proof to release.
519 : : */
520 : : void release(cvc5_proof_t* proof);
521 : : /**
522 : : * Increment the external ref count of a proof.
523 : : * @param proof The proof to copy.
524 : : * @return The copied proof.
525 : : */
526 : : cvc5_proof_t* copy(cvc5_proof_t* proof);
527 : :
528 : : /**
529 : : * Export C++ grammar to C API.
530 : : * @param grammar The grammar to export.
531 : : */
532 : : Cvc5Grammar export_grammar(const cvc5::Grammar& grammar);
533 : : /**
534 : : * Decrement the external ref count of a grammar. If the ref count reaches
535 : : * zero, the grammar is released (freed).
536 : : * @param grammar The grammar to release.
537 : : */
538 : : void release(cvc5_grammar_t* grammar);
539 : : /**
540 : : * Increment the external ref count of a grammar.
541 : : * @param grammar The grammar to copy.
542 : : * @return The copied grammar.
543 : : */
544 : : cvc5_grammar_t* copy(cvc5_grammar_t* grammar);
545 : :
546 : : /** The associated cvc5 instance. */
547 : : cvc5::Solver d_solver;
548 : : /** The associated term manager. */
549 : : Cvc5TermManager* d_tm = nullptr;
550 : :
551 : : /** Cache of allocated results. */
552 : : std::unordered_map<cvc5::Result, cvc5_result_t> d_alloc_results;
553 : : /** Cache of allocated syntheis results. */
554 : : std::unordered_map<cvc5::SynthResult, cvc5_synth_result_t>
555 : : d_alloc_synth_results;
556 : : /** Cache of allocated proofs. */
557 : : std::unordered_map<cvc5::Proof, cvc5_proof_t> d_alloc_proofs;
558 : : /** Cache of allocated grammars. */
559 : : std::unordered_map<cvc5::Grammar, cvc5_grammar_t> d_alloc_grammars;
560 : : /** Out file stream for output tag (configured via `cvc5_get_output()`. */
561 : : std::ofstream d_output_tag_file_stream;
562 : : /**
563 : : * Out file stream for output tag returned by `Solver::getOutput()`. Cached
564 : : * to reset on `cvc5_output_close()` or on destruction of `Cvc5` to
565 : : * `d_output_tag_streambuf`.
566 : : */
567 : : std::ostream* d_output_tag_stream = nullptr;
568 : : /**
569 : : * Cache output stream buffer of the stream returned by `Solver::getOutput()`
570 : : * before it was redirected to the file configured via `cvc5_get_output()`.
571 : : * Cached to reset on `cvc5_output_close()` or on destruction of `Cvc5`.
572 : : */
573 : : std::streambuf* d_output_tag_streambuf = nullptr;
574 : :
575 : : /** The configured plugin. */
576 : : class PluginCpp : public cvc5::Plugin
577 : : {
578 : : public:
579 : 24 : PluginCpp(cvc5::TermManager& tm, Cvc5* cvc5, Cvc5Plugin* plugin)
580 : 24 : : Plugin(tm), d_cvc5(cvc5), d_plugin(plugin)
581 : : {
582 : 24 : }
583 : : std::vector<cvc5::Term> check() override;
584 : : void notifySatClause(const cvc5::Term& clause) override;
585 : : void notifyTheoryLemma(const cvc5::Term& lemma) override;
586 : : std::string getName() override;
587 : :
588 : : private:
589 : : Cvc5* d_cvc5;
590 : : Cvc5Plugin* d_plugin;
591 : : };
592 : : std::unique_ptr<PluginCpp> d_plugin = nullptr;
593 : : };
594 : :
595 : : /** Wrapper for cvc5 C++ statistic. */
596 : : struct cvc5_stat_t
597 : : {
598 : : /**
599 : : * Constructor.
600 : : * @param tm The associated term manager instance.
601 : : * @param result The wrapped C++ statistic.
602 : : */
603 : 6519 : cvc5_stat_t(Cvc5TermManager* tm, const cvc5::Stat& stat)
604 : 6519 : : d_stat(stat), d_tm(tm)
605 : : {
606 : 6519 : }
607 : : /**
608 : : * Constructor.
609 : : * @param cvc5 The associated solver instance.
610 : : * @param result The wrapped C++ statistic.
611 : : */
612 : : cvc5_stat_t(Cvc5* cvc5, const cvc5::Stat& stat)
613 : : : d_stat(stat), d_tm(cvc5->d_tm)
614 : : {
615 : : }
616 : : /** The wrapped C++ statistic. */
617 : : cvc5::Stat d_stat;
618 : : /** External refs count. */
619 : : uint32_t d_refs = 1;
620 : : /** The associated term manager instance. */
621 : : Cvc5TermManager* d_tm = nullptr;
622 : : };
623 : :
624 : : /** Wrapper for cvc5 C++ statistics. */
625 : : struct cvc5_stats_t
626 : : {
627 : : /**
628 : : * Constructor.
629 : : * @param tm The associated term manager instance.
630 : : * @param result The wrapped C++ statistics.
631 : : */
632 : 285 : cvc5_stats_t(Cvc5TermManager* tm, const cvc5::Statistics& stat)
633 : 285 : : d_stat(stat), d_tm(tm)
634 : : {
635 : 285 : }
636 : : /**
637 : : * Constructor.
638 : : * @param cvc5 The associated solver instance.
639 : : * @param result The wrapped C++ statistics.
640 : : */
641 : : cvc5_stats_t(Cvc5* cvc5, const cvc5::Statistics& stat)
642 : : : d_stat(stat), d_tm(cvc5->d_tm)
643 : : {
644 : : }
645 : : /** The wrapped C++ statistics. */
646 : : cvc5::Statistics d_stat;
647 : : /** External refs count. */
648 : : uint32_t d_refs = 1;
649 : : /** The associated term manager instance. */
650 : : Cvc5TermManager* d_tm = nullptr;
651 : : /** The associated iterator. */
652 : : std::unique_ptr<cvc5::Statistics::iterator> d_iter = nullptr;
653 : : };
654 : :
655 : : /* -------------------------------------------------------------------------- */
656 : : #endif
|
