Sort 

class cvc5. Sort 

The sort of a cvc5 term.

Wrapper class for cvc5::Sort .

getAbstractedKind ( self ) 

Returns :

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

of sorts that this abstract sort denotes.

Warning

This method is experimental and may change in future versions.

getArrayElementSort ( self ) 

Returns :

The array element sort of an array sort.

getArrayIndexSort ( self ) 

Returns :

The array index sort of an array sort.

getBagElementSort ( self ) 

Returns :

The element sort of a bag sort.

getBitVectorSize ( self ) 

Returns :

The bit-width of the bit-vector sort.

getDatatype ( self ) 

Returns :

The underlying datatype of a datatype sort

getDatatypeArity ( self ) 

Returns :

The arity of a datatype sort.

getDatatypeConstructorArity ( self ) 

Returns :

The arity of a datatype constructor sort.

getDatatypeConstructorCodomainSort ( self ) 

Returns :

The codomain sort of a datatype constructor sort.

getDatatypeConstructorDomainSorts ( self ) 

Returns :

The domain sorts of a datatype constructor sort.

getDatatypeSelectorCodomainSort ( self ) 

Returns :

The codomain sort of a datatype selector sort.

getDatatypeSelectorDomainSort ( self ) 

Returns :

The domain sort of a datatype selector sort.

getDatatypeTesterCodomainSort ( self ) 

Returns :

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

getDatatypeTesterDomainSort ( self ) 

Returns :

The domain sort of a datatype tester sort.

getFiniteFieldSize ( self ) 

Returns :

The size of the finite field sort.

getFloatingPointExponentSize ( self ) 

Returns :

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

getFloatingPointSignificandSize ( self ) 

Returns :

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

getFunctionArity ( self ) 

Returns :

The arity of a function sort.

getFunctionCodomainSort ( self ) 

Returns :

The codomain sort of a function sort.

getFunctionDomainSorts ( self ) 

Returns :

The domain sorts of a function sort.

getInstantiatedParameters ( self ) 

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

Warning

This method is experimental and may change in future versions.

Returns :

The SortKind of this sort.

getNullableElementSort ( self ) 

Returns :

The element sort of a nullable sort.

getSequenceElementSort ( self ) 

Returns :

The element sort of a sequence sort.

getSetElementSort ( self ) 

Returns :

The element sort of a set sort.

getSymbol ( self ) 

Note

Asserts hasSymbol() .

Returns :

The raw symbol of the sort.

getTupleLength ( self ) 

Returns :

The length of a tuple sort.

getTupleSorts ( self ) 

Returns :

The element sorts of a tuple sort.

getUninterpretedSortConstructor ( self ) 

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

Returns :

The uninterpreted sort constructor sort

getUninterpretedSortConstructorArity ( self ) 

Returns :

The arity of a sort constructor sort.

hasSymbol ( self ) 

Returns :

True iff this sort has a symbol.

instantiate ( self , params ) 

Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.

Create sorts parameter with Solver.mkParamSort()

Warning

This method is experimental and may change in future versions.

Parameters :

params – The list of sort parameters to instantiate with

Returns :

The instantiated sort

isAbstract ( self ) 

Determine if this is an abstract sort.

Returns :

True if the sort is an abstract sort.

Warning

This method is experimental and may change in future versions.

isArray ( self ) 

Determine if this is an array sort.

Returns :

True if the sort is an array sort.

isBag ( self ) 

Determine if this is a bag sort.

Returns :

True if the sort is a bag sort.

isBitVector ( self ) 

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

Returns :

True if the sort is a bit-vector sort.

isBoolean ( self ) 

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

Returns :

True if the sort is the Boolean sort.

isDatatype ( self ) 

Determine if this is a datatype sort.

Returns :

True if the sort is a datatype sort.

isDatatypeConstructor ( self ) 

Determine if this is a datatype constructor sort.

Returns :

True if the sort is a datatype constructor sort.

isDatatypeSelector ( self ) 

Determine if this is a datatype selector sort.

Returns :

True if the sort is a datatype selector sort.

isDatatypeTester ( self ) 

Determine if this is a tester sort.

Returns :

True if the sort is a selector sort.

isDatatypeUpdater ( self ) 

Determine if this is a datatype updater sort.

Returns :

True if the sort is a datatype updater sort.

isFiniteField ( self ) 

Determine if this is a finite field sort.

Returns :

True if the sort is an array sort.

isFloatingPoint ( self ) 

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

Returns :

True if the sort is a bit-vector sort.

isFunction ( self ) 

Determine if this is a function sort.

Returns :

True if the sort is a function sort.

isInstantiated ( self ) 

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

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

Returns :

True if the sort is the integer sort.

isNull ( self ) 

Returns :

True if this Sort is a null sort.

isNullable ( self ) 

Determine if this is a nullable sort.

Returns :

True if the sort is a nullable sort.

isPredicate ( self ) 

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

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

Returns :

True if the sort is the real sort.

isRecord ( self ) 

Determine if this is a record sort.

Warning

This method is experimental and may change in future versions.

Returns :

True if the sort is a record sort.

isRegExp ( self ) 

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

Returns :

True if the sort is the regexp sort.

isRoundingMode ( self ) 

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

Returns :

True if the sort is the rounding mode sort.

isSequence ( self ) 

Determine if this is a sequence sort.

Returns :

True if the sort is a sequence sort.

isSet ( self ) 

Determine if this is a set sort.

Returns :

True if the sort is a set sort.

isString ( self ) 

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

Returns :

True if the sort is the string sort.

isTuple ( self ) 

Determine if this is a tuple sort.

Returns :

True if the sort is a tuple sort.

isUninterpretedSort ( self ) 

Determine if this is a sort uninterpreted.

Returns :

True if the sort is uninterpreted.

isUninterpretedSortConstructor ( self ) 

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 ( self , sort_or_list_1 , sort_or_list_2 ) 

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