diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 3a8cb39df090fcb5ca3d3d902bedf6a52557026b..3e848994835d9e8bc6a4506576ede13439c0664b 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -44,15 +44,15 @@ object Main {
val description = "Selection of Leon functionality. Default: verify"
val optEval = LeonStringOptionDef("eval", "Evaluate ground functions through code generation or evaluation (default: evaluation)", "default", "[code|default]")
- val optTermination = LeonFlagOptionDef("termination", "Check program termination. Can be used along --verify", false)
- val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
- val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
- val optIsabelle = LeonFlagOptionDef("isabelle", "Run Isabelle verification", false)
- val optNoop = LeonFlagOptionDef("noop", "No operation performed, just output program", false)
- val optVerify = LeonFlagOptionDef("verify", "Verify function contracts", false)
- val optHelp = LeonFlagOptionDef("help", "Show help message", false)
- val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false)
- val optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
+ val optTermination = LeonFlagOptionDef("termination", "Check program termination. Can be used along --verify", false)
+ val optRepair = LeonFlagOptionDef("repair", "Repair selected functions", false)
+ val optSynthesis = LeonFlagOptionDef("synthesis", "Partial synthesis of choose() constructs", false)
+ val optIsabelle = LeonFlagOptionDef("isabelle", "Run Isabelle verification", false)
+ val optNoop = LeonFlagOptionDef("noop", "No operation performed, just output program", false)
+ val optVerify = LeonFlagOptionDef("verify", "Verify function contracts", false)
+ val optHelp = LeonFlagOptionDef("help", "Show help message", false)
+ val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false)
+ val optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
Set(optTermination, optRepair, optSynthesis, optIsabelle, optNoop, optHelp, optEval, optVerify, optInstrument, optInferInv)
@@ -74,7 +74,7 @@ object Main {
}
reporter.info("")
- reporter.info("Additional options, by component:")
+ reporter.title("Additional options, by component:")
for (c <- (allComponents - MainComponent - SharedOptions).toSeq.sortBy(_.name) if c.definedOptions.nonEmpty) {
reporter.info("")
diff --git a/src/main/scala/leon/solvers/isabelle/Component.scala b/src/main/scala/leon/solvers/isabelle/Component.scala
index cf8db26a5d5516222665c2769a005b2eeea74f2e..3b75a8c64fb7a68db86fc30456a53d8df8e2626d 100644
--- a/src/main/scala/leon/solvers/isabelle/Component.scala
+++ b/src/main/scala/leon/solvers/isabelle/Component.scala
@@ -10,7 +10,7 @@ import leon._
object Component extends LeonComponent {
- val name = "isabelle"
+ val name = "Isabelle"
val description = "Isabelle solver"
val leonBase =
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index dfcfbcc3fffa1cc9ae190b169ab1f34ad1bf4310..dc267825c8356451944b5fb6b7f9de5d55504232 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -29,9 +29,9 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
}
object SMTLIBCVC4Component extends LeonComponent {
- val name = "cvc4 solver"
+ val name = "CVC4 solver"
- val description = "Solver invoked when --solvers=smt-cvc4"
+ val description = "Solver invoked with --solvers=smt-cvc4"
val optCVC4Options = new LeonOptionDef[Set[String]] {
val name = "solver:cvc4"
diff --git a/src/sphinx/options.rst b/src/sphinx/options.rst
index c5495f40a99086a3accddd87a7f74fc2769a99a1..5648b042c47f3a252672d698d496a2b3309221a8 100644
--- a/src/sphinx/options.rst
+++ b/src/sphinx/options.rst
@@ -18,7 +18,7 @@ Choosing which Leon feature to use
----------------------------------
The first group of options determine which feature of Leon will be used.
-These options are mutually exclusive. By default, ``--verify`` is chosen.
+These options are mutually exclusive (except when noted). By default, ``--verify`` is chosen.
* ``--eval``
@@ -62,7 +62,7 @@ These options are mutually exclusive. By default, ``--verify`` is chosen.
Additional top-level options
----------------------------
-These options are available by all Leon components:
+These options are available to all Leon components:
* ``--debug=d1,d2,...``
@@ -197,49 +197,19 @@ These options are available by all Leon components:
Support for additional language constructs described in :ref:`xlang`.
These constructs are desugared into :ref:`purescala` before other operations.
-Invariant Inference
--------------------
-
-These options are to be used in conjuction with ``--inferInv`` and ``--instrument``.
-
-* ``--cegis``
-
- Use cegis instead of farkas
-
-* ``--disableInfer``
-
- Disable automatic inference of auxiliary invariants
-
-* ``--fullunroll``
-
- Unroll all calls in every unroll step
-
-* ``--inferTemp``
-
- Infer templates by enumeration
-
-* ``--minbounds``
-
- Tighten the inferred time bounds
-
-* ``--stats-suffix=s``
-
- Specifies the suffix of the statistics file
-
-* ``--usereals``
-
- Interpret the input program as a program over real numbers
-
-* ``--wholeprogram``
+Additional Options (by component)
+---------------------------------
- Perform a non-modular whole program analysis
+The following options relate to specific components in Leon. Bear in mind
+that related components might still use these options, e.g. repair will use
+synthesis options and verification options.
-* ``--withmult``
+Verification
+************
- Do not convert multiplication into a recursive function inside verification conditions
+* ``--parallel``
-Additional Options (by component)
----------------------------------
+ Check verification conditions in parallel.
File Output
***********
@@ -259,8 +229,6 @@ Code Extraction
Synthesis
*********
-These options are also used by repair during the synthesis stage.
-
* ``--cegis:opttimeout``
Consider a time-out of CE-search as untrusted solution.
@@ -366,3 +334,45 @@ Isabelle
library when verifiying a Leon source file. Keeping it enabled prevents
unsound proofs when postconditions or mappings in the library are wrong.
When disabled, a warning is printed.
+
+Invariant Inference
+*******************
+
+These options are to be used in conjunction with ``--inferInv`` and ``--instrument``.
+
+* ``--cegis``
+
+ Use cegis instead of farkas
+
+* ``--disableInfer``
+
+ Disable automatic inference of auxiliary invariants
+
+* ``--fullunroll``
+
+ Unroll all calls in every unroll step
+
+* ``--inferTemp``
+
+ Infer templates by enumeration
+
+* ``--minbounds``
+
+ Tighten the inferred time bounds
+
+* ``--stats-suffix=s``
+
+ Specifies the suffix of the statistics file
+
+* ``--usereals``
+
+ Interpret the input program as a program over real numbers
+
+* ``--wholeprogram``
+
+ Perform a non-modular whole program analysis
+
+* ``--withmult``
+
+ Do not convert multiplication into a recursive function inside verification conditions
+