Cvc5

This struct represents a cvc5 solver instance.

Terms, sorts and operators are not tied to a Cvc5 instance but associated with a Cvc5TermManager instance, which can be shared between solver instances.

Solver options are configured via cvc5_set_option() and queried via cvc5_get_option() (for more information on configuration options, see Options). Information about a specific option can be retrieved via cvc5_get_option_info() (see Cvc5OptionInfo).

typedef struct Cvc5 Cvc5: A cvc5 solver.

Cvc5 *cvc5_new(Cvc5TermManager *tm)

Construct a new instance of a cvc5 solver.

Parameters:: tm – The associated term manager instance.
Returns:: The cvc5 solver instance.

void cvc5_delete(Cvc5 *cvc5)

Delete a cvc5 solver instance.

Parameters:: cvc5 – The solver instance.

Cvc5TermManager *cvc5_get_tm(Cvc5 *cvc5)

Get the associated term manager of a cvc5 solver instance.

Parameters:: cvc5 – The solver instance.
Returns:: The term manager.

Cvc5Sort cvc5_declare_dt(Cvc5 *cvc5, const char *symbol, size_t size, const Cvc5DatatypeConstructorDecl ctors[])

Create datatype sort.

SMT-LIB:

(declare-datatype <symbol> <datatype_decl>)

Parameters:

cvc5 – The solver instance.
symbol – The name of the datatype sort.
size – The number of constructor declarations of the datatype sort.
ctors – The constructor declarations.

Returns:

The datatype sort.

Cvc5Term cvc5_declare_fun(Cvc5 *cvc5, const char *symbol, size_t size, const Cvc5Sort sorts[], Cvc5Sort sort, bool fresh)

Declare n-ary function symbol.

SMT-LIB:

(declare-fun <symbol> ( <sort>* ) <sort>)

Parameters:

cvc5 – The solver instance.
symbol – The name of the function.
size – The number of domain sorts of the function.
sorts – The domain sorts of the function.
sort – The codomain sort of the function.
fresh – If true, then this method always returns a new Term. Otherwise, this method will always return the same Term for each call with the given sorts and symbol where fresh is false.

Returns:

The function.

Cvc5Sort cvc5_declare_sort(Cvc5 *cvc5, const char *symbol, uint32_t arity, bool fresh)

Declare uninterpreted sort.

SMT-LIB:

(declare-sort <symbol> <numeral>)

Note

This corresponds to cvc5_mk_uninterpreted_sort() if arity = 0, and to cvc5_mk_uninterpreted_sort_constructor_sort() if arity > 0.

Parameters:

cvc5 – The solver instance.
symbol – The name of the sort.
arity – The arity of the sort.
fresh – If true, then this method always returns a new Sort.

Returns:

The sort.

Cvc5Term cvc5_define_fun(Cvc5 *cvc5, const char *symbol, size_t size, const Cvc5Term vars[], const Cvc5Sort sort, const Cvc5Term term, bool global)

Define n-ary function.

SMT-LIB:

(define-fun <function_def>)

Parameters:

cvc5 – The cvc5 solver instance.
symbol – The name of the function.
size – The number of parameters of the function.
vars – The parameters.
sort – The sort of the return value of this function.
term – The function body.
global – Determines whether this definition is global (i.e., persists when popping the context).

Returns:

The function.

Cvc5Term cvc5_define_fun_rec(Cvc5 *cvc5, const char *symbol, size_t size, const Cvc5Term vars[], const Cvc5Sort sort, const Cvc5Term term, bool global)

Define recursive function.

SMT-LIB:

(define-fun-rec <function_def>)

Parameters:

cvc5 – The cvc5 solver instance.
symbol – The name of the function.
size – The number of parameters of the function.
vars – The parameters to this function.
sort – The sort of the return value of this function.
term – The function body.
global – Determines whether this definition is global (i.e., persists when popping the context).

Returns:

The function.

Cvc5Term cvc5_define_fun_rec_from_const(Cvc5 *cvc5, Cvc5Term fun, size_t size, const Cvc5Term vars[], const Cvc5Term term, bool global)

Define recursive function.

SMT-LIB:

(define-fun-rec <function_def>)

Create parameter fun with mkConst().

Parameters:

cvc5 – The cvc5 solver instance.
fun – The sorted function.
size – The number of parameters of the function.
vars – The parameters to this function.
term – The function body.
global – Determines whether this definition is global (i.e., persists when popping the context).

Returns:

The function.

void cvc5_define_funs_rec(Cvc5 *cvc5, size_t nfuns, const Cvc5Term funs[], size_t nvars[], const Cvc5Term *vars[], const Cvc5Term terms[], bool global)

