Make sine solver sound with respect to region boundaries (#8117)
Fixes the last benchmark on #7948.
Fixes a refutation soundness issue in the transcendental solver where a concavity region would be incorrectly assigned to a point if it was between the current model value of c*PI and its true value, where c in {-1, -1/2, 1/2, 1}.
We now only assign a concavity region if the model value of the argument lies within sound lower/upper bounds for the boundaries.
Notice that this means that points may be unassignable to a region if they lie inside the approximation interval for c*PI. An application of sin applied to an argument whose model value is that point cannot be refined.
A followup PR will address termination issues where the Taylor degree is incremented even when no function can be refined.