The latest SMT-LIB release has standardized arithmetic/bitvector
conversions (https://smt-lib.org/theories-FixedSizeBitVectors.shtml).
This adds support for them.
In particular, the kind Kind::INT_TO_BITVECTOR now has recommended
syntax int_to_bv, while int2bv is supported (deprecated) in non-strict
mode for now for backwards compatibility.
The kind Kind::BITVECTOR_TO_NAT and the smt2 syntax bv2nat for now is
maintained but should be deprecated. In particular,
Kind::BITVECTOR_TO_NAT is silently converted to
Kind::BITVECTOR_UBV_TO_INT in the API.
We add Kind::BITVECTOR_UBV_TO_INT and Kind::BITVECTOR_SBV_TO_INT in the
API.
The internal kind BITVECTOR_TO_NAT is renamed BITVECTOR_UBV_TO_INT, and
add internal kind BITVECTOR_SBV_TO_INT.
Updates the proof infrastructure to use the new naming scheme.
Support for function cvc5::Solver::getOutput() is still missing as it is
currently unclear how to change its C++ interface to allow support in
other language bindings.
