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
).
Information about a specific option can be retrieved via
cvc5::getOptionInfo()
(see
OptionInfo
).

class
Solver

A cvc5 solver.
Public Functions

Solver
(
)

Constructor.
Warning
This constructor is deprecated and replaced by
Solver::Solver(TermManager&)
. It will be removed in a future release. Returns :

The Solver .

Solver
(
TermManager
&
tm
)

Constructor.
Constructs solver instance from a given term manager instance.
 Parameters :

tm – The associated term manager.
 Returns :

The Solver .

~Solver
(
)

Destructor.

Sort
getBooleanSort
(
)
const

Get the Boolean sort.
Warning
This function is deprecated and replaced by
TermManager::getBooleanSort()
. It will be removed in a future release. Returns :

Sort Boolean.

Sort
getIntegerSort
(
)
const

Get the Integer sort.
Warning
This function is deprecated and replaced by
TermManager::getIntegerSort()
. It will be removed in a future release. Returns :

Sort Integer.

Sort
getRealSort
(
)
const

Get the Real sort.
Warning
This function is deprecated and replaced by
TermManager::getRealSort()
. It will be removed in a future release. Returns :

Sort Real.

Sort
getRegExpSort
(
)
const

Get the regular expression sort.
Warning
This function is deprecated and replaced by
TermManager::getRegExpSort()
. It will be removed in a future release. Returns :

Sort RegExp.

Sort
getRoundingModeSort
(
)
const

Get the rounding mode sort.
Warning
This function is deprecated and replaced by
TermManager::getRoundingModeSort()
. It will be removed in a future release. Returns :

Sort RoundingMode.

Sort
getStringSort
(
)
const

Get the string sort.
Warning
This function is deprecated and replaced by
TermManager::getStringSort()
. It will be removed in a future release. Returns :

Sort String.

Sort
mkArraySort
(
const
Sort
&
indexSort
,
const
Sort
&
elemSort
)
const

Create an array sort.
Warning
This function is deprecated and replaced by
TermManager::mkArraySort()
. It will be removed in a future release. Parameters :


indexSort – The array index sort.

elemSort – The array element sort.

 Returns :

The array sort.

Sort
mkBitVectorSort
(
uint32_t
size
)
const

Create a bitvector sort.
Warning
This function is deprecated and replaced by
TermManager::mkBitVectorSort()
. It will be removed in a future release. Parameters :

size – The bitwidth of the bitvector sort.
 Returns :

The bitvector sort.

Sort
mkFloatingPointSort
(
uint32_t
exp
,
uint32_t
sig
)
const

Create a floatingpoint sort.
Warning
This function is deprecated and replaced by
TermManager::mkFloatingPointSort()
. It will be removed in a future release. Parameters :


exp – The bitwidth of the exponent of the floatingpoint sort.

sig – The bitwidth of the significand of the floatingpoint sort.


Sort
mkFiniteFieldSort
(
const
std
::
string
&
size
,
uint32_t
base
=
10
)
const

Create a finitefield sort from a given string of base n.
Warning
This function is deprecated and replaced by
TermManager::mkFiniteFieldSort()
. It will be removed in a future release. Parameters :


size – The modulus of the field. Must be prime.

base – The base of the string representation of
size
.

 Returns :

The finitefield sort.

Sort
mkDatatypeSort
(
const
DatatypeDecl
&
dtypedecl
)
const

Create a datatype sort.
Warning
This function is deprecated and replaced by
TermManager::mkDatatypeSort()
. It will be removed in a future release. Parameters :

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

The datatype sort.

std
::
vector
<
Sort
>
mkDatatypeSorts
(
const
std
::
vector
<
DatatypeDecl
>
&
dtypedecls
)
const

Create a vector of datatype sorts.
Note
The names of the datatype declarations must be distinct.
Warning
This function is deprecated and replaced by
TermManager::mkDatatypeSorts()
. It will be removed in a future release. Parameters :

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

The datatype sorts.

Sort
mkFunctionSort
(
const
std
::
vector
<
Sort
>
&
sorts
,
const
Sort
&
codomain
)
const

Create function sort.
Warning
This function is deprecated and replaced by
TermManager::mkFunctionSort()
. It will be removed in a future release. Parameters :


sorts – The sort of the function arguments.

codomain – The sort of the function return value.

 Returns :

The function sort.

Sort
mkParamSort
(
const
std
::
optional
<
std
::
string
>
&
symbol
=
std
::
nullopt
)
const

Create a sort parameter.
Warning
This function is experimental and may change in future versions.
Warning
This function is deprecated and replaced by
TermManager::mkParamSort()
. It will be removed in a future release. Parameters :

symbol – The name of the sort.
 Returns :

The sort parameter.

Sort
mkPredicateSort
(
const
std
::
vector
<
Sort
>
&
sorts
)
const

Create a predicate sort.
This is equivalent to calling mkFunctionSort() with the Boolean sort as the codomain.
Warning
This function is deprecated and replaced by
TermManager::mkPredicateSort()
. It will be removed in a future release. Parameters :

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

The predicate sort.

Sort
mkRecordSort
(
const
std
::
vector
<
std
::
pair
<
std
::
string
,
Sort
>
>
&
fields
)
const

Create a record sort
Warning
This function is experimental and may change in future versions.
Warning
This function is deprecated and replaced by
TermManager::mkRecordSort()
. It will be removed in a future release. Parameters :

fields – The list of fields of the record.
 Returns :

The record sort.

Sort
mkSetSort
(
const
Sort
&
elemSort
)
const

Create a set sort.
Warning
This function is deprecated and replaced by
TermManager::mkSetSort()
. It will be removed in a future release. Parameters :

