Cvc5Sort 

The Cvc5Sort struct represents the sort of a Cvc5Term . Its kind is represented as enum Cvc5SortKind .

A Cvc5Sort can be hashed (using cvc5_sort_hash() ) represented as a string (via cvc5_sort_to_string() ).

Cvc5Sort instances are created via factory functions associated with a Cvc5TermManager instance, e.g., cvc5_get_boolean_sort() for the Boolean sort and cvc5_mk_bv_sort() 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_mk_bag_sort()

• Set ( Theory of Sets and Relations )

  • Created with cvc5_mk_set_sort()

• Relation ( Theory of Sets and Relations )

  • Created with cvc5_mk_set_sort() as a set of tuple sorts

• Table

  • Created with cvc5_mk_bag_sort() as a bag of tuple sorts

typedef struct cvc5_sort_t * Cvc5Sort 

The sort of a cvc5 term.

Cvc5Sort cvc5_sort_copy ( Cvc5Sort sort ) 

Make copy of sort, increases reference counter of sort .

Note

This step is optional and allows users to manage resources in a more fine-grained manner.

Parameters :

sort – The sort to copy.

Returns :

The same sort with its reference count increased by one.

void cvc5_sort_release ( Cvc5Sort sort ) 

Release copy of sort, decrements reference counter of sort .

Note

This step is optional and allows users to release resources in a more fine-grained manner. Further, any API function that returns a Cvc5Sort returns a copy that is owned by the callee of the function and thus, can be released.

Parameters :

sort – The sort to release.

bool cvc5_sort_is_equal ( Cvc5Sort a , Cvc5Sort b ) 

Compare two sorts for structural equality.

Parameters :

• a – The first sort.

• b – The second sort.

Returns :

True if the sorts are equal.

bool cvc5_sort_is_disequal ( Cvc5Sort a , Cvc5Sort b ) 

Compare two sorts for structural disequality.

Parameters :

• a – The first sort.

• b – The second sort.

Returns :

True if the sorts are not equal.

int64_t cvc5_sort_compare ( Cvc5Sort a , Cvc5Sort b ) 

Compare two sorts for ordering.

Parameters :

• a – The first sort.

• b – The second sort.

Returns :

An integer value indicating the ordering: 0 if both sorts are equal, -1 if a < b , and 1 if b > a .

Cvc5SortKind cvc5_sort_get_kind ( Cvc5Sort sort ) 

Get the kind of the given sort.

Warning

This function is experimental and may change in future versions.

Parameters :

sort – The sort.

Returns :

The kind of the sort.

bool cvc5_sort_has_symbol ( Cvc5Sort sort ) 

Determine if the given sort has a symbol (a name).

For example, uninterpreted sorts and uninterpreted sort constructors have symbols.

Parameters :

sort – The sort.

Returns :

True if the sort has a symbol.

const char * cvc5_sort_get_symbol ( Cvc5Sort sort ) 

Get the symbol of this Sort.

The symbol of this sort is the string that was provided when constructing it via cvc5_mk_uninterpreted_sort(), cvc5_mk_unresolved_sort(), or cvc5_mk_uninterpreted_sort_constructor_sort().

Note

Asserts cvc5_sort_has_symbol() .

Note

The returned char* pointer is only valid until the next call to this function.

Parameters :

sort – The sort.

Returns :

The raw symbol of the sort.

bool cvc5_sort_is_boolean ( Cvc5Sort sort ) 

Determine if given sort is the Boolean sort (SMT-LIB: Bool ).

Parameters :

sort – The sort.

Returns :

True if given sort is the Boolean sort.

bool cvc5_sort_is_integer ( Cvc5Sort sort ) 

Determine if given sort is the integer sort (SMT-LIB: Int ).

Parameters :

sort – The sort.

Returns :

True if given sort is the integer sort.

bool cvc5_sort_is_real ( Cvc5Sort sort ) 

Determine if given sort is the real sort (SMT-LIB: Real ).

Parameters :

sort – The sort.

Returns :

True if given sort is the real sort.

bool cvc5_sort_is_string ( Cvc5Sort sort ) 

Determine if given sort is the string sort (SMT-LIB: String ).

Parameters :

sort – The sort.

Returns :

True if given sort is the string sort.

bool cvc5_sort_is_regexp ( Cvc5Sort sort ) 

Determine if given sort is the regular expression sort (SMT-LIB: RegLan ).

Parameters :

sort – The sort.

Returns :

True if given sort is the regular expression sort.

