LTL fragment checking

[frankjjiang]

• Check if corresponding set operator is implemented in Set class
• Set operators return whether under approximation, over approximation, or exact.

Check details for approximation:

• Not operator flips between under and over approximation
• Cannot apply under approximation to over approximation and vice versa
• Binary operators cannot combine under and over approximation. Can combine exact with either.
• Root needs to be under approximation