elemSort – The sort of the set elements.
 Returns :

The set sort.

Sort
mkBagSort
(
const
Sort
&
elemSort
)
const

Create a bag sort.
Warning
This function is deprecated and replaced by
TermManager::mkBagSort()
. It will be removed in a future release. Parameters :

elemSort – The sort of the bag elements.
 Returns :

The bag sort.

Sort
mkSequenceSort
(
const
Sort
&
elemSort
)
const

Create a sequence sort.
Warning
This function is deprecated and replaced by
TermManager::mkSequenceSort()
. It will be removed in a future release. Parameters :

elemSort – The sort of the sequence elements.
 Returns :

The sequence sort.

Sort
mkAbstractSort
(
SortKind
k
)
const

Create an abstract sort. An abstract sort represents a sort for a given kind whose parameters and arguments are unspecified.
The kind
k
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 kindk
to this function, while #INTEGER_SORT and #STRING_SORT cannot.Note
Providing the kind #ABSTRACT_SORT as an argument to this function returns the (fully) unspecified sort, denoted
?
.Note
Providing a kind
k
that has no indices and a fixed arity of argument sorts will return the sort of kindk
whose arguments are the unspecified sort. For example,mkAbstractSort(SortKind::ARRAY_SORT)
will return the sort(ARRAY_SORT ? ?)
instead of the abstract sort whose abstract kind is #ARRAY_SORT.Warning
This function is experimental and may change in future versions.
Warning
This function is deprecated and replaced by
TermManager::mkAbstractSort()
. It will be removed in a future release. Parameters :

k – The kind of the abstract sort
 Returns :

The abstract sort.

Sort
mkUninterpretedSort
(
const
std
::
optional
<
std
::
string
>
&
symbol
=
std
::
nullopt
)
const

Create an uninterpreted sort.
Warning
This function is deprecated and replaced by
TermManager::mkUninterpretedSort()
. It will be removed in a future release. Parameters :

symbol – The name of the sort.
 Returns :

The uninterpreted sort.

Sort
mkUnresolvedDatatypeSort
(
const
std
::
string
&
symbol
,
size_t
arity
=
0
)
const

Create an unresolved datatype sort.
This is for creating yet unresolved sort placeholders for mutually recursive parametric datatypes.
Warning
This function is experimental and may change in future versions.
Warning
This function is deprecated and replaced by
TermManager::mkUnresolvedDatatypeSort()
. It will be removed in a future release. Parameters :


symbol – The symbol of the sort.

arity – The number of sort parameters of the sort.

 Returns :

The unresolved sort.

Sort
mkUninterpretedSortConstructorSort
(
size_t
arity
,
const
std
::
optional
<
std
::
string
>
&
symbol
=
std
::
nullopt
)
const

Create an uninterpreted sort constructor sort.
An uninterpreted sort constructor is an uninterpreted sort with arity > 0.
Warning
This function is deprecated and replaced by
TermManager::mkUninterpretedSortConstructorerSort()
. It will be removed in a future release. Parameters :


symbol – The symbol of the sort.

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

 Returns :

The uninterpreted sort constructor sort.

Sort
mkTupleSort
(
const
std
::
vector
<
Sort
>
&
sorts
)
const

Create a tuple sort.
Warning
This function is deprecated and replaced by
TermManager::mkTupleSort()
. It will be removed in a future release. Parameters :

sorts – The sorts of the elements of the tuple.
 Returns :

The tuple sort.

Sort
mkNullableSort
(
const
Sort
&
sort
)
const

Create a nullable sort.
Warning
This function is deprecated and replaced by
TermManager::mkNullableSort()
. It will be removed in a future release. Parameters :

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

The nullable sort.

Term
mkTerm
(
Kind
kind
,
const
std
::
vector
<
Term
>
&
children
=
{
}
)
const

Create nary term of given kind.
Warning
This function is deprecated and replaced by
TermManager::mkTerm()
. It will be removed in a future release. Parameters :


kind – The kind of the term.

children – The children of the term.

 Returns :

The Term

Term
mkTerm
(
const
Op
&
op
,
const
std
::
vector
<
Term
>
&
children
=
{
}
)
const

Create nary term of given kind from a given operator. Create operators with mkOp() .
Warning
This function is deprecated and replaced by
TermManager::mkTerm()
. It will be removed in a future release. Parameters :


op – The operator.

children – The children of the term.

 Returns :

The Term .

Term
mkTuple
(
const
std
::
vector
<
Term
>
&
terms
)
const

Create a tuple term.
Warning
This function is deprecated and replaced by
TermManager::mkTuple()
. It will be removed in a future release. Parameters :

terms – The elements in the tuple.
 Returns :

The tuple Term .

Term
mkNullableSome
(
const
Term
&
term
)
const

Create a nullable some term.
Warning
This function is deprecated and replaced by
TermManager::mkNullableSome()
. It will be removed in a future release. Parameters :

term – The element value.
 Returns :

the Element value wrapped in some constructor.

Term
mkNullableVal
(
const
Term
&
term
)
const

Create a selector for nullable term.
Warning
This function is deprecated and replaced by
TermManager::mkNullableVal()
. It will be removed in a future release. Parameters :

term – A nullable term.
 Returns :

The element value of the nullable term.

Term
mkNullableIsNull
(
const
Term
&
term
)
const

Create a null tester for a nullable term.
Warning
This function is deprecated and replaced by
TermManager::mkNullableisNull()
. It will be removed in a future release. Parameters :

term – A nullable term.
 Returns :

A tester whether term is null.

