From e47f89e085ffbbccb8bcdf008ca9a65f9e75b404 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 26 Jul 2023 17:11:33 +0200 Subject: [PATCH 1/5] Update model documentation --- docs/sphinx_docs/Usage/index.md | 109 +++++++++++++++++++++++++++----- 1 file changed, 94 insertions(+), 15 deletions(-) diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index 33ac75f65..4e4f486fe 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -24,22 +24,101 @@ 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: +Alt-Ergo generates best-effort models in the case it cannot conclude the unsatisfiability of +the context or the validity of a goal. By default, the model format is the SMT format. + +By default the model generation is disable. There is three ways to activate it: + +- with the `--dump-models` option, Alt-Ergo will produce a model after each `goal` in the native language + or each `(check-sat)` in the SMT-LIB language. For instance 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) + + (assert (distinct a b)) + (check-sat) + ``` + and the command `$ alt-ergo --dump-models INPUT.smt2` produces the output models + + ``` + ( + (define-fun a () Int 0) + (define-fun b () Int 0) + (define-fun c () Int 0) + ) + + ( + (define-fun a () Int (- 2)) + (define-fun b () Int 0) + (define-fun c () Int (- 2)) + ) + ``` + +- with the `--produce-models` option, you turn the model generation on. You can display + a model after a `(check-sat)` using the statement `(get-model)`. For instance 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 model + ``` + ( + (define-fun a () Int 0) + (define-fun b () Int 0) + (define-fun c () Int 0) + ) + ``` + +- with the statement `(set-option :produce-models true)`, you turn the model generation on and + you can use the statement `(get-model)` as explained above. For instance the input file `INPUT.smt2`: + ``` + (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. + +You can fine-tune the moment Alt-Ergo computes its models by using the option `--interpretation=VALUE` where VALUE can be: + * "none", to disable model generation (by default); + * "first", to output the first model found; + * "every", to compute a model before each decision; + * "last", to output the last model computed before returning 'unknown'. + + Note: this option only works with the option `--sat-solver tableaux`. -- 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. ### Output The results of an Alt-ergo's execution have the following form : From 0c14b72315f1337126de270f4a348dcd9d6d8b05 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 27 Jul 2023 14:14:41 +0200 Subject: [PATCH 2/5] Review changes --- docs/sphinx_docs/Usage/index.md | 64 +++++++++++++++++---------------- 1 file changed, 33 insertions(+), 31 deletions(-) diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index 4e4f486fe..e027b6a6d 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -24,44 +24,55 @@ Alt-Ergo supports file extensions: See the [Input section] for more information about the format of the input files ### Generating models -Alt-Ergo generates best-effort models in the case it cannot conclude the unsatisfiability of -the context or the validity of a goal. By default, the 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. -By default the model generation is disable. There is three ways to activate it: +#### Activation -- with the `--dump-models` option, Alt-Ergo will produce a model after each `goal` in the native language - or each `(check-sat)` in the SMT-LIB language. For instance the input file `INPUT.smt2`: +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 counter-example after each `goal` it cannot prove `valid`. + +- 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`: ``` - (set-logic ALL) - (declare-fun a () Int) - (declare-fun b () Int) - (declare-fun c () Int) + logic a, b, c : int - (assert (= a (+ b c))) - (check-sat) + goal g1: a <> b + c - (assert (distinct a b)) - (check-sat) + goal g2: a = b ``` - and the command `$ alt-ergo --dump-models INPUT.smt2` produces the output models + and the command `$ alt-ergo --dump-models INPUT.ae`, Alt-Ergo produces the + output models: ``` + ; Model for g1 ( (define-fun a () Int 0) (define-fun b () Int 0) (define-fun c () Int 0) ) + ; Model for g2 ( - (define-fun a () Int (- 2)) + (define-fun a () Int 2) (define-fun b () Int 0) - (define-fun c () Int (- 2)) ) ``` + *Note*: In this example the counter-example for the goal `g2` is not a + counter-example for the goal `g1` since goals are independent in the native + language. -- with the `--produce-models` option, you turn the model generation on. You can display - a model after a `(check-sat)` using the statement `(get-model)`. For instance the input file `INPUT.smt2`: + Using the SMT-LIB language in the input file `INPUT.ae`: ``` (set-logic ALL) @@ -86,8 +97,7 @@ By default the model generation is disable. There is three ways to activate it: ) ``` -- with the statement `(set-option :produce-models true)`, you turn the model generation on and - you can use the statement `(get-model)` as explained above. For instance the input file `INPUT.smt2`: + Alternatively, using the statement `(set-option :produce-models true)` ``` (set-logic ALL) (set-option :produce-models true) @@ -108,17 +118,9 @@ By default the model generation is disable. There is three ways to activate it: (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. - -You can fine-tune the moment Alt-Ergo computes its models by using the option `--interpretation=VALUE` where VALUE can be: - * "none", to disable model generation (by default); - * "first", to output the first model found; - * "every", to compute a model before each decision; - * "last", to output the last model computed before returning 'unknown'. - - Note: this option only works with the option `--sat-solver tableaux`. - + *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 : From e71837697a8ffc444d32cec5fd491853ac85d457 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 27 Jul 2023 15:51:40 +0200 Subject: [PATCH 3/5] Review changes bis --- docs/sphinx_docs/Usage/index.md | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index e027b6a6d..8850b69f7 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -31,7 +31,9 @@ the context. The model format is a SMT-LIB compatible format, even if you use th 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 counter-example after each `goal` it cannot prove `valid`. + 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 @@ -46,31 +48,32 @@ Model generation is disabled by default. There are two recommanded ways to enabl ``` logic a, b, c : int + axiom A : a <> c - goal g1: a <> b + c - - goal g2: a = b + 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 g1 + ; Model for c1 ( - (define-fun a () Int 0) - (define-fun b () Int 0) + (define-fun a () Int 2) + (define-fun b () Int 2) (define-fun c () Int 0) ) - ; Model for g2 + ; Model for c2 ( (define-fun a () Int 2) (define-fun b () Int 0) + (define-fun c () Int 0) ) ``` - *Note*: In this example the counter-example for the goal `g2` is not a - counter-example for the goal `g1` since goals are independent in the native - language. + *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`: @@ -219,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: From 5d1bc68bdac57952699a1c18beb938f4c95f6b79 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Thu, 27 Jul 2023 16:47:05 +0200 Subject: [PATCH 4/5] Review changes ter --- docs/sphinx_docs/Usage/index.md | 32 +++++++++++++++++++++----------- 1 file changed, 21 insertions(+), 11 deletions(-) diff --git a/docs/sphinx_docs/Usage/index.md b/docs/sphinx_docs/Usage/index.md index 8850b69f7..0a4106c50 100644 --- a/docs/sphinx_docs/Usage/index.md +++ b/docs/sphinx_docs/Usage/index.md @@ -29,7 +29,7 @@ the context. The model format is a SMT-LIB compatible format, even if you use th #### Activation -Model generation is disabled by default. There are two recommanded ways to enable it: +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 @@ -40,7 +40,8 @@ Model generation is disabled by default. There are two recommanded ways to enabl on demand using the statement `(get-model)`. Alternatively, you can enable model generation using the statement - `(set-option :produce-models true)`. + `(set-option :produce-models true)` and the options `--sat-solver tableaux` + and `--frontend dolmen`. #### Examples @@ -53,7 +54,7 @@ Model generation is disabled by default. There are two recommanded ways to enabl check_sat c1: a = b + c check_sat c2: a <> b ``` - and the command `$ alt-ergo --dump-models INPUT.ae`, Alt-Ergo produces the + and the command `alt-ergo --dump-models INPUT.ae`, Alt-Ergo produces the output models: ``` @@ -63,6 +64,7 @@ Model generation is disabled by default. There are two recommanded ways to enabl (define-fun b () Int 2) (define-fun c () Int 0) ) + I don't known ; Model for c2 ( @@ -70,12 +72,13 @@ Model generation is disabled by default. There are two recommanded ways to enabl (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.ae`: + Using the SMT-LIB language in the input file `INPUT.smt2`: ``` (set-logic ALL) @@ -91,14 +94,19 @@ Model generation is disabled by default. There are two recommanded ways to enabl (check-sat) ``` - and the command `$ alt-ergo --produce-models INPUT.smt2` produces the output model + 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)` ``` @@ -113,13 +121,15 @@ Model generation is disabled by default. There are two recommanded ways to enabl (get-model) ``` - and the command `$ alt-ergo --sat-solver tableaux INPUT.smt2` produces the output model + and the command `alt-ergo --frontend model --sat-solver tableaux INPUT.smt2` produces + the output model ``` - ( - (define-fun a () Int 0) - (define-fun b () Int 0) - (define-fun c () Int 0) - ) + unknown + ( + (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` From 43fca3e934d3f574839867eb48ad4eeffcccefd1 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 28 Jul 2023 09:47:28 +0200 Subject: [PATCH 5/5] 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 :