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.

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 will only be released when these instances are deleted via cvc5_delete() and 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);
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. 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));
// we can release 'a' here, not needed anymore
cvc5_term_release(a);
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);
cvc5_term_manager_delete(tm);