Update model documentation (#759)

* Update model documentation

* Review changes

* Review changes bis

* Review changes ter

* Clarify the dolmen option

docs/sphinx_docs/Usage/index.md

@@ -35,22 +35,117 @@ Alt-Ergo integrates two frontends:
   default in a future release.
 
 ### Generating models
-Since 2.5.0, Alt-Ergo also generates models in the case it concludes on the satisfiability of
-the formula.
-There is two ways to activate model generation:
-
-- with the `--model` option;
-
-- `with the --interpretation=VALUE`, where VALUE can be equal to:
-  * "none", and alt-ergo will not generate models (by default);
-  * "first", and alt-ergo will output the first model it finds;
-  * "every", alt alt-ergo will compute a model before each decision
-  * "last", and alt-ergo will output the last model it computes before returning 'unknown'.
-  Note that this mode only works with the option `--sat-solver tableaux`.
-
-NB: the `--model` option is equivalent to `--interpretation every --sat-solver tableaux`.
-
-The default model format is the SMT format.
+Alt-Ergo can generates best-effort models in the case it cannot conclude the unsatisfiability of
+the context. The model format is a SMT-LIB compatible format, even if you use the native input language.
+
+#### Activation
+
+Model generation is disabled by default. There are two recommended ways to enable it:
+- with the native language and the `--dump-models` option, Alt-Ergo tries to produce
+  a model after each `check_sat` that returns `I don't known` or
+  a counter-example after each `goal` it cannot prove `valid`. Note that both
+  `goal` and `check_sat` statements are independent in the native language.
+
+- with the SMT-LIB language and the `--produce-models` option, Alt-Ergo tries to
+  produce a model after each `(check-sat)` that returns `unknown`. Models are output
+  on demand using the statement `(get-model)`.
+
+  Alternatively, you can enable model generation using the statement
+  `(set-option :produce-models true)`. This currently requires using the options
+  `--sat-solver tableaux` and `--frontend dolmen`.
+
+#### Examples
+
+  Using the native language in the input file `INPUT.ae`:
+
+  ```
+    logic a, b, c : int
+    axiom A : a <> c
+
+    check_sat c1: a = b + c
+    check_sat c2: a <> b
+  ```
+  and the command `alt-ergo --dump-models INPUT.ae`, Alt-Ergo produces the
+  output models:
+
+  ```
+    ; Model for c1
+    (
+      (define-fun a () Int 2)
+      (define-fun b () Int 2)
+      (define-fun c () Int 0)
+    )
+    I don't known
+
+    ; Model for c2
+    (
+      (define-fun a () Int 2)
+      (define-fun b () Int 0)
+      (define-fun c () Int 0)
+    )
+    I don't known
+  ```
+  *Note*: In this example the model for the statement `check_sat c2` is not a
+  model for the statement `check_sat c1` since `check_sat` are independent in
+  the native language. The same goes for `goals`.
+
+  Using the SMT-LIB language in the input file `INPUT.smt2`:
+
+  ```
+    (set-logic ALL)
+    (declare-fun a () Int)
+    (declare-fun b () Int)
+    (declare-fun c () Int)
+
+    (assert (= a (+ b c)))
+    (check-sat)
+    (get-model)
+
+    (assert (distinct a b))
+    (check-sat)
+
+  ```
+  and the command `alt-ergo --produce-models INPUT.smt2` produces the output
+  ```
+    unknown
+    (
+      (define-fun a () Int 0)
+      (define-fun b () Int 0)
+      (define-fun c () Int 0)
+    )
+
+    unknown
+  ```
+  *Note*: There is no model printed after the second `(check-sat)` since we
+  don't demand it with the statement `(get-model)`.
+
+  Alternatively, using the statement `(set-option :produce-models true)`
+  ```
+   (set-logic ALL)
+   (set-option :produce-models true)
+   (declare-fun a () Int)
+   (declare-fun b () Int)
+   (declare-fun c () Int)
+
+   (assert (= a (+ b c)))
+   (check-sat)
+   (get-model)
+
+  ```
+  and the command `alt-ergo --frontend dolmen --sat-solver tableaux INPUT.smt2` produces
+  the output model
+  ```
+  unknown
+  (
+    (define-fun a () Int 0)
+    (define-fun b () Int 0)
+    (define-fun c () Int 0)
+  )
+  ```
+  *Note*: you need to select the Dolmen frontend and the SAT solver Tableaux as the
+  model generation is not supported yet by the other SAT solvers. The options
+  `--dump-models` and `--produce-models` select the right frontend and SAT solver
+  for you.
 
 ### Output
 The results of an Alt-ergo's execution have the following form :
@@ -143,7 +238,7 @@ The worker also take a Json file that correspond to the options to set in Alt-Er
  "steps_bound": 1000 }
 ```
 
-#### Outpus
+#### Outputs
 
 At the end of solving it returns a Json file corresponding to results, debug informations, etc: