Yices

Yices is an SMT (Satisfiability Modulo Theories) solver developed by SRI International. It is designed to determine the satisfiability of logical formulas that combine a propositional skeleton with background theories, such as arithmetic and data structures, a common need in formal verification, software analysis, and research.

Yices implements a DPLL(T) architecture, using a SAT-like engine to decide the boolean structure while invoking specialized theory solvers for the underlying domains. Its design emphasizes speed and scalability, with support for incremental solving, activity management, and the ability to add and retract constraints via push and pop operations.

Yices supports several quantifier-free theories and combinations, including linear arithmetic over integers and reals, bit-vectors, arrays, and uninterpreted functions, as well as their mixes. The second version, Yices 2, introduced a modular engine with improved theory solvers, model generation, and better integration with programming languages. It also provides a more complete API surface and support for additional data types and backends.

The solver is available as a standalone tool and as a library with APIs for C and higher-level languages such as OCaml and Python. It is used in academia and industry for tasks ranging from verification of software and hardware to automated reasoning research. Yices competes with other SMT solvers by offering fast specialized solvers and efficient incremental reasoning.