Add inference enumeration to datatypes (#5275)

Add inference enumeration to datatypes (#5275)

This adds an inference enumeration for datatypes, which is analogous to what is done in strings and non-linear arithmetic. Inferences are informal identifiers that serve the purpose of (1) debugging the code, (2) providing hints on how proofs can be reconstructed.

This PR also splits the InferenceManager file in datatypes into 2.