diff --git a/doc/index.rst b/doc/index.rst index 2a5bd13d12be2ef67c44df48aebbed9eca7d1e7c..2862cb2a406384e7a7797c8fff673b03192ec633 100644 --- a/doc/index.rst +++ b/doc/index.rst @@ -27,6 +27,5 @@ Indices and tables ================== * :ref:`genindex` -* :ref:`modindex` * :ref:`search` diff --git a/doc/installation.rst b/doc/installation.rst index 8c5e0df06eac3558d826271db69edf229fcb421b..39b89cbf28db66910ad036bdf170d02d9033e763 100644 --- a/doc/installation.rst +++ b/doc/installation.rst @@ -13,7 +13,7 @@ Windows. **Requirements:** -* 1.7 Java Development Kit. *(Java 8 is not officially supported)* +* `1.7 Java Development Kit <http://www.oracle.com/technetwork/java/javase/downloads/jdk7-downloads-1880260.html>`_ *(Java 8 is not officially supported)* * SBT 0.13.X (Available from http://www.scala-sbt.org/) @@ -63,7 +63,7 @@ all the appropriate settings: $ sbt script -You will now need to either port the bash script to Windows, or by running it +You will now need to either port the bash script to Windows, or to run it under Cygwin. .. _smt-solvers: @@ -72,20 +72,25 @@ SMT Solvers ----------- Leon relies on SMT solvers to solve the constraints it generates. We currently -support two major SMT solvers: Z3 and CVC4. +support two major SMT solvers: + * CVC4, http://cvc4.cs.nyu.edu/web/ + * Z3, https://github.com/Z3Prover/z3 For Linux users, a native Z3 API is bundled with Leon and should work out of the box. For OS-X and Windows users, you will either have to recompile the native communication layer yourself or use the SMT-LIB API. +Solver binaries that you install should match your operating system and +your architecture. + In any case, we recommend that you install both solvers separately and have their binaries available in the ``$PATH``. Since the default solver uses the native Z3 API, you will have to explicitly -specify another solver if this native layer is not available for you: - +specify another solver if this native layer is not available for you. Check the +the ``--solvers`` command line option: -.. code-block:: bash +:: --solvers=s1,s2 Use solvers s1 and s2 Available: diff --git a/doc/r b/doc/r new file mode 100755 index 0000000000000000000000000000000000000000..d210288c6c7b8e7cbb94f8591be3af6d2c4c32e6 --- /dev/null +++ b/doc/r @@ -0,0 +1 @@ +make html