INSTALL

Requirements:
-------------
  OCaml (reasonably recent version; I use version 4.01.0)
  OCamlgraph (reasonably recent version; I use version 1.8.3)
  One or more of the following SMT-solvers:
    yices, yices2, z3, cvc4, mathsat5
  Optionally:
   * APRON
   * z3 ML bindings:
      To get z3 to work with kittel/koat directly, install the new ML
      bindings. At this time (z3 stable version 4.3), they are only
      available from the z3 source code repository on codeplex, in the
      "ml-ng" branch.
      To install them, check out this branch, configure z3 with
      --ml (you will need ocamlfind, ocamlidl and some other libraries
      as well, refer to the z3 documentation) and build as usual.
      "make install" should then install the files into
      /usr(/local)/lib/ocaml/$VERSION/, where VERSION corresponds to
      your OCaml version.
      You may need to add this path to the include path of your compiler,
      cf. Makefile.

  Use of APRON and the z3 ML bindings can be disabled by creating a
  file "user.cfg".  To disable use of APRON, add a line
  "HAVE_APRON=false" to that file.  To disable use of the z3 ML
  bindings, add a line "HAVE_Z3=false" to that file.

Build instructions:
-------------------
  "make kittel" builds the termination analysis backend "kittel.native"
  "make koat" builds the complexity analysis backend "koat.native"
  "make convert" builds "convert.native" which converts Simple programs to C

  You might need to modify the KITTEL_LIBPATH and KOAT_LIBPATH lines in the
  Makefile to ensure that OCamlgraph and/or APRON is found (the
  "-I,+ocamlgraph" resp. "-I,+apron" parts).