Update model documentation

docs/sphinx_docs/Usage/index.md

@@ -24,22 +24,106 @@ Alt-Ergo supports file extensions:
 See the [Input section] for more information about the format of the input files
 
 ### 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 recommanded 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)`.
+
+#### 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)
+    )
+
+    ; Model for c2
+    (
+      (define-fun a () Int 2)
+      (define-fun b () Int 0)
+      (define-fun c () Int 0)
+    )
+  ```
+  *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.ae`:
+
+  ```
+    (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 model
+  ```
+    (
+      (define-fun a () Int 0)
+      (define-fun b () Int 0)
+      (define-fun c () Int 0)
+    )
+  ```
+
+  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 --sat-solver tableaux INPUT.smt2` produces the output model
+  ```
+    (
+      (define-fun a () Int 0)
+      (define-fun b () Int 0)
+      (define-fun c () Int 0)
+    )
+  ```
+  *Note*: you need to select 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 SAT solver for you.
 
 ### Output
 The results of an Alt-ergo's execution have the following form :
@@ -138,7 +222,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: