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
(define-type [name])
For example, the following yices declarations declare t1 and t2 as new basic types.
(define-type t1) (define-type t2)
(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))
(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)
(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))
Function, record, and tuple types may also be dependent.
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.
(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)))
(-> [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 [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 [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))
(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.
(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 [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))
(bitvector [size])
where size is a positive number.
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))))
(= [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 [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 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)))
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])
<, <=, >, 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)))
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 ([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))
(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))
(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)
(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
(bv-concat [bv1] [bv2])
bv1 and bv2 are bitvector terms, Example: (bv-concat 0b0010 0b0000) => 0b00100000
(bv-extract [end] [begin] [bv])
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 1 3 0b000101101) => 0b110
(bv-left-shift0 [bv] [n]) (bv-left-shift1 [bv] [n])
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
(bv-right-shift0 [bv] [n]) (bv-right-shift1 [bv] [n])
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
(bv-sign-extend [bv] [num-copies])
(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.
(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]) (unsigned) less than (bv-sle [bv1] [bv2]) (unsigned) less than or equal to (bv-sgt [bv1] [bv2]) (unsigned) greater than (bv-sge [bv1] [bv2]) (unsigned) greater than or equal to
It is required that all the arguments (bitvector terms) of bit-vector arithmetic functions have the same size.
(assert [expr])
Assert the formula [expr] into the current logical context. Example:
(define x::bool) (define y::bool) (assert (or x y))
(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.
assert+ when the verbosity level is greater than 2. See Verbosity level.assert+.
(set-evidence! true) (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 folling 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 [idx])
Retract an assertion from the logical context.
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.max-sat can be used to extract the maximal satisfying model. See Extended Assert.set-evidence! enables/disables the construction of evidence: models and unsatisfiable cores.Examples:
(set-evidence! true) (set-evidence! false)
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)
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)
(push)
Saves the current logical context on the stack.
(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 [string])
Prints the string [string]. Example:
(echo "hello world.") => hello world
(include [file])
Include the file [file]. That is, process the declarations and commands in this file. Example:
(include "~/examples/tst.yices")
(reset)
Reset the current logical context.
(status)
dump-context can be used to display the contents of the logical context. This command is mainly used for debugging purposes.
(dump-context)
1.4.5