12 Commits

Author SHA1 Message Date
Daniel Larraz
478876f4d8 Add missing Java and Python API tests (#12186) 2025-10-28 11:29:03 +00:00
Aina Niemetz
0647c4c107 Update copyright headers. (#11561)
Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com>
2025-01-23 17:54:20 +00:00
Aina Niemetz
a3f060fce4 c api: Add API test reset_assertions. (#11102)
Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com>
2024-07-31 07:01:09 +00:00
Aina Niemetz
fdf9ce7138 Update copyright headers. (#10459) 2024-03-12 09:35:09 -07:00
Aina Niemetz
58d7c6d556 c++ api: Expose TermManager to the API. (#10426)
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.
2024-03-08 19:39:13 +00:00
Aina Niemetz
0a8baa0f0a Update copyright headers. (#9736) 2023-05-09 18:06:18 +00:00
Mathias Preiner
56e14c4639 Move public headers into top-level include directory. (#9555)
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 #9553
Fixes #9556
2023-03-07 23:39:29 +00:00
Andrew Reynolds
42e503ba7d More preparation for strict type rules (#8733)
This is work towards making equalities and substitutions between terms of equal types.
2022-05-07 02:22:12 +00:00
Mathias Preiner
d01e59c13b Update copyright headers for release 1.0 (#8539) 2022-04-05 20:38:57 +00:00
Mathias Preiner
bbcd471ed4 Introduce internal namespace and remove api namespace. (#8443)
The public cvc5 API now lives in the cvc5 namespace. All internal parts were moved into the (new) internal namespace.
The final hierarchy will be as follows:

cvc5
  ~~ public API
  ::context
  ::internal
  ::parser
  ::main

After this PR it will be:

cvc5
  ~~ public API
  ::internal
      ::context
      ::main
  ::parser
2022-03-29 23:23:01 +00:00
Mathias Preiner
4a58ed7daf api: Unify mkTerm variants. (#8357) 2022-03-22 00:22:41 +00:00
yoni206
40272d5f3a Translating API tests to Python — part 1 (#7597)
This PR translates some of the API tests from here to Python. The other tests are translated in a private branch and will be added in a separate PR.
2021-11-16 18:56:37 +00:00