Term
mkNullableIsSome
(
const
Term
&
term
)
const

Create a some tester for a nullable term.
Warning
This function is deprecated and replaced by
TermManager::mkNullableisSome()
. It will be removed in a future release. Parameters :

term – A nullable term.
 Returns :

A tester whether term is some.

Term
mkNullableNull
(
const
Sort
&
sort
)
const

Create a constant representing an null of the given sort.
Warning
This function is deprecated and replaced by
TermManager::mkNullableNull()
. It will be removed in a future release. Parameters :

sort – The sort of the Nullable element.
 Returns :

The null constant.

Term
mkNullableLift
(
Kind
kind
,
const
std
::
vector
<
Term
>
&
args
)
const

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)
Warning
This function is deprecated and replaced by
TermManager::mkNullableLift()
. It will be removed in a future release. 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.

Op
mkOp
(
Kind
kind
,
const
std
::
vector
<
uint32_t
>
&
args
=
{
}
)
const

Create operator of Kind:

#BITVECTOR_EXTRACT

#BITVECTOR_REPEAT

#BITVECTOR_ROTATE_LEFT

#BITVECTOR_ROTATE_RIGHT

#BITVECTOR_SIGN_EXTEND

#BITVECTOR_ZERO_EXTEND

#DIVISIBLE

#FLOATINGPOINT_TO_FP_FROM_FP

#FLOATINGPOINT_TO_FP_FROM_IEEE_BV

#FLOATINGPOINT_TO_FP_FROM_REAL

#FLOATINGPOINT_TO_FP_FROM_SBV

#FLOATINGPOINT_TO_FP_FROM_UBV

#FLOATINGPOINT_TO_SBV

#FLOATINGPOINT_TO_UBV

#INT_TO_BITVECTOR

#TUPLE_PROJECT
See cvc5::Kind for a description of the parameters.
Note
If
args
is empty, the Op simply wraps the cvc5::Kind . The Kind can be used in Solver::mkTerm directly without creating an Op first.Warning
This function is deprecated and replaced by
TermManager::mkOp()
. It will be removed in a future release. Parameters :


kind – The kind of the operator.

args – The arguments (indices) of the operator.



Op
mkOp
(
Kind
kind
,
const
std
::
string
&
arg
)
const

Create operator of kind:

#DIVISIBLE (to support arbitrary precision integers) See cvc5::Kind for a description of the parameters.
Warning
This function is deprecated and replaced by
TermManager::mkOp()
. It will be removed in a future release. Parameters :


kind – The kind of the operator.

arg – The string argument to this operator.



Term
mkTrue
(
)
const

Create a Boolean true constant.
Warning
This function is deprecated and replaced by
TermManager::mkTrue()
. It will be removed in a future release. Returns :

The true constant.

Term
mkFalse
(
)
const

Create a Boolean false constant.
Warning
This function is deprecated and replaced by
TermManager::mkFalse()
. It will be removed in a future release. Returns :

The false constant.

Term
mkBoolean
(
bool
val
)
const

Create a Boolean constant.
Warning
This function is deprecated and replaced by
TermManager::mkBoolean()
. It will be removed in a future release. Parameters :

val – The value of the constant.
 Returns :

The Boolean constant.

Term
mkPi
(
)
const

Create a constant representing the number Pi.
Warning
This function is deprecated and replaced by
TermManager::mkPi()
. It will be removed in a future release.Warning
This function is deprecated and replaced by
TermManager::mkPi()
. It will be removed in a future release. Returns :

A constant representing Pi.

Term
mkInteger
(
const
std
::
string
&
s
)
const

Create an integer constant from a string.
Warning
This function is deprecated and replaced by
TermManager::mkInteger()
. It will be removed in a future release. Parameters :

s – The string representation of the constant, may represent an integer (e.g., “123”).
 Returns :

A constant of sort Integer assuming
s
represents an integer)

Term
mkInteger
(
int64_t
val
)
const

Create an integer constant from a c++ int.
Warning
This function is deprecated and replaced by
TermManager::mkInteger()
. It will be removed in a future release. Parameters :

val – The value of the constant.
 Returns :

A constant of sort Integer.

Term
mkReal
(
const
std
::
string
&
s
)
const

Create a real constant from a string.
Warning
This function is deprecated and replaced by
TermManager::mkReal()
. It will be removed in a future release. Parameters :

s – The string representation of the constant, may represent an integer (e.g., “123”) or real constant (e.g., “12.34” or “12/34”).
 Returns :

A constant of sort Real.

Term
mkReal
(
int64_t
val
)
const

Create a real constant from an integer.
Warning
This function is deprecated and replaced by
TermManager::mkReal()
. It will be removed in a future release. Parameters :

val – The value of the constant.
 Returns :

A constant of sort Real.

Term
mkReal
(
int64_t
num
,
int64_t
den
)
const

Create a real constant from a rational.
Warning
This function is deprecated and replaced by
TermManager::mkReal()
. It will be removed in a future release. Parameters :


num – The value of the numerator.

den – The value of the denominator.

 Returns :

A constant of sort Real.

Term
mkRegexpAll
(
)
const

Create a regular expression all (re.all) term.
Warning
This function is deprecated and replaced by
TermManager::mkRegExpAll()
. It will be removed in a future release. Returns :

The all term.

Term
mkRegexpAllchar
(
)
const

Create a regular expression allchar (re.allchar) term.
Warning
This function is deprecated and replaced by
TermManager::mkRegExpAllChar()
. It will be removed in a future release. Returns :

The allchar term.

Term
mkRegexpNone
(
)
const

