From 48c4a5af26a4e836556749a9c1b868d1f13abd18 Mon Sep 17 00:00:00 2001 From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch> Date: Fri, 24 Apr 2015 19:06:47 +0200 Subject: [PATCH] More options section --- doc/options.rst | 287 +++++++++++++++++++++++++++++++++++++----------- 1 file changed, 220 insertions(+), 67 deletions(-) diff --git a/doc/options.rst b/doc/options.rst index be0f961b1..b9661bdb4 100644 --- a/doc/options.rst +++ b/doc/options.rst @@ -1,71 +1,224 @@ Command Line Options ==================== -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 +Here is an overview of the command-line options that Leon recognizes: +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. -- GitLab