Add two reduction schemas for sin terms (#8171)

Add two reduction schemas for sin terms (#8171)

This restores our reasoning for symmetry of sine, now on-demand and without introducing sin terms eagerly.

It also ensures that sin terms whose arguments fall exactly on boundary points are removed from consideration from the transcendental solver. This allows us to answer sat for inputs involving sin(k) when k = pi/2.

It also cleans the relationship of sine solver and transcendental state, and makes a small fix to the monotonicity of sin schema.