Create a regular expression none (re.none) term.
Warning
This function is deprecated and replaced by
TermManager::mkRegExpNone()
. It will be removed in a future release. Returns :

The none term.

Term
mkEmptySet
(
const
Sort
&
sort
)
const

Create a constant representing an empty set of the given sort.
Warning
This function is deprecated and replaced by
TermManager::mkEmptySet()
. It will be removed in a future release. Parameters :

sort – The sort of the set elements.
 Returns :

The empty set constant.

Term
mkEmptyBag
(
const
Sort
&
sort
)
const

Create a constant representing an empty bag of the given sort.
Warning
This function is deprecated and replaced by
TermManager::mkEmptyBag()
. It will be removed in a future release. Parameters :

sort – The sort of the bag elements.
 Returns :

The empty bag constant.

Term
mkSepEmp
(
)
const

Create a separation logic empty term.
Warning
This function is experimental and may change in future versions.
Warning
This function is deprecated and replaced by
TermManager::mkSepEmp()
. It will be removed in a future release. Returns :

The separation logic empty term.

Term
mkSepNil
(
const
Sort
&
sort
)
const

Create a separation logic nil term.
Warning
This function is experimental and may change in future versions.
Warning
This function is deprecated and replaced by
TermManager::mkSepNil()
. It will be removed in a future release. Parameters :

sort – The sort of the nil term.
 Returns :

The separation logic nil term.

Term
mkString
(
const
std
::
string
&
s
,
bool
useEscSequences
=
false
)
const

Create a String constant from a
std::string
which may contain SMTLIB compatible escape sequences like\u1234
to encode unicode characters.Warning
This function is deprecated and replaced by
TermManager::mkString()
. It will be removed in a future release. 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.

Term
mkString
(
const
std
::
wstring
&
s
)
const

Create a String constant from a
std::wstring
. This function does not support escape sequences asstd::wstring
already supports unicode characters.Warning
This function is deprecated and replaced by
TermManager::mkString()
. It will be removed in a future release. Parameters :

s – The string this constant represents.
 Returns :

The String constant.

Term
mkEmptySequence
(
const
Sort
&
sort
)
const

Create an empty sequence of the given element sort.
Warning
This function is deprecated and replaced by
TermManager::mkEmptySequence()
. It will be removed in a future release. Parameters :

sort – The element sort of the sequence.
 Returns :

The empty sequence with given element sort.

Term
mkUniverseSet
(
const
Sort
&
sort
)
const

Create a universe set of the given sort.
Warning
This function is deprecated and replaced by
TermManager::mkUniverseSet()
. It will be removed in a future release. Parameters :

sort – The sort of the set elements.
 Returns :

The universe set constant.

Term
mkBitVector
(
uint32_t
size
,
uint64_t
val
=
0
)
const

Create a bitvector constant of given size and value.
Note
The given value must fit into a bitvector of the given size.
Warning
This function is deprecated and replaced by
TermManager::mkBitVector()
. It will be removed in a future release. Parameters :


size – The bitwidth of the bitvector sort.

val – The value of the constant.

 Returns :

The bitvector constant.

Term
mkBitVector
(
uint32_t
size
,
const
std
::
string
&
s
,
uint32_t
base
)
const

Create a bitvector constant of a given bitwidth from a given string of base 2, 10 or 16.
Note
The given value must fit into a bitvector of the given size.
Warning
This function is deprecated and replaced by
TermManager::mkBitVector()
. It will be removed in a future release. Parameters :


size – The bitwidth of the constant.

s – The string representation of the constant.

base – The base of the string representation (
2
for binary,10
for decimal, and16
for hexadecimal).

 Returns :

The bitvector constant.

Term
mkFiniteFieldElem
(
const
std
::
string
&
value
,
const
Sort
&
sort
,
uint32_t
base
=
10
)
const

Create a finite field constant in a given field from a given string of base n.
If
size
is the field size, the constant needs not be in the range [0,size). If it is outside this range, it will be reduced modulo size before being constructed.Warning
This function is deprecated and replaced by
TermManager::mkFiniteFieldElem()
. It will be removed in a future release. Parameters :


value – The string representation of the constant.

sort – The field sort.

base – The base of the string representation of
value
.


Term
mkConstArray
(
const
Sort
&
sort
,
const
Term
&
val
)
const

Create a constant array with the provided constant value stored at every index.
Warning
This function is deprecated and replaced by
TermManager::mkConstArray()
. It will be removed in a future release. 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.

Term
mkFloatingPointPosInf
(
uint32_t
exp
,
uint32_t
sig
)
const

Create a positive infinity floatingpoint constant (SMTLIB:
+oo
).Warning
This function is deprecated and replaced by
TermManager::mkFloatingPointPosInf()
. It will be removed in a future release. Parameters :


exp – Number of bits in the exponent.

sig – Number of bits in the significand.

 Returns :

The floatingpoint constant.

Term
mkFloatingPointNegInf
(
uint32_t
exp
,
uint32_t
sig
)
const

Create a negative infinity floatingpoint constant (SMTLIB:
oo
).Warning
This function is deprecated and replaced by
TermManager::mkFloatingPointNegInf()
. It will be removed in a future release. Parameters :


exp – Number of bits in the exponent.

sig – Number of bits in the significand.

 Returns :

The floatingpoint constant.

Term
mkFloatingPointNaN
(
uint32_t
exp
,
uint32_t
sig
)
const

Create a notanumber floatingpoint constant (SMTLIB:
NaN
).Warning
This function is deprecated and replaced by
TermManager::mkFloatingPointNaN()
. It will be removed in a future release. Parameters :


exp – Number of bits in the exponent.

