From f78aeb22790944449d428be0848debbb4768c785 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Wed, 30 Sep 2015 15:22:55 +0200
Subject: [PATCH] Update changelog; stub of invariant inference docs

---
 CHANGELOG.md                |  2 ++
 src/sphinx/index.rst        |  1 +
 src/sphinx/invinference.rst | 13 +++++++++
 src/sphinx/options.rst      | 54 ++++++++++++++++++++++++++++++++++++-
 4 files changed, 69 insertions(+), 1 deletion(-)
 create mode 100644 src/sphinx/invinference.rst

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 33ad5147e..862ea523b 100644
--- a/CHANGELOG.md
+++ b/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
diff --git a/src/sphinx/index.rst b/src/sphinx/index.rst
index d02cf0293..a20401170 100644
--- a/src/sphinx/index.rst
+++ b/src/sphinx/index.rst
@@ -19,6 +19,7 @@ Contents:
    library
    xlang
    verification
+   invinference
    neon
    isabelle
    limitations
diff --git a/src/sphinx/invinference.rst b/src/sphinx/invinference.rst
new file mode 100644
index 000000000..4c79f79c7
--- /dev/null
+++ b/src/sphinx/invinference.rst
@@ -0,0 +1,13 @@
+.. _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.
diff --git a/src/sphinx/options.rst b/src/sphinx/options.rst
index 492c3e3b4..9a89e77a3 100644
--- a/src/sphinx/options.rst
+++ b/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)
 ---------------------------------
 
-- 
GitLab