Sort

The Sort class represents the sort of a Term. Its kind is represented as enum class cvc5.SortKind.

A Sort can be hashed (using std.hash<cvc5.Sort>) and represented as a string (using cvc5.Sort.__str__()).

Class cvc5.Sort only provides the default constructor to create a null Sort. Class TermManager provides factory functions for all other sorts, e.g., cvc5.TermManager.getBooleanSort() for the Boolean sort and cvc5.TermManager.mkBitVectorSort() for bit-vector sorts.

Sorts are defined as standardized in the SMT-LIB standard for standardized theories. Additionally, we introduce the following sorts for non-standardized theories:

class cvc5.Sort

The sort of a cvc5 term.

Wrapper class for cvc5::Sort.

getAbstractedKind()
Returns:

The sort kind of an abstract sort, which denotes the kind

of sorts that this abstract sort denotes.

Warning

This function is experimental and may change in future versions.

getArrayElementSort()
Returns:

The array element sort of an array sort.

getArrayIndexSort()
Returns:

The array index sort of an array sort.

getBagElementSort()
Returns:

The element sort of a bag sort.

getBitVectorSize()
Returns:

The bit-width of the bit-vector sort.

getDatatype()
Returns:

The underlying datatype of a datatype sort

getDatatypeArity()
Returns:

The arity of a datatype sort.

getDatatypeConstructorArity()
Returns:

The arity of a datatype constructor sort.

getDatatypeConstructorCodomainSort()
Returns:

The codomain sort of a datatype constructor sort.

getDatatypeConstructorDomainSorts()
Returns:

The domain sorts of a datatype constructor sort.

getDatatypeSelectorCodomainSort()
Returns:

The codomain sort of a datatype selector sort.

getDatatypeSelectorDomainSort()
Returns:

The domain sort of a datatype selector sort.

getDatatypeTesterCodomainSort()
Returns:

the codomain sort of a datatype tester sort, which is the Boolean sort

getDatatypeTesterDomainSort()
Returns:

The domain sort of a datatype tester sort.

getFiniteFieldSize()
Returns:

The size of the finite field sort.

getFloatingPointExponentSize()
Returns:

The bit-width of the exponent of the floating-point sort.

getFloatingPointSignificandSize()
Returns:

The width of the significand of the floating-point sort.

getFunctionArity()
Returns:

The arity of a function sort.

getFunctionCodomainSort()
Returns:

The codomain sort of a function sort.

getFunctionDomainSorts()
Returns:

The domain sorts of a function sort.

getInstantiatedParameters()

Get the sorts used to instantiate the sort parameters of a parametric sort (parametric datatype or uninterpreted sort constructor sort, see instantiate()).

Returns:

The sorts used to instantiate the sort parameters of a parametric sort

getKind()

Warning

This function is experimental and may change in future versions.

Returns:

The SortKind of this sort.

getNullableElementSort()
Returns:

The element sort of a nullable sort.

getSequenceElementSort()
Returns:

The element sort of a sequence sort.

getSetElementSort()
Returns:

The element sort of a set sort.

getSymbol()

Note

Asserts hasSymbol().

Returns:

The raw symbol of the sort.

getTupleLength()
Returns:

The length of a tuple sort.

getTupleSorts()
Returns:

The element sorts of a tuple sort.

getUninterpretedSortConstructor()

Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.

Returns:

The uninterpreted sort constructor sort

getUninterpretedSortConstructorArity()
Returns:

The arity of a sort constructor sort.

hasSymbol()
Returns:

True iff this sort has a symbol.

instantiate()

Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.

Create sorts parameter with TermManager.mkParamSort()

Warning

This function is experimental and may change in future versions.

Parameters:

params – The list of sort parameters to instantiate with

Returns:

The instantiated sort

isAbstract()

Determine if this is an abstract sort.

Returns:

True if the sort is an abstract sort.

Warning

This function is experimental and may change in future versions.

