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