Solver

This class represents a cvc5 solver instance.

Terms, Sorts and Ops are not tied to a cvc5.Solver but associated with a cvc5.TermManager instance, which can be shared between solver instances.

Solver options are configured via cvc5.Solver.setOption() and queried via cvc5.Solver.getOption() (for more information on configuration options, see Options).

class cvc5.Solver

A cvc5 solver.

Wrapper class for cvc5::Solver.

addPlugin()

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

Parameters:: p – The plugin to add to this solver.

addSygusAssume()

Add a formula to the set of Sygus assumptions.

SyGuS v2:

( assume <term> )

Parameters:: term – The formuula to add as an assumption.

addSygusConstraint()

Add a formula to the set of SyGuS constraints.

SyGuS v2:

( constraint <term> )

Parameters:: term – The formula to add as a constraint.

addSygusInvConstraint()

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:

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

assertFormula()

Assert a formula

SMT-LIB:

( assert <term> )

Parameters:: term – The formula to assert.

blockModel()

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 to a mode other than none.

Warning

This function is experimental and may change in future versions.

Parameters:: mode – The mode to use for blocking

blockModelValues()

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.

checkSat()

Check satisfiability.

SMT-LIB:

( check-sat )

Returns:: The result of the satisfiability check.

checkSatAssuming()

Check satisfiability assuming the given formula.

SMT-LIB:

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

Parameters:: assumptions – The formulas to assume.
Returns:: The result of the satisfiability check.

checkSynth()

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 )

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.

checkSynthNext()

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. Requires incremental mode.

SyGuS v2:

( check-synth )

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.

declareDatatype()

Create datatype sort.

SMT-LIB:

( declare-datatype <symbol> <datatype_decl> )

Parameters:

symbol – The name of the datatype sort.
ctors – The constructor declarations of the datatype sort.

Returns:

The datatype sort.

declareFun()

Declare n-ary function symbol.

SMT-LIB:

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

Parameters:

symbol – The name of the function.
sorts – The sorts of the parameters to this function.
sort – The sort of the return value of this 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.

declarePool()

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

SMT-LIB:

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

Warning

This function is experimental and may change in future versions.

Parameters:

symbol – The name of the pool.
sort – The sort of the elements of the pool.
initValue – The initial value of the pool.

declareSepHeap()

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:

locSort – The location sort of the heap.
dataSort – The data sort of the heap.

declareSort()

Declare uninterpreted sort.

SMT-LIB:

( declare-sort <symbol> <numeral> )

Note

This corresponds to Solver.mkUninterpretedSort() if arity = 0, and to Solver.mkUninterpretedSortConstructorSort() if arity > 0.

Parameters:

symbol – The name of the sort.
arity – The arity of the sort.
fresh – If true, then this method always returns a new Sort. Otherwise, this method will always return the same Sort for each call with the given arity and symbol where fresh is false.

Returns:

The sort.

declareSygusVar()

Append symbol to the current list of universal variables.

SyGuS v2:

( declare-var <symbol> <sort> )

Parameters:

sort – The sort of the universal variable.
symbol – The name of the universal variable.

Returns:

The universal variable.

defineFun()

Define n-ary function.

SMT-LIB:

( define-fun <function_def> )

Parameters:

symbol – The name of the function.
bound_vars – The parameters to this function.
sort – The sort of the return value of this function.
term – The function body.
glbl – Determines whether this definition is global (i.e. persists when popping the context).

Returns:

The function.

defineFunRec()

Define recursive functions.

Supports the following arguments:

Term defineFunRec(str symbol, List[Term] bound_vars, Sort sort, Term term, bool glbl)
Term defineFunRec(Term fun, List[Term] bound_vars, Term term, bool glbl)

SMT-LIB:

( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )

Create elements of parameter funs with mkConst().

Parameters:

funs – The sorted functions.
bound_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).

Returns:

The function.

defineFunsRec()

Define recursive functions.

SMT-LIB:

( define-funs-rec ( <function_decl>^n ) ( <term>^n ) )

Create elements of parameter funs with mkConst().

Parameters:

funs – The sorted functions.
bound_vars – The list of parameters to the functions.
terms – The list of function bodies of the functions.
glb – Determines whether this definition is global (i.e. persists when popping the context).

findSynth()

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

SyGuS v2:

( find-synth :target G)