Define recursive functions.

SMT-LIB:

(define-funs-rec
    ( <function_decl>_1 ... <function_decl>_n )
    ( <term>_1 ... <term>_n )
)

Create elements of parameter funs with cvc5_mk_const().

Parameters:

cvc5 – The cvc5 solver instance.
nfuns – The number of sorted functions.
funs – The sorted functions.
nvars – The numbers of parameters for each function.
vars – The list of parameters to the functions.
terms – The list of function bodies of the functions.
global – Determines whether this definition is global (i.e., persists when popping the context).

Cvc5Term cvc5_simplify(Cvc5 *cvc5, Cvc5Term term, bool apply_subs)

Simplify a formula without doing “much” work.

Does not involve the SAT Engine in the simplification, but uses the current definitions, and assertions. It also involves theory normalization.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
term – The formula to simplify.
apply_subs – True to apply substitutions for solved variables.

Returns:

The simplified formula.

void cvc5_assert_formula(Cvc5 *cvc5, Cvc5Term term)

Assert a formula.

SMT-LIB:

(assert <term>)

Parameters:

cvc5 – The solver instance.
term – The formula to assert.

Cvc5Result cvc5_check_sat(Cvc5 *cvc5)

Check satisfiability.

SMT-LIB:

(check-sat)

Parameters:: cvc5 – The solver instance.
Returns:: The result of the satisfiability check.

Cvc5Result cvc5_check_sat_assuming(Cvc5 *cvc5, size_t size, const Cvc5Term assumptions[])

Check satisfiability assuming the given formulas.

SMT-LIB:

(check-sat-assuming ( <prop_literal>+ ))

Parameters:

cvc5 – The solver instance.
size – The number of assumptions.
assumptions – The formulas to assume.

Returns:

The result of the satisfiability check.

const Cvc5Term *cvc5_get_assertions(Cvc5 *cvc5, size_t *size)

Get the list of asserted formulas.

SMT-LIB:

(get-assertions)

Note

The returned Cvc5Term array pointer is only valid until the next call to this function.

Parameters:

cvc5 – The solver instance.
size – The size of the resulting assertions array.

Returns:

The list of asserted formulas.

const char *cvc5_get_info(Cvc5 *cvc5, const char *flag)

Get info from the solver.

SMT-LIB:

(get-info <info_flag>)

Note

The returned char* pointer is only valid until the next call to this function.

Parameters:: cvc5 – The solver instance.
Returns:: The info.

const char *cvc5_get_option(Cvc5 *cvc5, const char *option)

Get the value of a given option.

SMT-LIB:

(get-option <keyword>)

Note

The returned char* pointer is only valid until the next call to this function.

Parameters:

cvc5 – The solver instance.
option – The option for which the value is queried.

Returns:

A string representation of the option value.

const char **cvc5_get_option_names(Cvc5 *cvc5, size_t *size)

Get all option names that can be used with cvc5_set_option(), cvc5_get_option() and cvc5_get_option_info().

Note

The returned char* pointer is only valid until the next call to this function.

Parameters:

cvc5 – The solver instance.
size – The size of the resulting option names array.

Returns:

All option names.

void cvc5_get_option_info(Cvc5 *cvc5, const char *option, Cvc5OptionInfo *info)

Get some information about a given option. See struct Cvc5OptionInfo for more details on which information is available.

Note

The returned Cvc5OptionInfo data is only valid until the next call to this function.

Parameters:

cvc5 – The solver instance.
option – The option for which the info is queried.
info – The output parameter for the queried info.

const Cvc5Term *cvc5_get_unsat_assumptions(Cvc5 *cvc5, size_t *size)

Get the set of unsat (“failed”) assumptions.

SMT-LIB:

(get-unsat-assumptions)

Requires to enable option produce-unsat-assumptions.

Note

The returned Cvc5Term array pointer is only valid until the next call to this function.

Parameters:

cvc5 – The solver instance.
size – The number of the resulting unsat assumptions.

Returns:

The set of unsat assumptions.

const Cvc5Term *cvc5_get_unsat_core(Cvc5 *cvc5, size_t *size)

Get the unsatisfiable core.

SMT-LIB:

(get-unsat-core)

Requires to enable option produce-unsat-cores.

Note

In contrast to SMT-LIB, cvc5’s API does not distinguish between named and unnamed assertions when producing an unsatisfiable core. Additionally, the API allows this option to be called after a check with assumptions. A subset of those assumptions may be included in the unsatisfiable core returned by this function.

Note

The returned Cvc5Term array pointer is only valid until the next call to this function.

Parameters:

