[doc] Fixed supported solver links, added VNN-LIB warning and added cmdline options.

doc/contributing.rst

@@ -35,12 +35,14 @@ Setting up a development environment
 With an Opam switch
 -------------------
 
-Need to download `ocaml language server <https://github.com/ocaml/ocaml-lsp>`_, `ocamlformat <https://github.com/ocaml-ppx/ocamlformat>`_ v0.25.1 and
-`ocp-indent <https://github.com/OCamlPro/ocp-indent>`_.
+Once an opam switch is setup, one needs to download `ocaml language server <https://github.com/ocaml/ocaml-lsp>`_, `ocamlformat <https://github.com/ocaml-ppx/ocamlformat>`_ v0.25.1 and `ocp-indent <https://github.com/OCamlPro/ocp-indent>`_.
 
 With nix-shell
 --------------
-TODO
+
+With nix setup as detailed in :ref:`nix`, typing `nix develop` will create a
+shell environment tailored for CAISAR development. You can build CAISAR by
+following the :ref:`source` instructions.
 
 .. index:: Prover;prover
 

doc/foreword.rst

@@ -30,17 +30,6 @@ provide both the specification language, called WhyML, and the infrastructure
 needed to interoperate with external provers. These are generally called
 *provers*, although some of them do not directly provide a logical proof.
 
-.. _supported-provers:
-
-Supported Provers
------------------
-
-.. toctree::
-   :maxdepth: 2
-   :caption: Supported Provers:
-
-   provers
-
 
 Availability
 ------------

doc/index.rst

@@ -35,6 +35,7 @@ This work has been partly supported by the `Confiance.ai`_ program.
    examples
    interpretation
    contributing
+   provers
    genindex
    CAISAR website <http://www.caisar-platform.com>
 

doc/installation.rst

@@ -53,6 +53,8 @@ To run the CAISAR Docker image, do the following:
 
    $ docker run -it laiser/caisar:pub sh
 
+.. _nix:
+
 Install through Nix
 -------------------
 
@@ -101,6 +103,8 @@ It will contain the ocaml toolchain already setup and installed, and the ocaml l
 
    $ nix develop
 
+.. _source:
+
 Compile from source
 -------------------
 

doc/provers.rst

+.. _provers:
+
+Supported provers
+*****************
 
 The supported provers are the following:
 
@@ -31,3 +35,10 @@ SMT solvers
 -----------
 Standard SAT/SMT solvers that support the SMT-LIBv2 input language.
 As of now, only CVC5 had been tested.
+
+
+.. warning ::
+   Marabou and VNN-LIB provers (PyRAT, alpha-beta-CROWN) do not accept strict
+   inequalities. Thus CAISAR treats strict inequalities as non-strict ones. We
+   are aware this is incorrect in general, but it is as of today the common
+   practice for the community.

doc/usage.rst

@@ -17,16 +17,15 @@ Command line options
 
 * ``-D name:value`` or ``--define=name:value``: define a declared constant ``name`` with the given value ``value``. Constant must be declared in the theory file.
 * ``--dataset=FILE``: Path of a dataset file. To be deprecated.
-* ``-g theory,..,theory:goal,..,goal``: Verify only the ``goal`` in the
-  ``theory``. Theory must already be defined in the specification file. It is
-  possible to verify all goals for one ``theory`` only using ``theory:*``
+* ``-g [theory]:goal,..,goal`` or ``--goal [theory]:goal,...,goal``: Verify only the ``goal`` in the ``theory``. Theory must already be defined in the specification file. When no theory is provided, verify the specified goals for all theories.
+* ``-t theory`` or ``--theory=theory``: Verify all goals in ``theory``.
 * ``-m MEM`` or ``--memlimit=MEM``: Memory limit. ``MEM`` is intended in megabytes
   (MB); (GB) and (TB) can also be specified. Default: 4000MB.
 * ``-t TIME`` or ``--timelimit=TIME``: Time limit. ``TIME`` is intended in seconds (s); minutes (m) and hours (h) can also be specified.
   (MB), (GB) and (TB) can also be specified. Default: 20s.
 * ``-p PROVER`` or ``--prover=PROVER``. Prover to use. Support is provided for
   the following: Marabou, PyRAT, SAVer, AIMOS, CVC5, nnenum, alpha-beta-CROWN.
-  See :ref:`supported-provers` for a detailed description of each prover
+  See :ref:`provers` for a detailed description of each prover
   capacity.
 * ``--prover-altern=VAL``: alternative prover alternatives to use. Prover
   alternatives are prover-specific configurations that help provers to better perform on specific problems. Supported prover alternative are ``ACAS`` for alpha-beta-CROWN and PyRAT.
@@ -60,7 +59,7 @@ CAISAR relies on external provers to work. You must install
 them first, then point CAISAR to their location. Please
 refer to each prover documentation to install them.
 
-CAISAR already support several provers, listed in :ref:`supported-provers`.
+CAISAR already support several provers, listed in :ref:`provers`.
 Assuming you have installed a prover with an entry in the
 ``caisar-detection.conf`` file, you can register the prover to CAISAR using the
 following command: ``PATH=$PATH:/path/to/solver/executable caisar config -d``.
@@ -79,7 +78,7 @@ documentation to get a first grasp on using WhyML.
 
 Provided a file ``trust.why`` containing a goal to verify, the command ``caisar verify --prover=PROVER trust.why``
 will verify the goals using the specified prover. A list of
-supported provers is available in :ref:`supported-provers`. The prover
+supported provers is available in :ref:`provers`. The prover
 must already be registered by CAISAR. Currently, only one
 prover can be selected at a time; future work will allow
 selecting multiple provers and orchestrate verification