Yices' language is strongly typed, meaning that every expression has
an associated type. The yices type system is based on structural
equivalence instead of name equivalence, so types are closely re-
lated to sets, in that two types are equal iff they have the same
elements.
Function, record, and tuple types may also be dependent.
The basic types in Yices are real, int, nat, and bool.
real is the type of real numbers, int integer numbers, nat natural numbers
and bool is the type of boolean expressions. In Yices,
there is no distinction between formulas and terms.
The current version of yices is incomplete for mixed real and integer problems.
Any collection of elements of a given type itself forms a type, called a subtype.
The type from which the elements are taken is called the sypertype. The elements
which form the subtype are determined by a subtype predicate on the supertype.
The notion used to define a subtype is:
(subtype (id::type) expr)
where expr is an boolean expression. Example:
(define v::(subtype (n::int) (and (> n 2) (/= n 4)))
In this example, v is a constant greater than 2 and different from 4.
The notation
(subrange expr_l expr_u)
is a syntax sugar for
(subtype (n::int) (and (>= n expr_l) (<= n expr_u)))
Function types are of the form:
(-> domain_1 ... domain_n range)
where domain_i and range are types. In yices, arrays are
represented as functions. Examples:
(define f1::(-> int int))
(define p1::(-> real real bool))
Tuple (product) types are of the form:
(tuple type_1 ... type_n)
where n is at least 2, and type_i are types. Examples:
(define t1::(tuple int bool int))
(define t2::(tuple bool real))
(define t3::(tuple int (-> int bool) (tuple int int)))
Record types are of the form:
(record id_1::type_1 ... id_ntype_n)
where n is at least 1, id_i are identifiers, and type_i are types.
id_i are called the field names of the record type. Examples:
(define r1::(record idx::int flag::bool))
(define r2::(record x::int y::int))
Records are not supported in the current version. In the meantime, tuples may be used to substitute records.
Function, tuple, and record types may be dependent; in other words, some of the
type components may depend on earlier components. Here are some examples:
(define rem::(-> nat d::(subtype (n::nat) (/= n 0)) (subtype (r::nat) (< r d))))
(define pfn::(tuple d::(-> dom bool) (-> (subtype (x::dom) (d x)) ran)))
(define int-stack::(record size::nat elements::(-> (subtype (n::nat) (< n size)) int)))
(define f::(-> x::int y::int (subtype (n::int) (>= n (+ x y)))))
The declaration for rem indicates explicitly the range of the remainder function, which
depends on the second argument. Function types may also have dependencies within
the domain types; e.g., the second domain type may depend on the first.
Note that for function and tuple dependent types, local identifiers need be associated only with
those types on which later types depend.
The tuple type pfn encodes partial functions as pairs consisting of a predicate on
the domain type dom and a function from the subtype defined by that predicate to the
range ran.
int-stack encodes a stack of integers as a pair consisting of a size and an array mapping initial
segments of the natural numbers to int.
The general form for recursive datatypes is:
(datatype constructor_def_1 ... constructor_def_n)
where each constructor_def_i is one of the following forms
c-name
(c-name a-name_1::type_1 ... a-name_n::type_n)
Here, c-name is the name of the constructor (e.g. cons). a-name_i
are the names of the accessors, and type_i are the domain types for the constructor.
Yices automatically declares a recognizer (tester) c-name?, 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-name.
Examples:
(define-type list (datatype nil (cons car::int cdr::list)))
(define l1::list (cons 1 nil))
(define l2::list (cdr l1))
(theorem simple1 (cons? l1))
(theorem simple2 (nil? l2))
(define-type tree (datatype (leaf val::int) (branch left::tree right::tree)))
Scalar types are a special case of datatypes. They are of the form:
(scalar name_1 ... name_n)
where n is at least 1, and name_i are new identifiers. Example
(define-type msg-type (scalar ping data ack))