Simplifications to the datatypes API (#8511)

Simplifications to the datatypes API (#8511)

This PR makes it so that common users of the datatypes API do not need to use "unresolved" datatypes sorts. Instead, these are automatically inferred by the NodeManager when calling mkMutualDatatypeTypes.

API Changes:
(1) adds addSelectorUnresolved to DatatypeConstructorDecl, which is the sole method needed to specify ordinary recursive selectors.
(2) adds to unit test examples that use this variant instead of using unresolved sorts.
(3) the API method mkUnresolvedSort is renamed to mkUnresolvedDatatypeSort and is marked experimental.

Note that unresolved datatype sorts are still needed to support mixed parametric datatypes and nested recursive datatypes in the smt2 parser, so they cannot be deleted yet.

Followup PR will add to documentation on elaborate further on how to use the datatypes API.