Support for special Z3 relations

[fpoli]

With Z3 it's possible to declare special relations such as partial order, linear order, etc. The documentation explains that the decision procedure is efficient and avoids the quadratic number of quantifier instantiations of a naive axiomatization. These special relations would be very convenient in our axiomatization of mathematical data types (subset relations, contains relations, probably even equality relations etc).

With Z3 there is even a way to declare a "transitive closure" relation, which is not first-order axiomatizable.

I'm not sure what the limitations of these special relations are, but the potential benefits sound great.

[mschwerhoff]

Yes! 🕺 I saw these in PyZ3, but did not knew that they were usable via the SMT-LIB frontend. I'm curious to see how much they can improve performance.