Parameters:

fst – 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.

findSynthNext()

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. Requires incremental mode.

SyGuS v2:

( find-synth-next )

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

getAbduct()

Get an abduct.

SMT-LIB:

( get-abduct <conj> )
( get-abduct <conj> <grammar> )

Requires to enable option produce-abducts.

Warning

This function is experimental and may change in future versions.

Parameters:

conj – The conjecture term.
grammar – A grammar for the abduct.

Returns:

The abduct. See cvc5::Solver::getAbduct() for details.

getAbductNext()

Get the next abduct.

Can only be called immediately after a successful call to Solver.getAbduct() or Solver.getAbductNext(). 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:: output – The term where the result will be stored.
Returns:: True iff an abduct was found.

getAssertions()

Get the list of asserted formulas.

SMT-LIB:

( get-assertions )

Returns:: The list of asserted formulas.

getBooleanSort(): Get the Boolean sort. :return: Sort Boolean. .. warning:: This function is deprecated and will be removed in a

future release.

getDifficulty()

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

Warning

This function is experimental and may change in future versions.

Returns:: A map from (a subset of) the input assertions to a real value that is an estimate of how difficult each assertion was to solver. Unmentioned assertions can be assumed to have zero difficulty.

getInfo()

Get info from the solver.

SMT-LIB:

( get-info <info_flag> )

Parameters:: flag – The info flag.
Returns:: The info.

getInstantiations(): Return a string that contains information about all instantiations made by the quantifiers module.

Warning

This function is experimental and may change in future versions.

getIntegerSort(): Get the integer sort. :return: Sort Integer. .. warning:: This function is deprecated and will be removed in a

future release.

getInterpolant()

Get an interpolant.

This determines a term \(I\), optionally with respect to a 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> )
( 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:

conj – The conjecture term.
grammar – A grammar for the interpolant.

Returns:

The interpolant, if such a term exists.

getInterpolantNext()

Get the next interpolant.

Can only be called immediately after a successful call to Solver.getInterpolant() or Solver.getInterpolantNext(). 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:: output – The term where the result will be stored.
Returns:: True iff an interpolant was found.

getLearnedLiterals()

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

SMT-LIB:

( get-learned-literals )

Warning

This function is experimental and may change in future versions.

Parameters:: type – The type of learned literals to return
Returns:: The list of literals.

getLogic()

Get the logic set the solver.

Note

Asserts isLogicSet().

Returns:: The logic used by the solver.

getModel()

Get the model

SMT-LIB:

(get-model)

Requires to enable option produce-models.

Warning

This function is experimental and may change in future versions.

Parameters:

sorts – The list of uninterpreted sorts that should be printed in the model.
vars – The list of free constants that should be printed in the model. A subset of these may be printed based on Solver.isModelCoreSymbol().

Returns:

A string representing the model.

getModelDomainElements()

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

Parameters:: s – The uninterpreted sort in question.
Returns:: The domain elements of s in the current model.

getNumIndicesForSkolemId()

Get the number of indices for a skolem id.

Parameters:: id – The skolem id.
Returns:: The number of indice for a skolem with the given id.

getOption()

Get the value of a given option.

SMT-LIB:

( get-option <keyword> )

Parameters:: option – The option for which the value is queried.
Returns:: A string representation of the option value.

getOptionInfo()

Get some information about the given option. Returns the information provided by the C++ OptionInfo as a dictionary.

Returns:: Information about the given option.

getOptionNames()

Get all option names that can be used with Solver.setOption(), Solver.getOption() and Solver.getOptionInfo().

Returns:: All option names.

getProof()

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

SMT-LIB:

(get-proof :c)

Requires to enable option produce-proofs.

Warning

This function is experimental and may change in future versions.

Parameters:: c – The component of the proof to return.
Returns:: A vector of proof nodes.

getQuantifierElimination()

Do quantifier elimination.

SMT-LIB:

( get-qe <q> )

Requires a logic that supports quantifier elimination. Currently, the only logics supported by quantifier elimination are LRA and LIA.

Warning

This function is experimental and may change in future versions.

Parameters:

q – A quantified formula of the form \(Q\bar{x_1}\dots Q\bar{x}_n. P( x_1 \dots x_i, y_1 \dots 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)\) \((A \wedge \phi)\) are equivalent
\(\phi\) is quantifier-free formula containing only free variables in \(y_1...y_n\).

getQuantifierEliminationDisjunct()

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

SMT-LIB:
( get-qe-disjunct <q> )
Requires a logic that supports quantifier elimination. Currently, the only logics supported by quantifier elimination are LRA and LIA.

Warning

This function is experimental and may change in future: versions.

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

return:

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 getQuantifierEliminationDisjunct() 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\).

