6 Commits

Author SHA1 Message Date
Aina Niemetz
ec5e78f730 api: Refactor sort and term (like) objects to not depend on Solver. (#9020)
This refactors Sort, Term, Op and datatype objects to not maintain a
reference (and depend) on Solver, but an associated NodeManager. This
allows to share node managers between solver instances.
2022-08-03 10:15:50 -05: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
Andres Noetzli
c0bfa39a98 Remove Op::getIndices() (#8355)
This commit removes `Op::getIndices()`. As discussed offline, the
semantics of that method were confusing and the use cases are covered by
`Op::getNumIndices()` and `Op::operator[]()` (which mirror
`Term::getNumChildren()` and `Term::operator[]()`).

Future changes are going to update the Python and Java bindings to
support `Op::operator[]()`.
2022-03-21 23:27:40 +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
Aina Niemetz
eea329d3e0 Reorganize test/unit/api directory. (#7612)
This moves .cpp files to directory test/unit/api/cpp and python files in
test/python/unit/api to test/unit/api/python.
2021-11-10 00:08:29 +00:00