sig – Number of bits in the significand.

 Returns :

The floatingpoint constant.

Term
mkFloatingPointPosZero
(
uint32_t
exp
,
uint32_t
sig
)
const

Create a positive zero floatingpoint constant (SMTLIB: +zero).
Warning
This function is deprecated and replaced by
TermManager::mkFloatingPointPosZero()
. It will be removed in a future release. Parameters :


exp – Number of bits in the exponent.

sig – Number of bits in the significand.

 Returns :

The floatingpoint constant.

Term
mkFloatingPointNegZero
(
uint32_t
exp
,
uint32_t
sig
)
const

Create a negative zero floatingpoint constant (SMTLIB: zero).
Warning
This function is deprecated and replaced by
TermManager::mkFloatingPointNegZero()
. It will be removed in a future release. Parameters :


exp – Number of bits in the exponent.

sig – Number of bits in the significand.

 Returns :

The floatingpoint constant.

Term
mkRoundingMode
(
RoundingMode
rm
)
const

Create a rounding mode value.
Warning
This function is deprecated and replaced by
TermManager::mkRoundingMode()
. It will be removed in a future release. Parameters :

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

The rounding mode value.

Term
mkFloatingPoint
(
uint32_t
exp
,
uint32_t
sig
,
const
Term
&
val
)
const

Create a floatingpoint value from a bitvector given in IEEE754 format.
Warning
This function is deprecated and replaced by
TermManager::mkFloatingPoint()
. It will be removed in a future release. Parameters :


exp – Size of the exponent.

sig – Size of the significand.

val – Value of the floatingpoint constant as a bitvector term.

 Returns :

The floatingpoint value.

Term
mkFloatingPoint
(
const
Term
&
sign
,
const
Term
&
exp
,
const
Term
&
sig
)
const

Create a floatingpoint value from its three IEEE754 bitvector value components (sign bit, exponent, significand).
Warning
This function is deprecated and replaced by
TermManager::mkFloatingPoint()
. It will be removed in a future release. Parameters :


sign – The sign bit.

exp – The bitvector representing the exponent.

sig – The bitvector representing the significand.

 Returns :

The floatingpoint value.

Term
mkCardinalityConstraint
(
const
Sort
&
sort
,
uint32_t
upperBound
)
const

Create a cardinality constraint for an uninterpreted sort.
Warning
This function is experimental and may change in future versions.
Warning
This function is deprecated and replaced by
TermManager::mkCardinalityConstraint()
. It will be removed in a future release. Parameters :


sort – The sort the cardinality constraint is for.

upperBound – The upper bound on the cardinality of the sort.

 Returns :

The cardinality constraint.

Term
mkConst
(
const
Sort
&
sort
,
const
std
::
optional
<
std
::
string
>
&
symbol
=
std
::
nullopt
)
const

Create a free constant.
Note that the returned term is always fresh, even if the same arguments were provided on a previous call to mkConst() .
SMTLIB:
(declareconst <symbol> <sort>) (declarefun <symbol> () <sort>)
Warning
This function is deprecated and replaced by
TermManager::mkConst()
. It will be removed in a future release. Parameters :


sort – The sort of the constant.

symbol – The name of the constant (optional).

 Returns :

The constant.

Term
mkVar
(
const
Sort
&
sort
,
const
std
::
optional
<
std
::
string
>
&
symbol
=
std
::
nullopt
)
const

Create a bound variable to be used in a binder (i.e., a quantifier, a lambda, or a witness binder).
Note that the returned term is always fresh, even if the same arguments were provided on a previous call to mkConst.
Warning
This function is deprecated and replaced by
TermManager::mkVar()
. It will be removed in a future release. Parameters :


sort – The sort of the variable.

symbol – The name of the variable (optional).

 Returns :

The variable.

DatatypeConstructorDecl
mkDatatypeConstructorDecl
(
const
std
::
string
&
name
)

Create a datatype constructor declaration.
Warning
This function is deprecated and replaced by
TermManager::mkDatatypeConstructorDecl()
. It will be removed in a future release. Parameters :

name – The name of the datatype constructor.
 Returns :

The DatatypeConstructorDecl .

DatatypeDecl
mkDatatypeDecl
(
const
std
::
string
&
name
,
bool
isCoDatatype
=
false
)

Create a datatype declaration.
Warning
This function is deprecated and replaced by
TermManager::mkDatatypeDecl()
. It will be removed in a future release. Parameters :


name – The name of the datatype.

isCoDatatype – True if a codatatype is to be constructed.

 Returns :

The DatatypeDecl .

DatatypeDecl
mkDatatypeDecl
(
const
std
::
string
&
name
,
const
std
::
vector
<
Sort
>
&
params
,
bool
isCoDatatype
=
false
)

Create a datatype declaration. Create sorts parameter with Solver::mkParamSort() .
Warning
This function is experimental and may change in future versions.
Warning
This function is deprecated and replaced by
TermManager::mkDatatypeDecl()
. It will be removed in a future release. Parameters :


name – The name of the datatype.

params – A list of sort parameters.

isCoDatatype – True if a codatatype is to be constructed.

 Returns :

The DatatypeDecl .

Term
simplify
(
const
Term
&
t
,
bool
applySubs
=
false
)

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 ofx
with0
.Warning
This function is experimental and may change in future versions.
 Parameters :


t – The term to simplify.

applySubs – True to apply substitutions for solved variables.

 Returns :

The simplified term.

void
assertFormula
(
const
Term
&
term
)
const

Assert a formula.
SMTLIB:
(assert <term>)
 Parameters :

term – The formula to assert.

Result
checkSat
(
)
const