cvc5 – The solver instance.
size – The size of the resulting unsat core.

Returns:

A set of terms representing the unsatisfiable core.

const Cvc5Term *cvc5_get_unsat_core_lemmas(Cvc5 *cvc5, size_t *size)

Get the lemmas used to derive unsatisfiability.

SMT-LIB:

(get-unsat-core-lemmas)

Requires the SAT proof unsat core mode, so to enable option unsat-core-mode=sat-proof.

Note

The returned Cvc5Term array pointer is only valid until the next call to this function.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
size – The size of the resulting unsat core.

Returns:

A set of terms representing the lemmas used to derive unsatisfiability.

void cvc5_get_difficulty(Cvc5 *cvc5, size_t *size, Cvc5Term *inputs[], Cvc5Term *values[])

Get a difficulty estimate for an asserted formula. This function is intended to be called immediately after any response to a checkSat.

Note

The resulting mapping from inputs (which is a subset of the inputs) to real values is an estimate of how difficult each assertion was to solve. Unmentioned assertions can be assumed to have zero difficulty.

Note

The resulting inputs and values array pointers are only valid until the next call to this function.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
size – The resulting size of inputs and values.
inputs – The resulting inputs that are mapped to the resulting values.
values – The resulting real values.

const Cvc5Term *cvc5_get_timeout_core(Cvc5 *cvc5, Cvc5Result *result, size_t *size)

Get a timeout core.

This function computes a subset of the current assertions that cause a timeout. It may make multiple checks for satisfiability internally, each limited by the timeout value given by timeout-core-timeout.

If the result is unknown and the reason is timeout, then the list of formulas correspond to a subset of the current assertions that cause a timeout in the specified time timeout-core-timeout. If the result is unsat, then the list of formulas correspond to an unsat core for the current assertions. Otherwise, the result is sat, indicating that the current assertions are satisfiable, and the returned set of assertions is empty.

SMT-LIB:

(get-timeout-core)

Note

This command does not require being preceeded by a call to cvc5_check_sat().

Note

The resulting result and term array pointer are only valid until the next call to this function.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
result – The resulting result.
size – The resulting size of the timeout core.

Returns:

The list of assertions determined to be the timeout core. The resulting result is stored in result.

const Cvc5Term *cvc5_get_timeout_core_assuming(Cvc5 *cvc5, size_t size, const Cvc5Term assumptions[], Cvc5Result *result, size_t *rsize)

Get a timeout core of the given assumptions.

This function computes a subset of the given assumptions that cause a timeout when added to the current assertions.

If the result is unknown and the reason is timeout, then the set of assumptions corresponds to a subset of the given assumptions that cause a timeout when added to the current assertions in the specified time timeout-core-timeout. If the result is unsat, then the set of assumptions together with the current assertions correspond to an unsat core for the current assertions. Otherwise, the result is sat, indicating that the given assumptions plus the current assertions are satisfiable, and the returned set of assumptions is empty.

SMT-LIB:

(get-timeout-core (<assert>*))

Note

This command does not require being preceeded by a call to cvc5_check_sat().

Note

The resulting result and term array pointer are only valid until the next call to this function.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
size – The number of assumptions.
assumptions – The (non-empty) set of formulas to assume.
result – The resulting result.
rsize – The resulting size of the timeout core.

Returns:

The list of assumptions determined to be the timeout core. The resulting result is stored in result.

const Cvc5Proof *cvc5_get_proof(Cvc5 *cvc5, Cvc5ProofComponent c, size_t *size)

Get a proof associated with the most recent call to checkSat.

SMT-LIB:

(get-proof :c)

Requires to enable option produce-proofs. The string representation depends on the value of option produce-proofs.

Note

The returned Cvc5Proof array pointer is only valid until the next call to this function.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
c – The component of the proof to return
size – The size of the resulting array of proofs.

Returns:

An array of proofs.

const Cvc5Term *cvc5_get_learned_literals(Cvc5 *cvc5, Cvc5LearnedLitType type, size_t *size)

Get a list of learned literals that are entailed by the current set of assertions.

Note

The resulting Cvc5Term array pointer is only valid until the next call to this function.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
type – The type of learned literalsjto return
size – The size of the resulting list of literals.

Returns:

A list of literals that were learned at top-level.

Cvc5Term cvc5_get_value(Cvc5 *cvc5, Cvc5Term term)

Get the value of the given term in the current model.

SMT-LIB:

(get-value ( <term> ))

Parameters:

cvc5 – The solver instance.
term – The term for which the value is queried.

Returns:

The value of the given term.

