===============================================================================
The veriT SMT solver
Instructions to enable experimental support for non-linear real arithmetics
===============================================================================

veriT can cooperate with the computer algebra system Reduce/Redlog for reasoning
on non linear arithmetic expressions. The instructions to enable this
experimental feature follow. They must be executed before veriT is built to be
effective.

1. Getting Reduce's source code
===============================

To compile this capability, put the Reduce directory in extern/reduce:
  svn export svn://svn.code.sf.net/p/reduce-algebra/code/trunk extern/reduce

2. Build Reduce and libreduce
=============================

Go in the directory
  cd extern/reduce
and compile Reduce [*,**]
  ./configure --with-psl
  make

[*] Reduce relies on some packages being installed, including
    python2.7, python-dev, automake, libtools.
[**] Note to OS X users: If compilation fails, try issuing the 
following command ahead of the configuration step, :
  export DONT_USE_XPORT=1

You should also compile libreduce in extern/reduce/generic/libreduce
  cd extern/reduce/generic/libreduce
  make

This should create a directory containing library files in
extern/reduce/generic/libreduce named according to your OS distribution
(e.g. x86_64-unknown-ubuntu13.04)

3. Environment setup
====================

Before running veriT, set environment variable VERIT_REDUCE_PATH to the path for
redpsl (created while compiling Reduce).  For instance:
  export VERIT_REDUCE_PATH=$HOME/veriT/extern/reduce/bin/redpsl

4. Summary
==========

After unpacking veriT-201310 distribution, and before building veriT, execute
the following commands:

  cd veriT-201310
  export VERIT_HOME=$PWD
  svn export svn://svn.code.sf.net/p/reduce-algebra/code/trunk extern/reduce
  cd $VERIT_HOME/extern/reduce
  ./configure --with-psl
  make
  cd $VERIT_HOME/extern/reduce/generic/libreduce
  make
  export VERIT_REDUCE_PATH=$VERIT_HOME/extern/reduce/bin/redpsl
  echo "export VERIT_REDUCE_PATH=$VERIT_REDUCE_PATH" >> $HOME/.bash_profile

5. Final words
==============

Please note that this is highly experimental.

