Documentation for optimization

Makefile

@@ -160,7 +160,7 @@ doc: odoc sphinx-doc
 sphinx-doc:
 	# cp LICENSE.md $(SPHINX_DOC_DIR)/About/license.md
 	# cp -r licenses $(SPHINX_DOC_DIR)/About
-	$(SPHINXBUILD) "$(SPHINX_DOC_DIR)" "$(SPHINX_BUILD_DIR)"
+	$(SPHINXBUILD) -W "$(SPHINX_DOC_DIR)" "$(SPHINX_BUILD_DIR)"
 
 # Build the odoc
 odoc:

docs/sphinx_docs/Install/index.md

@@ -3,7 +3,7 @@
 ## From a package manager
 
 Alt-ergo is available on [opam], the ocaml package manager with the following command :
-```
+```console
 opam install alt-ergo
 ```
 
@@ -29,33 +29,36 @@ External dependencies graph generated with `dune-deps` (use `make archi` for sou
 To compile the sources of the library `alt-ergo-lib` and the binary `alt-ergo`, you will need the
 following libraries :
 ```
-  ocaml >= 4.08.0
+  ocaml >= 4.08.1
   dune >= 3.0
   dune-build-info
-  dolmen >= 0.9
-  dolmen_loop >= 0.9
-  ocplib-simplex >= 0.5
-  zarith >= 1.4
+  dune-site
+  dolmen >= 0.10
+  dolmen_type >= 0.10
+  dolmen_loop >= 0.10
+  ocplib-simplex >= 0.5.1
+  zarith >= 1.11
   seq
-  fmt
-  ppx_blob
+  fmt >= 0.9.0
+  ppx_blob >= 0.7.2
   camlzip >= 1.07
   menhir
   dune-site
-  cmdliner
+  cmdliner >= 1.1.0
   psmt2-frontend >= 0.4
   stdlib-shims
+  ppx_deriving
 ```
 
 You can install dependencies using:
 
-```
+```console
 $ make deps
 ```
 
 and create a development switch with:
 
-```
+```console
 $ make dev-switch
 ```
 
@@ -104,8 +107,8 @@ $ make js-deps
 
 For this build rule you will need the following aditional libraries :
 ```
-js_of_ocaml between 4.0.1 and 5.0.1
-zarith_stubs_js
+js_of_ocaml >= 5.4.0
+zarith_stubs_js >= v0.16.1
 ```
 
 #### Alt-Ergo web worker
@@ -114,9 +117,9 @@ zarith_stubs_js
 
 For this build rule you will need the following aditional libraries :
 ```
-js_of_ocaml between 4.0.1 and 5.0.1
+js_of_ocaml >= 5.4.0
 js_of_ocaml-lwt
-zarith_stubs_js
+zarith_stubs_js >= v0.16.1
 data-encoding
 ```
 
@@ -128,11 +131,11 @@ This command create a `www/` directory in which you can find a small js example
 
 For this build rule you will need the following aditional libraries :
 ```
-js_of_ocaml between 4.0.1 and 5.0.1
+js_of_ocaml >= 5.4.0
 js_of_ocaml-lwt
 js_of_ocaml-ppx
 lwt_ppx
-zarith_stubs_js
+zarith_stubs_js >= v0.16.1
 data-encoding
 ```
 

docs/sphinx_docs/Model_generation.md

@@ -63,7 +63,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
 
   - Using the native language in the input file `INPUT.ae`:
 
-  ```
+  ```smt-lib
     logic a, b, c : int
     axiom A : a <> c
 
@@ -101,7 +101,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
 
   - Using the SMT-LIB language in the input file `INPUT.smt2`:
 
-  ```
+  ```smt-lib
     (set-logic ALL)
     (declare-fun a () Int)
     (declare-fun b () Int)
@@ -116,7 +116,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
 
   ```
   and the command `alt-ergo --produce-models INPUT.smt2` produces the output
