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

• std::ostream& cvc5::operator<< (std::ostream& out, const Sort& s)

• std::hash<cvc5::Sort>

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 a tuple sort.

Returns :

True if this sort is a tuple 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.

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

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

Returns :

The element sorts of a tuple sort.

Friends

friend class parser::Cmd

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 