bool cvc5_sort_is_rm ( Cvc5Sort sort ) 

Determine if given sort is the rounding mode sort (SMT-LIB: Cvc5RoundingMode ).

Parameters :

sort – The sort.

Returns :

True if given sort is the rounding mode sort.

bool cvc5_sort_is_bv ( Cvc5Sort sort ) 

Determine if given sort is a bit-vector sort (SMT-LIB: (_ BitVec i) ).

Parameters :

sort – The sort.

Returns :

True if given sort is a bit-vector sort.

bool cvc5_sort_is_fp ( Cvc5Sort sort ) 

Determine if given sort is a floatingpoint sort (SMT-LIB: (_ FloatingPoint eb sb) ).

Parameters :

sort – The sort.

Returns :

True if given sort is a floating-point sort.

bool cvc5_sort_is_dt ( Cvc5Sort sort ) 

Determine if given sort is a datatype sort.

Parameters :

sort – The sort.

Returns :

True if given sort is a datatype sort.

bool cvc5_sort_is_dt_constructor ( Cvc5Sort sort ) 

Determine if given sort is a datatype constructor sort.

Parameters :

sort – The sort.

Returns :

True if given sort is a datatype constructor sort.

bool cvc5_sort_is_dt_selector ( Cvc5Sort sort ) 

Determine if given sort is a datatype selector sort.

Parameters :

sort – The sort.

Returns :

True if given sort is a datatype selector sort.

bool cvc5_sort_is_dt_tester ( Cvc5Sort sort ) 

Determine if given sort is a datatype tester sort.

Parameters :

sort – The sort.

Returns :

True if given sort is a datatype tester sort.

bool cvc5_sort_is_dt_updater ( Cvc5Sort sort ) 

Determine if given sort is a datatype updater sort.

Parameters :

sort – The sort.

Returns :

True if given sort is a datatype updater sort.

bool cvc5_sort_is_fun ( Cvc5Sort sort ) 

Determine if given sort is a function sort.

Parameters :

sort – The sort.

Returns :

True if given sort is a function sort.

bool cvc5_sort_is_predicate ( Cvc5Sort sort ) 

Determine if given sort is a predicate sort.

A predicate sort is a function sort that maps to the Boolean sort. All predicate sorts are also function sorts.

Parameters :

sort – The sort.

Returns :

True if given sort is a predicate sort.

bool cvc5_sort_is_tuple ( Cvc5Sort sort ) 

Determine if given sort is a tuple sort.

Parameters :

sort – The sort.

Returns :

True if given sort is a tuple sort.

bool cvc5_sort_is_nullable ( Cvc5Sort sort ) 

Determine if given sort is a nullable sort.

Parameters :

sort – The sort.

Returns :

True if given sort is a nullable sort.

bool cvc5_sort_is_record ( Cvc5Sort sort ) 

Determine if given sort is a record sort.

Warning

This function is experimental and may change in future versions.

Parameters :

sort – The sort.

Returns :

True if the sort is a record sort.

bool cvc5_sort_is_array ( Cvc5Sort sort ) 

Determine if given sort is an array sort.

Parameters :

sort – The sort.

Returns :

True if the sort is an array sort.

bool cvc5_sort_is_ff ( Cvc5Sort sort ) 

Determine if given sort is a finite field sort.

Parameters :

sort – The sort.

Returns :

True if the sort is a finite field sort.

bool cvc5_sort_is_set ( Cvc5Sort sort ) 

Determine if given sort is a Set sort.

Parameters :

sort – The sort.

Returns :

True if the sort is a Set sort.

bool cvc5_sort_is_bag ( Cvc5Sort sort ) 

Determine if given sort is a Bag sort.

Parameters :

sort – The sort.

Returns :

True if the sort is a Bag sort.

bool cvc5_sort_is_sequence ( Cvc5Sort sort ) 

Determine if given sort is a Sequence sort.

Parameters :

sort – The sort.

Returns :

True if the sort is a Sequence sort.

bool cvc5_sort_is_abstract ( Cvc5Sort sort ) 

Determine if given sort is an abstract sort.

Warning

This function is experimental and may change in future versions.

Parameters :

sort – The sort.

Returns :

True if the sort is a abstract sort.

bool cvc5_sort_is_uninterpreted_sort ( Cvc5Sort sort ) 

Determine if given sort is an uninterpreted sort.

Parameters :

sort – The sort.

Returns :

True if given sort is an uninterpreted sort.

bool cvc5_sort_is_uninterpreted_sort_constructor ( Cvc5Sort sort ) 

