This pull requests makes the enum that lists all proof rules a part of the API.
It also renames the enum from PfRule to ProofRule. It also renames some unrelated types and function names that share the PfRule name (such as DslPfRule).
This rename unfortunately touches many files since PfRule is not an uncommon type. (second to last commit)
This PR moves the public API headers into a top-level include directory. This makes it easier to find the public API of cvc5 and makes the install headers script obsolete.
Fixes#9553Fixes#9556
We are renaming files in the pythonic API to make it look less like it is somehow part of z3 (but still acknowledge that we took code from z3Py properly). This PR follows the change in cvc5/cvc5_pythonic_api#80.
This PR starts to refactor the proof rule comments so that they generate proper sphinx documentation.
It sets up doxygen to include the proof_rule.h, includes some useful configuration for mathjax and provides proper documentation for all core rules and Boolean rules.
This PR initializes some documentation for our proofs. It adds some almost empty files and makes sure that we can show documentation for the PfRule enum.
We decided to rename statistics from "public / expert" to "public / internal". Also, this adds some reasonable documentation about statistics to our online docs.
This fixes a bunch of warnings when generating our sphinx documentation.
They are mostly related to incorrect indentation/spacing, line breaks where
no line breaks should be, or missing code blocks.
Note that running clang-format causes some of these issues.
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)
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.
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.
