CVC's presentation language is typed. The type system currently is fairly simple. There is no polymorphism or subtyping (although a form of the latter will be added in a later release). In addition to built-in basic types, there are tuple types, record types, array types, scalar types (aka, enumerations) inductive datatypes, and function types. Structural equivalence is used to compare all types except scalar types and inductive datatypes, where name equivalence is used (see the remarks on type definitions).
CVC works with first-order logic only. Types must therefore be
first-order. So no type T can contain a function type as a
subexpression, unless T is itself a function type.
The basic types in CVC are REAL and BOOLEAN. REAL is the type of numbers, and BOOLEAN is the type of formulas.
Technically, since CVC's language is first-order, types should not
contain BOOLEAN, except as the range of a function type (which is then
the type of a predicate). In CVC, however, BOOLEAN may appear
arbitrarily in types. This is achieved by having two versions of the
BOOLEAN type, one for formulas and one for boolean terms. This
distinction is made only internally; the input language just has a
single type BOOLEAN.
The types for tuples are of the form
The types of functions are of the form
The types for records are of the form
Here is an example (see also the records example):
f : REAL;
r : [# f : BOOLEAN, f2 : REAL #];
An example of an inductive datatype (also known as an abstract
datatype, or ADT) is
DATATYPE cons (car : REAL, cdr : rList), null END
This is the type of finite lists of REALs (see the ADTs example).
The general form for inductive datatypes is
When a datatype is declared, CVC automatically declares each constructor c as the appropriate function; if c has no selectors, it is declared as a constant. The selectors for c are also declared as the appropriate functions. Applying the i'th selector of c to c(a_1, ..., a_n) returns a_i. Selectors are treated as partial functions in CVC. So "car(null)" is considered to be undefined (see the section on partiality).
CVC automatically declares a tester "c?", which is a predicate on the datatype. It returns true for a given element e of that datatype iff e was constructed using constructor c.
The types for arrays are of the form
This example declares a multi-dimensional array (see also the arrays example):
a : ARRAY REAL OF ARRAY REAL OF ARRAY REAL OF REAL;