Yices SMT Solver, Copyright SRI International
=============================================

This file is part of the Yices __YICES__ binary distribution for Cygwin.

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

  bin/yices.exe       (for the Yices 2 language)
  bin/yices-smt.exe   (for SMT-LIB 1.2)
  bin/yices-smt2.exe  (for SMT-LIB 2.0)
  bin/yices-sat.exe   (sat solver, DIMACS format)

and the Yices libraries and header files

  bin/cygyices.dll

  lib/libyices.dll.a
  include/yices.h
  include/yices_types.h
  include/yices_limits.h
  include/yices_exit_codes.h


Examples and documentation are in the examples and doc directories.


The binaries and library require the GNU Multiprecision library (GMP)
version __GMP__ or compatible. GMP must be installed as a DLL on Cygwin
for Yices to work. GMP is copyright Free Software Foundation (see NOTICES).



Recommended Installation
------------------------

1) Copy cygyices.dll and the executables in /usr/bin:

   cp bin/* /usr/bin


2) Copy libyices.dll.a in /usr/lib:

   cp lib/libyices.dll.a /usr/lib


3) Copy the header files in /usr/include



For more information, please visit http://yices.csl.sri.com.