Finite Quantifiers, Contingency, and Optimization

Z3's quantifiers have been replaced by functions which generate finite conjunctions and disjunctions, leading to a massive performance gain. The following new features have also been included:

• The user can specify a max_time and is prompted to increase the time if the model-checker times out.
• The user can set an optimize variable with override flag -o to have the model-checker find a model with the smallest number of atomic elements within the max_time.
• The user can set the contingent variable with override flag -c to require all propositions to be contingent, i.e., to have some possible verifier and some possible falsifier. Since the null state cannot verify nor falsify a contingent proposition, constraints on propositions to only have non-null verifiers and falsifiers have been removed.

In addition to these features, the unit tests have been expanded to now include 120 examples which are divided by logical operators.

Interpreted propositions and disjunctive conclusions

This release provides more detailed printing and interprets conclusions disjunctively.