Introduction

Yices is a high-performance SMT solver developed at SRI International. Yices decides the satisfiability of propositional formulas that mix uninterpreted function symbols and equality with interpreted symbols from the following theories:

• linear real and integer arithmetic
• extensional arrays
• fixed-size bit-vectors
• recursive datatypes, tuples, and records
• lambda expressions
• quantifiers

Yices also does MaxSMT (given an unsatisfiable set of weighted clauses, find the satisfiable subset of maximum weight); dually, it can find the unsat core (the set of unsatisfiable clauses of minimum weight).

Using Yices

The Yices input language is similar to the SAL languages. Yices also accepts specifications written in the SMT-LIB language. Yices can be used as a regular SAT solver and can read boolean problems in the CNF DIMACS format.

Yices can also be used as a library in other applications. A light-weight API is provided for this purpose. A richer API is under construction.

What About ICS?

ICS was the first SMT solver developed at SRI International. Until recently, ICS2.0 was the default backend solver used by the SAL infinite-state bounded model checker.

ICS has several inefficiencies and performance limitations and it should no longer be considered state-of-the-art. We do not maintain or develop ICS anymore, but ICS 2.0 can still be downloaded at http://ics.csl.sri.com.

In 2005, we implemented from scratch two new prototype SMT solvers that greatly outperformed ICS. Both solvers participated in the SMT-COMP05 competition associated with CAV 2005.

• Simplics was specialized for quantifier-free linear real arithmetic (QF_LRA). It finished first in the QF_LRA division in SMT-COMP05.
• Our other solver was an early version of Yices (Yices 0.1). It participated in all divisions of the SMT-COMP05 competition, and finished first in two of them (QF_LIA and QF_AULIA) and second in all the others.

Based on our experiments with Yices 0.1 and Simplics, we reimplemented a new SMT solver from scratch, with a new architecture and more efficient solvers. This new SMT solver is Yices 1.0, the first official release of Yices. It is substantially faster and more robust than Simplics and Yices 0.1 and it is several orders of magnitude faster than ICS.

Although Yices is better than ICS in most dimensions (it has a richer input language with records, dependent typing and subtyping, and it provides more complete and vastly faster automation), Yices does lack some of ICS' capabilities: Yices does not include a canonizer, it does not have applicative state (only push/pop and assert/retract), and it does it offer a capability for displaying and querying its internal state. It remains to be seen whether these lacks are significant in practice.

Last modified: Thu 10 Dec 2009 10:43 PST