===============================================================================
                         The veriT SMT solver
              Compilation and installation instructions
===============================================================================


Requirements
============

veriT depend on the following software being already installed:

- GNU make
- GCC's C and C++ compilers (gcc/g++)
- ar & ranlib
- flex & bison
- wget, tar, patch, unzip, to fetch and build external dependices
- doxygen , to generate the documenation

veriT depends on other program and libraries, which will be automatically
dowloaded and compiled under the extern subdirectory during the installation
process. This third-party software is the following:
- gmp: GNU Multiple Precision Arithmetic Library 
    [http://gmplib.org]
- reduce: Computer Algebra System
    [http://reduce-algebra.com]

Compilation and installation
============================

% make

Then as superuser:

% make install

If you do not have superuser rights to your machine, change the PREFIX_BIN
variable to the directory you would like veriT to be installed.

Do not forget to extend your PATH variable accordingly if it is needed.
In bash/zsh it is done by the following command.

% export PATH=$PATH:<veriT install directory>.

To reason on non-linear arithmetic constraints, veriT makes calls to reduce.
You have to set and compile reduce in veriT's directory, in subdirectory 
extern.reduce.  The user shall also set the shell environment variable to
the directory where it can find the binary redpsl:
% export VERIT_REDUCE_PATH=$HOME/veriT/extern/reduce/bin/redpsl

Documentation
=============

Optionally, you may want to generate documentation for veriT.
The following command generates both user and developer documentation:

% make doc

Note
----
Generating the documentation takes much more time and space than the compilation
itself.
