=============
Pre-requisites
=============

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

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.


============================== 
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 compile and install Kind with the Yices wrapper (which is recommended), 
issue the following command:

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

If you would like to compile and install KIND in a local directory, issue the following command:

  > ./configure --prefix=[LOCAL-DIR] --with-yicesw --yices-dir=[YICES DIR]

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

To compile KIND:
  
  > make

To install KIND:

  > make install  (might need a "sudo")

If you have configured and installed KIND in a local directory (i.e. by using --prefix=[LOCAL-DIR] in ./configure); 
you need to add the [LOCAL-DIR] to your system path.


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


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

For more information please contact:

    * Temesghen Kahsai (temesghen-kahsaiazene@uiowa.edu) 
    * Cesare Tinelli (cesare-tinelli@uiowa.edu).


