This PR addresses two issues reported by Sphinx. First, the
`docs/api/python/base/modes.rst` document was not included in any
toctree. Second, the `proofrule.rst` and `cvc5proofrule.rst` documents
were included in multiple toctrees. The latter is resolved by including
each document in only one toctree and referencing it elsewhere in the
documentation using cross-references.
This moves term statistics collection from Solver to TermManager.
TermManager and Solver now both provide `getStatistics()`, the former
captures API level term statistics, the latter internal solver
statistics.
This also adds iterator capabilities to the Python Statistics class.
This exports SkolemFunId to the API, and adds it to the Java, Python APIs, and adds unit tests.
It does some minor refactoring to remove unnecessary ids and to move abstract value to an internal skolem id.
Followup PRs will add methods for constructing/parsing skolems. I will also rename SkolemFunId -> SkolemId throughout the code base after this PR is merged.
This introduces a TermManager object, which will, in the future, be the
sole object responsible for handling/managing terms and sorts. For now,
all corresponding functions in `cvc5::Solver` are marked as deprecated,
as is constructor `cvc5::Solver::Solver()`, since in the future a solver
instance must be constructed from a term manager instance. Currently, we
maintain a static thread_local term manager instance to not break the
API and continue providing constructor `cvc5::Solver::Solver()`.
Note that this already converts all C++ unit tests to use the
TermManager except for a single test `getStatistics()` in
`test/unit/api/cpp/solver_black.cpp`. Statistics handling is currently
still maintained on the solver level. The statistics we maintain,
however, concern terms only and will eventually be refactored to be
tracked in the NodeManager.
Further note that the Java and Python APIs will be refactored in
separate PRs.
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.
