SMT: Case Consistency Checks

[d-xo]

Act specs allow us to define various branching behaviours with the use of the case syntax. In order for properties proved against a spec involving cases to be sound, we must be sure that:

1. The cases are exhaustive
2. The cases do not overlap

We can use an smt solver to provide automated proofs for both of these properties by:

1. Asking the solver to find an assignment of variables which would satisfy the negation of the conjunction of all case predicates
2. For each pair of cases in a behaviour, asking the solver to find an assignment of variables that would satisfy the conjunction of both of their predicates

If all of the above queries return unsat, then we have a proof that the cases are both exhaustive and disjoint.

@MrChico in #14 you mention checks for redundancy of cases? I think that lack of redundant cases should be implied by the non-overlapping property, or am I missing something?

[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.