Standardize uses of inference manager in datatypes (#5035)

Standardize uses of inference manager in datatypes (#5035)

Datatypes now has an inference manager. This is work towards making it use the inference manager in all places where it should.

In particular, this makes many of the places where conflicts are determined using `InferenceManager::conflictExp` (explained conflict) instead of `InferenceManager::conflict` + custom calls to explain in TheoryDatatypes.  The goal here is to ensure that all explanations from the equality engine are managed by inference manager, which is required for proofs.