getRealSort(): Get the real sort. :return: Sort Real. .. warning:: This function is deprecated and will be removed in a

future release.

getRegExpSort(): Get the regular expression sort. :return: The sort of regular expressions. .. warning:: This function is deprecated and will be removed in a

future release.

getRoundingModeSort(): Get the rounding mode sort. :return: Sort RoundingMode. .. warning:: This function is deprecated and will be removed in a

future release.

getStatistics(): Return 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.

getStringSort()

Returns:: Sort String.

Warning

This function is deprecated and will be removed in a future release.

getSygusAssumptions(): Get the list of sygus assumptions. :return: The list of sygus assumptions.

getSygusConstraints(): Get the list of sygus constraints. :return: The list of sygus constraints.

getSynthSolution()

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

Parameters:: term – The term for which the synthesis solution is queried.
Returns:: The synthesis solution of the given term.

getSynthSolutions()

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

Parameters:: terms – The terms for which the synthesis solutions is queried.
Returns:: The synthesis solutions of the given terms.

getTermManager(): Get the associated term manager instance. :return: The term manager instance.

getTimeoutCore()

Get a timeout core, which computes a subset of the current assertions that cause a timeout. Note it does not require being proceeded by a call to checkSat.

(get-timeout-core)

Warning

This function is experimental and may change in future versions.

Returns:: The result of the timeout core computation. This is a pair

containing a result and a list of formulas. 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 list of formulas is empty.

This function may make multiple checks for satisfiability internally, each limited by the timeout value given by timeout-core-timeout.

getTimeoutCoreAssuming()

Get a timeout core, which computes a subset of the given assumptions that cause a timeout when added to the current assertions. Note it does not require being proceeded by a call to checkSat.

(get-timeout-core)

Warning

This function is experimental and may change in future versions.

Parameters:: assumptions – The formulas to assume.
Returns:: The result of the timeout core computation. This is a pair containing a result and a list of formulas. If the result is unknown and the reason is timeout, then the list of formulas correspond to a subset of 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 list of formulas plus 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 list of formulas is empty.

This function may make multiple checks for satisfiability internally, each limited by the timeout value given by timeout-core-timeout.

getUnsatAssumptions()

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

SMT-LIB:

( get-unsat-assumptions )

Requires to enable option produce-unsat-assumptions.

Returns:: The set of unsat assumptions.

getUnsatCore()

Get the unsatisfiable core.

SMT-LIB:

(get-unsat-core)

Requires to enable option produce-unsat-cores.

Note

In contrast to SMT-LIB, the 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 method.

Returns:: A set of terms representing the unsatisfiable core.

getUnsatCoreLemmas()

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.

Warning

This function is experimental and may change in future versions.

Returns:: A set of terms representing the lemmas used to derive

unsatisfiability.

getValue()

Get the value of the given term or list of terms in the current model.

SMT-LIB:

( get-value ( <term>* ) )

Parameters:: term_or_list – The term or list of terms for which the value is queried.
Returns:: The value or list of values of the given term or list of terms.

getValueSepHeap()

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

Warning

This function is experimental and may change in future versions.

Returns:: The term for the heap.

getValueSepNil()

When using separation logic, obtain the term for nil.

Warning

This function is experimental and may change in future versions.

Returns:: The term for nil.

getVersion(): Return a string representation of the version of this solver.

isLogicSet()

Is logic set? Returns whether we called setLogic yet for this solver.

Returns:: whether we called setLogic yet for this solver.

isModelCoreSymbol()

This returns False if the model value of free constant v was not essential for showing the satisfiability of the last call to checkSat using the current model. This function will only return false (for any v) if the model-cores option has been set.

Warning

This function is experimental and may change in future versions.

Parameters:: v – The term in question.
Returns:: True if v is a model core symbol.

mkAbstractSort()

Create an abstract sort. An abstract sort represents a sort for a given kind whose parameters and arguments are unspecified.

