Update changelog; stub of invariant inference docs

CHANGELOG.md

@@ -4,7 +4,9 @@ Change Log
 #### v?.?
 
 Among the changes are (see the commits for details):
+* Resource bound inference engine Orb, developed by Ravi is now merged into master
 * Leon can now do program repair, thanks to Etienne and Manos
+* Experimental support for first-order quantifiers inside Leon
 * Isabelle proof assistant can now be used as a solver, thanks to Lars Hupel
 * A DSL for writing equational proofs in Leon, thanks to Sandro Stucki and Marco Antognini
 * Leon now uses the improved SMT-LIB library, thanks to the continuous work of Regis Blanc

src/sphinx/index.rst

@@ -19,6 +19,7 @@ Contents:
    library
    xlang
    verification
+   invinference
    neon
    isabelle
    limitations

src/sphinx/invinference.rst

+.. _infinference:
+
+Invariant Inference
+===================
+
+The command line options relevant for invariant inference are 
+listed under Invariant Inference section of :ref:`cmdlineoptions`.
+
+
+For examples, check out the directory ``testcases/orb-testcases/``.
+
+For any questions, please consult Ravi and check the paper
+`Symbolic resource bound inference for functional programs <http://lara.epfl.ch/~kuncak/papers/MadhavanKuncak14SymbolicResourceBoundInferenceFunctionalPrograms.pdf>`_, by *Ravichandhran Madhavan* and *Viktor Kuncak*. Computer Aided Verification (CAV), 2014.

src/sphinx/options.rst

@@ -11,7 +11,8 @@ or ``off`` or ``no``.
 Additionally, if you need to pass options to the ``scalac`` frontend of Leon,
 you can do it by using a single dash ``-``. For example, ``-Ybrowse:typer``.
 
-The rest of this section presents all command-line options that Leon recognizes.
+The rest of this section presents command-line options that Leon recognizes.
+For more up-to-date list, please invoke ``leon --help``.
 
 Choosing which Leon feature to use
 ----------------------------------
@@ -39,6 +40,14 @@ These options are mutually exclusive. By default, ``--verify`` is chosen.
   
   Runs termination analysis. Can be used along ``--verify``.
 
+* ``--inferInv`` 
+
+  Infer invariants from (instrumented) the code (using Orb)
+
+* ``--instrument``                
+
+  Instrument the code for inferring time/depth/stack bounds (using Orb)
+
 * ``--noop``
   
   Runs the program through the extraction and preprocessing phases, then outputs it in the specified
@@ -48,6 +57,8 @@ These options are mutually exclusive. By default, ``--verify`` is chosen.
   
   Prints a helpful message, then exits.
 
+
+
 Additional top-level options
 ----------------------------
 
@@ -186,6 +197,47 @@ 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``
+
+  Perform a non-modular whole program analysis
+
+* ``--withmult``
+
+  Do not convert multiplication into a recursive function inside verification conditions
+
 Additional Options (by component)
 ---------------------------------