Tuples without (declare-datatypes)?

Question

I wrote a large-ish library in the Z3 dialect of SMT-LIB. Unfortunately, my use of (declare-datatypes) to create tuples means that I cannot set the logic to QF_AUFBV as I desire. This has the side effect of making my scripts slower (sometimes timing out) than when I manually create the formulas programmatically and solve using QF_ABV. Thus, I want to eliminate (declare-datatypes) from my script. Most of the data types can be encoded as bit vectors. However, the most important sort in the library is a tuple of a bitvector term and three arrays. Is there a solution where I can make a sort like this, while still using QF_AUFBV logic?

Answer 1

You can always concatenate the bitvectors of the tuple and extract the relevant half whenever needed.