Boolean operators

The usual boolean operators and, or, not, and =>(implication) have the following form:

(and expr_1 ... expr_n)
(or expr_1 ... expr_n)
(not expr)
(=> expr_1 expr_2)

Where expr_i are boolean expressions. The bi-implication and exclusive-or are represented using equality and disequality. Examples:

(define p::bool)
(define q::bool)
(define r::bool)
(theorem simple1 (=> (and (=> p q) (=> q r)) (=> p r)))
(theorem simple2 (=> (not (or p q)) (and (not p) (not q))))

Equality and disequality

Equations (=) and disequations (/=) between expressions are written using the following notation.

(= expr_1 expr_2)
(/= expr_1 expr_2)

In Yices, there is no distinction between formulas and terms. So, so equations and disequations can be used to express bi-implication and exclusive-or. Examples:

(define x::(subrange 0 2))
(theorem simple1 (or (= x 0) (= x 1) (= x 2)))
(define y::(subrange 0 1))
(define z::(subrange 0 1))
(define w::(subrange 0 1))
(theorem simple2 (not (and (/= y z) (/= y w) (/= z w))))
(define p::bool)
(theorem simple3 (= p p))

If-then-else

Conditional expressions have the following equivalent forms:

(if c-expr t-expr e-epxr)
(ite c-expr t-expr e-epxr)

where c-expr is a boolean expression, and t-expr and e-expr are required to be of the same type, which is the type of the conditional. Example:

(define x::real)
(define y::real)
(theorem simple (>= (if (>= x y) x y) x))

Let

Parallel local aliases can be made using let, with the following syntax:

(let (binding_1 ... binding_n) expr)

where n is at least 1, and each binding_i is of the form:

(name::type expr)

Examples:

(define x::int)
(define f::(-> int int))
(define g::(-> int int int))
(define y::int (let ((aux::int (f (f x)))) (g aux aux)))

Quantifiers

Quantified expressions are introduced with the keywords forall and exists. These expressions are of type bool. They have the following form:

(forall (name_1::type_1 ... name_n::type_n) expr)
(exists (name_1::type_1 ... name_n::type_n) expr)

Quantifiers are not supported int the current version.

Arithmetic

Arithmetic inequalities between reals and integers are written using <, <=, >, and >= symbols. Inequalities are of type bool. Examples:

(define x::int)
(define y::int)
(theorem simple (or (< x y) (> x y) (= x y)))

The symbols +, -, *, /, div, and mod are used for addition, subtraction, multiplication, division, integer division, and modulo, respectively. Example:

(define x::int)
(define y::int)
(theorem simple (=> (and (= (+ x (* 2 y)) 5) (>= x 1)) (<= y 2)))

Yices only supports linear arithmetic in the current version.

Functions

The application of a function f to arguments a_1, ..., a_n is written as:

(f a_1 ... a_n)

Notice that f does not need to be a function symbol. Examples:

(define f::(-> int (-> int int)))
(define x::int)
(define y::int ((f x) x))
(define g::(-> int int int))
(define w::int (g x y))

Functions can be functionally updated using the update constructor. The syntax is:

(update f (pos_1 ... pos_n) new-val)

The update expression is semantically equivalent to:

(lambda (a_1::t_1 ... a_n::t_n) (if (and (= a_1 pos_1) ... (= a_n pos_n)) new-val (f a_1 ... a_n)))

Example:

(define f1::(-> int int))
(define f2::(-> int int))
(define i1::int)
(define i2::int)
(define v1::int)
(define v2::int)
(define v3::int)
(define a1::bool (/= v1 v2))
(define a2::bool (/= i1 i2))
(define a3::bool (= (update f1 (i1) v1) (update (update f2 (i1) v2) (i2) v3)))
(theorem main (not (and a1 a2 a3)))

Lambda expressions

Lambda expressions denote unnamed functions. They have the following form:

(lambda (name_1::type_1 ... name_n::type_n) expr)

For example, the function which adds 3 to an integer may be written:

(lambda (x::int) (+ x 3))

Lambda expressions are not supported in the current version.

Tuples

Tuples are of the form:

(mk-tuple expr_1 ... expr_n)

where n is at least 2 and expr_i are expressions. The i'th component of a tuple t which has at least i components is selected using the following syntax:

(select t i)

i is a numeral. The numbering of the components starts at 1.Examples:

(define t::(tuple int int) (mk-tuple 10 20))
(define x::int (select t 1))
(define y::int (select t 2))

Tuples can be functionally updated using the update constructor. The syntax is:

(update tuple index new-val)

Example:

(define t1::(tuple int int int) (mk-tuple 3 8 2))
(define t2::(tuple int int int) (update t1 2 100))

Records

Records are of the form:

(mk-record name_1::expr_1 ... name_n::expr_n)

where n is at least 1, name_i are identifiers (field names), and expr_i are expressions. The field f of a record r is selected using the following syntax:

(select r f)

f is an identifier. Examples:

(define r::(record x::int y::int) (mk-record x::10 y::20))
(define a::int (select r x))
(define b::int (select r y))

Records can be functionally updated using the update constructor. The syntax is:

(update record field-name new-val)

Example:

(define r1::(record x::int y::int) (mk-record x::3 y::8))
(define r2::(record x::int y::int) (update r1 x 100)

Records are not supported in the current version. In the meantime, tuples may be used to substitute records.