Parameter kind must be the kind of a sort that can be abstracted, i.e., a sort that has indices or argument sorts. For example, ARRAY_SORT and BITVECTOR_SORT can be passed as the to this function, while INTEGER_SORT and STRING_SORT cannot.

Providing the kind ABSTRACT_SORT as an argument to this method returns the (fully) unspecified sort, denoted ?.

Providing a kind of sort that has no indices and a fixed arity of argument sorts will return the sort of kind whose arguments are the unspecified sort. For example, mkAbstractSort(ARRAY_SORT) will return the sort (ARRAY_SORT ? ?) instead of the abstract sort whose abstract kind is py:obj:ARRAY_SORT <Kind.ARRAY_SORT>.

Parameters:: k – The kind of the abstract sort
Returns:: The abstract sort.

Warning

This function is experimental and may change in future versions.

Warning

This function is deprecated and will be removed in a future release.

mkArraySort()

Create an array sort.

Parameters:

indexSort – The array index sort.
elemSort – The array element sort.

Returns:

The array sort.

Warning

This function is deprecated and will be removed in a future release.

mkBagSort()

Create a bag sort.

Parameters:: elemSort – The sort of the bag elements.
Returns:: The bag sort.

Warning

This function is deprecated and will be removed in a future release.

mkBitVector()

Create bit-vector value.

Supports the following arguments:

Term mkBitVector(int size, int val=0)
Term mkBitVector(int size, string val, int base)

Parameters:

size – The bit-width.
val – An integer representating the value, in the first form. In the second form, a string representing the value.
base – The base of the string representation (second form only).

Returns:

A Term representing a bit-vector value.

Warning

This function is deprecated and will be removed in a future release.

mkBitVectorSort()

Create a bit-vector sort.

Parameters:: size – The bit-width of the bit-vector sort
Returns:: The bit-vector sort

Warning

This function is deprecated and will be removed in a future release.

mkBoolean()

Create a Boolean constant.

Parameters:: val – The value of the constant.
Returns:: The Boolean constant.

Warning

This function is deprecated and will be removed in a future release.

mkCardinalityConstraint()

Create cardinality constraint.

Warning

This function is experimental and may change in future versions.

Parameters:

sort – Sort of the constraint.
index – The upper bound for the cardinality of the sort.

Warning

This function is deprecated and will be removed in a future release.

mkConst()

Create (first-order) constant (0-arity function symbol).

SMT-LIB:

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

Parameters:

sort – The sort of the constant.
symbol – The name of the constant. If None, a default symbol is used.

Returns:

The first-order constant.

Warning

This function is deprecated and will be removed in a future release.

mkConstArray()

Create a constant array with the provided constant value stored at every index

Parameters:

sort – The sort of the constant array (must be an array sort).
val – The constant value to store (must match the sort’s element sort).

Returns:

The constant array term.

Warning

This function is deprecated and will be removed in a future release.

mkDatatypeConstructorDecl()

Create datatype constructor declaration.

Parameters:: name – The name of the constructor.
Returns:: The datatype constructor declaration.

Warning

This function is deprecated and will be removed in a future release.

mkDatatypeDecl()

Create a datatype declaration.

Parameters:

name – The name of the datatype.
isCoDatatype – True if a codatatype is to be constructed.

Returns:

The datatype declaration.

Warning

This function is deprecated and will be removed in a future release.

mkDatatypeSort()

Create a datatype sort.

Parameters:: dtypedecl – The datatype declaration from which the sort is created.
Returns:: The datatype sort.

Warning

This function is deprecated and will be removed in a future release.

mkDatatypeSorts()

Create a vector of datatype sorts using unresolved sorts. The names of the datatype declarations in dtypedecls must be distinct.

When constructing datatypes, unresolved sorts are replaced by the datatype sort constructed for the datatype declaration it is associated with.

Parameters:: dtypedecls – The datatype declarations from which the sort is created.
Returns:: The datatype sorts.

Warning

This function is deprecated and will be removed in a future release.

mkEmptyBag()

Create a constant representing an empty bag of the given sort.

Parameters:: sort – The sort of the bag elements.
Returns:: The empty bag constant.

Warning

This function is deprecated and will be removed in a future release.

mkEmptySequence()

Create an empty sequence of the given element sort.

Parameters:: sort – The element sort of the sequence.
Returns:: The empty sequence with given element sort.

