This introduces a general way to use public enums both in the C++ and
the (upcoming) C API. For the C++ case, we now use enum classes rather
than enums for public enums. This also includes definitions for
C API to_string conversions for public enums. C API definitions in
cvc5_types.h are only included from the C API, guarded via a macro
(thus, for now, not included yet when the header is included).
mkFunctionSort that takes two sorts as arguments is redundant, because
the first argument is equivalent to a vector of size one passed to the
other overload of mkFunctionSort. This commit removes the method from
the C++ API but keeps the existing semantics for the Java and Python
bindings for convenience and consistency with, e.g. mkTerm.
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
Removes checkEntailed from Solver.
Removes isEntailed, isNotEntailed, isEntailedUnknown from Result.
Removes isSubsortOf, isFunctionLike, getUninterpretedSortName, getSortConstructorName from Sort.
Updates examples and unit tests.
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).
This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details:
- for consistency, all cpp examples are moved from examples/api to examples/api/cpp
- add capabilities for SMT-LIB examples, and two simple smt2 examples
- more docs/examples/*.rst files
- two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary)
