Documentation

The on-line documentation includes the Yices manual and the API Reference

The manual describes the Yices language and type system. It explains how to download and install Yices, and how to use the different solvers included in the distributions. More documentation and many examples are also included in all the distributions.

Technical Background

Tool paper:

• Bruno Dutertre, Yices 2.2, presented at CAV'2014, Vienna, Austria, 2014. BibTeX.

Presentation at the SMT Workshop 2016:

• Bruno Dutertre, The Nuts and Bolts of Yices. This describes some data structures and algorithm used in Yices 2

The basics of SMT solving:

• Leonardo de Moura, Bruno Dutertre, and Natarajan Shankar, A Tutorial on Satisfiability Modulo Theories, presented at CAV'2007, Berlin, Germany, 2007. BibTeX.

Simplex-based arithmetic solver used by Yices:

• Bruno Dutertre and Leonardo de Moura, A Fast Linear-Arithmetic Solver for DPLL(T), presented at CAV'2006, Seattle, WA, August 2006. BibTeX
• Bruno Dutertre and Leonardo de Moura, Integrating Simplex with DPPL(T), Technical Report, CSL-06-01, Computer Science Laboratory, SRI International, May 2006. BibTeX. This is an expanded version of the CAV'2006 paper above.

A more advanced linear-arithmetic solver for SMT:

• Tim King, Clark Barrett, and Bruno Dutertre, Simplex with Sum of Infeasibilities for SMT, presented at FMCAD, Portland, OR, October 2013. BibTeX.

A technique for learning lemmas used in Yices as a preprocessing step to learn implied equalities.

• Nikolaj Bjørner, Bruno Dutertre, and Leonardo de Moura, Accelerating Lemma Learning Using Joins, short paper presented at LPAR 2008, Doha, Qatar, November 2008. BibTeX.

Exists/forall solving with Yices and applications:

• Bruno Dutertre, Solving Exists/Forall Problems with Yices, extended abstract presented at the 2015 SMT Workshop, San Francsico, CA, July 2015, BibTeX.
• Ashish Tiwari, Adrià Gascón, and Bruno Dutertre, Program Synthesis Using Dual Interpretation, presented at CADE-25, Berlin, Germany, August 2015, BibTeX.
• Adrià Gascón, Pramod Subramanyan, Bruno Dutertre, Ashish Tiwari, Dejan Jovanović, Sharad Malik, Template-Based Circuit Understanding, presented at FMCAD, Lausanne, Switzerland, October 2014. BibTeX.

MCSAT solver:

• Leonardo de Moura and Dejan Jovanović, A Model-Constructing Satisfiability Calculus, presented at VMCAI, Rome, Italy, January 2013, BibTeX.
• Dejan Jovanović, Solving Nonlinear Integer Arithmetic with MCSAT, presented at VMCAI, Paris, France, January 2017, BibTeX.
• Stéphane Graham-Lengrand, Dejan Jovanović, and B. Dutertre, Solving bitvectors with MCSAT: explanations from bits and pieces, accepted at IJCAR, Paris, France, July 2020, BibTeX.