TermManager 

This class represents a cvc5 term manager 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 (and thus allows sharing of terms and sorts between solver instances). Term kinds are defined via enum class cvc5::Kind , and sort kinds via enum class cvc5::SortKind .

class TermManager 

A cvc5 term manager.

Public Functions

TermManager ( ) 

Constructor.

~TermManager ( ) 

Destructor.

Statistics getStatistics ( ) const 

Get a snapshot of the current state of the statistic values of this term manager.

Term manager statistics are independent from any solver instance. The returned object is completely decoupled from the term manager 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.

Sort getBooleanSort ( ) 

Get the Boolean sort.

Returns :

Sort Bool .

Sort getIntegerSort ( ) 

Get the Integer sort.

Returns :

Sort Int .

Sort getRealSort ( ) 

Get the Real sort.

Returns :

Sort Real .

Sort getRegExpSort ( ) 

Get the regular expression sort.

Returns :

Sort RegExp .

Sort getRoundingModeSort ( ) 

Get the rounding mode sort.

Returns :

Sort RoundingMode .

Sort getStringSort ( ) 

Get the string sort.

Returns :

Sort String .

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

Create an array sort.

Parameters :

• indexSort – The array index sort.

• elemSort – The array element sort.

Returns :

The array sort.

Sort mkBitVectorSort ( uint32_t size ) 

Create a bit-vector sort.

Parameters :

size – The bit-width of the bit-vector sort.

Returns :

The bit-vector sort.

Sort mkFloatingPointSort ( uint32_t exp , uint32_t sig ) 

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.

Returns :

The floating-point sort.

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

Create a finite-field sort from a given string of base n.

Parameters :

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

• base – The base of the string representation of size .

Returns :

The finite-field sort.

Sort mkDatatypeSort ( const DatatypeDecl & dtypedecl ) 

Create a datatype sort.

Parameters :

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

Returns :

The datatype sort.

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

Create a vector of datatype sorts.

Note

The names of the datatype declarations must be distinct.

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

Create function sort.

Parameters :

• sorts – The sort of the function arguments.

• codomain – The sort of the function return value.

Returns :

The function sort.

Term mkSkolem ( SkolemId id , const std :: vector < Term > & indices ) 

Create a skolem.

Parameters :

• id – The skolem identifier.

• indices – The indices of the skolem.

Returns :

The skolem.

size_t getNumIndicesForSkolemId ( SkolemId id ) 

Get the number of indices for a skolem id.

Parameters :

id – The skolem id.

Returns :

The number of indices for the skolem id.

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

Create a sort parameter.

Warning

This function is experimental and may change in future versions.

Parameters :

symbol – The name of the sort.

Returns :

The sort parameter.

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

Create a predicate sort.

This is equivalent to calling mkFunctionSort() with the Boolean sort as the codomain.

Parameters :

sorts – The list of sorts of the predicate.

Returns :

The predicate sort.

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

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.

Sort mkSetSort ( const Sort & elemSort ) 

Create a set sort.

Parameters :

elemSort – The sort of the set elements.

Returns :

The set sort.

Sort mkBagSort ( const Sort & elemSort ) 

Create a bag sort.

Parameters :

elemSort – The sort of the bag elements.

Returns :

The bag sort.

Sort mkSequenceSort ( const Sort & elemSort ) 

Create a sequence sort.

Parameters :

elemSort – The sort of the sequence elements.

Returns :

The sequence sort.

Sort mkAbstractSort ( SortKind k ) 

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

Parameters :

k – The kind of the abstract sort

Returns :

The abstract sort.

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

Create an uninterpreted sort.

Parameters :

symbol – The name of the sort.

Returns :

The uninterpreted sort.

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

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.

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

Create an uninterpreted 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 uninterpreted sort constructor sort.

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

Create a tuple sort.

Parameters :

sorts – The sorts of the elements of the tuple.

Returns :

The tuple sort.

Sort mkNullableSort ( const Sort & sort ) 

Create a nullable sort.

Parameters :

sort – The sort of the element of the nullable.

Returns :

The nullable sort.

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

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.

Parameters :

• kind – The kind of the operator.

• args – The arguments (indices) of the operator.

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

Create operator of kind:

• #DIVISIBLE (to support arbitrary precision integers) See cvc5::Kind for a description of the parameters.

Parameters :

• kind – The kind of the operator.

• arg – The string argument to this operator.

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

Create n-ary term of given kind.

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 = { } ) 

Create n-ary term of given kind from a given operator.

Create operators with mkOp() .

Parameters :

• op – The operator.

• children – The children of the term.

Returns :

The Term .

Term mkTrue ( ) 

Create a Boolean true constant.

Returns :

The true constant.

Term mkFalse ( ) 

Create a Boolean false constant.

Returns :

The false constant.

Term mkBoolean ( bool val ) 

Create a Boolean constant.

Parameters :

val – The value of the constant.

Returns :

The Boolean constant.

Term mkPi ( ) 

Create a constant representing the number Pi.

Returns :

A constant representing Pi.

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

Create an integer constant from a string.

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

Create an integer constant from a c++ int.

Parameters :

val – The value of the constant.

Returns :

A constant of sort Integer.

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

Create a real constant from a string.

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

Create a real constant from an integer.

Parameters :

val – The value of the constant.

Returns :

A constant of sort Integer.

Term mkReal ( int64_t num , int64_t den ) 

