Commit Graph

8 Commits

Author SHA1 Message Date
Gereon Kremer
a9ae5086d1 Various improvements and fixes in the documentation (#8551)
This PR contains a variety of fixed and improvements to the documentation.
2022-04-04 19:09:47 +00:00
Gereon Kremer
b08ef33d5a Refactor documentation (#8288)
This PR moves some stuff around in our documentation. Most notably, it moves some sections out of the "Binary documentation" to become their own top-level sections. While doing so, it refactors a few things in options and statistics to be more agnostic to the way cvc5 is used. To allow for command-output being used in regular (not auto-generated) documentation, we add a new extension that takes care of injecting the build folder into a new wrapper run-command.
2022-03-21 21:19:11 +00:00
Gereon Kremer
aaab98c449 Rename expert statistics to internal, add documentation (#8262)
We decided to rename statistics from "public / expert" to "public / internal". Also, this adds some reasonable documentation about statistics to our online docs.
2022-03-09 15:40:43 -08:00
Gereon Kremer
42f4798be4 Add user documentation for resource limits (#8058)
Though we regularly get questions about how resource limits work, they were entirely undocumented. This PR adds some general explanation to the user docs.
2022-02-07 21:49:31 +00:00
Gereon Kremer
5cfbb67e22 Various minor docs improvements (#7626)
This PR does a number of minor improvements to the docs.
2021-11-12 02:27:53 +00:00
Gereon Kremer
5ea33ca829 Add documentation on output tags (#7499)
This PR adds documentation on how users can use -o. After some offline discussion, we decided it makes sense to generate them automatically in mkoptions.py and also include example outputs.
2021-10-27 23:27:31 +00:00
Gereon Kremer
e5e727c868 Add a binary / SMT-LIB quickstart (#7315)
This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example.
2021-10-07 18:26:31 +00:00
Gereon Kremer
7440f0568b Add more examples to the documentation (#6569)
This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details:
- for consistency, all cpp examples are moved from examples/api to examples/api/cpp
- add capabilities for SMT-LIB examples, and two simple smt2 examples
- more docs/examples/*.rst files
- two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)
2021-05-26 06:30:45 +00:00