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.
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
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[]()`.
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).