C API 

The C API of cvc5 is based on its C++ API and is feature complete , within the limits of the C language. The quickstart guide gives a short introduction of how to use cvc5 via its C API. For most applications, the Cvc5 solver struct is the main entry point to cvc5.

One of the key differences is the way how memory is managed . While users of the C++ API can rely on memory being efficiently managed automatically, on the C level, management to maintain a low overhead needs more manual intervention .

All objects created via a term manager ( Cvc5TermManager ) or a solver ( Cvc5 ) instance, e.g., sorts, terms, datatypes and statistics, are managed by the term manager . As in the C++ API, these objects keep the term manager alive: they remain valid after the term manager and solver instances that created them have been deleted via cvc5_term_manager_delete() and cvc5_delete() , until they are released, either individually via the corresponding cvc5_*_release() function or all at once via cvc5_term_manager_release() . Consequently, deleting a term manager does not free objects that are still referenced, and does not free the term manager itself while any of them are alive: its memory is freed once it has been deleted and all of its managed objects have been released. Calling cvc5_term_manager_release() before cvc5_term_manager_delete() thus frees everything right away.

Results ( Cvc5Result ), synthesis results ( Cvc5SynthResult ), proofs ( Cvc5Proof ) and grammars ( Cvc5Grammar ) are instead managed by the solver that created them: deleting the solver drops one reference to each of them. To use such an object afterwards, keep a reference to it via the corresponding cvc5_*_copy() function; it then outlives the solver, as in the C++ API, and is freed by its final cvc5_*_release() . Proofs additionally keep the term manager alive, since querying them creates new terms and proofs.

Command objects ( Cvc5Command ) are managed by the input parser ( Cvc5InputParser ) that created them in the same way: they keep the parser alive and remain valid after cvc5_parser_delete() , until they are released via cvc5_cmd_release() or, all at once, via cvc5_parser_release() .

The C API offers two modes of memory management:

1. Let cvc5 handle memory management without manual intervention. All memory allocated by the C API via a term manager ( Cvc5TermManager ) or solver ( Cvc5 ) instance is released all at once via cvc5_term_manager_release() before the term manager is deleted via cvc5_term_manager_delete() . For example:

Cvc5TermManager* tm = cvc5_term_manager_new();
Cvc5* cvc5 = cvc5_new(tm);
Cvc5Term a = cvc5_mk_const(tm, cvc5_get_integer_sort(tm), "a");
Cvc5Term two = cvc5_mk_integer_int64(tm, 2);
Cvc5Term args1[2] = {a, two};
cvc5_assert_formula(cvc5, cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args1));
Cvc5Term b = cvc5_mk_const(tm, cvc5_get_integer_sort(tm), "b");
Cvc5Term args2[2] = {b, two};
cvc5_assert_formula(cvc5, cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2));
cvc5_check_sat(cvc5);
cvc5_delete(cvc5);
// release all objects managed by the term manager
cvc5_term_manager_release(tm);
cvc5_term_manager_delete(tm);

2. Introduce a more fine-grained, user-level memory management for objects created via a term manager or solver via the corresponding cvc5_*_copy() and cvc5_*_release() functions. The copy functions increment the reference counter of an object, the release functions decrement the reference counter and free its allocated memory when the counter reaches 0. Objects that have not been released when the term manager is deleted keep the term manager alive and remain valid until they are released. For example:

Cvc5TermManager* tm = cvc5_term_manager_new();
Cvc5* cvc5 = cvc5_new(tm);
Cvc5Sort int_sort = cvc5_get_integer_sort(tm);
Cvc5Term a = cvc5_mk_const(tm, int_sort, "a");
Cvc5Term two = cvc5_mk_integer_int64(tm, 2);
Cvc5Term args1[2] = {a, two};
Cvc5Term eq = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args1);
cvc5_assert_formula(cvc5, eq);
// we can release 'a' and 'eq' here, not needed anymore
cvc5_term_release(a);
cvc5_term_release(eq);
Cvc5Term b = cvc5_mk_const(tm, int_sort, "b");
Cvc5Term args2[2] = {b, two};
Cvc5Term distinct = cvc5_mk_term(tm, CVC5_KIND_DISTINCT, 2, args2);
cvc5_assert_formula(cvc5, distinct);
Cvc5Result res = cvc5_check_sat(cvc5);
cvc5_delete(cvc5);
cvc5_term_manager_delete(tm);
// the remaining objects are still valid here, they keep the term manager
// alive until the last one of them is released
printf("%s\n", cvc5_result_to_string(res));
cvc5_result_release(res);
cvc5_term_release(distinct);
cvc5_term_release(b);
cvc5_term_release(two);
cvc5_sort_release(int_sort);