From 43fca3e934d3f574839867eb48ad4eeffcccefd1 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 28 Jul 2023 09:47:28 +0200 Subject: [PATCH] Clarify the dolmen option --- docs/sphinx_docs/Usage/index.md | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index 0a4106c50..f3de6b50a 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -40,8 +40,8 @@ Model generation is disabled by default. There are two recommended ways to enabl on demand using the statement `(get-model)`. Alternatively, you can enable model generation using the statement - `(set-option :produce-models true)` and the options `--sat-solver tableaux` - and `--frontend dolmen`. + `(set-option :produce-models true)`. This currently requires using the options + `--sat-solver tableaux` and `--frontend dolmen`. #### Examples @@ -121,7 +121,7 @@ Model generation is disabled by default. There are two recommended ways to enabl (get-model) ``` - and the command `alt-ergo --frontend model --sat-solver tableaux INPUT.smt2` produces + and the command `alt-ergo --frontend dolmen --sat-solver tableaux INPUT.smt2` produces the output model ``` unknown @@ -131,9 +131,10 @@ Model generation is disabled by default. There are two recommended ways to enabl (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. + *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 :