Update model documentation #759

Halbaroth · 2023-07-27T08:33:06Z

This PR has to be backported on the release 2.5.0.

bclement-ocp

Some wording/organization suggestions.

Do we want to mention --model-type constraints?

bclement-ocp · 2023-07-27T08:41:07Z

docs/sphinx_docs/Usage/index.md

-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


Suggested change

Alt-Ergo generates best-effort models in the case it cannot conclude the unsatisfiability of

Alt-Ergo can generate best-effort models in the case it cannot conclude the unsatisfiability of

bclement-ocp · 2023-07-27T08:41:29Z

docs/sphinx_docs/Usage/index.md

+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:


Suggested change

By default the model generation is disable. There is three ways to activate it:

Model generation is disabled by default. There are three ways to enable it:

We should list the three ways succinctly, then expand on more details for each of them. We also should provide clear guidance on which way is recommended -- I think that's --dump-models in the native language, and --produce-models for smtlib2.

bclement-ocp · 2023-07-27T08:46:10Z

docs/sphinx_docs/Usage/index.md

+
+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


--dump-models is mostly useful with the native language because SMT-LIB users are more likely to want --produce-models to enable the standard (check-sat) + (get-model) workflow, so the example should be in the native language maybe?

Also, goal is confusing in the context of model generation because the formula is negated, we should advertise check_sat rather than goal for model generation.

bclement-ocp · 2023-07-27T08:52:12Z

docs/sphinx_docs/Usage/index.md

+    )
+  ```
+
+- with the `--produce-models` option, you turn the model generation on. You can display


I think --produce-models and (set-option :produce-models true) should be bundled together, because they do the same thing: enable support for (get-model), so that's probably the way to explain it (turn it around from "Model generation can be enabled. Once enabled, you can use (get-model)." into "We support (get-model). To use it enable model generation with --produce-models or (set-option :produce-models true).")

bclement-ocp · 2023-07-27T08:57:28Z

docs/sphinx_docs/Usage/index.md

+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'.


I'm not sure we want to document the --interpretation option, except maybe advertise --interpretation every for debugging? If we talk about it, we also should be clear that --interpretation last is what --dump-models and --produce-models do.

Can't comment on --interpretation first because I am not sure what it does...

I agree. Actually I hesitated to remove it.

bclement-ocp · 2023-07-27T08:58:11Z

docs/sphinx_docs/Usage/index.md

+      (define-fun c () Int 0)
+    )
+  ```
+  Note: you need to select the SAT solver Tableaux as the model generation is not


Suggested change

Note: you need to select the SAT solver Tableaux as the model generation is not

*Note*: you need to select the SAT solver Tableaux as the model generation is not

Also we should make it clear that --sat-solver Tableaux is only necessary with (set-option :produce-models true), it is not needed for --produce-models or --dump-models (it is implicit currently but we should make it explicit).

bclement-ocp · 2023-07-27T09:03:07Z

docs/sphinx_docs/Usage/index.md

-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.


We should make it clearer that models are printed in a SMT-LIB compatible format, even if the input problem is in the native language.

Also, we should probably remove the "By default" part -- if we keep it, we should document how to use a different format, and also check that the different forma still works, because I don't think it does...

In my opinion, the SMT-LIB format would be the only one to output models. I will ask to remove the other formats for the next release or we can do it now but if there is no documentation about it, we can keep the code in the 2.5.0.

Halbaroth · 2023-07-27T11:51:35Z

Some wording/organization suggestions.

Do we want to mention --model-type constraints?

We didn't test this feature so we shouldn't mention it.

docs/sphinx_docs/Usage/index.md

bclement-ocp · 2023-07-27T14:08:42Z

docs/sphinx_docs/Usage/index.md

+  *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.


Also needs --frontend dolmen (which --produce-models uses, but not --dump-models).

This is still relevant, the text should mention --frontend dolmen.

bclement-ocp · 2023-07-27T15:06:49Z

docs/sphinx_docs/Usage/index.md

+  `(set-option :produce-models true)` and the options `--sat-solver tableaux`
+  and `--frontend dolmen`.


Suggested change

`(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`.

bclement-ocp · 2023-07-27T15:07:14Z

docs/sphinx_docs/Usage/index.md

+  *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.


This is still relevant, the text should mention --frontend dolmen.

* Update model documentation * Review changes * Review changes bis * Review changes ter * Clarify the dolmen option

Update model documentation

e47f89e

Halbaroth added the documentation label Jul 27, 2023

Halbaroth added this to the 2.5.0 milestone Jul 27, 2023

bclement-ocp reviewed Jul 27, 2023

View reviewed changes

bclement-ocp mentioned this pull request Jul 27, 2023

Add documentation for new features #648

Closed

4 tasks

Review changes

0c14b72

Halbaroth requested a review from bclement-ocp July 27, 2023 13:51

Review changes bis

e718376

bclement-ocp requested changes Jul 27, 2023

View reviewed changes

Review changes ter

5d1bc68

Halbaroth requested a review from bclement-ocp July 27, 2023 14:49

bclement-ocp requested changes Jul 27, 2023

View reviewed changes

Halbaroth requested a review from bclement-ocp July 28, 2023 07:47

Clarify the dolmen option

43fca3e

bclement-ocp approved these changes Jul 28, 2023

View reviewed changes

Halbaroth merged commit b83152c into OCamlPro:next Jul 28, 2023

Halbaroth added a commit to Halbaroth/alt-ergo that referenced this pull request Jul 28, 2023

Update model documentation (OCamlPro#759)

4e2dded

* Update model documentation * Review changes * Review changes bis * Review changes ter * Clarify the dolmen option

Halbaroth mentioned this pull request Jul 28, 2023

Backporting 2.5.0 #758

Merged

Halbaroth mentioned this pull request Aug 23, 2023

Backporting 2.5.0 bis #787

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Update model documentation #759

Update model documentation #759

Halbaroth commented Jul 27, 2023 •

edited

Loading

bclement-ocp left a comment

bclement-ocp Jul 27, 2023

bclement-ocp Jul 27, 2023

bclement-ocp Jul 27, 2023

bclement-ocp Jul 27, 2023

bclement-ocp Jul 27, 2023

bclement-ocp Jul 27, 2023

Halbaroth Jul 27, 2023

bclement-ocp Jul 27, 2023

bclement-ocp Jul 27, 2023

Halbaroth Jul 27, 2023

Halbaroth commented Jul 27, 2023 •

edited

Loading

bclement-ocp Jul 27, 2023

bclement-ocp Jul 27, 2023

bclement-ocp Jul 27, 2023

bclement-ocp Jul 27, 2023

	Alt-Ergo generates best-effort models in the case it cannot conclude the unsatisfiability of
	Alt-Ergo can generate best-effort models in the case it cannot conclude the unsatisfiability of

	By default the model generation is disable. There is three ways to activate it:
	Model generation is disabled by default. There are three ways to enable it:


		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

	Note: you need to select the SAT solver Tableaux as the model generation is not
	Note: you need to select the SAT solver Tableaux as the model generation is not

		`(set-option :produce-models true)` and the options `--sat-solver tableaux`
		and `--frontend dolmen`.

Update model documentation #759

Update model documentation #759

Conversation

Halbaroth commented Jul 27, 2023 • edited Loading

bclement-ocp left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth commented Jul 27, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Halbaroth commented Jul 27, 2023 •

edited

Loading

Halbaroth commented Jul 27, 2023 •

edited

Loading