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

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.
SMTLIB:
(declaredatatype <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 nary function symbol.
SMTLIB:
(declarefun <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.
SMTLIB:
(declaresort <symbol> <numeral>)
Note
This corresponds to
cvc5_mk_uninterpreted_sort()
if arity = 0, and tocvc5_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 nary function.
SMTLIB:
(definefun <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.
SMTLIB:
(definefunrec <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.
SMTLIB:
(definefunrec <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.
SMTLIB:
(definefunsrec ( <function_decl>_1 ... <function_decl>_n ) ( <term>_1 ... <term>_n ) )
Create elements of parameter
funs
withcvc5_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.
SMTLIB:
(assert <term>)
 Parameters :


cvc5 – The solver instance.

term – The formula to assert.


Cvc5Result
cvc5_check_sat
(
Cvc5
*
cvc5
)

Check satisfiability.
SMTLIB:
(checksat)
 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.
SMTLIB:
(checksatassuming ( <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.
SMTLIB:
(getassertions)
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.
SMTLIB:
(getinfo <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.
SMTLIB:
(getoption <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()
andcvc5_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.
SMTLIB:
(getunsatassumptions)
Requires to enable option produceunsatassumptions .
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.
SMTLIB:
(getunsatcore)
Requires to enable option produceunsatcores .
Note
In contrast to SMTLIB, 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.
SMTLIB:
(getunsatcorelemmas)
Requires the SAT proof unsat core mode, so to enable option unsatcoremode=satproof .
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 realvalues
is an estimate of how difficult each assertion was to solve. Unmentioned assertions can be assumed to have zero difficulty.Note
The resulting
inputs
andvalues
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
andvalues
. 
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 timeoutcoretimeout .
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 timeoutcoretimeout . 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.
SMTLIB:
(gettimeoutcore)
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 timeoutcoretimeout . 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.
SMTLIB:
(gettimeoutcore (<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 (nonempty) 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.
SMTLIB:
(getproof :c)
Requires to enable option produceproofs . The string representation depends on the value of option produceproofs .
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 toplevel.

Cvc5Term
cvc5_get_value
(
Cvc5
*
cvc5
,
Cvc5Term
term
)

Get the value of the given term in the current model.
SMTLIB:
(getvalue ( <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.
SMTLIB:
(getvalue ( <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 modelcores* 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
SMTLIB:
(getmodel)
Requires to enable option producemodels .
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.
SMTLIB:
(getqe <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 quantifierfree 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 quantifierfree 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.
SMTLIB:
(getqedisjunct <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 quantifierfree 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 quantifierfree 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_{i1})\) . 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.
SMTLIB:
(declarepool <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:
(declareoraclefun <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
SMTLIB:
(getinterpolant <conj>)
Requires option produceinterpolants 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 :

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_interpolant_with_grammar
(
Cvc5
*
cvc5
,
Cvc5Term
conj
,
Cvc5Grammar
grammar
)

Get an interpolant
SMTLIB:
(getinterpolant <conj> <grammar>)
Requires option produceinterpolants 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 :

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_interpolant_next
(
Cvc5
*
cvc5
)

Get the next interpolant. Can only be called immediately after a successful call to getinterpolant or getinterpolantnext. Is guaranteed to produce a syntactically different interpolant wrt the last returned interpolant if successful.
SMTLIB:
(getinterpolantnext)
Requires to enable incremental mode, and option produceinterpolants 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.
SMTLIB:
(getabduct <conj>)
Requires to enable option produceabducts .
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.
SMTLIB:
(getabduct <conj> <grammar>)
Requires to enable option produceabducts .
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 getabduct or getabductnext. Is guaranteed to produce a syntactically different abduct wrt the last returned abduct if successful.
SMTLIB:
(getabductnext)
Requires to enable incremental mode, and option produceabducts .
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.
SMTLIB:
(blockmodel)
Requires enabling option producemodels .
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.
SMTLIB:
(blockmodelvalues ( <terms>+ ))
Requires enabling option producemodels .
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.
SMTLIB:
(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.
SMTLIB:
(pop <numeral>)
 Parameters :


cvc5 – The solver instance.

nscopes – The number of levels to pop.


void
cvc5_reset_assertions
(
Cvc5
*
cvc5
)

Remove all assertions.
SMTLIB:
(resetassertions)
 Parameters :

cvc5 – The solver instance.

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

Set info.
SMTLIB:
(setinfo <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.
SMTLIB:
(setlogic <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.
SMTLIB:
(setoption :<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:
(declarevar <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 nonterminal is treated as the starting nonterminal, so the order of nonterminals matters.
 Parameters :


cvc5 – The solver instance.

nbound_vars – The number of bound variabls.

bound_vars – The parameters to corresponding synthfun/synthinv.

nsymbols – The number of symbols.

symbols – The predeclaration of the nonterminal symbols.

 Returns :

The grammar.

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

Synthesize nary function.
SyGuS v2:
(synthfun <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 nary function following specified syntactic constraints.
SyGuS v2:
(synthfun <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:
(invconstraint <inv> <pre> <trans> <post>)
 Parameters :


cvc5 – The solver instance.

inv – The functiontosynthesize.

pre – The precondition.

trans – The transition relation.

post – The postcondition.


Cvc5SynthResult
cvc5_check_synth
(
Cvc5
*
cvc5
)

Try to find a solution for the synthesis conjecture corresponding to the current list of functionstosynthesize, universal variables and constraints.
SyGuS v2:
(checksynth)
 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 functionstosynthesize, universal variables and constraints. Must be called immediately after a successful call to checksynth or checksynthnext.
SyGuS v2:
(checksynthnext)
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)tosynthesize in the current context.
SyGuS v2:
(findsynth :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:
(findsynth :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 findsynth or findsynthnext.
SyGuS v2:
(findsynthnext)
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 (ando <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 (ando <tag>
on the command line). Requires that the given tag is valid.Note
Close file
filename
before reading viacvc5_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 thanmodes::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 ifassertions_size
is 0. 
names – The names of the
assertions
(1:1 mapping). May by NULL ifassertions
is NULL.

 Returns :

The string representation of the proof in the given format.