======================================================================

 The Yices SMT Solver. Copyright 2017 SRI International.

 Yices is free software: you can redistribute it and/or modify
 it under the terms of the GNU General Public License as published by
 the Free Software Foundation, either version 3 of the License, or
 (at your option) any later version.

 Yices is distributed in the hope that it will be useful,
 but WITHOUT ANY WARRANTY; without even the implied warranty of
 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 GNU General Public License for more details.

 You should have received a copy of the GNU General Public License
 along with Yices.  If not, see <http://www.gnu.org/licenses/>.

======================================================================


CONTENT
-------

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

Yices 2 is developed by Bruno Dutertre, Dejan Jovanovic, and Ian Mason
at the Computer Science Laboratory, SRI International. To contact us,
report a bug, or to get more information about Yices, please visit our
website at http://yices.csl.sri.com.


PREREQUISITES
-------------

To build Yices from the source, you need:

- GCC version 4.0.x or newer (or clang 3.0 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:

  sudo easy_install -U Sphinx

Sphinx 1.3.x or better is needed.


QUICK INSTALLATION
------------------

Do this:

  autoconf
  ./configure
  make
  sudo make install

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
---------------------------------

Yices supports non-linear real and integer arithmetic, but this is not 
enabled by default. If you want non-linear arithmetic, follow these 
instructions:

1) Install SRI's library for polynomial manipulation. It's available
   on github (https://github.com/SRI-CSL/libpoly).

2) Install the CUDD library for binary-decision diagrams. We recommend
   using the github distribution: https://github.com/ivmai/cudd.

3) After you've installed libpoly and cudd, add option --enable-mcsat 
   to the configure command. In details, type this in the toplevel
   Yices directory:

    autoconf
    ./configure --enable-mcsat
    make
    sudo make install

   You may need to provide LDFLAGS/CPPFLAGS if ./configure fails to
   find the libpoly library. Other options may be useful too.  Try
   ./configure --help to see what's there.


WINDOWS BUILDS
--------------

We recommend compiling using Cygwin. If you want a version that works
natively on Windows (i.e., does not depend on the Cygwin DLLs), you
can compile from Cygwin using the MinGW cross-compilers. This is
explained in doc/COMPILING.


DOCUMENTATION
-------------

To build the manual from the source, type

   make doc

This will build ./doc/manual/manual.pdf.

Other documentation is in the ./doc directory:

- doc/COMPILING explains the compilation process and options in detail.
- doc/NOTES gives an overview of the source code.
- doc/YICES-LANGUAGE explains the syntax of the Yices language, and
  describes commands, functions, and heuristic parameters.


To build the Sphinx documentation:

  cd doc/sphinx
  make html

This will build the documentation in build/html (within directory
doc/sphinx). You can also do:

  make epub

and you'll have the doc in build/epub/Yices.ebup.