Migrate basic EqualityEngine management from CongruenceManager to EqSolver (#8684)

Migrate basic EqualityEngine management from CongruenceManager to EqSolver (#8684)

This is work towards having the linear arithmetic solver not impose restrictions on equalities.

The linear arithmetic solver using a CongruenceManager which involves many non-standard uses of the equality engine.

The responsibilities of the CongruenceManager should be migrated to the arithmetic EqSolver, which manages the equality engine in the default way.

This PR is the first step. It makes it so that the memory management and notifications of the equality engine are now solely the responsibility of the EqSolver.

All relevant notifications from the EqSolver are directly forwarded to CongruenceManager. Thus there are no significant behavior changes in this PR.

This PR required removing the experimental option arithCongMan, which forces having the CongruenceManager and the EqSolver both use equality engines.