Towards proper usage of TO_REAL (#8680)

Towards proper usage of TO_REAL (#8680)

This is work towards making the rewriter preserve types, which is work towards eliminating subtyping.

This makes it so that the arithmetic rewriter does not simply drop TO_REAL from all terms, as this may change the type of the Node. Instead, TO_REAL is pulled upwards, and can be removed beneath arithmetic relations. TO_REAL is not eliminated if it occurs as a child of an operator not belonging to arithmetic. For example if x,y : Int:

(= (+ (to_real x) y) 0.0) ---> (= (to_real (+ x y)) 0.0) ---> (= (+ x y) 0.0) ; note this is the same rewritten form as before
(P (+ (to_real x) y)) ---> (P (to_real (+ x y))).

The one exception is that to_real applied to constants is simply dropped (for now), for example:

(to_real 5) ---> 5

where above, a Real term is rewritten to an Int term. (Fixing this will require further PRs that make integer constants of kind CONST_INTEGER and integral CONST_RATIONAL have Real type, thus we can have the above rewrite return 5 that is constant and has type Real).

Several quantifiers utilities are patched to preserve their behavior wrt handling TO_REAL.

Finally, a few fixes for subtypes are made to the regressions that we were not catching as errors before, and adds one regression.

The net effect of this PR is that the rewritten form of terms may have to_real applications that occur as direct children of symbols from other theories. Special care is required for preregistration, shared terms, and getting model values in the linear solver to strip off TO_REAL if necessary before using the (unmodified) interface to the linear solver.

FYI @barrettcw