Determine if given sort is an uninterpreted sort constructor.

An uninterpreted sort constructor has arity > 0 and can be instantiated to construct uninterpreted sorts with given sort parameters.

Parameters :

sort – The sort.

Returns :

True if given sort is of sort constructor kind.

bool cvc5_sort_is_instantiated ( Cvc5Sort sort ) 

Determine if given sort 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 cvc5_sort_instantiate() .

Parameters :

sort – The sort.

Returns :

True if given sort is an instantiated sort.

Cvc5Sort cvc5_sort_get_uninterpreted_sort_constructor ( Cvc5Sort sort ) 

Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort.

Parameters :

sort – The sort.

Returns :

The uninterpreted sort constructor sort.

Cvc5Datatype cvc5_sort_get_datatype ( Cvc5Sort sort ) 

Get the underlying datatype of a datatype sort.

Parameters :

sort – The sort.

Returns :

The underlying datatype of a datatype sort.

Cvc5Sort cvc5_sort_instantiate ( Cvc5Sort sort , size_t size , const Cvc5Sort params [ ] ) 

Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.

Create sort parameters with cvc5_mk_param_sort().

Parameters :

• sort – The sort to instantiate.

• size – The number of sort parameters to instantiate with.

• params – The list of sort parameters to instantiate with.

Returns :

The instantiated sort.

const Cvc5Sort * cvc5_sort_get_instantiated_parameters ( Cvc5Sort sort , size_t * size ) 

