14 Commits

Author SHA1 Message Date
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
2e5ab8def5 c api: Add API test sep_log_api. (#11105)
Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>
2024-08-05 22:04:46 +00:00
Aina Niemetz
82be2ff2fc c api: Add term creation functions and tests. (#10804) 2024-06-11 21:41:39 +00:00
Aina Niemetz
5eeb791635 Revert "c api: Add tests for op. (#10828)"
This reverts commit 6efe0fae41.

This got merged in prematurely by accident.
2024-06-11 07:32:57 -07:00
Aina Niemetz
6efe0fae41 c api: Add tests for op. (#10828)
This is based on #10827.
2024-06-11 02:48:34 +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
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
Gereon Kremer
5108f5c667 Fix 32bit issue in sep_log_api test (#7752)
This uses the proper `t.getInt64Value()` getter instead of `std::stoll(t.toString())`, fixing an issue on 32bit platforms.
2021-12-07 01:46:54 +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