FAQ
From SRI YICES
Frequently Asked Questions About Yices
Crashes and Installation Problems
Yices crashes or segfaults (1)
Yices is intended to operate as the backend to other tools, which are assumed to generate good input. Hence, by default, Yices does no checking and can behave unpredictably if given bad input. Use the -tc flag to enable modest typechecking and improved error messages. Please try this option before sending bug reports. Also, please make sure you have the latest version of Yices.
Yices crashes or segfaults (2)
If you are using a dynamically-linked version of Yices, make sure you are using a recent version of GMP (4.1.2 is known to cause problems).
You can sometimes test the version by
grep GNU_MP_VERSION /usr/include/gmp.h
but otherwise, you will need to compile (with the -lgmp flag) and run the following program
#include <stdio.h>
#include <gmp.h>
extern int main() {
printf("GMP: %s\n", gmp_version);
return 0;
}
Alternatively, just download and use one of the versions of Yices with gmp statically linked.
Installing GMP
Unless you're using a version of Yices with gmp statically linked, you need to have GMP installed as a shared library on your machine.
GMP is preinstalled on several Linux distributions. Just make sure the version you have is recent enough (see above). The shared library is usually installed as
/usr/lib/libgmp.so.
Alternatively, you can download the latest GMP distribution, compile, and install it yourself. On most platforms both static and shared libraries can be built. On some platforms (e.g., cygwin), GMP builds only as a static library by default. To build the DLL instead, use
./configure --disable-static --enable-dynamic
when building GMP. It's a good idea to check the GMP documentation.
On cygwin, it is easier to download GMP precompiled: use setup.exe to download a recent version of GMP. This version should be installed as a DLL so Yices should work.
On cywgin, yices.exe exits and does nothing
This is probably because of a missing library (typically GMP). Install it as explained above.
Yices bugs
I'm using Yices 1.0.4 and ....
Stop! Download the latest version. Do not report bugs unless you can reproduce them in the current version of Yices.
... and I think there's a bug in bitvectors
Big-endian and little-endian representations were mixed up in some parts of the Yices code. That was fixed in yices 1.0.6. There was a major performance improvement for bitvectors in Yices 1.0.8.
Yices Input Language
How do I specify a real number to Yices?
Yices decides the theory of linear arithmetic (i.e., rationals), not reals, so non-integer constants are written as fractions. For example, 10.5 is (/ 105 10).
Constructing rationals and big numbers using the C-API
There are two functions for constructing numerical constants in the Yices C-API (see yices_c.h)
yices_expr yices_mk_num(yices_context ctx, int n)
This constructs a constant of value n, which can be any 32 bit integer.
For big numbers and rational numbers, the following function must be used:
yices_expr yices_mk_num_from_string(yices_context ctx, char * n)
n must be a null-terminated string of characters, in one of the following formats:
- +/- <number>
- +/- <number>.<fractional part>
- +/- <numerator>/<denominator>
where <number>, <fractional part>, <numerator>, and <denominator> are strings of decimal digits (<denominator> should be non-zero). The + sign is optional.
Why is (- 10) equal to 10 ?
Yices does not have unary minus. The expression
(- x_1 x_2 ... x_n)
is interpreted as x_1 - x_2 - ... - x_n as in Lisp. This convention was also used in the SMT-LIB notation. The expression '(- 10)' is a special case of this rule: it is intepreted as '10 - nothing', so it's equal to '10'.
The opposite of x must be written
(- 0 x).
Note: the space between '-' and '10' in the example is significant; '-10' with no space is parsed as an integer constant.
Yices interactive mode crashes on big formulas
Interactive mode is intended for direct human interaction and has hard limits on its buffer size. If you have a big formula, read it in directly without the -i flag as follows, and it can be as big as you want.
yices <options> < big_formula.ys
Yices doesn't do proper typechecking
That's correct. Yices is intended as a backend analyzer for other tools, and those tools are assumed to typecheck their own inputs and to generate type-correct input to Yices. The behavior of Yices on type-incorrect inputs such as the following is unpredictable.
(define-type s5 (subrange 0 4)) (define f::(-> s5 nat) (lambda (i::s5) i)) (assert (= (f 12) 12))
Here, the function f is applied outside its domain; this input is meaningless to Yices and its output is arbitrary. Notice that the 4 here could have been a variable, so determining type-correctness requires theorem proving; this should be done in the front end tool (e.g., as PVS does it).
So what's the -tc flag for?
When you are developing a tool that uses Yices, your early attempts might generate really bad input that causes Yices to crash without trace. The -tc flag causes Yices to do a bit of checking that may help you diagnose your problem.
What's the best way to say distinct?
The SMT-LIB language has a distinct predicate but it generates a quadratic number of disequalities. A better way to encode (distinct t1 ... tn) is
(define f::(-> T int)) (assert (and (= (f t1) 1) (= (f t2) 2) .... (= (f tn) n)))
where T is the type of t1 ... tn, and f is not used anywhere else.
Yices Output
What is the meaning of the sii... strings Yices sometime prints?
If you run yices with option -v 10 (or higher). Yices prints various characters to give some feedback about what it's doing.
There's information from the SAT solver:
- . is printed every 1000 decisions (i.e., every case split)
- r is printed at every restart
- s means "simplifying clause database"
- c means "compressing clause database" (deletion of learned clauses)
And information from the decision procedures:
- i means "interface equalities generated"
- L means "some closure axioms asserted" (to deal with lambda expressions)
- u or U means "update axiom instantiated" (to deal with array updates)
- I means "quantifier instantiation performed"
Timeouts
How do I tell if Yices Timed Out?
Yices' timeout is implemented via the Unix alarm function You can tell if Yices was interrupted by checking the exit status of the process. From a shell, you can check this via the variable $?. For example, if you do
yices --timeout=100 < input > output 2>&1 echo $?
you'll see a nonzero code if Yices timed out, and zero otherwise.
From a calling program, you can get the exit status of a child process using the wait system call.
SAT topics
Implementing allsat with Yices
Since Yices is an SMT solver, it cannot support a generic all-sat functionality (formulas may have infinitely many models). If you use only booleans then all-sat can be implemented using the C-API (see yices_c.h).
The standard way to do this is:
- construct and assert the formula(s)
- call yices_check
- if the result is l_true then get the value assigned to all boolean variables by calling yices_get_value
- construct a blocking clause from this and assert it
- repeat from 2 until yices_check returns l_false
There's currently no support for all-sat in the Yices language so this cannot be done using the yices executable.
Yices C API - Java Binding
This section contains some notes to remember when creating a JNI binding for Yices C (non-lite) API.
Mac OS X Leopard 10.5.2, Intel 32/64-bit
Yices supports both 32-bit and 64-bit Intel Macs, and a JNI binding can work for both using the dynamically-linked 32/64-bit versions. Moreover, the 32-bit version can be used under a 64-bit Mac. Note that Yices dynamically-linked library libyices.dylib assumes that the GMP library libgmp.3.dylib and itself are installed in /usr/local/lib. The paths can be inspected using otool as follows:
otool -L libyices.dylib
One can modify the paths by using the install_name_tool (see its man page).
The default version of GMP in MacPorts is 32-bit; one can get a 64-bit version by compiling GMP from its source distribution.
When using Yices 32-bit version, make sure to use a 32-bit JVM (and similarly with 64-bit). Java 5 that ships with Leopard supports both 32-bit and 64-bit. The latest Apple Java 6 Developer Preview (DP9) only supports 64-bit. Soylatte - a FreeBSD port of Java, provides an alternative implementation to Apple's and it has both 32/64-bit Java 6 versions which known to work with Yices.
Ubuntu 7.10, 32/64-bit
When developing a JNI binding, one way to make sure that libyices.so and libgmp.3.so can be loaded is by putting the paths to the libraries in the LD_LIBRARY_PATH. ldd is a similar tool to otool under Linux which can be used to inspect dynamically linked libraries. For example,
ldd -d libyices.so
