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 serialized to an output stream
(using
cvc5::operator<<()
).
Class
cvc5::Sort
only provides the default constructor
to create a null Sort. Class
Solver
provides factory functions for all other sorts, e.g.,
cvc5::Solver::getBooleanSort()
for the Boolean sort and
cvc5::Solver::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::Solver::mkBagSort()
-
-
Set ( Theory of Sets and Relations )
-
Created with
cvc5::Solver::mkSetSort()
-
-
Relation ( Theory of Sets and Relations )
-
Created with
cvc5::Solver::mkSetSort()
as a set of tuple sorts
-
-
Table
-
Created with
cvc5::Solver::mkBagSort()
as a bag of tuple sorts
-
-
class
Sort
-
The sort of a cvc5 term.
Public Functions
-
Sort
(
)
-
Constructor.
-
~Sort
(
)
-
Destructor.
-
bool
operator
==
(
const
Sort
&
s
)
const
-
Comparison for structural equality.
- Parameters :
-
s – The sort to compare to.
- Returns :
-
True if the sorts are equal.
-
bool
operator
!=
(
const
Sort
&
s
)
const
-
Comparison for structural disequality.
- Parameters :
-
s – The sort to compare to.
- Returns :
-
True if the sorts are not equal.
-
bool
operator
<
(
const
Sort
&
s
)
const
-
Comparison for ordering on sorts.
- Parameters :
-
s – The sort to compare to.
- Returns :
-
True if this sort is less than s.
-
bool
operator
>
(
const
Sort
&
s
)
const
-
Comparison for ordering on sorts.
- Parameters :
-
s – The sort to compare to.
- Returns :
-
True if this sort is greater than s.
-
bool
operator
<=
(
const
Sort
&
s
)
const
-
Comparison for ordering on sorts.
- Parameters :
-
s – The sort to compare to.
- Returns :
-
True if this sort is less than or equal to s.
-
bool
operator
>=
(
const
Sort
&
s
)
const
-
Comparison for ordering on sorts.
- Parameters :
-
s – The sort to compare to.
- Returns :
-
True if this sort is greater than or equal to s.
-
SortKind
getKind
(
)
const
-
Get the kind of this sort.
Warning
This function is experimental and may change in future versions.
- Returns :
-
The kind of the sort.
-
bool
hasSymbol
(
)
const
-
Determine if this sort has a symbol (a name).
For example, uninterpreted sorts and uninterpreted sort constructors have symbols.
- Returns :
-
True if the sort has a symbol.
-
std
::
string
getSymbol
(
)
const
-
Get the symbol of this Sort .
The symbol of this sort is the string that was provided when constructing it via Solver::mkUninterpretedSort(const std::string&) const, Solver::mkUnresolvedSort(const std::string&, size_t) const, or Solver::mkUninterpretedSortConstructorSort(const std::string&, size_t).
Note
Asserts hasSymbol() .
- Returns :
-
The raw symbol of the sort.
-
bool
isNull
(
)
const
-
Determine if this is the null sort ( Sort::Sort() ).
- Returns :
-
True if this Sort is the null sort.
-
bool
isBoolean
(
)
const
-
Determine if this is the Boolean sort (SMT-LIB:
Bool
).- Returns :
-
True if this sort is the Boolean sort.
-
bool
isInteger
(
)
const
-
Determine if this is the integer sort (SMT-LIB:
Int
).- Returns :
-
True if this sort is the integer sort.
-
bool
isReal
(
)
const
-
Determine if this is the real sort (SMT-LIB:
Real
).- Returns :
-
True if this sort is the real sort.
-
bool
isString
(
)
const
-
Determine if this is the string sort (SMT-LIB:
String
).- Returns :
-
True if this sort is the string sort.
-
bool
isRegExp
(
)
const
-
Determine if this is the regular expression sort (SMT-LIB:
RegLan
).- Returns :
-
True if this sort is the regular expression sort.
-
bool
isRoundingMode
(
)
const
-
Determine if this is the rounding mode sort (SMT-LIB:
RoundingMode
).- Returns :
-
True if this sort is the rounding mode sort.
-
bool
isBitVector
(
)
const
-
Determine if this is a bit-vector sort (SMT-LIB:
(_ BitVec i)
).- Returns :
-
True if this sort is a bit-vector sort.
-
bool
isFloatingPoint
(
)
const
-
Determine if this is a floatingpoint sort (SMT-LIB:
(_ FloatingPoint eb sb)
).- Returns :
-
True if this sort is a floating-point sort.
-
bool
isDatatype
(
)
const
-
Determine if this is a datatype sort.
- Returns :
-
True if this sort is a datatype sort.
-
bool
isDatatypeConstructor
(
)
const
-
Determine if this is a datatype constructor sort.
- Returns :
-
True if this sort is a datatype constructor sort.
-
bool
isDatatypeSelector
(
)
const
-
Determine if this is a datatype selector sort.
- Returns :
-
True if this sort is a datatype selector sort.
-
bool
isDatatypeTester
(
)
const
-
Determine if this is a datatype tester sort.
- Returns :
-
True if this sort is a datatype tester sort.
-
bool
isDatatypeUpdater
(
)
const
-
Determine if this is a datatype updater sort.
- Returns :
-
True if this sort is a datatype updater sort.
-
bool
isFunction
(
)
const
-
Determine if this is a function sort.
- Returns :
-
True if this sort is a function sort.
-
bool
isPredicate
(
)
const
-
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 this sort is a predicate sort.
-
bool
isTuple
(
)
const
-
Determine if this is a tuple sort.
- Returns :
-
True if this sort is a tuple sort.
-
bool
isNullable
(
)
const
-
Determine if this is a nullable sort.
- Returns :
-
True if the sort is a nullable sort.
-
bool
isRecord
(
)
const
-
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.
-
bool
isArray
(
)
const
-
Determine if this is an array sort.
- Returns :
-
True if the sort is an array sort.
-
bool
isFiniteField
(
)
const
-
Determine if this is a finite field sort.
- Returns :
-
True if the sort is a finite field sort.
-
bool
isSet
(
)
const
-
Determine if this is a Set sort.
- Returns :
-
True if the sort is a Set sort.
-
bool
isBag
(
)
const
-
Determine if this is a Bag sort.
- Returns :
-
True if the sort is a Bag sort.
-
bool
isSequence
(
)
const
-
Determine if this is a Sequence sort.
- Returns :
-
True if the sort is a Sequence sort.
-
bool
isAbstract
(
)
const
-
Determine if this is an abstract sort.
Warning
This function is experimental and may change in future versions.
- Returns :
-
True if the sort is a abstract sort.
-
bool
isUninterpretedSort
(
)
const
-
Determine if this is an uninterpreted sort.
- Returns :
-
True if this is an uninterpreted sort.
-
bool
isUninterpretedSortConstructor
(
)
const
-
Determine if this is an uninterpreted sort constructor.
An uninterpreted sort constructor has arity > 0 and can be instantiated to construct uninterpreted sorts with given sort parameters.
- Returns :
-
True if this is of sort constructor kind.
-
bool
isInstantiated
(
)
const
-
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 with sort arguments (see Sort::instantiate(const std::vector<Sort>&) const )).
- Returns :
-
True if this is an instantiated sort.
-
Sort
getUninterpretedSortConstructor
(
)
const
-
Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.
- Returns :
-
The uninterpreted sort constructor sort.
-
Sort
instantiate
(
const
std
::
vector
<
Sort
>
&
params
)
const
-
Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.
Create sort parameters with Solver::mkParamSort() .
- Parameters :
-
params – The list of sort parameters to instantiate with.
- Returns :
-
The instantiated sort.
-
std
::
vector
<
Sort
>
getInstantiatedParameters
(
)
const
-
Get the sorts used to instantiate the sort parameters of a parametric sort (parametric datatype or uninterpreted sort constructor sort, see Sort::instantiate(const std::vector<Sort>& const)).
- Returns :
-
The sorts used to instantiate the sort parameters of a parametric sort
-
Sort
substitute
(
const
Sort
&
sort
,
const
Sort
&
replacement
)
const
-
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.
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 – The subsort to be substituted within this sort.
-
replacement – The sort replacing the substituted subsort.
-
-
Sort
substitute
(
const
std
::
vector
<
Sort
>
&
sorts
,
const
std
::
vector
<
Sort
>
&
replacements
)
const
-
Simultaneous 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 sorts contains duplicates, the replacement earliest in the vector takes priority.
Warning
This function is experimental and may change in future versions.
- Parameters :
-
-
sorts – The subsorts to be substituted within this sort.
-
replacements – The sort replacing the substituted subsorts.
-
-
void
toStream
(
std
::
ostream
&
out
)
const
-
Output a string representation of this sort to a given stream.
- Parameters :
-
out – The output stream.
-
std
::
string
toString
(
)
const
-
- Returns :
-
A string representation of this sort.
-
size_t
getDatatypeConstructorArity
(
)
const
-
- Returns :
-
The arity of a datatype constructor sort.
-
std
::
vector
<
Sort
>
getDatatypeConstructorDomainSorts
(
)
const
-
- Returns :
-
The domain sorts of a datatype constructor sort.
-
Sort
getDatatypeConstructorCodomainSort
(
)
const
-
- Returns :
-
The codomain sort of a constructor sort.
-
Sort
getDatatypeSelectorDomainSort
(
)
const
-
- Returns :
-
The domain sort of a datatype selector sort.
-
Sort
getDatatypeSelectorCodomainSort
(
)
const
-
- Returns :
-
The codomain sort of a datatype selector sort.
-
Sort
getDatatypeTesterCodomainSort
(
)
const
-
Note
We mainly need this for the symbol table, which doesn’t have access to the solver object.
- Returns :
-
The codomain sort of a datatype tester sort, which is the Boolean sort.
-
size_t
getFunctionArity
(
)
const
-
- Returns :
-
The arity of a function sort.
-
std
::
vector
<
Sort
>
getFunctionDomainSorts
(
)
const
-
- Returns :
-
The domain sorts of a function sort.
-
SortKind
getAbstractedKind
(
)
const
-
Warning
This function is experimental and may change in future versions.
- Returns :
-
The sort kind of an abstract sort, which denotes the kind of sorts that this abstract sort denotes.
-
size_t
getUninterpretedSortConstructorArity
(
)
const
-
- Returns :
-
The arity of an uninterpreted sort constructor sort.
-
uint32_t
getBitVectorSize
(
)
const
-
- Returns :
-
The bit-width of the bit-vector sort.
-
std
::
string
getFiniteFieldSize
(
)
const
-
- Returns :
-
The size of the finite field sort.
-
uint32_t
getFloatingPointExponentSize
(
)
const
-
- Returns :
-
The bit-width of the exponent of the floating-point sort.
-
uint32_t
getFloatingPointSignificandSize
(
)
const
-
- Returns :
-
The width of the significand of the floating-point sort.
-
size_t
getDatatypeArity
(
)
const
-
Get the arity of a datatype sort, which is the number of type parameters if the datatype is parametric, or 0 otherwise.
- Returns :
-
The arity of a datatype sort.
-
size_t
getTupleLength
(
)
const
-
- Returns :
-
The length of a tuple sort.
Friends
- friend class parser::Cmd
- friend struct std::hash< Sort >
-
Sort
(
)
-
std
::
ostream
&
cvc5
::
operator
<<
(
std
::
ostream
&
out
,
const
Sort
&
s
)
-
Serialize a sort to given stream.
- Parameters :
-
-
out – The output stream.
-
s – The sort to be serialized to the given output stream.
-
- Returns :
-
The output stream.