c++ api: Expose TermManager to the API. #10426
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 API will be refactored in a separate PR.
mpreiner
reviewed
Feb 26, 2024
ajreynol
requested changes
Mar 4, 2024
mpreiner
approved these changes
Mar 6, 2024
aniemetz
added a commit
to aniemetz/cvc5
that referenced
this pull request
Mar 8, 2024
This refactors the base Python API to expose TermManager (related to previous refactor of the C++ API to expose TermManager in cvc5#10426).
aniemetz
added a commit
that referenced
this pull request
Mar 14, 2024
This refactors the base Python API to expose TermManager (related to previous refactor of the C++ API to expose TermManager in #10426).
aniemetz
added a commit
to aniemetz/cvc5
that referenced
this pull request
Mar 20, 2024
This is related to the previous refactor of the C++ API in cvc5#10426.
aniemetz
added a commit
to aniemetz/cvc5
that referenced
this pull request
Mar 21, 2024
This is related to the previous refactor of the C++ API in cvc5#10426.
aniemetz
added a commit
to aniemetz/cvc5
that referenced
this pull request
Apr 2, 2024
This is related to the previous refactor of the C++ API in cvc5#10426.
aniemetz
added a commit
that referenced
this pull request
Apr 2, 2024
This is related to the previous refactor of the C++ API in #10426.
daniel-raffler
added a commit
to sosy-lab/java-smt
that referenced
this pull request
Apr 4, 2024
…. See cvc5/cvc5#10426 for the interface. This will solve issue #310.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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::Solverare marked as deprecated, as is constructorcvc5::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 constructorcvc5::Solver::Solver().Note that this already converts all C++ unit tests to use the TermManager except for a single test
getStatistics()intest/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.