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