const Cvc5Term *cvc5_get_values(Cvc5 *cvc5, size_t size, const Cvc5Term terms[], size_t *rsize)

Get the values of the given terms in the current model.

SMT-LIB:

(get-value ( <term>* ))

Parameters:

cvc5 – The solver instance.
size – The number of terms for which the value is queried.
terms – The terms.
rsize – The resulting size of the timeout core.

Returns:

The values of the given terms.

const Cvc5Term *cvc5_get_model_domain_elements(Cvc5 *cvc5, Cvc5Sort sort, size_t *size)

Get the domain elements of uninterpreted sort s in the current model. The current model interprets s as the finite sort whose domain elements are given in the return value of this function.

Parameters:

cvc5 – The solver instance.
sort – The uninterpreted sort in question.
size – The size of the resulting domain elements array.

Returns:

The domain elements of s in the current model.

bool cvc5_is_model_core_symbol(Cvc5 *cvc5, Cvc5Term v)

Determine if the model value of the given free constant was essential for showing satisfiability of the last cvc5_check_sat() query based on the current model.

For any free constant v, this will only return false if model-cores* has been set to true.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
v – The term in question.

Returns:

True if v was essential and is thus a model core symbol.

const char *cvc5_get_model(Cvc5 *cvc5, size_t nsorts, const Cvc5Sort sorts[], size_t nconsts, const Cvc5Term consts[])

Get the model

SMT-LIB:

(get-model)

Requires to enable option produce-models.

Note

The returned char* pointer is only valid until the next call to this function.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
nsorts – The number of uninterpreted sorts that should be printed in the model.
sorts – The list of uninterpreted sorts.
nconsts – The size of the list of free constants that should be printed in the model.
consts – The list of free constants that should be printed in the model. A subset of these may be printed based on isModelCoreSymbol().

Returns:

A string representing the model.

Cvc5Term cvc5_get_quantifier_elimination(Cvc5 *cvc5, Cvc5Term q)

Do quantifier elimination.

SMT-LIB:

(get-qe <q>)

Note

Quantifier Elimination is is only complete for logics such as LRA, LIA and BV.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
q – A quantified formula of the form \(Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)\) where \(Q\bar{x}\) is a set of quantified variables of the form \(Q x_1...x_k\) and \(P( x_1...x_i, y_1...y_j )\) is a quantifier-free formula

Returns:

A formula \(\phi\) such that, given the current set of formulas \(A\) asserted to this solver:

\((A \wedge q)\) and \((A \wedge \phi)\) are equivalent
\(\phi\) is quantifier-free formula containing only free variables in \(y_1...y_n\).

Cvc5Term cvc5_get_quantifier_elimination_disjunct(Cvc5 *cvc5, Cvc5Term q)

Do partial quantifier elimination, which can be used for incrementally computing the result of a quantifier elimination.

SMT-LIB:

(get-qe-disjunct <q>)

Note

Quantifier Elimination is is only complete for logics such as LRA, LIA and BV.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
q – A quantified formula of the form \(Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)\) where \(Q\bar{x}\) is a set of quantified variables of the form \(Q x_1...x_k\) and \(P( x_1...x_i, y_1...y_j )\) is a quantifier-free formula

Returns:

A formula \(\phi\) such that, given the current set of formulas \(A\) asserted to this solver:

\((A \wedge q \implies A \wedge \phi)\) if \(Q\) is \(\forall\), and \((A \wedge \phi \implies A \wedge q)\) if \(Q\) is \(\exists\)
\(\phi\) is quantifier-free formula containing only free variables in \(y_1...y_n\)
If \(Q\) is \(\exists\), let \((A \wedge Q_n)\) be the formula \((A \wedge \neg (\phi \wedge Q_1) \wedge ... \wedge \neg (\phi \wedge Q_n))\) where for each \(i = 1...n\), formula \((\phi \wedge Q_i)\) is the result of calling cvc5_get_quantifier_elimination_disjunct() for \(q\) with the set of assertions \((A \wedge Q_{i-1})\). Similarly, if \(Q\) is \(\forall\), then let \((A \wedge Q_n)\) be \((A \wedge (\phi \wedge Q_1) \wedge ... \wedge (\phi \wedge Q_n))\) where \((\phi \wedge Q_i)\) is the same as above. In either case, we have that \((\phi \wedge Q_j)\) will eventually be true or false, for some finite j.

void cvc5_declare_sep_heap(Cvc5 *cvc5, Cvc5Sort loc, Cvc5Sort data)

When using separation logic, this sets the location sort and the datatype sort to the given ones. This function should be invoked exactly once, before any separation logic constraints are provided.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
loc – The location sort of the heap.
data – The data sort of the heap.

