Skip to content
Snippets Groups Projects
Commit 48c4a5af authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

More options section

parent 672e403a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 220 additions and 67 deletions
doc/options.rst
+ 220
− 67
View file @ 48c4a5af
Command Line Options Command Line Options
==================== ====================
Here is an overview of the command-line options that Leon recognizes: :: Here is an overview of the command-line options that Leon recognizes:
[ Info ] Options that determine the feature of Leon to be used (mutually exclusive). Default: verify
[ Info ] --eval Evaluate ground functions
[ Info ] --help Show help message
[ Info ] --noop No operation performed, just output program
[ Info ] --repair Repair selected functions
[ Info ] --synthesis Partial synthesis of choose() constructs
[ Info ] --termination Check program termination
[ Info ] --verify Verify function contracts
[ Info ] --xlang Support for extra program constructs (imperative,...)
[ Info ]
[ Info ] Additional top-level options
[ Info ] --debug=d1,d2,... Enable detailed messages per component.
[ Info ] Available:
[ Info ] datagen
[ Info ] eval
[ Info ] leon
[ Info ] options
[ Info ] positions
[ Info ] repair
[ Info ] solver
[ Info ] synthesis
[ Info ] termination
[ Info ] timers
[ Info ] trees
[ Info ] verification
[ Info ] xlang
[ Info ] --functions=f1,f2,... Only consider functions f1, f2, ...
[ Info ] --solvers=s1,s2,... Use solvers s1, s2,...
[ Info ] Available:
[ Info ] enum : Enumeration-based counter-example-finder
[ Info ] fairz3 : Native Z3 with z3-templates for unfolding (default)
[ Info ] smt-cvc4 : CVC4 through SMT-LIB
[ Info ] smt-cvc4-cex : CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only
[ Info ] smt-cvc4-proof : CVC4 through SMT-LIB, in-solver inductive reasonning, for proofs only
[ Info ] smt-z3 : Z3 through SMT-LIB
[ Info ] smt-z3-q : Z3 through SMT-LIB, with quantified encoding
[ Info ] unrollz3 : Native Z3 with leon-templates for unfolding
[ Info ] --strict Terminate after each phase if there is an error
[ Info ] --timeout=t Set a timeout for each verification/repair (in sec.)
[ Info ]
[ Info ] Additional options, by component:
[ Info ]
[ Info ] File output (Output parsed/generated program to the specified directory (default: leon.out))
[ Info ] --o=dir Output directory
[ Info ]
[ Info ] Scalac Extraction (Extraction of trees from the Scala Compiler)
[ Info ] --strictCompilation Exit Leon after an error in compilation
[ Info ]
[ Info ] Synthesis (Partial synthesis of "choose" constructs)
[ Info ] --cegis:opttimeout Consider a time-out of CE-search as untrusted solution
[ Info ] --cegis:shrink Shrink non-det programs when tests pruning works well
[ Info ] --cegis:vanuatoo Generate inputs using new korat-style generator
[ Info ] --costmodel=cm Use a specific cost model for this search
[ Info ] --derivtrees Generate derivation trees
[ Info ] --manual=cmd Manual search
[ Info ]
[ Info ] Z3-f (Fair Z3 Solver)
[ Info ] --checkmodels Double-check counter-examples with evaluator
[ Info ] --codegen Use compiled evaluator instead of interpreter
[ Info ] --evalground Use evaluator on functions applied to ground arguments
[ Info ] --feelinglucky Use evaluator to find counter-examples early
[ Info ] --unrollcores Use unsat-cores to drive unrolling while remaining fair
[ Info ]
[ Info ] cvc4 solver (Solver invoked when --solvers=smt-cvc4)
[ Info ] --solver:cvc4=<cvc4-opt>Pass extra arguments to CVC4
Choosing the feature to use:
----------------------------
The first group of options determine which feature of Leon will be used. They are mutually exclusive,
with ``--verify`` being the default.
* ``--eval``
Evaluates parameterless functions and value definitions.
* ``--verify``
Proves or disproves function contracts, as explained in the :ref:`verification` section.
* ``--repair``
Runs program :ref:`repair <repair>`.
* ``--synthesis``
Partially synthesizes ``choose()`` constructs (see :ref:`synthesis` section).
* ``--termination``
Runs a simple termination analysis.
* ``--xlang``
Transforms a program written in the :ref:`xlang` language extension into a :ref:`purescala` program,
then runs program verification.
* ``--noop``
Runs the program through the extraction and preprocessing phases, then outputs it in the specified
directory. Used mostly for debugging purposes.
* ``--help``
Prints a helpful message, then exits.
Additional top-level options
----------------------------
These options are available by all Leon components:
* ``--debug=d1,d2,...``
Enables printing detailed messages for the components d1,d2,... .
Available components are:
* ``datagen`` (Data generators)
* ``eval`` (Evaluators)
* ``leon`` (The top-level component)
* ``options`` (Prints parsed options)
* ``repair`` (Program repair)
* ``solver`` (SMT solvers)
* ``synthesis`` (Program synthesis)
* ``termination`` (Termination analysis)
* ``timers`` (Timers, timer pools)
* ``trees`` (Manipulation of trees)
* ``verification`` (Verification)
* ``xlang`` (Transformation of xlang into purescala programs)
* ``--functions=f1,f2,...``
Only consider functions f1, f2, ... . This applies to all functionalities where Leon manipulates
the input in a per-function basis.
* ``--solvers=s1,s2,...``
Use solvers s1, s2,... . If more than one solver is chosen, all chosen solvers will be used in parallel,
and the best result will be presented. By default, the ``fairz3`` solver is picked.
Some solvers are specialized to proving verification conditions and will have hard time finding
a counterexample in case of an invalid verification condition, some are specialized on finding
counterexamples, and some provide a compromise between the two.
Available solvers include:
* ``enum``
Uses enumeration-based techniques to discover counter-examples.
This solver actually does not invoke an SMT solver and operates entirely on the level
of Leon trees.
* ``fairz3``
Native Z3 with z3-templates for unfolding recursive functions (default).
* ``smt-cvc4``
CVC4 through SMT-LIB. An algorithm within Leon takes up the unfolding of recursive functions,
lambdas etc. To use this and the following CVC4-based solvers, you will need to have the ``cvc4``
executable in your system path (recommended is the latest unstable version).
* ``smt-cvc4-cex``
CVC4 through SMT-LIB, in-solver finite-model-finding, for counter-examples only.
* ``smt-cvc4-proof``
CVC4 through SMT-LIB, for proofs only. Inductive reasoning happens within the solver,
through use of the SMTLIB-2.5 standard.
* ``smt-z3``
Z3 through SMT-LIB. To use this or the next solver, you will need to have the ``z3``
executable in your program path (recommended: latest unstable version).
Inductive reasoning happens on the Leon side (similarly to ``smt-cvc4``).
* ``smt-z3-q``
Z3 through SMT-LIB, but (recursive) functions are encoded with universal quantification,
and inductive reasoning happens within the solver.
* ``unrollz3``
Native Z3, but inductive reasoning happens within Leon (similarly to ``smt-z3``).
* ``--strict``
Terminate Leon after each phase if a non-fatal error is encountered
(such as a failed verification condition). By default, this option is activated.
* ``--timeout=t``
Set a timeout for attempting to prove a verification condition/ repair a function (in sec.)
Additional Options, by Component:
---------------------------------
File Output
***********
* ``--o=dir``
Output files to the directory ``dir`` (default: leon.out).
Used when ``--noop`` is selected.
Code extraction
***************
* ``--strictCompilation``
Do not try to recover after an error in compilation and exit Leon.
Synthesis
*********
* ``--cegis:opttimeout``
Consider a time-out of CE-search as untrusted solution
* ``--cegis:shrink``
Shrink non-det programs when tests pruning works well
* ``--cegis:vanuatoo``
Generate inputs using new korat-style generator
* ``--costmodel=cm``
Use a specific cost model for this search
* ``--derivtrees``
Generate a derivation tree for every synthesized function.
The trees will be output in ``*.dot`` files.
* ``--manual=cmd``
Override Leon's automated search through the space of programs during synthesis.
When this option is chosen, the user gets to traverse the space manually
and choose how deductive synthesis rules are instantiated.
The optional ``cmd`` argument is a series of natural numbers in the form ``n1,n1,...,nk``.
It represents the series of command indexes that the search should instantiate at the
beginning of the search. Useful for repeated search attempts.
Fair-z3 Solver
**************
* ``--checkmodels``
Double-check counter-examples with evaluator
* ``--codegen``
Use compiled evaluator instead of interpreter
* ``--evalground``
Use evaluator on functions applied to ground arguments
* ``--feelinglucky``
Use evaluator to find counter-examples early
* ``--unrollcores``
Use unsat-cores to drive unrolling while remaining fair
CVC4-solver
***********
* ``--solver:cvc4=<cvc4-opt>``
Pass extra command-line arguments to CVC4.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment