General bitvector type of any length

Question

For the same reasons that are described here ( user-defined uninterpreted function ) I want to define my own uninterpreted function

bvredxnor (): xnor over the bits of this bitvector.

If I follow the example given here ( an example of universal quantifiers with an API), I don't know which sort to provide an argument to my function (a bitvector)

I could create a bitvector view of a certain length, but I would like to have it for bitvectors of any length.

Looking at the bitvector functions available in the C API, I noticed that the type of all arguments is Z3_ast, so I thought I could use the same generic type. But there is no function in the API that generates Z3_ast sorting ... (by writing this, I feel like touching the difference between types and sorts, but it's still a bit unclear)

Is the decision to use uninterpreted varieties? And if so, at the same time, will I not lose some accuracy in my model by increasing the type too much, while this artifact is intended only for debugging purposes? I mean, if I applied this function to a bitvector, would it work?

Thanks in advance,

AG.

Answer 1

SMTLib does not allow variable length bit vectors. That is, you cannot express problems that are parameterized along the length of the battlevector. The reason for this is that the properties about bit vectors do not necessarily have parametric lengths due to power problems. Let's pretend that:

exists x0, x1, x2, x3, x4. distinct [x0, x1, x2, x3, x4] 

This property says that there are at least 5 different values ​​of the bit vector. This is true if the region x has a length of at least 3, but not otherwise. Therefore, the validity of a statement depends on the domain. You can also see this as a limitation of the nature of first-order SMTLibs in general.

Of course, the above applies to SMTLib and not necessarily to Z3. Leo and Co. have always been ahead of the curve, and the Z3 has many tricks that go beyond what SMTLib requires. It would be a pleasant surprise if Z3 really supports some notion of parametric tasks of a bit vector in the way you describe.