Cvc5Term cvc5_get_value_sep_heap(Cvc5 *cvc5)

When using separation logic, obtain the term for the heap.

Warning

This function is experimental and may change in future versions.

Parameters:: cvc5 – The solver instance.
Returns:: The term for the heap.

Cvc5Term cvc5_get_value_sep_nil(Cvc5 *cvc5)

When using separation logic, obtain the term for nil.

Warning

This function is experimental and may change in future versions.

Parameters:: cvc5 – The solver instance.
Returns:: The term for nil.

Cvc5Term cvc5_declare_pool(Cvc5 *cvc5, const char *symbol, Cvc5Sort sort, size_t size, const Cvc5Term init_value[])

Declare a symbolic pool of terms with the given initial value.

For details on how pools are used to specify instructions for quantifier instantiation, see documentation for the #INST_POOL kind.

SMT-LIB:

(declare-pool <symbol> <sort> ( <term>* ))

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
symbol – The name of the pool.
sort – The sort of the elements of the pool.
size – The number of initial values of the pool.
init_value – The initial value of the pool.

Returns:

The pool symbol.

Cvc5Term cvc5_declare_oracle_fun(Cvc5 *cvc5, const char *symbol, size_t size, const Cvc5Sort sorts[], Cvc5Sort sort, void *state, Cvc5Term (*fun)(size_t, const Cvc5Term*, void*))

Declare an oracle function with reference to an implementation.

Oracle functions have a different semantics with respect to ordinary declared functions. In particular, for an input to be satisfiable, its oracle functions are implicitly universally quantified.

This function is used in part for implementing this command:

(declare-oracle-fun <sym> (<sort>*) <sort> <sym>)

In particular, the above command is implemented by constructing a function over terms that wraps a call to binary sym via a text interface.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
symbol – The name of the oracle
size – The number of domain sorts of the oracle function.
sorts – The domain sorts.
sort – The sort of the return value of this function.
state – The state data for the oracle function, may be NULL.
fun – The function that implements the oracle function, taking a an array of term arguments and its size and a void pointer to optionally capture any state data the function may need.

Returns:

The oracle function.

void cvc5_add_plugin(Cvc5 *cvc5, Cvc5Plugin *plugin)

Add plugin to this solver. Its callbacks will be called throughout the lifetime of this solver.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
plugin – The plugin to add to this solver.

Cvc5Term cvc5_get_interpolant(Cvc5 *cvc5, Cvc5Term conj)

Get an interpolant.

Given that \(A \rightarrow B\) is valid, this function determines a term \(I\) over the shared variables of \(A\) and \(B\), such that \(A \rightarrow I\) and \(I \rightarrow B\) are valid, if such a term exits. \(A\) is the current set of assertions and \(B\) is the conjecture, given as conj.

SMT-LIB:

(get-interpolant <symbol> <conj>)

Note

In SMT-LIB, <symbol> assigns a symbol to the interpolant.

Note

Requires option produce-interpolants to be set to a mode different from none.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
conj – The conjecture term.

Returns:

The interpolant, if an interpolant exists, else the null term.

Cvc5Term cvc5_get_interpolant_with_grammar(Cvc5 *cvc5, Cvc5Term conj, Cvc5Grammar grammar)

Get an interpolant

Given that \(A \rightarrow B\) is valid, this function determines a term \(I\) over the shared variables of \(A\) and \(B\), with respect to a given grammar, such that \(A \rightarrow I\) and \(I \rightarrow B\) are valid, if such a term exits. \(A\) is the current set of assertions and \(B\) is the conjecture, given as conj.

SMT-LIB:

(get-interpolant <symbol> <conj> <grammar>)

Note

In SMT-LIB, <symbol> assigns a symbol to the interpolant.

Note

Requires option produce-interpolants to be set to a mode different from none.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
conj – The conjecture term.
grammar – The grammar for the interpolant I.

Returns:

The interpolant, if an interpolant exists, else the null term.

Cvc5Term cvc5_get_interpolant_next(Cvc5 *cvc5)

Get the next interpolant. Can only be called immediately after a successful call to get-interpolant or get-interpolant-next. Is guaranteed to produce a syntactically different interpolant wrt the last returned interpolant if successful.

SMT-LIB:

(get-interpolant-next)

Requires to enable incremental mode, and option produce-interpolants to be set to a mode different from none.

Warning

This function is experimental and may change in future versions.

Parameters:: cvc5 – The solver instance.
Returns:: A Term \(I\) such that \(A \rightarrow I\) and \(I \rightarrow B\) are valid, where \(A\) is the current set of assertions and \(B\) is given in the input by conj, or the null term if such a term cannot be found.

