72 Commits

Author SHA1 Message Date
Alex Ozdemir
e8a14a4051 Add new idiomatic examples (#7912) 2022-01-11 00:49:02 +00:00
Alex Ozdemir
5a3a6090c6 Python Idomatic API: Document solver, results, utilities, and fns (#7882)
I put fns into "Core & Booleans".
2022-01-07 20:42:28 +00:00
Alex Ozdemir
a2f099d72f Document quantifiers in idiomatic python API (#7880) 2022-01-07 04:37:08 +00:00
Alex Ozdemir
e1c81278ec Py idiomatic API: Doc sets, datatypes, FP (#7877) 2022-01-05 20:47:09 +00:00
Alex Ozdemir
48e880074f More documentation for idiomatic python API (#7798)
Arithmetic, bit-vectors, arrays.
2021-12-17 18:42:48 +00:00
Aina Niemetz
eb3b04319a api: Fix smt-lib code blocks and math in C++ docs. (#7795) 2021-12-15 15:09:51 -08:00
Gereon Kremer
881464ade1 Turn kinds in python API into a proper Enum (#7686)
This PR does multiple things:
- the kinds are changed from custom objects to a proper enum.Enum class
  (including according changes to the cython code and the kind generation scripts)
- all examples and tests are modified to account for the change how to use kinds
  (Kind instead of kinds)
- add docstrings to the kind enum values
- add a custom documenter that properly renders enums via autodoc
- extend doxygen setup so that we can write comments as rst (allowing us to copy
  the documentation for kinds from the cpp api to the other apis)
2021-12-08 04:16:03 +00:00
Gereon Kremer
774770af22 Fix a few broken links (#7734)
This PR fixes a few broken links in our documentation.
2021-12-03 19:07:46 +00:00
Gereon Kremer
bcabf70ae1 Extend docs example extension (#7717)
This PR extends the custom sphinx extension for examples. It now allows for simple patterns in the file names and matches the file types using arbitrary regular expressions instead of just looking at the file extensions. This is necessary to integrate examples from the z3pycompat API: the examples live at a nontrivial place (in the build folder), which we inject via the file name patterns; we will have two separate examples which both end in .py but can be distinguished via the pattern used in the beginning.
2021-11-30 22:37:30 +00:00
Alex Ozdemir
0b287939ef Scaffold the idiomatic API's documentation (#7715)
Scaffolding the documentation, and fleshing it out for the Boolean functions and terms.
2021-11-30 21:06:30 +00:00
Gereon Kremer
38e4cf3fe6 Add kinds to python docs (#7672)
This PR adds the kinds to the documentation for the regular python docs.
2021-11-23 20:59:26 +00:00
yoni206
feae0b3040 Python API documentation: terms (#7659)
This PR adds documentation for the Terms class in the python API.
Co-authored-by: Gereon Kremer gereon.kremer@cs.rwth-aachen.de
2021-11-23 17:34:14 +00:00
Gereon Kremer
21b15a0464 Add documentation for z3py compatibility API (#7652)
This PR includes documentation for the z3py compatibility API into our general API.
It does so by adding the z3py compatibility API as an external project to download it and then have sphinx document it via the autodoc extension that we already use for our regular python API.
Right now we simply show everything on one page, which should be refactored in the future.
2021-11-17 19:40:49 +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
46f5a39730 Remove separate cpp docs for UnknownExplanation (#7516)
This removes the separate documentation for the `UnknownExplanation` enum, as it is already included in the documentation of the `Result` class.
2021-10-28 10:07:59 +00:00
yoni206
cd5fb80d86 Python api documentation for sorts (#7440)
This PR adds documentation for the Sort python API.
2021-10-27 17:41:24 +00:00
yoni206
538eea94a5 Python api documentation: Op, Grammar, Result, Enums (#7095)
This PR adds documentation to the python class Op, Grammar, Result, and for API enums.
Additionally, documentation for isNull functions in the datatype classes is added for the python API, and a small change in the cpp API documentation is introduced.
2021-10-15 23:09:02 +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
Alex Ozdemir
41b0ff8aa9 Start python API Solver documentation (#7064) 2021-09-20 22:12:17 +00:00
yoni206
be403c18c6 python docs for Datatype-related classes (#7058) 2021-08-30 12:32:24 -07:00
yoni206
63ad6f0ce1 Add python quick start guide (#7024) 2021-08-19 23:32:57 +00:00
Aina Niemetz
cc666c9a93 docs: Restructure index page, fix style issue. (#6657) 2021-06-01 17:05:52 -07:00