Create a real constant from a rational.

Parameters :

• num – The value of the numerator.

• den – The value of the denominator.

Returns :

A constant of sort Real.

Term mkRegexpAll ( ) 

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

Returns :

The all term.

Term mkRegexpAllchar ( ) 

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

Returns :

The allchar term.

Term mkRegexpNone ( ) 

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

Returns :

The none term.

Term mkEmptySet ( const Sort & sort ) 

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

Parameters :

sort – The sort of the set elements.

Returns :

The empty set constant.

Term mkEmptyBag ( const Sort & sort ) 

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

Parameters :

sort – The sort of the bag elements.

Returns :

The empty bag constant.

Term mkSepEmp ( ) 

Create a separation logic empty term.

Warning

This function is experimental and may change in future versions.

Returns :

The separation logic empty term.

Term mkSepNil ( const Sort & sort ) 

Create a separation logic nil term.

Warning

This function is experimental and may change in future versions.

Parameters :

sort – The sort of the nil term.

Returns :

The separation logic nil term.

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

Create a String constant from a std::string 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.

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

Create a String constant from a std::wstring .

This function does not support escape sequences as std::wstring already supports unicode characters.

Parameters :

s – The string this constant represents.

Returns :

The String constant.

Term mkEmptySequence ( const Sort & sort ) 

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.

Term mkUniverseSet ( const Sort & sort ) 

Create a universe set of the given sort.

Parameters :

sort – The sort of the set elements.

Returns :

The universe set constant.

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

Create a bit-vector constant of given size and value.

Note

The given value must fit into a bit-vector of the given size.

Parameters :

• size – The bit-width of the bit-vector sort.

• val – The value of the constant.

Returns :

The bit-vector constant.

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

Create a bit-vector constant of a given bit-width from a given string of base 2, 10 or 16.

Note

The given value must fit into a bit-vector of the given size.

Parameters :

• size – The bit-width of the constant.

• s – The string representation of the constant.

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

Returns :

The bit-vector constant.

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

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.

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

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.

Term mkFloatingPointPosInf ( uint32_t exp , uint32_t sig ) 

Create a positive infinity floating-point constant (SMT-LIB: +oo ).

Parameters :

• exp – Number of bits in the exponent.

• sig – Number of bits in the significand.

Returns :

The floating-point constant.

Term mkFloatingPointNegInf ( uint32_t exp , uint32_t sig ) 

Create a negative infinity floating-point constant (SMT-LIB: -oo ).

Parameters :

• exp – Number of bits in the exponent.

• sig – Number of bits in the significand.

Returns :

The floating-point constant.

Term mkFloatingPointNaN ( uint32_t exp , uint32_t sig ) 

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

Parameters :

• exp – Number of bits in the exponent.

• sig – Number of bits in the significand.

Returns :

The floating-point constant.

Term mkFloatingPointPosZero ( uint32_t exp , uint32_t sig ) 

Create a positive zero floating-point constant (SMT-LIB: +zero).

Parameters :

• exp – Number of bits in the exponent.

• sig – Number of bits in the significand.

Returns :

The floating-point constant.

Term mkFloatingPointNegZero ( uint32_t exp , uint32_t sig ) 

Create a negative zero floating-point constant (SMT-LIB: -zero).

Parameters :

• exp – Number of bits in the exponent.

• sig – Number of bits in the significand.

Returns :

The floating-point constant.

Term mkRoundingMode ( RoundingMode rm ) 

Create a rounding mode value.

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

Create a floating-point value from a bit-vector given in IEEE-754 format.

Parameters :

• exp – Size of the exponent.

• sig – Size of the significand.

• val – Value of the floating-point constant as a bit-vector term.

Returns :

The floating-point value.

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

Create a floating-point value from its three IEEE-754 bit-vector value components (sign bit, exponent, significand).

Parameters :

• sign – The sign bit.

• exp – The bit-vector representing the exponent.

• sig – The bit-vector representing the significand.

Returns :

The floating-point value.

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

Create a cardinality constraint for an uninterpreted sort.

Warning

This function is experimental and may change in future versions.

Parameters :

• sort – The sort the cardinality constraint is for.

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

Returns :

The cardinality constraint.

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

Create a tuple term.

Parameters :

terms – The elements in the tuple.

Returns :

The tuple Term .

Term mkNullableSome ( const Term & term ) 

Create a nullable some term.

Parameters :

term – The element value.

Returns :

the Element value wrapped in some constructor.

Term mkNullableVal ( const Term & term ) 

Create a selector for nullable term.

Parameters :

term – A nullable term.

Returns :

The element value of the nullable term.

Term mkNullableIsNull ( const Term & term ) 

Create a null tester for a nullable term.

Parameters :

term – A nullable term.

Returns :

A tester whether term is null.

Term mkNullableIsSome ( const Term & term ) 

Create a some tester for a nullable term.

Parameters :

term – A nullable term.

Returns :

A tester whether term is some.

Term mkNullableNull ( const Sort & sort ) 

Create a constant representing an null of the given sort.

Parameters :

sort – The sort of the Nullable element.

Returns :

The null constant.

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

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.

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

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

SMT-LIB:

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

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

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

Note

The returned term is always fresh, even if the same arguments were provided on a previous call to mkConst() .

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.

Parameters :

name – The name of the datatype constructor.

Returns :

The DatatypeConstructorDecl .

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

Create a datatype declaration.

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.

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 .