Sort

The Sort class represents the sort of a Term .

A Sort can be hashed (using std::hash<cvc5::Sort> ) and serialized to an output stream (using cvc5::operator<<() ).

Class Sort offers the default constructor only to create a null Sort. Instead, the Solver class provides factory functions for all other sorts, e.g., cvc5::Solver::getBooleanSort() for Sort Bool 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:

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

Warning

This method is experimental and may change in future versions.

Returns :

The kind of the sort.

bool hasSymbol ( ) const

Does this sort have a symbol, that is, 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 a tuple sort.

Returns :

True if this sort is a tuple sort.

bool isRecord ( ) const

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.

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

Datatype getDatatype ( ) const
Returns :

The underlying datatype of a datatype 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 method 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 method 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 getDatatypeTesterDomainSort ( ) const
Returns :

The domain sort of a datatype tester 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.

Sort getFunctionCodomainSort ( ) const
Returns :

The codomain sort of a function sort.

Sort getArrayIndexSort ( ) const
Returns :

The array index sort of an array sort.

Sort getArrayElementSort ( ) const
Returns :

The array element sort of an array sort.

Sort getSetElementSort ( ) const
Returns :

The element sort of a set sort.

Sort getBagElementSort ( ) const
Returns :

The element sort of a bag sort.

Sort getSequenceElementSort ( ) const
Returns :

The element sort of a sequence sort.

SortKind getAbstractedKind ( ) const

Warning

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

std :: vector < Sort > getTupleSorts ( ) const
Returns :

The element sorts of a tuple sort.

Friends

friend class parser::Command
friend struct std::hash< 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.

template < >
struct hash < cvc5 :: Sort >

Hash function for Sorts.

Public Functions

size_t operator () ( const cvc5 :: Sort & s ) const