Home Docs Download Mail Status FM Tools
Yices

Yices Input Language

The yices input language is based on the PVS and SAL languages, but the concrete syntax is similar to Scheme and Lisp. Any text after the character ';' and to the end of the current line is a comment:

;; This is a comment in yices

Declarations

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))

Datatypes and scalartypes 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))

Types

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 related to sets, in that two types are equal iff they have the same elements.

Function, record, and tuple types may also be dependent.

Basic types

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.

Subtypes

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 supertype. 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

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 types

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

Record types are of the form:

(record [id_1]::[type_1] ... [id_n]::[type_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))

Dependent types

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.

Recursive datatypes

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))
(define-type tree (datatype (leaf val::int) (branch left::tree right::tree)))

Scalar types

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))

Bit-vector types

Fixed size bit-vectors are of the form:

(bitvector [size])

where size is a positive number.

Expressions

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)
(define t1::bool (=> (and (=> p q) (=> q r)) (=> p r)))
(define t2::bool (=> (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))
(define t1::bool (or (= x 0) (= x 1) (= x 2)))
(define y::(subrange 0 1))
(define z::(subrange 0 1))
(define w::(subrange 0 1))
(define t2::bool (not (and (/= y z) (/= y w) (/= z w))))
(define p::bool)
(define t3::bool (= 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)
(define t1::bool (>= (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] has one of the following forms:

([name]::[type] [expr])
(name 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])

Warning:
Yices is not complete when quantifiers are used. So, it may return "unknown", and a "potential" model.

Arithmetic

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

(define x::int)
(define y::int)
(define t1::bool (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)
(define t1::bool (=> (and (= (+ x (* 2 y)) 5) (>= x 1)) (<= y 2)))

Warning:
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)
(assert (/= v1 v2))
(assert (/= i1 i2))
(assert (= (update f1 (i1) v1) (update (update f2 (i1) v2) (i2) v3)))
(check)

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))

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)

Bit-vectors

Bit-vector constants are of the form

(mk-bv [size] [value])

where size (number of bits) is a positive integer and value a nonnegative integer. Example:

(mk-bv 8 120)

Bit-vector constants can be also represented in binary format. The rightmost bit is called the least significant bit (LSB), and the leftmost bit is the most significant bit(MSB). The index of the LSB is 0, and the index of the MSB is n-1 for an n-bit constant. This convention naturally extends to all bit-vector expressions. Following are some examples of bit-vector constants:

0b00010100
0b10001001

Word-level functions

Bitwise functions

(bv-and [bv1] [bv2])
(bv-or [bv1] [bv2])
(bv-xor [bv1] [bv2])
(bv-not [bv])

It is required that all the arguments (bitvector terms) of bitwise functions have the same size.

Bit-vector arithmetic functions

(bv-add [bv1] [bv2])
(bv-sub [bv1] [bv2])
(bv-mul [bv1] [bv2])
(bv-neg [bv])
(bv-lt  [bv1] [bv2])   (unsigned) less than
(bv-le  [bv1] [bv2])   (unsigned) less than or equal to
(bv-gt  [bv1] [bv2])   (unsigned) greater than
(bv-ge  [bv1] [bv2])   (unsigned) greater than or equal to
(bv-slt [bv1] [bv2])   (signed) less than
(bv-sle [bv1] [bv2])   (signed) less than or equal to
(bv-sgt [bv1] [bv2])   (signed) greater than
(bv-sge [bv1] [bv2])   (signed) greater than or equal to

It is required that all the arguments (bitvector terms) of bit-vector arithmetic functions have the same size.

Commands

In addition to declarations of types and constants, Yices' language contains the following commands:

Assert

(assert [expr])

Assert the formula [expr] into the current logical context. Example:

(define x::bool)
(define y::bool)
(assert (or x y))

Extended Assert

(assert+ [expr])
(assert+ [expr] [weight])

Assert a formula to the current logical context. This command is similar to assert, but it more flexible and expensive. It can be used to compute unsatisfiable cores; can be retracted using the command retract; and compute max-sat when weights are provided. If a weight is not provided the constraint is assumed to have infinite weight with respect to the max-sat command.

The following example shows how an assertion can be retracted.

(define x::bool)
(define y::bool)
(assert (not x))
(assert (not y))
(assert+ (or x y))
  => 1
(check)
  => unsat
(retract 1)
(check)
  => sat