Check satisfiability.
SMTLIB:
(checksat)
 Returns :

The result of the satisfiability check.

Result
checkSatAssuming
(
const
Term
&
assumption
)
const

Check satisfiability assuming the given formula.
SMTLIB:
(checksatassuming ( <prop_literal> ))
 Parameters :

assumption – The formula to assume.
 Returns :

The result of the satisfiability check.

Result
checkSatAssuming
(
const
std
::
vector
<
Term
>
&
assumptions
)
const

Check satisfiability assuming the given formulas.
SMTLIB:
(checksatassuming ( <prop_literal>+ ))
 Parameters :

assumptions – The formulas to assume.
 Returns :

The result of the satisfiability check.

Sort
declareDatatype
(
const
std
::
string
&
symbol
,
const
std
::
vector
<
DatatypeConstructorDecl
>
&
ctors
)
const

Create datatype sort.
SMTLIB:
(declaredatatype <symbol> <datatype_decl>)
 Parameters :


symbol – The name of the datatype sort.

ctors – The constructor declarations of the datatype sort.

 Returns :

The datatype sort.

Term
declareFun
(
const
std
::
string
&
symbol
,
const
std
::
vector
<
Sort
>
&
sorts
,
const
Sort
&
sort
,
bool
fresh
=
true
)
const

