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:
-
Bag ( Theory of Bags )
-
Created with
cvc5.TermManager.mkBagSort()
-
-
Set ( Theory of Sets and Relations )
-
Created with
cvc5.TermManager.mkSetSort()
-
-
Relation ( Theory of Sets and Relations )
-
Created with
cvc5.TermManager.mkSetSort()as a set of tuple sorts
-
-
Table
-
Created with
cvc5.TermManager.mkBagSort()as a bag of tuple sorts
-
- 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.
-