Yices Input Language

• Declarations
  • Basic types
  • Type definitions
  • Constant declarations
  • Constant definitions
• Types
  • Basic types
  • Subtypes
  • Function types
  • Tuple types
  • Record types
  • Dependent types
  • Recursive datatypes
  • Scalar types
  • Bit-vector types
• Expressions
  • Boolean operators
  • Equality and disequality
  • If-then-else
  • Let
  • Quantifiers
  • Arithmetic
  • Functions
  • Lambda expressions
  • Tuples
  • Records
  • Bit-vectors
• Commands
  • Assert
  • Extended Assert
  • Retract
  • Check
  • MaxSat
  • Evidence flag
  • Verbosity level
  • Arithmetic only
  • Recursion limit
  • Limit on conflicts for max-sat
  • Iteration limit for max-sat
  • Push
  • Pop
  • Echo
  • Include
  • Reset
  • Status
  • Dump context

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

(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

(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

(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

(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

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

Basic types

Subtypes

(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

(-> [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 [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 [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

(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

(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 [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

(bitvector [size])

where size is a positive number.

Expressions

Boolean operators

(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

(= [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

(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

(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

(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

(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

(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 ([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

(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

(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

(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

• Concatenation:

  (bv-concat [bv1] [bv2])
  

  where bv1 and bv2 are bitvector terms, Example:

  (bv-concat 0b0010 0b0000)
    => 0b00100000
  

• Extraction:

  (bv-extract [end] [begin] [bv])
  

  where end and begin are nonegative integers, and bv is a bitvector term. Moreover, begin >= 0, end >= begin, and end < size, where size is the size of the bitvector bv. Example:

  (bv-extract 3 1 0b000101101)
    => 0b110
  

• Left Shift:

  (bv-shift-left0 [bv] [n])
  (bv-shift-left1 [bv] [n])
  

  where bv is a bitvector term, and n is a nonnegative integer, and n < size, where size is the of the bitvector bv. Example:

  (bv-shift-left0 0b10110101 2)
    => 0b11010100
  (bv-shift-left1 0b10110101 2)
    => 0b11010111
  

• Right Shift:

  (bv-shift-right0 [bv] [n])
  (bv-shift-right1 [bv] [n])
  

  where bv is a bitvector term, and n is a nonnegative integer, and n < size, where size is the of the bitvector bv. Example:

  (bv-shift-right0 0b10110101 2)
    => 0b00101101
  (bv-shift-right1 0b10110101 2)
    => 0b11110101
  

• Sign extension: This operator operator simply extends the bit-vector with copies of its most-significant bit.

  (bv-sign-extend [bv] [num-copies])
  

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

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.

(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

MaxSat

Evidence flag

Examples:

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

Verbosity level

Examples:

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

Arithmetic only

Examples:

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

Recursion limit

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

(set-nested-rec-limit! 50)

Limit on conflicts for max-sat

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

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

(status)

Dump context

(dump-context)