Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Frontend documentation #766

Merged
merged 3 commits into from
Jul 27, 2023
Merged

Frontend documentation #766

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
af1f3a5
Update the frontend documentation
Halbaroth Jul 27, 2023
0735690
Removing the `fully` adjective
Halbaroth Jul 27, 2023
9f917ec
Review changes
Halbaroth Jul 27, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 12 additions & 1 deletion docs/sphinx_docs/Usage/index.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,18 @@ Alt-Ergo supports file extensions:
- `.psmt2`, `.smt2` for (our polymorphic extension of) the SMT-LIB 2
standard

See the [Input section] for more information about the format of the input files
See the [Input section] for more information about the format of the input files.

### Frontend option

The `--frontend` option let's you select the frontend used to parse and type the input file. Since version 2.5.0,
Alt-Ergo integrates two frontends:
- The `legacy` frontend is the historical frontend of Alt-Ergo supporting the native language
and (partially) supporting the SMT-LIB language. The legacy frontend is currently the default.
- The `dolmen` frontend is a new frontend using the [Dolmen library](https://github.com/Gbury/dolmen).
The native and SMT-LIB languages are both supported by this frontend.
You can select it with the `--frontend dolmen` option, which is planned to become the
default in a future release.

### Generating models
Since 2.5.0, Alt-Ergo also generates models in the case it concludes on the satisfiability of
Expand Down
Loading