• Type declarations
• Type definitions
• Constant declarations
• Constant definitions
• Theorems

Type declarations

New basic (uninterpreted) types can be declared in yices using the following syntax:

(define-type name)

For example, the following yices declarations declare t1 and t2 as new basic types.

(define-type t1)
(define-type t2)

Type definitions

New types can be defined in terms of existing ones using the following syntax:

(define-type name type)

Here, type is a well-formed type expression. name is a new identifier, and it becomes an alias for the type expression type.

For example, the following yices declaration defines an alias f1 for the function type (-> int int):

(define-type f1 (-> int int))

Recursive datatypes and scalar types must be given a name using a type definition. They cannot appear anywhere else, except in type definitions. For example, the following declaration defines msg-type to be the scalar type (scalar ping data ack):

(define-type msg-type (scalar ping data ack))

Constant declarations

Constant, function, and predicate symbols are all referred as constants. Constants can be declared using the following syntax:

(define name::type)

Here, name is a new identifier, and type is a well-formed type expression.

For example, the following declarations declare x to be an integer, f to be a function from integer to integer, t to be a tuple, and b a boolean.

(define x::int)
(define f::(-> int int))
(define t::(tuple bool int real))
(define b::bool)

Constant definitions

Constants may be defined using the following syntax:

(define name::type expr)

Here, name is a new identifier, type is a well-formed type expression, and expr is a well-formed expression.

For example, the following definitions declare f0 to be (f 0):

(define f::(-> int int))
(define f0::int (f 0))

Theorems

Theorem declarations allow properties to be stated. These are just boolean-valued expressions, which are thus just logical formulas. A yices file may contain several theorem declarations. Theorems may be defined using the following syntax:

(theorem name expr)

Here, name is a new identifier, and expr is a well-formed boolean expression.

Example:

(define f::(-> int int))
(define a::int)
(define b::int)
(theorem simple (=> (= a b) (= (f a) (f b))))