The notation

cmd
  => [result]

is used to represent the result produced by the command cmd.

Remarks:
The assertion id is only displayed after the execution of assert+ when the verbosity level is greater than 2. See Verbosity level.
The following example shows how unsatisfiable cores can be extracted when using the command assert+.

(set-evidence! true)
(set-verbosity! 2)
(define x::bool)
(define y::bool)
(define z::bool)
(define w::bool)

(assert+ (/= x y))
  => id: 1
(assert+ (/= y z))
  => id: 2
(assert+ (or w x y))
  => id: 3
(assert+ (/= z x))
  => id: 4
(assert+ (or w z))
  => id: 5
(check)
  => unsat
  => unsat core ids: 1 2 4

The following example shows how to obtain maximal satisfying assingment using the command assert+.

(set-evidence! true)
(define x::bool)
(define y::bool)
(define z::bool)
(define w::bool)

(assert+ (/= x y) 10)
  => id: 1
(assert+ (/= y z) 6)
  => id: 2
(assert+ (or w x y) 8)
  => id: 3
(assert+ (/= z x) 12)
  => id: 4
(assert+ (or w z) 6)
  => id: 5
(max-sat)
  => sat
  => inconsistent assertion ids: 2
  => (= x true)
  => (= y false)
  => (= z false)
  => (= w true)

If the verbosity level is greater than 2, then yices display line number information when printing assertion ids. See Verbosity level.

Retract

(retract [idx])

Retract an assertion from the logical context.

Check

The command check checks whether the current logical context is satisfiable or not. The weights associated with constraints are ignored by this command. It the problem is unsatisfiable this command displays which constraints asserted with the command assert+ are in the unsatisfiable core. Remark: This core is not minimal. If the problem is satisfiable it the command displays a model. The core and models are displayed when evidence is enable. The command set-evidence! can be used to enable evidence.

MaxSat

The command max-sat can be used to extract the maximal satisfying model. See Extended Assert.

Evidence flag

The command set-evidence! enables/disables the construction of evidence: models and unsatisfiable cores.

Examples:

(set-evidence! true)
(set-evidence! false)

Verbosity level

The command set-verbosity! defines the verbosity level. The verbosity level specify the ammount of feedback messages yices will produce.

Examples:

(set-verbosity! 3)
(set-verbosity! 1)

Arithmetic only

The command set-arith-only! tells yices that only boolean combinations of arithmetic constraints are going to be asserted. This command may improve the performance for pure arithmetic formulas.

Examples:

(set-arith-only! true)
(set-arith-only! false)

Recursion limit

Yices has limited support for recursive functions: recursive function are expanded during pre-processing. The command set-nested-rec-limit! sets a limit on the expansion of recursive functions.

By default the limit is 30. It can be changed as follows:

(set-nested-rec-limit! 50)

Limit on conflicts for max-sat

Yices's max-sat algorithm performs a sequence of satisfiability check until it finds a model of maximal cost. In a first phase of this algorithm, Yices uses a bounded search intended to find a possibly suboptimal solution quickly.

The search is bounded by setting a limit on the number of conflicts in the SAT solver. This limit is 10000 by default. It can be changed using set-maxsat-conflict-limit! as follows:

(set-maxsat-conflict-limit! 50000)

Iteration limit for max-sat

This commands sets a limit on the number of iteration performed by Yices's max-sat algorithm. If this limit is reached and no model has been found, (max-sat) will return unknown.

By default, the limit is 10000. It can be changed as follows:

(set-maxsat-iteration-limit! 5000)

Push

(push)

Saves the current logical context on the stack.

Pop

(pop)

Restores the context from the top of the stack, and pops it off the stack. Any changes to the logical context (by assert or other commands) between the matching push and pop operators are flushed, and the context is completely restored to what it was right before the push.

Echo

(echo [string])

Prints the string [string]. Example:

(echo "hello world.")
   => hello world

Include

(include [file])

Include the file [file]. That is, process the declarations and commands in this file. Example:

(include "~/examples/tst.yices")

Reset

(reset)

Reset the current logical context.

Status

Display the status of the logical context.
(status)

Dump context

The command dump-context can be used to display the contents of the logical context. This command is mainly used for debugging purposes.

(dump-context)
Home Docs Download Mail Status FM Tools

Last modified: Wed 05 Mar 2014 14:16 PST