Skip to content

Commit

Permalink
review changes
Browse files Browse the repository at this point in the history
  • Loading branch information
Halbaroth committed Aug 26, 2024
1 parent 8508f37 commit a12b034
Show file tree
Hide file tree
Showing 7 changed files with 24 additions and 21 deletions.
2 changes: 1 addition & 1 deletion docs/sphinx_docs/Alt_ergo_native/04_setting_goals.md
Original file line number Diff line number Diff line change
Expand Up @@ -65,7 +65,7 @@ logic x, y : int
check_sat g: x = y
```

```sh
```console
$ alt-ergo test.ae --model
```

Expand Down
4 changes: 3 additions & 1 deletion docs/sphinx_docs/Dev/architecture.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,9 @@
If you're new to Alt-Ergo (or not), you may want to get the list of
modules (files) with their dependencies with the following command:

make modules-dep-graph
```console
$ make modules-dep-graph
```

If everything goes well with the command above, a file
modules-dep-graph.pdf will be generated.
8 changes: 4 additions & 4 deletions docs/sphinx_docs/Install/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -49,13 +49,13 @@ following libraries :

You can install dependencies using:

```sh
```console
$ make deps
```

and create a development switch with:

```sh
```console
$ make dev-switch
```

Expand Down Expand Up @@ -96,7 +96,7 @@ Note: these are somewhat obsolete; nowadays you can just use `dune`

You can install dependencies using:

```sh
```console
$ make js-deps
```

Expand Down Expand Up @@ -165,6 +165,6 @@ You can find more information in the [AB-Why3 README]

This plugin has been "inlined" in Alt-Ergo sources.

# Links
## Links
- [AB-Why3 README](../Plugins/ab_why3.md)
- [opam](https://opam.ocaml.org/)
2 changes: 1 addition & 1 deletion docs/sphinx_docs/Model_generation.md
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@ Model generation is known to be sometimes incomplete in the presence of arrays.
(get-model)
```
Execute the command
```sh
```console
alt-ergo --produce-models INPUT.smt2
```
We got the output
Expand Down
2 changes: 1 addition & 1 deletion docs/sphinx_docs/Plugins/ab_why3.md
Original file line number Diff line number Diff line change
Expand Up @@ -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:


```sh
```console
$ alt-ergo b-why3-POs.why --add-parser ABWhy3Plugin.cmxs --prelude b-set-theory-prelude-2020-02-28.ae
```

Expand Down
2 changes: 1 addition & 1 deletion docs/sphinx_docs/Plugins/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ 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:

```sh
```console
$ alt-ergo --inequalities-plugin fm-simplex [other-options] file.<ext>
```

Expand Down
25 changes: 13 additions & 12 deletions docs/sphinx_docs/Usage/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,14 +4,14 @@

Alt-Ergo is executed with the following command:

```sh
```console
$ alt-ergo [options] file.<ext>
```

The CDCL solver is now the default SAT engine. The command below
allows to enable the old Tableaux-like SAT-solver:

```sh
```console
$ alt-ergo [options] --sat-solver Tableaux file.<ext>

```
Expand Down Expand Up @@ -46,7 +46,7 @@ SMT-LIB features will not work with the `legacy` frontend. Use the (default)

Preludes can be passed to Alt-Ergo as follows:

```sh
```console
$ alt-ergo --prelude p.ae --prelude some-path/q.ae [other-options] file.ae
```

Expand All @@ -64,7 +64,7 @@ Alt-Ergo can be compiled in Javascript see the [install section] for more inform

The Javascript version of Alt-Ergo compatible with node-js is executed with the following command:

```sh
```console
$ node alt-ergo.js [options] file.<ext>
```

Expand Down Expand Up @@ -120,11 +120,12 @@ Since version 2.2.0, Alt-Ergo's library is also compiled and installed. See the
[API documentation] (also available [on ocaml.org](https://ocaml.org/p/alt-ergo-lib/latest/doc/index.html))
for more information.

[install section]: ../Install/index.md
[Lwt]: https://ocsigen.org/lwt/
[js_of_ocaml]: https://ocsigen.org/js_of_ocaml/
[API documentation]: ../API/index
[AB-Why3 README]: ../Plugins/ab_why3.md
[Alt-ergo native language]: ../Alt_ergo_native/index
[SMT-LIB language]: ../SMT-LIB_language/index
[Dune-site plugins]: https://dune.readthedocs.io/en/stable/sites.html#plugins
## Links
- [install section](../Install/index.md)
- [Lwt](https://ocsigen.org/lwt/)
- [js_of_ocaml](https://ocsigen.org/js_of_ocaml/)
- [API documentation](../API/index)
- [AB-Why3 README](../Plugins/ab_why3.md)
- [Alt-ergo native language](../Alt_ergo_native/index)
- [SMT-LIB language](../SMT-LIB_language/index)
- [Dune-site plugins](https://dune.readthedocs.io/en/stable/sites.html#plugins)

0 comments on commit a12b034

Please sign in to comment.