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

 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 and Dejan Jovanovic, 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


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

Do this:

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

This release has experimental support for non-linear real arithmetic,
but it 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) After you've installed libpoly, configure yices with the
   flag '--enable-mcsat', then build Yices as usual:

    ./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 BUILD
-------------

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.