yices2 for Mac

SRI Yices 2

SRI Yices 2 is a solver for Satisfiability Modulo Theories (SMT) problems. Yices 2 can process input written in the SMT-LIB language, or in Yices' own specification language. We also provide a C API and bindings for Java, Python, Go, and OCaml.

This repository includes the source of Yices 2, documentation, tests, and examples.

Yices 2 is developed by Bruno Dutertre, Dejan Jovanovic, Stéphane Graham-Lengrand, Ian A. Mason, and Ahmed Irfan at the Computer Science Laboratory, SRI International. To contact us, or to get more information about Yices, please visit our website.

Simple Examples

Here are a few typical small examples that illustrate the use of Yices using the SMT2 language.

Linear Real Arithmetic

Bit-Vectors

Non-Linear Arithmetic

Running Yices on the above problem gives

Parallel Yices Example

Yices can be run in parallel using a portfolio approach, which launches several instances of yices_smt2 with different configurations and returns as soon as one instance finds a solution. This is useful for hard SMT problems where different configurations may solve the problem faster.

A Python script is provided in utils/yices2_parallel.py for this purpose. Example usage: --yices specifies the path to the yices_smt2 executable (default: yices_smt2 in the script directory) -n sets the number of parallel threads/configurations (default: 4) --verbose enables detailed output The last argument is the path to your SMT2 file

The script will run several Yices instances in parallel and print the result (sat, unsat, or unknown) as soon as one instance finishes.

For more options, run:

Installing Prebuilt Binaries

Currently you can install Yices either using Homebrew or Apt.

Homebrew

Installing on Darwin using homebrew can be achieved via:

This will install the full mcsat-enabled version of Yices, including dynamic library and header files.

Apt

To install Yices on Ubuntu or Debian, do the following:

This will install the executables. If you also need the Yices library and header files, replace the last step with:

Building From Source

Prerequisites

To build Yices from the source, you need: GCC version 4.9.x or newer (or clang 3.3 or newer) gperf version 3.0 or newer the GMP library version 4.1 or newer other standard tools: make (gnumake is required), sed, etc.

To build the manual, you also need: a latex installation the latexmk tool

To build the on-line documentation, you need to install the Sphinx python package. The simplest method is:

Sphinx 1.4.x or better is needed.

Quick Installation

Do this:

This will install binaries and libraries in /usr/local/. You can change the installation location by giving option --prefix=... to the ./configure script.

For more explanations, please check doc/COMPILING.

Support for Non-Linear Arithmetic and MC-SAT