Cvc5Term cvc5_get_abduct(Cvc5 *cvc5, Cvc5Term conj)

Get an abduct.

SMT-LIB:

(get-abduct <conj>)

Requires to enable option produce-abducts.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
conj – The conjecture term.

Returns:

A term \(C\) such that \((A \wedge C)\) is satisfiable, and \((A \wedge \neg B \wedge C)\) is unsatisfiable, where \(A\) is the current set of assertions and \(B\) is given in the input by conj, or the null term if such a term cannot be found.

Cvc5Term cvc5_get_abduct_with_grammar(Cvc5 *cvc5, Cvc5Term conj, Cvc5Grammar grammar)

Get an abduct.

SMT-LIB:

(get-abduct <conj> <grammar>)

Requires to enable option produce-abducts.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
conj – The conjecture term.
grammar – The grammar for the abduct \(C\)

Returns:

A term C such that \((A \wedge C)\) is satisfiable, and \((A \wedge \neg B \wedge C)\) is unsatisfiable, where \(A\) is the current set of assertions and \(B\) is given in the input by conj, or the null term if such a term cannot be found.

Cvc5Term cvc5_get_abduct_next(Cvc5 *cvc5)

Get the next abduct. Can only be called immediately after a successful call to get-abduct or get-abduct-next. Is guaranteed to produce a syntactically different abduct wrt the last returned abduct if successful.

SMT-LIB:

(get-abduct-next)

Requires to enable incremental mode, and option produce-abducts.

Warning

This function is experimental and may change in future versions.

Parameters:: cvc5 – The solver instance.
Returns:: A term C such that \((A \wedge C)\) is satisfiable, and \((A \wedge \neg B \wedge C)\) is unsatisfiable, where \(A\) is the current set of assertions and \(B\) is given in the input by the last call to getAbduct(), or the null term if such a term cannot be found.

void cvc5_block_model(Cvc5 *cvc5, Cvc5BlockModelsMode mode)

Block the current model. Can be called only if immediately preceded by a SAT or INVALID query.

SMT-LIB:

(block-model)

Requires enabling option produce-models.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
mode – The mode to use for blocking.

void cvc5_block_model_values(Cvc5 *cvc5, size_t size, const Cvc5Term terms[])

Block the current model values of (at least) the values in terms. Can be called only if immediately preceded by a SAT query.

SMT-LIB:

(block-model-values ( <terms>+ ))

Requires enabling option produce-models.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
size – The number of values to block.
terms – The values to block.

const char *cvc5_get_instantiations(Cvc5 *cvc5)

Note

The returned char* pointer is only valid until the next call to this function.

Warning

This function is experimental and may change in future versions.

Parameters:: cvc5 – The solver instance.
Returns:: A string that contains information about all instantiations made by the quantifiers module.

void cvc5_push(Cvc5 *cvc5, uint32_t nscopes)

Push (a) level(s) to the assertion stack.

SMT-LIB:

(push <numeral>)

Parameters:

cvc5 – The solver instance.
nscopes – The number of levels to push.

void cvc5_pop(Cvc5 *cvc5, uint32_t nscopes)

Pop (a) level(s) from the assertion stack.

SMT-LIB:

(pop <numeral>)

Parameters:

cvc5 – The solver instance.
nscopes – The number of levels to pop.

void cvc5_reset_assertions(Cvc5 *cvc5)

Remove all assertions.

SMT-LIB:

(reset-assertions)

Parameters:: cvc5 – The solver instance.

void cvc5_set_info(Cvc5 *cvc5, const char *keyword, const char *value)

Set info.

SMT-LIB:

(set-info <attribute>)

Parameters:

cvc5 – The solver instance.
keyword – The info flag.
value – The value of the info flag.

void cvc5_set_logic(Cvc5 *cvc5, const char *logic)

Set logic.

SMT-LIB:

(set-logic <symbol>)

Parameters:

cvc5 – The solver instance.
logic – The logic to set.

bool cvc5_is_logic_set(Cvc5 *cvc5)

Determine if cvc5_set_logic() has been called.

Returns:: True if setLogic() has already been called for the given solver instance.

const char *cvc5_get_logic(Cvc5 *cvc5)

Get the logic set the solver.

Note

