10 Commits

Author SHA1 Message Date
Mathias Preiner
f19f42f377 Update copyright headers, add missing header documentation. (#11990)
Adds missing header documentation for new files, remove carriage returns
from new files.
2025-06-18 19:41:07 +00:00
Aina Niemetz
cf8c5f3ade NodeManager as a static thread_local singleton is no more. (#11816)
Co-authored-by: Daniel Larraz <daniel-larraz@users.noreply.github.com>
2025-04-16 01:39:01 +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
Daniel Larraz
abbcf00bbb node/type_node/flatten: Eliminate calls to NodeManager::currentNM() (#11435) 2024-12-11 00:29:10 +00:00
Aina Niemetz
fdf9ce7138 Update copyright headers. (#10459) 2024-03-12 09:35:09 -07:00
Aina Niemetz
0a8baa0f0a Update copyright headers. (#9736) 2023-05-09 18:06:18 +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
Aina Niemetz
c335e4d3fa Rename kind PLUS -> ADD. (#8036)
This renames the arithmetic internal and API kind PLUS to ADD for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_ADD, FLOATINGPOINT_ADD).
2022-02-03 04:25:14 +00:00
Gereon Kremer
ac2a185f28 Add utilities for flattening nodes (#7961)
This PR adds new utilities for flattening nodes and checking whether they can be flattened. They replace the custom implementation we used in the arithmetic rewriter.
2022-01-31 21:49:21 +00:00