isArray()

Determine if this is an array sort.

Returns:

True if the sort is an array sort.

isBag()

Determine if this is a bag sort.

Returns:

True if the sort is a bag sort.

isBitVector()

Determine if this is a bit-vector sort (SMT-LIB: (_ BitVec i)).

Returns:

True if the sort is a bit-vector sort.

isBoolean()

Determine if this is the Boolean sort (SMT-LIB: Bool).

Returns:

True if the sort is the Boolean sort.

isDatatype()

Determine if this is a datatype sort.

Returns:

True if the sort is a datatype sort.

isDatatypeConstructor()

Determine if this is a datatype constructor sort.

Returns:

True if the sort is a datatype constructor sort.

isDatatypeSelector()

Determine if this is a datatype selector sort.

Returns:

True if the sort is a datatype selector sort.

isDatatypeTester()

Determine if this is a tester sort.

Returns:

True if the sort is a selector sort.

isDatatypeUpdater()

Determine if this is a datatype updater sort.

Returns:

True if the sort is a datatype updater sort.

isFiniteField()

Determine if this is a finite field sort.

Returns:

True if the sort is an array sort.

isFloatingPoint()

Determine if this is a floatingpoint sort (SMT-LIB: (_ FloatingPoint eb sb)).

Returns:

True if the sort is a bit-vector sort.

isFunction()

Determine if this is a function sort.

Returns:

True if the sort is a function sort.

isInstantiated()

Determine if this is an instantiated (parametric datatype or uninterpreted sort constructor) sort.

An instantiated sort is a sort that has been constructed from instantiating a sort parameters with sort arguments (see instantiate()).

Returns:

True if this is an instantiated sort.

isInteger()

Determine if this is the integer sort (SMT-LIB: Int).

Returns:

True if the sort is the integer sort.

isNull()
Returns:

True if this Sort is a null sort.

isNullable()

Determine if this is a nullable sort.

Returns:

True if the sort is a nullable sort.

isPredicate()

Determine if this is a predicate sort.

A predicate sort is a function sort that maps to the Boolean sort. All predicate sorts are also function sorts.

Returns:

True if the sort is a predicate sort.

isReal()

Determine if this is the real sort (SMT-LIB: Real).

Returns:

True if the sort is the real sort.

isRecord()

Determine if this is a record sort.

Warning

This function is experimental and may change in future versions.

Returns:

True if the sort is a record sort.

isRegExp()

Determine if this is the regular expression sort (SMT-LIB: RegLan).

Returns:

True if the sort is the regexp sort.

isRoundingMode()

Determine if this is the rounding mode sort (SMT-LIB: RoundingMode).

Returns:

True if the sort is the rounding mode sort.

isSequence()

Determine if this is a sequence sort.

Returns:

True if the sort is a sequence sort.

isSet()

Determine if this is a set sort.

Returns:

True if the sort is a set sort.

isString()

Determine if this is the string sort (SMT-LIB: String).

Returns:

True if the sort is the string sort.

isTuple()

Determine if this is a tuple sort.

Returns:

True if the sort is a tuple sort.

isUninterpretedSort()

Determine if this is a sort uninterpreted.

Returns:

True if the sort is uninterpreted.

isUninterpretedSortConstructor()

Determine if this is a sort constructor kind.

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

Returns:

True if this a sort constructor kind.

substitute()

Substitution of Sorts.

Note that this replacement is applied during a pre-order traversal and only once to the sort. It is not run until fix point. In the case that sort_or_list_1 contains duplicates, the replacement earliest in the list takes priority.

For example, (Array A B) .substitute([A, C], [(Array C D), (Array A B)]) will return (Array (Array C D) B).

Warning

This function is experimental and may change in future versions.

Parameters:

  • sort_or_list_1 – The subsort or subsorts to be substituted within this sort.

  • sort_or_list_2 – The sort or list of sorts replacing the substituted subsort.