=============
Prerequisites
=============

Kind relies on the following systems/solvers:

1. OCaml (version 3.11.2 or greater). More information can be found at http://www.ocaml.org

2. An MPI implementation: 
    * OPENMPI (http://www.open-mpi.org/)
    * MPICH2  (http://www.mcs.anl.gov/research/projects/mpich2/)

3. A compatible SMT solver, including
     * Yices, available at http://yices.csl.sri.com/
         Get the latest version, with GMP statically linked
         (this requires a click-through license agreement)
     * CVC3, available at http://www.cs.nyu.edu/acsys/cvc3/ 
         (version 1.5 or later)


=================
Required packages
=================

Kind relies on the following OCaml libraries:

  * ExtLib: Extended library for OCaml
  * OcamlMpi: Mpi wrapper for OCaml

If not present, both libraries will be installed in the './lib' directory


============
SMT Solvers
============

It is possible to use either the CVC3 pre-compiled executable or to compile
your own version.  Similarly, with a command flag, it is possible to use
the pre-compiled Yices executable.

The default operation of Kind uses a wrapper version of the Yices solver.
The wrapper is written in C and, when compiled, calls the Yices (statically
linked) library.  (Yices' command line version's interactive mode is limited 
in the size of formulas it can accept).  Depending on the version of Yices 
you use, you may need to upgrade your compiler version.


============================== 
Configuration and Installation
==============================

The './configure' script examines your system and checks for the
required packages and solvers. The script has some options, that can
be listed using the command `./configure --help'.

If you would like to use Kind with the Yices wrapper:

./configure  --with-yicesw --yices-dir [YICES DIR]

If the configuration process was a successful, it will generate the
necessary Makefile. 

To compile Kind:

> make

To install Kind:

> make install



=======
Contact
=======

For more information please contact:
    Temesghen Kahsai (temesghen-kahsaiazene@uiowa.edu) 
or Cesare Tinelli (cesare-tinelli@uiowa.edu).


