Sort ¶

class cvc5. Sort ¶

The sort of a cvc5 term.

Wrapper class for cvc5::Sort .

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.

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

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

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.

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.

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.