Warning

This function is deprecated and will be removed in a future release.

mkEmptySet()

Create a constant representing an empty set of the given sort.

Parameters:: sort – The sort of the set elements.
Returns:: The empty set constant.

Warning

This function is deprecated and will be removed in a future release.

mkFalse()

Create a Boolean false constant.

Returns:: The false constant.

Warning

This function is deprecated and will be removed in a future release.

mkFiniteFieldElem()

Create finite field value.

Supports the following arguments:

Term mkFiniteFieldElem(int value, Sort sort)
Term mkFiniteFieldElem(string value, Sort sort)
Term mkFiniteFieldElem(string value, Sort sort, int base)

Parameters:

value – The value of the element’s integer representation. An integer or string of base 10 if the base is not explicitly given, and else a string in the given base.
sort – The field to create the element in.
base – The base of the string representation of value.

Returns:

A Term representing a finite field value.

Warning

This function is deprecated and will be removed in a future release.

mkFiniteFieldSort()

Create a finite field sort.

Supports the following arguments:

Sort mkFiniteFieldSort(int size)
Sort mkFiniteFieldSort(string size)
Sort mkFiniteFieldSort(string size, int base)

Parameters:

size – The size of the field. Must be a prime-power. An integer or string of base 10 if the base is not explicitly given, and else a string in the given base.
base – The base of the string representation of size.

Warning

This function is deprecated and will be removed in a future release.

mkFloatingPoint()

Create a floating-point value from a bit-vector given in IEEE-754 format, or from its three IEEE-754 bit-vector value components (sign bit, exponent, significand). Arguments must be either given as (int, int, Term) or (Term, Term, Term).

:param arg0 The size of the exponent or the sign bit. :param arg1 The size of the signifcand or the bit-vector

representing the exponent.

Parameters:: arg2 – The value of the floating-point constant as a bit-vector term or the bit-vector representing the significand.

:return The floating-point value. .. warning:: This function is deprecated and will be removed in a

future release.

mkFloatingPointNaN()

Create a not-a-number (NaN) floating-point constant.

Parameters:

exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

Warning

This function is deprecated and will be removed in a future release.

mkFloatingPointNegInf()

Create a negative infinity floating-point constant.

Parameters:

exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

Warning

This function is deprecated and will be removed in a future release.

mkFloatingPointNegZero()

Create a negative zero (+0.0) floating-point constant.

Parameters:

exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

Warning

This function is deprecated and will be removed in a future release.

mkFloatingPointPosInf()

Create a positive infinity floating-point constant.

Parameters:

exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

Warning

This function is deprecated and will be removed in a future release.

mkFloatingPointPosZero()

Create a positive zero (+0.0) floating-point constant.

Parameters:

exp – Number of bits in the exponent.
sig – Number of bits in the significand.

Returns:

The floating-point constant.

Warning

This function is deprecated and will be removed in a future release.

mkFloatingPointSort()

Create a floating-point sort.

Parameters:

exp – The bit-width of the exponent of the floating-point sort.
sig – The bit-width of the significand of the floating-point sort.

Warning

This function is deprecated and will be removed in a future release.

mkFunctionSort()

Create function sort.

Parameters:

sorts – The sort of the function arguments.
codomain – The sort of the function return value.

Returns:

The function sort.

Warning

This function is deprecated and will be removed in a future release.

mkGrammar()

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

Parameters:

boundVars – The parameters to corresponding synth-fun/synth-inv.
ntSymbols – The pre-declaration of the non-terminal symbols.

Returns:

The grammar.

mkInteger()

Create an integer constant.

Parameters:: val – Representation of the constant: either a string or integer.
Returns:: A constant of sort Integer.

Warning

This function is deprecated and will be removed in a future release.

mkNullableIsNull()

Create a null tester for a nullable term.

Parameters:: term – A nullable term.
Returns:: A tester whether term is null.

Warning

This function is deprecated and will be removed in a future release.

mkNullableIsSome()

Create a some tester for a nullable term.

Parameters:: term – A nullable term.
Returns:: A tester whether term is some.

Warning

This function is deprecated and will be removed in a future release.

mkNullableLift()

Create a term that lifts kind to nullable terms. Example: If we have the term ((_ nullable.lift +) x y), where x, y of type (Nullable Int), then kind would be ADD, and args would be [x, y]. This function would return (nullable.lift (lambda ((a Int) (b Int)) (+ a b)) x y)

