Merge initialization steps in TheoryModelBuilder (#4901)

Merge initialization steps in TheoryModelBuilder (#4901)

Currently when constructing models, we traverse the equality engine of the model 3 times during initialization. This PR merges these 3 traversals.

This refactoring is necessary to update model building for the "centralized" approach for equality reasoning, where it will be important to traverse the equality engine of the model in a careful way (to skip irrelevant terms).

The PR also makes a few minor optimizations for e.g. reducing map lookups, and adds more documentation.