Declare nary function symbol.
SMTLIB:
(declarefun <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.

Sort
declareSort
(
const
std
::
string
&
symbol
,
uint32_t
arity
,
bool
fresh
=
true
)
const

Declare uninterpreted sort.
SMTLIB:
(declaresort <symbol> <numeral>)
Note
This corresponds to mkUninterpretedSort(const std::optional<std::string>&) if arity = 0, and to mkUninterpretedSortConstructorSort(size_t arity, const std::optional<std::string>&) if arity > 0.

Term
defineFun
(
const
std
::
string
&
symbol
,
const
std
::
vector
<
Term
>
&
bound_vars
,
const
Sort
&
sort
,
const
Term
&
term
,
bool
global
=
false
)
const

Define nary function.
SMTLIB:
(definefun <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.

global – Determines whether this definition is global (i.e., persists when popping the context).

 Returns :

The function.

Term
defineFunRec
(
const
std
::
string
&
symbol
,
const
std
::
vector
<
Term
>
&
bound_vars
,
const
Sort
&
sort
,
const
Term
&
term
,
bool
global
=
false
)
const

Define recursive function.
SMTLIB:
(definefunrec <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.

global – Determines whether this definition is global (i.e., persists when popping the context).

 Returns :

The function.

Term
defineFunRec
(
const
Term
&
fun
,
const
std
::
vector
<
Term
>
&
bound_vars
,
const
Term
&
term
,
bool
global
=
false
)
const

Define recursive function.
SMTLIB:
(definefunrec <function_def>)
Create parameter
fun
with TermManager::mkConst() . Parameters :


fun – The sorted function.

bound_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
defineFunsRec
(
const
std
::
vector
<
Term
>
&
funs
,
const
std
::
vector
<
std
::
vector
<
Term
>
>
&
bound_vars
,
const
std
::
vector
<
Term
>
&
terms
,
bool
global
=
false
)
const

Define recursive functions.
SMTLIB:
(definefunsrec ( <function_decl>_1 ... <function_decl>_n ) ( <term>_1 ... <term>_n ) )
Create elements of parameter
funs
withTermManager::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).


std
::
vector
<
Term
>
getAssertions
(
)
const

Get the list of asserted formulas.
SMTLIB:
(getassertions)
 Returns :

The list of asserted formulas.

std
::
string
getInfo
(
const
std
::
string
&
flag
)
const

Get info from the solver.
SMTLIB:
(getinfo <info_flag>)
 Returns :

The info.

std
::
string
getOption
(
const
std
::
string
&
option
)
const

Get the value of a given option.
SMTLIB:
(getoption <keyword>)
 Parameters :

option – The option for which the value is queried.
 Returns :

A string representation of the option value.

std
::
vector
<
std
::
string
>
getOptionNames
(
)
const

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

All option names.

OptionInfo
getOptionInfo
(
const
std
::
string
&
option
)
const

Get some information about the given option.
Check the OptionInfo class for more details on which information is available.
 Returns :

Information about the given option.

DriverOptions
getDriverOptions
(
)
const

Get the driver options, which provide access to options that can not be communicated properly via getOption() and getOptionInfo() .
 Returns :

A DriverOptions object.

std
::
vector
<
Term
>
getUnsatAssumptions
(
)
const

Get the set of unsat (“failed”) assumptions.
SMTLIB:
(getunsatassumptions)
Requires to enable option produceunsatassumptions .
 Returns :

The set of unsat assumptions.

std
::
vector
<
Term
>
getUnsatCore
(
)
const

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.
 Returns :

A set of terms representing the unsatisfiable core.

std
::
vector
<
Term
>
getUnsatCoreLemmas
(
)
const

Get the lemmas used to derive unsatisfiability.
SMTLIB:
(getunsatcorelemmas)
Requires the SAT proof unsat core mode, so to enable option unsatcoresmode=satproof .
Warning
This function is experimental and may change in future versions.
 Returns :

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

std
::
map
<
Term
,
Term
>
getDifficulty
(
)
const

Get a difficulty estimate for an asserted formula. This function is intended to be called immediately after any response to a checkSat.
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 solve. Unmentioned assertions can be assumed to have zero difficulty.

std
::
pair
<
Result
,
std
::
vector
<
Term
>
>
getTimeoutCore
(
)
const

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 returned the set of assertions corresponds 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)
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 set of assertions.

std
::
pair
<
Result
,
std
::
vector
<
Term
>
>
getTimeoutCoreAssuming
(
const
std
::
vector
<
Term
>
&
assumptions
)
const

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
checkSat()
.Warning
This function is experimental and may change in future versions.
 Parameters :

assumptions – The (nonempty) set of formulas to assume.
 Returns :

The result of the timeout core computation. This is a pair containing a result and a set of assumptions.

std
::
vector
<
Proof
>
getProof
(
modes
::
ProofComponent
c
=
modes
::
ProofComponent
::
FULL
)
const

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 .
Warning
This function is experimental and may change in future versions.
 Parameters :

c – The component of the proof to return
 Returns :

A vector of proofs.

std
::
string
proofToString
(
Proof
proof
,
modes
::
ProofFormat
format
=
modes
::
ProofFormat
::
DEFAULT
,
const
std
::
map
<
cvc5
::
Term
,
std
::
string
>
&
assertionNames
=
std
::
map
<
cvc5
::
Term
,
std
::
string
>
(
)
)
const

Prints a proof as a string in 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 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
. 
assertionNames – Mapping between assertions and names, if they were given by the user.

 Returns :

The string representation of the proof in the given format.

std
::
vector
<
Term
>
getLearnedLiterals
(
modes
::
LearnedLitType
t
=
modes
::
LearnedLitType
::
INPUT
)
const

Get a list of learned literals that are entailed by the current set of assertions.
Warning
This function is experimental and may change in future versions.
 Parameters :

t – The type of learned literals to return
 Returns :

A list of literals that were learned at toplevel.

Term
getValue
(
const
Term
&
term
)
const

Get the value of the given term in the current model.
SMTLIB:
(getvalue ( <term> ))
 Parameters :

term – The term for which the value is queried.
 Returns :

The value of the given term.

std
::
vector
<
Term
>
getValue
(
const
std
::
vector
<
Term
>
&
terms
)
const

Get the values of the given terms in the current model.
SMTLIB:
(getvalue ( <term>* ))
 Parameters :

terms – The terms for which the value is queried.
 Returns :

The values of the given terms.

std
::
vector
<
Term
>
getModelDomainElements
(
const
Sort
&
s
)
const

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 :

s – The uninterpreted sort in question.
 Returns :

The domain elements of s in the current model.

bool
isModelCoreSymbol
(
const
Term
&
v
)
const

Determine if the model value of the given free constant was essential for showing satisfiability of the last
checkSat()
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 :

v – The term in question.
 Returns :

True if
v
is a model core symbol.

std
::
string
getModel
(
const
std
::
vector
<
Sort
>
&
sorts
,
const
std
::
vector
<
Term
>
&
consts
)
const

Get the model
SMTLIB:
(getmodel)
Requires to enable option producemodels .
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.

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.

Term
getQuantifierElimination
(
const
Term
&
q
)
const

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 :

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


Term
getQuantifierEliminationDisjunct
(
const
Term
&
q
)
const

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 :

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 Solver::getQuantifierEliminationDisjunct() 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
declareSepHeap
(
const
Sort
&
locSort
,
const
Sort
&
dataSort
)
const

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.


Term
getValueSepHeap
(
)
const

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.

Term
getValueSepNil
(
)
const

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.

Term
declarePool
(
const
std
::
string
&
symbol
,
const
Sort
&
sort
,
const
std
::
vector
<
Term
>
&
initValue
)
const

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 :


symbol – The name of the pool.

sort – The sort of the elements of the pool.

initValue – The initial value of the pool.

 Returns :

The pool symbol.

Term
declareOracleFun
(
const
std
::
string
&
symbol
,
const
std
::
vector
<
Sort
>
&
sorts
,
const
Sort
&
sort
,
std
::
function
<
Term
(
const
std
::
vector
<
Term
>
&
)
>
fn
)
const

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 :


symbol – The name of the oracle

sorts – The sorts of the parameters to this function

sort – The sort of the return value of this function

fn – The function that implements the oracle function.

 Returns :

The oracle function

void
addPlugin
(
Plugin
&
p
)

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 :

p – The plugin to add to this solver.

void
pop
(
uint32_t
nscopes
=
1
)
const

Pop (a) level(s) from the assertion stack.
SMTLIB:
(pop <numeral>)
 Parameters :

nscopes – The number of levels to pop.

Term
getInterpolant
(
const
Term
&
conj
)
const

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 :

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.

Term
getInterpolant
(
const
Term
&
conj
,
Grammar
&
grammar
)
const

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 :


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.

Term
getInterpolantNext
(
)
const

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

Term
getAbduct
(
const
Term
&
conj
)
const

Get an abduct.
SMTLIB:
(getabduct <conj>)
Requires to enable option produceabducts .
Warning
This function is experimental and may change in future versions.
 Parameters :

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.

Term
getAbduct
(
const
Term
&
conj
,
Grammar
&
grammar
)
const

Get an abduct.
SMTLIB:
(getabduct <conj> <grammar>)
Requires to enable option produceabducts .
Warning
This function is experimental and may change in future versions.
 Parameters :


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.

Term
getAbductNext
(
)
const

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.
 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
blockModel
(
modes
::
BlockModelsMode
mode
)
const

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 :

mode – The mode to use for blocking.

void
blockModelValues
(
const
std
::
vector
<
Term
>
&
terms
)
const

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 :

terms – The model values to block.

std
::
string
getInstantiations
(
)
const

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

A string that contains information about all instantiations made by the quantifiers module.

void
push
(
uint32_t
nscopes
=
1
)
const

Push (a) level(s) to the assertion stack.
SMTLIB:
(push <numeral>)
 Parameters :

nscopes – The number of levels to push.

void
resetAssertions
(
)
const

Remove all assertions.
SMTLIB:
(resetassertions)

void
setInfo
(
const
std
::
string
&
keyword
,
const
std
::
string
&
value
)
const

Set info.
SMTLIB:
(setinfo <attribute>)
 Parameters :


keyword – The info flag.

value – The value of the info flag.


void
setLogic
(
const
std
::
string
&
logic
)
const

Set logic.
SMTLIB:
(setlogic <symbol>)
 Parameters :

logic – The logic to set.

bool
isLogicSet
(
)
const

Determine if
setLogic()
has been called. Returns :

True if
setLogic()
has already been called for this solver instance.

std
::
string
getLogic
(
)
const

Get the logic set the solver.
Note
Asserts isLogicSet() .
 Returns :

The logic used by the solver.

void
setOption
(
const
std
::
string
&
option
,
const
std
::
string
&
value
)
const

Set option.
SMTLIB:
(setoption :<option> <value>)
 Parameters :


option – The option name.

value – The option value.


Term
declareSygusVar
(
const
std
::
string
&
symbol
,
const
Sort
&
sort
)
const

Append
symbol
to the current list of universal variables.SyGuS v2:
(declarevar <symbol> <sort>)
 Parameters :


sort – The sort of the universal variable.

symbol – The name of the universal variable.

 Returns :

The universal variable.

Grammar
mkGrammar
(
const
std
::
vector
<
Term
>
&
boundVars
,
const
std
::
vector
<
Term
>
&
ntSymbols
)
const

Create a Sygus grammar. The first nonterminal is treated as the starting nonterminal, so the order of nonterminals matters.
 Parameters :


boundVars – The parameters to corresponding synthfun/synthinv.

ntSymbols – The predeclaration of the nonterminal symbols.

 Returns :

The grammar.

Term
synthFun
(
const
std
::
string
&
symbol
,
const
std
::
vector
<
Term
>
&
boundVars
,
const
Sort
&
sort
)
const

Synthesize nary function.
SyGuS v2:
(synthfun <symbol> ( <boundVars>* ) <sort>)
 Parameters :


symbol – The name of the function.

boundVars – The parameters to this function.

sort – The sort of the return value of this function.

 Returns :

The function.

Term
synthFun
(
const
std
::
string
&
symbol
,
const
std
::
vector
<
Term
>
&
boundVars
,
Sort
sort
,
Grammar
&
grammar
)
const

Synthesize nary function following specified syntactic constraints.
SyGuS v2:
(synthfun <symbol> ( <boundVars>* ) <sort> <grammar>)
 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.

void
addSygusConstraint
(
const
Term
&
term
)
const

Add a forumla to the set of Sygus constraints.
SyGuS v2:
(constraint <term>)
 Parameters :

term – The formula to add as a constraint.

std
::
vector
<
Term
>
getSygusConstraints
(
)
const

Get the list of sygus constraints.
 Returns :

The list of sygus constraints.

void
addSygusAssume
(
const
Term
&
term
)
const

Add a forumla to the set of Sygus assumptions.
SyGuS v2:
(assume <term>)
 Parameters :

term – The formula to add as an assumption.

std
::
vector
<
Term
>
getSygusAssumptions
(
)
const

Get the list of sygus assumptions.
 Returns :

The list of sygus assumptions.

void
addSygusInvConstraint
(
const
Term
&
inv
,
const
Term
&
pre
,
const
Term
&
trans
,
const
Term
&
post
)
const

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 :


inv – The functiontosynthesize.

pre – The precondition.

trans – The transition relation.

post – The postcondition.


SynthResult
checkSynth
(
)
const

Try to find a solution for the synthesis conjecture corresponding to the current list of functionstosynthesize, universal variables and constraints.
SyGuS v2:
(checksynth)
 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.

SynthResult
checkSynthNext
(
)
const

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. Requires incremental mode.
SyGuS v2:
(checksynthnext)
 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.

Term
getSynthSolution
(
const
Term
&
term
)
const

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.

std
::
vector
<
Term
>
getSynthSolutions
(
const
std
::
vector
<
Term
>
&
terms
)
const

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.

Term
findSynth
(
modes
::
FindSynthTarget
fst
)
const

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 :

fst – The identifier specifying what kind of term to find
 Returns :

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

Term
findSynth
(
modes
::
FindSynthTarget
fst
,
Grammar
&
grammar
)
const

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 :


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.

Term
findSynthNext
(
)
const

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.
 Returns :

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

Statistics
getStatistics
(
)
const

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.
 Returns :

A snapshot of the current state of the statistic values.

void
printStatisticsSafe
(
int
fd
)
const

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

fd – The file descriptor.

bool
isOutputOn
(
const
std
::
string
&
tag
)
const

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).Requires that a valid tag is given.
 Returns :

True if the given tag is enabled.

std
::
ostream
&
getOutput
(
const
std
::
string
&
tag
)
const

Get an output stream for the given tag.
Tags can be enabled with the
output
option (ando <tag>
on the command line). Raises an exception when an invalid tag is given.Warning
This function is experimental and may change in future versions.
 Parameters :

tag – The output tag.
 Returns :

The output stream.

std
::
string
getVersion
(
)
const

Get a string representation of the version of this solver.
 Returns :

The version string.

TermManager
&
getTermManager
(
)
const

Get the associated term manager instance.
 Returns :

The term manager.
Friends
 friend class parser::Cmd
 friend class main::CommandExecutor

Solver
(
)