@@ -10,6 +10,28 @@ The CAISAR executable provide several subcommands, called
...
@@ -10,6 +10,28 @@ The CAISAR executable provide several subcommands, called
using ``caisar [COMMAND]``. ``caisar --help`` provides a list of
using ``caisar [COMMAND]``. ``caisar --help`` provides a list of
all available commands. Additionally, ``caisar [COMMAND] --help`` gives a synopsis for each available command.
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
Logging
*******
*******
...
@@ -126,10 +148,5 @@ Parsing the output of the prover
...
@@ -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.
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
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>`_!
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``.
