Types¶
Yices has primitive types for Booleans, integers, reals, and bitvectors. Other atomic types can be created by declaring new uninterpreted types and new scalar types. In addition, the type system includes tuple and function types.
The API provides functions for accessing the primitive types, creating uninterpreted and scalar types, and for building tuple and function types. The API also includes various functions for examining types. Functions for printing types are documented in Pretty Printing.
All type constructors return an object of type type_t
, which
is either a type or the special value NULL_TYPE
if there is
an error. For error diagnostic, use the functions documented in
section Error Reporting.
Common error reports
All functions set the error report as follows if they receive a type parameter tau that is not valid:
– error code:
INVALID_TYPE
– type1 := tau (i.e., the invalid type)
If an integer parameter must be positive, the functions will report the following error when the input is zero:
– error code:
POS_INT_REQUIRED
– badval := 0
Other error reports are possible. They are listed for each function.
Type Constructors¶
-
type_t yices_bv_type(uint32_t size)¶
Constructs a bitvector type.
Parameter
size is the number of bits. It must be positive and no more than
YICES_MAX_BVSIZE
Error report
If size is more than
YICES_MAX_BVSIZE
:– error code:
MAX_BVSIZE_EXCEEDED
– badval := size
-
type_t yices_new_scalar_type(uint32_t card)¶
Creates a new scalar type.
Parameter
card is the type cardinality. It must be positive.
-
type_t yices_tuple_type(uint32_t n, const type_t tau[])¶
Creates the tuple type: (tuple tau[0] … tau[n-1]).
Parameters
n: number of components.
tau: array of n types
n must be positive and no more than
YICES_MAX_ARITY
Error report
If n is more than
YICES_MAX_ARITY
:– error code:
TOO_MANY_ARGUMENTS
– badval := n
-
type_t yices_tuple_type1(type_t tau1)¶
Creates the tuple type (tuple tau1).
This function is equivalent to
yices_tuple_type
with n=1.
-
type_t yices_tuple_type2(type_t tau1, type_t tau2)¶
Creates the tuple type (tuple tau1 tau2).
This function is equivalent to
yices_tuple_type
with n=2.
-
type_t yices_tuple_type3(type_t tau1, type_t tau2, type_t tau3)¶
Creates the tuple type (tuple tau1 tau2 tau3).
This function is equivalent to
yices_tuple_type
with n=3.
-
type_t yices_function_type(uint32_t n, const type_t dom[], type_t range)¶
Creates the function type (-> dom[0] … dom[n-1] range).
Parameters
n: function arity (i.e., size of array dom)
dom: array of domain types
range: range type
n must be positive and no more than
YICES_MAX_ARITY
Error report
If n is more than
YICES_MAX_ARITY
:– error code:
TOO_MANY_ARGUMENTS
– badval := n
-
type_t yices_function_type1(type_t tau1, type_t range)¶
Creates the unary function type: (-> tau1 range).
This function is equivalent to
yices_function_type
with n=1.
Tests on Types¶
The following functions check a property of a type tau. They return 0 for false and 1 for true.
If tau is not a valid type, these functions return false (i.e., 0)
and set the error report (error code: INVALID_TYPE
).
-
int32_t yices_type_is_arithmetic(type_t tau)¶
Checks whether tau is an arithmetic type (i.e., either integer or real).
-
int32_t yices_test_subtype(type_t tau, type_t sigma)¶
Checks whether tau is a subtype of sigma.
The function returns 1 for true and 0 for false. If tau or sigma is not a valid type, the function returns false and sets the error report.
-
int32_t yices_compatible_types(type_t tau, type_t sigma)¶
Checks whether tau and sigma are compatible.
The function returns 1 for true and 0 for false. If tau or sigma is not a valid type, the function returns false and sets the error report.
Two types are compatible if they have a common supertype. For example, real and int are compatible because their common supertype is real. Consult the manual for more details.
Access to Type Components¶
The following functions give access to attributes and components of a type.
-
uint32_t yices_bvtype_size(type_t tau)¶
Returns the number of bits of type tau, or 0 if there’s an error.
Error report
If tau is not a bitvector type:
– error code:
BVTYPE_REQUIRED
– type1 := tau
-
uint32_t yices_scalar_type_card(type_t tau)¶
Returns the cardinality of type tau, or 0 if there’s an error.
Error report
If tau is not a scalar type:
– error code:
INVALID_TYPE_OP
-
int32_t yices_type_num_children(type_t tau)¶
Number of children of type tau. or -1 if there’s an error.
If tau is a tuple type (tuple τ1 … τn), the function returns n
If tau is a function type (-> τ1 … τn σ), the function returns n+1
If tau is any other type, the function returns 0
-
type_t yices_type_child(type_t tau, int32_t i)¶
Returns the i-th child of type tau.
If tau has n children then index i must be in the interval [0 … n-1].
For a tuple type (tuple τ1 … τn),
– the first child (with index i=0) is τ1,
– the last child (with index i=n-1) is τn.
For a function type (-> τ1 … τn σ),
– the first child (with index i=0) is τ1,
– the last child (with index i=n) is σ.
For any other type, the function returns
NULL_TYPE
as the type has no children.
Error report
If i is negative or larger than the number of children minus one:
– error code:
INVALID_TYPE_OP
-
int32_t yices_type_children(type_t tau, type_vector_t *v)¶
Collects the children of a type.
The children of type tau are collected in vector v. The vector must be initialized first by calling function
yices_init_type_vector
.If tau is not a valid type, this function returns -1, sets the error report, and leaves v unchanged.
Otherwise, the children are stored in v in the same order as given by
yices_type_child
.v->size is the number of children of tau
v->data[i] contains the i-th child.
If tau is an atomic type, then v->size is set to 0 and v->data is empty.
Type Macros¶
Yices supports type macros and type constructors, which are uninterpreted type constructors that can be instantiated with type arguments.
The following functions are available for working with type macros:
-
type_t yices_type_variable(uint32_t id)¶
Creates a type variable with the given id.
Parameter
id is the identifier for the type variable
Returns
A type variable of type
type_t
-
int32_t yices_type_constructor(const char *name, uint32_t n)¶
Creates a type constructor with the given name and arity.
Parameters
name is the name of the type constructor
n is the arity (number of type parameters). It must be positive and no more than
TYPE_MACRO_MAX_ARITY
Returns
The constructor’s id (a non-negative integer) or -1 if there’s an error
Error reports
If n is zero:
– error code:
POS_INT_REQUIRED
– badval := 0
If n is more than
TYPE_MACRO_MAX_ARITY
:– error code:
TOO_MANY_MACRO_PARAMS
– badval := n
-
int32_t yices_type_macro(const char *name, uint32_t n, type_t *vars, type_t body)¶
Creates a type macro with the given name, arity, type variables, and body.
Parameters
name is the name of the type macro
n is the arity (number of type parameters)
vars is an array of n distinct type variables
body is the type expression that defines the macro
Returns
The macro’s id (a non-negative integer) or -1 if there’s an error
Error reports
If n is zero:
– error code:
POS_INT_REQUIRED
– badval := 0
If n is more than
TYPE_MACRO_MAX_ARITY
:– error code:
TOO_MANY_MACRO_PARAMS
– badval := n
If body or one of vars[i] is not a valid type:
– error code:
INVALID_TYPE
– type1 := body or vars[i]
If vars[i] is not a type variable:
– error code:
TYPE_VAR_REQUIRED
– type1 := vars[i]
If the same variable occurs twice or more in vars:
– error code:
DUPLICATE_TYPE_VAR
– type1 := the duplicate variable
-
type_t yices_instance_type(int32_t cid, uint32_t n, type_t tau[])¶
Creates an instance of a type macro or constructor by applying it to type arguments.
Parameters
cid is the constructor or macro id
n is the number of arguments
tau is an array of n argument types
Returns
The resulting type or
NULL_TYPE
if there’s an errorError reports
If cid is not a valid macro or constructor id:
– error code:
INVALID_MACRO
– badval := cid
If n is not the same as the macro/constructor arity:
– error code:
WRONG_NUMBER_OF_ARGUMENTS
– badval := n
If one of tau[i] is not a valid type:
– error code:
INVALID_TYPE
– type1 := tau[i]
-
int32_t yices_get_macro_by_name(const char *name)¶
Gets the macro id for a given name.
Parameter
name is the name of the macro or constructor
Returns
The macro’s id (a non-negative integer) or -1 if there’s no macro or constructor with that name
-
void yices_remove_type_macro_name(const char *name)¶
Removes the mapping of a name to a macro id.
Parameter
name is the name of the macro or constructor
No change is made if no such mapping exists.
-
void yices_delete_type_macro(int32_t id)¶
Removes a macro with the given id.
Parameter
id must be a valid macro index (non-negative)
-
TYPE_MACRO_MAX_ARITY¶
The maximum arity allowed for type macros and constructors. This is defined as 128.