Get the sorts used to instantiate the sort parameters of a given parametric sort (parametric datatype or uninterpreted sort constructor sort, see cvc5_sort_instantiate() ;

Parameters :

• sort – The sort.

• size – The size of the resulting array of sorts.

Returns :

The sorts used to instantiate the sort parameters of a parametric sort

Cvc5Sort cvc5_sort_substitute ( Cvc5Sort sort , Cvc5Sort s , Cvc5Sort replacement ) 

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

• s – The subsort to be substituted within the given sort.

• replacement – The sort replacing the substituted subsort.

Cvc5Sort cvc5_sort_substitute_sorts ( Cvc5Sort sort , size_t size , const Cvc5Sort sorts [ ] , const Cvc5Sort replacements [ ] ) 

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 :

• sort – The sort.

• sorts – The subsorts to be substituted within the given sort.

• replacements – The sort replacing the substituted subsorts.

• size – The size of sorts and replacements .

const char * cvc5_sort_to_string ( Cvc5Sort sort ) 

Get a string representation of a given sort.

Note

The returned char* pointer is only valid until the next call to this function.

Parameters :

sort – The sort.

Returns :

A string representation of the given sort.

size_t cvc5_sort_hash ( Cvc5Sort sort ) 

Compute the hash value of a sort.

Parameters :

sort – The sort.

Returns :

The hash value of the sort.

size_t cvc5_sort_dt_constructor_get_arity ( Cvc5Sort sort ) 

Get the arity of a datatype constructor sort.

Parameters :

sort – The sort.

Returns :

The arity of a datatype constructor sort.

const Cvc5Sort * cvc5_sort_dt_constructor_get_domain ( Cvc5Sort sort , size_t * size ) 

Get the domain sorts of a datatype constructor sort.

Parameters :

• sort – The sort.

• size – The size of the resulting array of domain sorts.

Returns :

The domain sorts of a datatype constructor sort.

Cvc5Sort cvc5_sort_dt_constructor_get_codomain ( Cvc5Sort sort ) 

Get the codomain sort of a datatype constructor sort.

Parameters :

sort – The sort.

Returns :

The codomain sort of a constructor sort.

Cvc5Sort cvc5_sort_dt_selector_get_domain ( Cvc5Sort sort ) 

Get the domain sort of a given datatype selector sort.

Parameters :

sort – The sort.

Returns :

The domain sort of a datatype selector sort.

Cvc5Sort cvc5_sort_dt_selector_get_codomain ( Cvc5Sort sort ) 

Get the codomain sort of a given datatype selector sort.

Parameters :

sort – The sort.

Returns :

The codomain sort of a datatype selector sort.

Cvc5Sort cvc5_sort_dt_tester_get_domain ( Cvc5Sort sort ) 

Get the domain sort of a given datatype tester sort.

Parameters :

sort – The sort.

Returns :

The domain sort of a datatype tester sort.

Cvc5Sort cvc5_sort_dt_tester_get_codomain ( Cvc5Sort sort ) 

Get the codomain dort of a given datatype tester sort (the Boolean sort).

Note

We mainly need this for the symbol table, which doesn’t have access to the solver object.

Parameters :

sort – The sort.

Returns :

The codomain sort of a datatype tester sort.

size_t cvc5_sort_fun_get_arity ( Cvc5Sort sort ) 

Get the aritye of a given function sort.

Parameters :

sort – The sort.

Returns :

The arity of a function sort.

const Cvc5Sort * cvc5_sort_fun_get_domain ( Cvc5Sort sort , size_t * size ) 

Get the domain of a given function sort.

Parameters :

• sort – The sort.

• size – The size of the resulting array of domain sorts.

Returns :

The domain sorts of a function sort.

Cvc5Sort cvc5_sort_fun_get_codomain ( Cvc5Sort sort ) 

Get the codomain of a given function sort.

Parameters :

sort – The sort.

Returns :

The codomain sort of a function sort.

Cvc5Sort cvc5_sort_array_get_index_sort ( Cvc5Sort sort ) 

Get the index sort of a given array sort.

Parameters :

sort – The sort.

Returns :

The array index sort of an array sort.

Cvc5Sort cvc5_sort_array_get_element_sort ( Cvc5Sort sort ) 

Get the element sort of a given array sort.

Parameters :

sort – The sort.

Returns :

The array element sort of an array sort.

Cvc5Sort cvc5_sort_set_get_element_sort ( Cvc5Sort sort ) 

Get the element sort of a given set sort.

Parameters :

sort – The sort.

Returns :

The element sort of a set sort.

Cvc5Sort cvc5_sort_bag_get_element_sort ( Cvc5Sort sort ) 

Get the element sort of a given bag sort.

Parameters :

sort – The sort.

Returns :

The element sort of a bag sort.

Cvc5Sort cvc5_sort_sequence_get_element_sort ( Cvc5Sort sort ) 

Get the element sort of a sequence sort.

Parameters :

sort – The sort.

Returns :

The element sort of a sequence sort.

Cvc5SortKind cvc5_sort_abstract_get_kind ( Cvc5Sort sort ) 

Get the kind of an abstract sort, which denotes the sort kinds that the abstract sort denotes.

Warning

This function is experimental and may change in future versions.

Parameters :

sort – The sort.

Returns :

The kind of an abstract sort.

size_t cvc5_sort_uninterpreted_sort_constructor_get_arity ( Cvc5Sort sort ) 

Get the arity of an uninterpreted sort constructor sort.

Parameters :

sort – The sort.

Returns :

The arity of an uninterpreted sort constructor sort.

uint32_t cvc5_sort_bv_get_size ( Cvc5Sort sort ) 

Get the size of a bit-vector sort.

Parameters :

sort – The sort.

Returns :

The bit-width of the bit-vector sort.

const char * cvc5_sort_ff_get_size ( Cvc5Sort sort ) 

Get the size of a finite field sort.

Note

The returned char* pointer is only valid until the next call to this function.

Parameters :

sort – The sort.

Returns :

The size of the finite field sort.

uint32_t cvc5_sort_fp_get_exp_size ( Cvc5Sort sort ) 

Get the exponent size of a floating-point sort.

Parameters :

sort – The sort.

Returns :

The bit-width of the exponent of the floating-point sort.

uint32_t cvc5_sort_fp_get_sig_size ( Cvc5Sort sort ) 

Get the significand size of a floating-point sort.

Parameters :

sort – The sort.

Returns :

The width of the significand of the floating-point sort.

size_t cvc5_sort_dt_get_arity ( Cvc5Sort sort ) 

Get the arity of a datatype sort, which is the number of type parameters if the datatype is parametric, or 0 otherwise.

Parameters :

sort – The sort.

Returns :

The arity of a datatype sort.

size_t cvc5_sort_tuple_get_length ( Cvc5Sort sort ) 

Get the length of a tuple sort.

Parameters :

sort – The sort.

Returns :

The length of a tuple sort.

const Cvc5Sort * cvc5_sort_tuple_get_element_sorts ( Cvc5Sort sort , size_t * size ) 

Get the element sorts of a tuple sort.

Parameters :

• sort – The sort.

• size – The size of the resulting array of tuple element sorts.

Returns :

The element sorts of a tuple sort.

Cvc5Sort cvc5_sort_nullable_get_element_sort ( Cvc5Sort sort ) 

Get the element sort of a nullable sort.

Parameters :

sort – The sort.

Returns :

The element sort of a nullable sort.