From b7dfd40bfd5417555c9f1beb208f3962f94311ef Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Wed, 8 Nov 2023 16:38:14 +0100
Subject: [PATCH] [doc] Documented command line options.

---
 doc/usage.rst | 27 ++++++++++++++++++++++-----
 1 file changed, 22 insertions(+), 5 deletions(-)

diff --git a/doc/usage.rst b/doc/usage.rst
index dce8d75..62e5bd3 100644
--- a/doc/usage.rst
+++ b/doc/usage.rst
@@ -10,6 +10,28 @@ The CAISAR executable provide several subcommands, called
 using ``caisar [COMMAND]``. ``caisar --help`` provides a list of
 all available commands. Additionally, ``caisar [COMMAND] --help`` gives a synopsis for each available command.
 
+Command line options
+--------------------
+
+``caisar verify`` have the following specific 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:*``
+* ``-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
+  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.
+
+
 Logging
 *******
 
@@ -126,10 +148,5 @@ Parsing the output of the prover
 ********************************
 CAISAR rely on Why3's `drivers <https://why3.lri.fr/doc/technical.html#drivers-for-external-provers>`_ to parse the output of the prover.
 
-
 If you add support for a new prover, consider opening a merge
 request on our `forge <https://git.frama-c.com/pub/caisar/-/merge_requests>`_!
-
-Assuming you have installed a prover and you filled 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``.
-- 
GitLab