Make equality solver the entry point for all equality engine explanations in arithmet...

Make equality solver the entry point for all equality engine explanations in arithmetic (#8719)

This makes it so that EqSolver is the main entry point for all equality engine explanations in arithmetic; it still defers to the CongruenceManager to compute these explanations.

To do this, when the core linear solver depends on an explanation from the equality engine, it instead provides a placeholder. Since explanations are computed recursively in TheoryEngine, this will trigger another call to TheoryArith::explain, which will then be handled by the EqSolver. Thus, there should be no net effect on the overall explanations in this commit.

This is work towards eliminating the dependency of the linear solver on the equality engine.