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:

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);

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);

Types

The following types are defined via typedefs but used as black boxes, their internals are hidden.

typedef struct Cvc5
typedef struct Cvc5Command
typedef struct Cvc5Datatype
typedef struct Cvc5DatatypeDecl
typedef struct Cvc5DatatypeConstructor
typedef struct Cvc5DatatypeConstructorDecl
typedef struct Cvc5DatatypeSelector
typedef struct Cvc5Grammar
typedef struct Cvc5InputParser
typedef struct Cvc5Op
typedef struct Cvc5Proof
typedef struct Cvc5Result
typedef struct Cvc5Sort
typedef struct Cvc5Stat
typedef struct Cvc5Statistics
typedef struct Cvc5SymbolManager
typedef struct Cvc5SynthResult
typedef struct Cvc5Term
typedef struct Cvc5TermManager

Structs

The following structs are fully exposed via the API.

struct Cvc5OptionInfo
struct Cvc5Plugin

Enums

enum Cvc5Kind
enum Cvc5SortKind
enum Cvc5OptionInfoKind
enum Cvc5RoundingMode
enum Cvc5UnknownExplanation
enums for configuration modes
- enum Cvc5BlockModelsMode
- enum Cvc5LearnedLitType
- enum Cvc5FindSynthTarget
- enum Cvc5OptionCategory
- enum Cvc5ProofComponent
- enum Cvc5ProofFormat
enums classes for proof rules
- enum Cvc5ProofRule
- enum Cvc5ProofRewriteRule