-  ```
+  ```smt-lib
     unknown
     (
       (define-fun a () Int 0)
@@ -135,7 +135,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
 
 
   - Alternatively, using the statement `(set-option :produce-models true)`
-  ```
+  ```smt-lib
    (set-logic ALL)
    (set-option :produce-models true)
    (declare-fun a () Int)
@@ -149,7 +149,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
   ```
   and the command `alt-ergo INPUT.smt2` produces
   the output model
-  ```
+  ```smt-lib
   unknown
   (
     (define-fun a () Int 0)
@@ -168,19 +168,19 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
   done
   ```
   we got the SMT-LIB file `INPUT.smt2`:
-  ```
+  ```smt-lib
   (set-logic ALL)
   (declare-const i Int)
   (assert (and (< i 5) (not (< (+ i 1) 5))))
   (check-sat)
   (get-model)
   ```
   Execute the command
-  ```sh
+  ```console
   alt-ergo --produce-models INPUT.smt2
   ```
   We got the output
-  ```
+  ```smt-lib
   ; File "INPUT.smt2", line 4, characters 1-12: I don't know (0.6689) (2 steps) (goal g_1)
 
   unknown
@@ -199,7 +199,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
   end
   ```
   and fix our SMT-LIB input accordingly:
-  ```
+  ```smt-lib
   (set-logic ALL)
   (declare-const i Int)
   (assert (and (< i 5) (not (<= (+ i 1) 5))))
@@ -214,20 +214,3 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
   (error "No model produced.")
   ```
   Our invariant is valid!
-
-### Output
-The results of an Alt-ergo's execution have the following form :
-```
-File "<path_to_file>/<filename>", line <l>, characters <n-m>: <status> (<time in seconde>) (<number of steps> steps) (goal <name of the goal>)
-```
-The status can be `Valid`, `Invalid` or `I don't know`. If the input file is in
-the SMT-LIB 2 format the status will be either `unsat`, `sat`, `unknown`.
-You can force the status to be print in the SMT-LIB 2 form with the option `--output smtlib2`.
-
-```{admonition} Note
-When Alt-Ergo tries to prove a `goal` (with the native input language), it
-actually tries to prove the unsatisfiability of its negation. That is
-why you get `unsat` answer as an SMT-LIB 2 format output while proving a `Valid`
-goal. The same goes for `Invalid` and `sat`.
-```
-

docs/sphinx_docs/Optimization.md

@@ -0,0 +1,104 @@
+# Optimization
+
+Since version 2.6.0, Alt-Ergo supports optimization for LIA and Bitvector
+theories.
+
+## MaxSMT syntax
+
+- Use `(maximize ...)` and `(minimize ...)` statements to specify an objective function.
+
+- Use `(get-objectives)` after `(check-sat)` to output the best values
+  for each objective function.
+
+## Activation
+
+You only need to [enable model generation](Model_generation.md#activation).
+The identifiers `maximize`, `minimize` and `get-objectives` are reserved by
+default. If you want to disable the `MaxSMT` extension, use the
+[strict mode](Usage/index.md#strict-mode).
+
+```{admonition} Note
+The optimization feature is only compatible with the SAT solver `CDCL-Tableaux`,
+which is the default.
+```
+
+## Examples
+
+First, consider a classical linear programming problem:
+```smt-lib
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+(assert (= (+ (* 5 x) (* 2 y) (* (- 0 3) z)) 25))
+(assert (= (+ (* (- 0 2) x) (* 4 y)) 8))
+(assert (<= x y))
+(maximize x)
+(check-sat)
+(get-model)
+(get-objectives)
+```
+Alt-Ergo outputs:
+```smt-lib
+unknown
+(
+  (define-fun x () Int 4)
+  (define-fun y () Int 4)
+  (define-fun z () Int 1)
+)
+(objectives
+  (x 4)
+)
+```
+
+- The optimization also works with an expression in `maximize`:
+```smt-lib
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-const x Int)
+(declare-const y Int)
+(assert (<= x 5))
+(assert (<= 0 y))
+(maximize (- (* 5 x) y))
+(check-sat)
+(get-objectives)
+```
+Alt-Ergo outputs:
+```smt-lib
+unknown
+(
+  (define-fun x () Int 5)
+  (define-fun y () Int 0)
+)
+(objectives
+  ((- (* 5 x) y) 25)
+)
+```
+
+- Finally, an example with bitvectors:
+```smt-lib
+(set-option :produce-models true)
+(set-logic ALL)
+(declare-const x (_ BitVec 32))
+(declare-const y (_ BitVec 32))
+(assert (bvult x (_ bv2 32)))
+(assert (bvule y (_ bv10 32)))
+(maximize x)
+(maximize y)
+(check-sat)
+(get-model)
+(get-objectives)
+```
+Alt-Ergo outputs:
+```smt-lib
+unknown
+(
+  (define-fun x () (_ BitVec 32) #x00000001)
+  (define-fun y () (_ BitVec 32) #x0000000a)
+)
+(objectives
+  (x #x00000001)
+  (y #x0000000a)
+)
+```

docs/sphinx_docs/Plugins/ab_why3.md

@@ -25,7 +25,7 @@ prove the goals given in a file `b-why3-POs.ae` with the following
 command:
 
 
-```
+```console
  ./alt-ergo b-why3-POs.why --add-parser ABWhy3Plugin.cmxs --prelude b-set-theory-prelude-2020-02-28.ae
 ```
 
@@ -37,7 +37,7 @@ theory for Alt-Ergo.
 For instance, using the following command to prove the goals in the
 file `examples/AB-Why3-plugin/p4_34.why.zip`:
 
-```
+```console
 ./alt-ergo examples/AB-Why3-plugin/p4_34.why.zip --add-parser ABWhy3Plugin.cmxs --prelude b-set-theory-prelude-2020-02-28.ae  --timelimit-per-goal --timelimit 3 --no-locs-in-answers
 ```
 
@@ -57,7 +57,7 @@ Valid (0.0525) (215 steps) (goal g_5)
 If you have already installed this version of Alt-Ergo and this plugin, you should be able to simply use the command:
 
 
-```
+```console
  alt-ergo b-why3-POs.why --add-parser ABWhy3Plugin.cmxs --prelude b-set-theory-prelude-2020-02-28.ae
 ```
 

docs/sphinx_docs/Plugins/index.md

@@ -13,7 +13,9 @@ The `fm-simplex` inequality plugin comes built-in with Alt-Ergo and no further
 installation is required. It is distributed under the same licensing conditions
 as Alt-Ergo. It can be used as follows:
 
-    $ alt-ergo --inequalities-plugin fm-simplex [other-options] file.<ext>
+```console
+$ alt-ergo --inequalities-plugin fm-simplex [other-options] file.<ext>
+```
 
 ```{note}
 If you are a developer of an external inequality plugin, your plugin needs to