Parameters:

kind – The lifted operator.
args – The arguments of the lifted operator.

Returns:

A term of Kind NULLABLE_LIFT where the first child is a lambda expression, and the remaining children are the original arguments.

Warning

This function is deprecated and will be removed in a future release.

mkNullableNull()

Create a constant representing an null of the given sort.

Parameters:: term – The sort of the Nullable element.
Returns:: The null constant.

Warning

This function is deprecated and will be removed in a future release.

mkNullableSome()

Create a nullable some term.

Parameters:: term – The elements value.
Returns:: The element value wrapped in some constructor.

Warning

This function is deprecated and will be removed in a future release.

mkNullableSort()

Create a nullable sort.

Parameters:: elemSort – The sort of the element of the nullable.
Returns:: The nullable sort.

Warning

This function is deprecated and will be removed in a future release.

mkNullableVal()

Create a selector for nullable term.

Parameters:: term – A nullable term.
Returns:: The element value of the nullable term.

Warning

This function is deprecated and will be removed in a future release.

mkOp()

Create operator.

Supports the following arguments:

Op mkOp(Kind kind)
Op mkOp(Kind kind, const string& arg)
Op mkOp(Kind kind, uint32_t arg0, ...)

Warning

This function is deprecated and will be removed in a future release.

mkParamSort()

Create a sort parameter.

Parameters:: symbol – The name of the sort.
Returns:: The sort parameter.

Warning

This function is experimental and may change in future versions.

Warning

This function is deprecated and will be removed in a future release.

mkPi()

Create a constant representing the number Pi.

Returns:: A constant representing PI.

Warning

This function is deprecated and will be removed in a future release.

mkPredicateSort()

Create a predicate sort.

Parameters:: sorts – The list of sorts of the predicate.
Returns:: The predicate sort.

Warning

This function is deprecated and will be removed in a future release.

mkReal()

Create a real constant from a numerator and an optional denominator.

First converts the arguments to a temporary string, either "<numerator>" or "<numerator>/<denominator>". This temporary string is forwarded to cvc5::Solver::mkReal() and should thus represent an integer, a decimal number or a fraction.

Parameters:

numerator – The numerator.
denominator – The denominator, or None.

Returns:

A real term with literal value.

Warning

This function is deprecated and will be removed in a future release.

mkRecordSort()

Create a record sort

Warning

This function is experimental and may change in future versions.

Parameters:: fields – The list of fields of the record.
Returns:: The record sort.
Note:: This function is deprecated and will be removed in a future release.

Warning

This function is experimental and may change in future versions.

Warning

This function is deprecated and will be removed in a future release.

mkRegexpAll()

Create a regular expression all (re.all) term.

Returns:: The all term.

Warning

This function is deprecated and will be removed in a future release.

mkRegexpAllchar()

Create a regular expression allchar (re.allchar) term.

Returns:: The allchar term.

Warning

This function is deprecated and will be removed in a future release.

mkRegexpNone()

Create a regular expression none (re.none) term.

Returns:: The none term.

Warning

This function is deprecated and will be removed in a future release.

mkRoundingMode()

Create a roundingmode constant.

Parameters:: rm – The floating point rounding mode this constant represents.

Warning

This function is deprecated and will be removed in a future release.

mkSepEmp()

Create a separation logic empty term.

Returns:: The separation logic empty term.

Warning

This function is experimental and may change in future versions.

Warning

This function is deprecated and will be removed in a future release.

mkSepNil()

Create a separation logic nil term.

Parameters:: sort – The sort of the nil term.
Returns:: The separation logic nil term.

Warning

This function is experimental and may change in future versions.

Warning

This function is deprecated and will be removed in a future release.

mkSequenceSort()

Create a sequence sort.

Parameters:: elemSort – The sort of the sequence elements
Returns:: The sequence sort.

Warning

This function is deprecated and will be removed in a future release.

mkSetSort()

Create a set sort.

Parameters:: elemSort – The sort of the set elements.
Returns:: The set sort.

Warning

This function is deprecated and will be removed in a future release.

mkSkolem()

Create a skolem.

Parameters:

id – The skolem id.
indices – The indices for the skolem.

Returns:

The skolem with the given id and indices.

mkString()

Create a String constant from a str which may contain SMT-LIB compatible escape sequences like \u1234 to encode unicode characters.

Parameters:

s – The string this constant represents.
useEscSequences – Determines whether escape sequences in s should be converted to the corresponding unicode character

Returns:

The String constant.

Warning

This function is deprecated and will be removed in a future release.

mkTerm()

Create a term.

Supports the following arguments:

Term mkTerm(Kind kind)
Term mkTerm(Op op)
Term mkTerm(Kind kind, *args)
Term mkTerm(Op op, *args)

where *args is a comma-separated list of terms.

Warning

This function is deprecated and will be removed in a future release.

mkTrue()

Create a Boolean true constant.

Returns:: The true constant.

Warning

This function is deprecated and will be removed in a future release.

mkTuple()

Create a tuple term. Terms are automatically converted if sorts are compatible.

Parameters:: terms – The elements in the tuple.
Returns:: The tuple Term.

Warning

This function is deprecated and will be removed in a future release.

mkTupleSort()

Create a tuple sort.

Parameters:: sorts – Of the elements of the tuple.
Returns:: The tuple sort.

Warning

This function is deprecated and will be removed in a future release.

mkUninterpretedSort()

Create an uninterpreted sort.

Parameters:: symbol – The name of the sort.
Returns:: The uninterpreted sort.

Warning

This function is deprecated and will be removed in a future release.

mkUninterpretedSortConstructorSort()

Create a sort constructor sort.

An uninterpreted sort constructor is an uninterpreted sort with arity > 0.

Parameters:

symbol – The symbol of the sort.
arity – The arity of the sort (must be > 0).

Returns:

The sort constructor sort.

Warning

This function is deprecated and will be removed in a future release.

mkUniverseSet()

Create a universe set of the given sort.

Parameters:: sort – The sort of the set elements
Returns:: The universe set constant

Warning

This function is deprecated and will be removed in a future release.

mkUnresolvedDatatypeSort()

Create an unresolved datatype sort.

This is for creating yet unresolved sort placeholders for mutually recursive datatypes.

Parameters:

symbol – The name of the sort.
arity – The number of sort parameters of the sort.

Returns:

The unresolved sort.

Warning

This function is deprecated and will be removed in a future release.

mkVar()

Create a bound variable to be used in a binder (i.e. a quantifier, a lambda, or a witness binder).

Parameters:

sort – The sort of the variable.
symbol – The name of the variable.

Returns:

The variable.

Warning

This function is deprecated and will be removed in a future release.

pop()

Pop nscopes level(s) from the assertion stack.

SMT-LIB:

( pop <numeral> )

Parameters:: nscopes – The number of levels to pop.

proofToString()

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

Warning

This function is experimental and may change in future versions.

Parameters:

proof – A proof, usually obtained from getProof().
format – The proof format used to print the proof. Must be “None” if the proof is not a full proof.
assertionNames – Mapping between assertions and names, if they were given by the user. This is used by the Alethe proof format.

Returns:

The proof printed in the current format.

push()

Push nscopes level(s) to the assertion stack.

SMT-LIB:

( push <numeral> )

Parameters:: nscopes – The number of levels to push.

resetAssertions()

Remove all assertions.

SMT-LIB:

( reset-assertions )

setInfo()

Set info.

SMT-LIB:

( set-info <attribute> )

Parameters:

keyword – The info flag.
value – The value of the info flag.

setLogic()

Set logic.

SMT-LIB:

( set-logic <symbol> )

Parameters:: logic – The logic to set.

setOption()

Set option.

SMT-LIB:

( set-option <option> )

Parameters:

option – The option name.
value – The option value.

simplify()

Simplify a term or formula based on rewriting and (optionally) applying substitutions for solved variables.

If applySubs is true, then for example, if (= x 0) was asserted to this solver, this method may replace occurrences of x with 0.

Warning

This function is experimental and may change in future versions.

Parameters:

t – The term to simplify.
applySubs – Whether to apply substitutions for solved variables.

Returns:

The simplified term.

synthFun()

Synthesize n-ary function following specified syntactic constraints.

SyGuS v2:

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

Parameters:

symbol – The name of the function.
boundVars – The parameters to this function.
sort – The sort of the return value of this function.
grammar – The syntactic constraints.

Returns:

The function.