SMT: Case Consistency Checks about act

[d-xo]

After discussing with @msooseth we came up with a more restricted case checking algorithm that should be decidable and very fast (even cases with 1000's of variables should be checkable in under a second).

The restrictions on the form of expressions that are allowable in a case would be:

• We allow arbitrary combinations of arbitrary expressions connected with or, and and negation
• The variables in a given expression in the case tree may only be used in that expression or it's negation. So if f(x,y,z) is an expression (e.g. x**2+y < z), then x, y, and z cannot be used anywhere else, except in the same form (i.e. x**2+y < z), or its negation (i.e x**2+y >= z).

This restriction works becase it allows us to abstract the expressions into a pure sat problem, and ensures that there are no connections between the variables in different expressions that would force abstraction refinement.

In order to implement this, we need to:

1. Introduce a typechecking stage that ensures the expressions in the case tree match the above restrictions
2. Introduce an SAT based consistency checking pass that actually checks that the expressions are all distinct and total

[d-xo]

The consistency checking routine remains as described in the first comment, the restrictions simply ensure that it can always be easily solved.

[zoep]

Completed with #157.