Asserts `cvc5_is_logic_set()1.

Note

The returned char* pointer is only valid until the next call to this function.

Returns:: The logic used by the solver.

void cvc5_set_option(Cvc5 *cvc5, const char *option, const char *value)

Set option.

SMT-LIB:

(set-option :<option> <value>)

Parameters:

cvc5 – The solver instance.
option – The option name.
value – The option value.

Cvc5Term cvc5_declare_sygus_var(Cvc5 *cvc5, const char *symbol, Cvc5Sort sort)

Append symbol to the current list of universal variables.

SyGuS v2:

(declare-var <symbol> <sort>)

Parameters:

cvc5 – The solver instance.
sort – The sort of the universal variable.
symbol – The name of the universal variable.

Returns:

The universal variable.

Cvc5Grammar cvc5_mk_grammar(Cvc5 *cvc5, size_t nbound_vars, const Cvc5Term bound_vars[], size_t nsymbols, const Cvc5Term symbols[])

Create a Sygus grammar. The first non-terminal is treated as the starting non-terminal, so the order of non-terminals matters.

Parameters:

cvc5 – The solver instance.
nbound_vars – The number of bound variabls.
bound_vars – The parameters to corresponding synth-fun/synth-inv.
nsymbols – The number of symbols.
symbols – The pre-declaration of the non-terminal symbols.

Returns:

The grammar.

Cvc5Term cvc5_synth_fun(Cvc5 *cvc5, const char *symbol, size_t size, const Cvc5Term bound_vars[], Cvc5Sort sort)

Synthesize n-ary function.

SyGuS v2:

(synth-fun <symbol> ( <boundVars>* ) <sort>)

Parameters:

cvc5 – The solver instance.
symbol – The name of the function.
size – The number of parameters.
bound_vars – The parameters to this function.
sort – The sort of the return value of this function.

Returns:

The function.

Cvc5Term cvc5_synth_fun_with_grammar(Cvc5 *cvc5, const char *symbol, size_t size, const Cvc5Term bound_vars[], Cvc5Sort sort, Cvc5Grammar grammar)

Synthesize n-ary function following specified syntactic constraints.

SyGuS v2:

(synth-fun <symbol> ( <boundVars>* ) <sort> <grammar>)

Parameters:

cvc5 – The solver instance.
symbol – The name of the function.
size – The number of parameters.
boundVars – The parameters to this function.
sort – The sort of the return value of this function.
grammar – The syntactic constraints.

Returns:

The function.

void cvc5_add_sygus_constraint(Cvc5 *cvc5, Cvc5Term term)

Add a forumla to the set of Sygus constraints.

SyGuS v2:

(constraint <term>)

Parameters:

cvc5 – The solver instance.
term – The formula to add as a constraint.

const Cvc5Term *cvc5_get_sygus_constraints(Cvc5 *cvc5, size_t *size)

Get the list of sygus constraints.

Parameters:

cvc5 – The solver instance.
size – The size of the resulting list of sygus constraints.

Returns:

The list of sygus constraints.

void cvc5_add_sygus_assume(Cvc5 *cvc5, Cvc5Term term)

Add a forumla to the set of Sygus assumptions.

SyGuS v2:

(assume <term>)

Parameters:

cvc5 – The solver instance.
term – The formula to add as an assumption.

const Cvc5Term *cvc5_get_sygus_assumptions(Cvc5 *cvc5, size_t *size)

Get the list of sygus assumptions.

Parameters:

cvc5 – The solver instance.
size – The size of the resulting list of sygus assumptions.

Returns:

The list of sygus assumptions.

void cvc5_add_sygus_inv_constraint(Cvc5 *cvc5, Cvc5Term inv, Cvc5Term pre, Cvc5Term trans, Cvc5Term post)

Add a set of Sygus constraints to the current state that correspond to an invariant synthesis problem.

SyGuS v2:

(inv-constraint <inv> <pre> <trans> <post>)

Parameters:

cvc5 – The solver instance.
inv – The function-to-synthesize.
pre – The pre-condition.
trans – The transition relation.
post – The post-condition.

Cvc5SynthResult cvc5_check_synth(Cvc5 *cvc5)

Try to find a solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints.

SyGuS v2:

(check-synth)

Parameters:: cvc5 – The solver instance.
Returns:: The result of the check, which is “solution” if the check found a solution in which case solutions are available via getSynthSolutions, “no solution” if it was determined there is no solution, or “unknown” otherwise.

Cvc5SynthResult cvc5_check_synth_next(Cvc5 *cvc5)

Try to find a next solution for the synthesis conjecture corresponding to the current list of functions-to-synthesize, universal variables and constraints. Must be called immediately after a successful call to check-synth or check-synth-next.

SyGuS v2:

(check-synth-next)

Note

Requires incremental mode.

Parameters:: cvc5 – The solver instance.
Returns:: The result of the check, which is “solution” if the check found a solution in which case solutions are available via getSynthSolutions, “no solution” if it was determined there is no solution, or “unknown” otherwise.

Cvc5Term cvc5_get_synth_solution(Cvc5 *cvc5, Cvc5Term term)

Get the synthesis solution of the given term. This function should be called immediately after the solver answers unsat for sygus input.

Parameters:

cvc5 – The solver instance.
term – The term for which the synthesis solution is queried.

Returns:

The synthesis solution of the given term.

const Cvc5Term *cvc5_get_synth_solutions(Cvc5 *cvc5, size_t size, const Cvc5Term terms[])

Get the synthesis solutions of the given terms. This function should be called immediately after the solver answers unsat for sygus input.

Parameters:

cvc5 – The solver instance.
size – The size of the terms array.
terms – The terms for which the synthesis solutions is queried.

Returns:

The synthesis solutions of the given terms.

Cvc5Term cvc5_find_synth(Cvc5 *cvc5, Cvc5FindSynthTarget target)

Find a target term of interest using sygus enumeration, with no provided grammar.

The solver will infer which grammar to use in this call, which by default will be the grammars specified by the function(s)-to-synthesize in the current context.

SyGuS v2:

(find-synth :target)

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
target – The identifier specifying what kind of term to find

Returns:

The result of the find, which is the null term if this call failed.

Cvc5Term cvc5_find_synth_with_grammar(Cvc5 *cvc5, Cvc5FindSynthTarget target, Cvc5Grammar grammar)

Find a target term of interest using sygus enumeration with a provided grammar.

SyGuS v2:

(find-synth :target G)

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
target – The identifier specifying what kind of term to find
grammar – The grammar for the term

Returns:

The result of the find, which is the null term if this call failed.

Cvc5Term cvc5_find_synth_next(Cvc5 *cvc5)

Try to find a next target term of interest using sygus enumeration. Must be called immediately after a successful call to find-synth or find-synth-next.

SyGuS v2:

(find-synth-next)

Warning

This function is experimental and may change in future versions.

Parameters:: cvc5 – The solver instance.
Returns:: The result of the find, which is the null term if this call failed.

Cvc5Statistics cvc5_get_statistics(Cvc5 *cvc5)

Get a snapshot of the current state of the statistic values of this solver. The returned object is completely decoupled from the solver and will not change when the solver is used again.

Parameters:: cvc5 – The solver instance.
Returns:: A snapshot of the current state of the statistic values.

void cvc5_print_stats_safe(Cvc5 *cvc5, int fd)

Print the statistics to the given file descriptor, suitable for usage in signal handlers.

Parameters:

cvc5 – The solver instance.
fd – The file descriptor.

bool cvc5_is_output_on(Cvc5 *cvc5, const char *tag)

Determines if the output stream for the given tag is enabled. Tags can be enabled with the output option (and -o <tag> on the command line).

Note

Requires that a valid tag is given.

Parameters:: cvc5 – The solver instance.
Returns:: True if the given tag is enabled.

void cvc5_get_output(Cvc5 *cvc5, const char *tag, const char *filename)

Configure a file to write the output for a given tag.

Tags can be enabled with the output option (and -o <tag> on the command line). Requires that the given tag is valid.

Note

Close file filename before reading via cvc5_close_output().

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
tag – The output tag.
filename – The file to write the output to. Use <stdout> to configure to write to stdout.

void cvc5_close_output(Cvc5 *cvc5, const char *filename)

Close output file configured for an output tag via cvc5_get_output().

Note

This is required before reading the file.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
filename – The file to close.

const char *cvc5_get_version(Cvc5 *cvc5)

Get a string representation of the version of this solver.

Note

The returned char* pointer is only valid until the next call to this function.

Parameters:: cvc5 – The solver instance.
Returns:: The version string.

const char *cvc5_proof_to_string(Cvc5 *cvc5, Cvc5Proof proof, Cvc5ProofFormat format, size_t size, const Cvc5Term assertions[], const char *names[])

Prints a proof as a string in a selected proof format mode. Other aspects of printing are taken from the solver options.

Note

The returned char* pointer is only valid until the next call to this function.

Warning

This function is experimental and may change in future versions.

Parameters:

cvc5 – The solver instance.
proof – A proof, usually obtained from Solver::getProof().
format – The proof format used to print the proof. Must be modes::ProofFormat::NONE if the proof is from a component other than modes::ProofComponent::FULL.
size – The number of assertions to names mappings given.
assertions – The list of assertions that are mapped to assertions_names. May be NULL if assertions_size is 0.
names – The names of the assertions (1:1 mapping). May by NULL if assertions is NULL.

Returns:

The string representation of the proof in the given format.