Is it possible to deal with tuples in Z3 with the Simplify format? I've tried what I would consider the more likely possibilities for functions, i.e. mk_tuple, tuple, etc., but nothing so far.
The tuple theory is not exposed over the Simplify front-end.You can approximate tuples by specifying that the selecctors are inverse to the constructor, but as in Simplify the default type is integer, you will not be able to force the occurs check (that you get for free with a stratified type system).
Thanks for the reply. While I'm not adverse to doing what you say, I would like to find out more. Is the tuple theory therefore exposed for either the SMT-LIB format or the Z3-native format?