INSTALLATION:

SMT-LIB:

====

Please read this file in its entirity before proceeding, as there are a 
number of pieces of information you will need to provide to complete the 
installation.

In brief:

What you need in addition to this source:
- CVCL source (the current unstable build)
- Ocaml 3.07-2
- OcamlMakefile
Locations for these are listed below.

Once these are installed, you will also need to run the configure.pl script
to tell the system where to find these files.

Then enter the dpllt/cvcl/smt directory and run make.  The file "sammy" will
then be created.

====

Obtain and install the following modules:

CVCL: Install the current "unstable" build of CVCL.
(http://verify.stanford.edu/CVCL/)  Configure this with the 
"--with-build=optimized" option.

Note the cvcl source files' location, as well as the install location 
for a later step (1).

Ocaml: There is an incompatability with the current Ocaml 3.08.x build;
please install and use Ocaml 3.07-2 (3.07, patch level 2) instead.
Ocaml sources and precompiled RPMs can be found at http://www.ocaml.org.

It is assumed that the ocaml files are within the appropriate PATH variables
(the RPMs should default to /usr, which is assumed; if you install the 
libraries elsewhere, please note the location (2)).

If you need to compile ocaml 3.07 yourself, you may get a few compilation 
errors in the ocamldoc compilation resulting from UTF-8 formatted characters.
If this is the case, remove the offending characters or lines (the first
will be odoc_sig.ml, line 1302, then two lines in odoc_ast.ml, and one line
in odoc.ml).  It may also be necessary to set the LC_ALL=C environment 
variable.

In order to ensure that all libraries will be visible, it may be necessary
to edit /etc/ld.so.conf and then run ldconfig (as root).  Make sure the
path /usr/local/lib appears in ls.so.conf.  Alternatively run the configure 
script and specify absolute directories.  (And you will need to move both 
the sammy executable and the libsatbox library file to the same directory 
to execute it in a different location.)

Ocaml packages:

This build currently only requires the OCamlMakefile, 1.64 or later.
    (http://www.ai.univie.ac.at/~markus/home/ocaml_sources.html)

Note the OcamlMakefile's location for a later step (2).

====

NOTE: There is a configure.pl script in this directory.  It can be run to 
tell the system about any relevant non-default directories (1,2,3 above).

It should also be possible to modify the dpllt/cvcl/interface/Makefile.in
by hand.

====

Installing sammy:

The sammy code tarball found at <ADDRESS> can be extracted via 
	tar -xfz sammy.tar.gz
which will create and populate a dpllt directory.  The SMT-LIB command-line
executable of sammy will be located in dpllt/cvcl/smt/ (the example client 
code is in dpllt/client/).

Configuration:
This currently requires some information generated by cvcl's installation.
Execute the configure.pl script to extract the necessary information.  To 
do so, run:
	perl configure.pl
and answer the provided questions about relevant directories and flags.
You will need to know the directory in which you had placed the cvcl source 
for compilation, as well as the location of the ocaml libraries and the
OCamlMakefile.

Once this is done, cd to dpllt/cvcl/smt/ and run make.  This will produce 
a command-line executable "sammy" in that directory.

Sammy is run by executing:
./sammy [flags] <benchmark file>
  or
./sammy [flags] -stdin

Important flags include:

-no_negate_queries
     Normal execution determines if the provided formula is VALID.
     Including this flag checks if the provided formula is SATISFIABLE.

-vsids_only
     Use the basic chaff VSIDS decision heuristic.

-quiet
     Only output the result, no other information.

-t <sec>
     System timeout (default 3600 sec).  The system will attempt to
     halt gracefully after this time has elapsed.

-stdin 
     The benchmark file is read from standard input.

--help
     list all command-line flags.

====

Documentation:
 
Hypertext code documentation can be automatically generated by executing 
	make -htdoc
from dpllt/cvcl/smt/ after the code has been compiled.  The documentation 
will be placed in dpllt/cvcl/smt/doc/.

API documentation is associated with the file dpllt/cvcl/api_native.mli 
(for direct ocaml calls).  Specifics on the various program parameters, 
many of which can be set through command-line options, are located in the 
dpllt/global.ml comments.

If you have any questions or problems, please contact tinelli@cs.uiowa.edu
or ghagen@cs.uiowa.edu.