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

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

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.

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 cvc5::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 std :: hash < cvc5 :: Sort >

Hash function for Sorts.

Public Functions

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