SPPoC: Symbolic Parameterized Polyhedral Calculator

	(http://www.lifl.fr/west/sppoc/)

Version: 1.2.1

What is it all about?

   SPPoC is a symbolic interface to the following polyhedral
   computation tools: PolyLib, PIP, Omega. 

   Applications: all the field of the static analysis of "static
   control" programs and surely many others.

Installing SPPoC

   Requirements

      SPPoC is written in Objective Caml. You will need version 3.00
      (or higher) of the Objective Caml compiler. You will
      also need the companion program camlp5.

      As the PolyLib uses the GNU MP library to handle multi-precision
      arithmetic, you will need to download it as well.

      You will also need the GNU versions of make and test and gcc
      v3.3 or higher.

      Finally, you can download the source files of SPPoC (current
      version: 1.2.1 released 2003/11/19, it includes the PolyLib v4.16,
      the omega library v1.1 and a modified version of PIP).

      Optionally you can download and install the ledit line editor
      that improves the editing facilities of sppoc.

   Compilation

          Extract the archive: tar xzf spocc.tgz. 
          Configure the Makefiles: edit file Etc/Makefile.config to
          suit your installation. You can also specify the C++ compiler
	  for omega with something like "CXX=g++-3.3.6 make".
          You may need to adjust some variables in Polylib/Makefile to
          compile the PolyLib.  
          Create the compilation dependences: make depend. 
          Compile SPPoC: make (if some problem occur, try make depend
          followed by make).
          You then have an interactive version of SPPoC:
          Bin/spocc. You can test this version with the examples from
          the Test and Calcom directories.   
          You can then install SPPoC: make install. 

User's Guide

          One way to use SPPoC is the sppoc interactive
          calculator. Actually it is an ocaml toplevel with the SPPoC
          module and all the required libraries preloaded. The
          quotations and the pretty-printers are also automatically
          started. (The preloading mechanism installs a .ocamlinit
          file in the current directory. If such a file already
          exists, it is not replaced. See the ocaml documentation for
          more details on this mechanism.)

          The sppoc command used alone starts the interactive
          calculator. If a file is given as an argument, the commands
          in this file are exectued as a script.

	  As sppoc tries to use the ledit line editor if you have it,
	  using sppoc by redirection of its input is not reliable. The
	  right way to interactively execute a file is: start sppoc
	  and type the command #use "file.ml";;.

          You can also use SPPoC as a library. To link an ocaml
          program with SSPoC, use a command line such as:

              ocaml -o yourprogram -I /path/to/libsppoc libsppoc.cma
              yourprogram.ml

          or 

              ocaml -o yourprogram -pp camlp5sppoc -I /path/to/libsppoc
              libsppoc.cma yourprogram.ml

          if you want to use the quotations. 

      In all the cases you have to open the SPPoC module (via the open
      SPPoC;; statement) to be able to avoid prefixing all the sppoc
      commands by SPPoC.

TO DO list

	  Upgrade to omega v1.2
          Smash the remaining bugs.
          Test the native code compilation. 
          Update the documentation.
          For a future version: handle equalities in QUASTs' predicates 

Documentation: see the Documentation directory (you will need LaTeX to
recompile the files).


                                               Pierre Boulet, Xavier Redon
                                               sppoc@lifl.fr